Is Essentially Self Adjoint of defect Number eq zero

lemma isEssentiallySelfAdjoint_of_defectNumber_eq_zero    (hdense : T.HasDenseDomain) (hpos : T.defectNumber I = 0) (hneg : T.defectNumber (-I) = 0) :    T.IsEssentiallySelfAdjoint := by  have hrange {z : ℂ} (hz : z.im ≠ 0) (hd : T.defectNumber z = 0) :      (T.closure - z • 1).toFun.range = ⊤ := by    have hz' : z ∈ T.regularityDomain := hT.mem_regularityDomain_of_im_ne_zero hz    have hcl : T.closure.IsClosed := (hT.isClosable hdense).closure_isClosed    rw [← hcl.defectNumber_eq_zero_iff (T.regularityDomain_closure ▸ hz'),      defectNumber_closure hz']    exact hd  rw [isEssentiallySelfAdjoint_def]  apply (hT.closure hdense).isSelfAdjoint_of_range_eq_top hdense.closure  · have hI : T.closure + I • 1 = T.closure - (-I) • 1 :=      LinearPMap.ext rfl fun x hf hg => by simp [sub_apply, add_apply, smul_apply, sub_neg_eq_add]    rw [hI]    exact hrange (by norm_num) hneg  · exact hrange (by norm_num) hpos