Is Symmetric is Self Adjoint of range eq top

lemma IsSymmetric.isSelfAdjoint_of_range_eq_top [CompleteSpace H] (hsym : T.IsSymmetric)    (hdense : T.HasDenseDomain)    (hadd : (T + I • 1).toFun.range = ⊤) (hsub : (T - I • 1).toFun.range = ⊤) :    IsSelfAdjoint T := by  have hplus : ∀ φ : H, ∃ ψ : T.domain, T ψ + I • (ψ : H) = φ := fun φ => by    obtain ⟨ψ, hψ⟩ := LinearMap.range_eq_top.mp hadd φ    exact ⟨⟨(ψ : H), (Submodule.mem_inf.mp ψ.2).1⟩, hψ⟩  have hminus : ∀ φ : H, ∃ ψ : T.domain, T ψ - I • (ψ : H) = φ := fun φ => by    obtain ⟨ψ, hψ⟩ := LinearMap.range_eq_top.mp hsub φ    exact ⟨⟨(ψ : H), (Submodule.mem_inf.mp ψ.2).1⟩, hψ⟩  rw [isSelfAdjoint_def]  have hle : T ≤ T.adjoint := (isSymmetric_def.mp hsym).le_adjoint hdense  apply le_antisymm _ hle  apply le_of_eqLocus_ge  intro w hw  let W : T.adjoint.domain := ⟨w, hw⟩  obtain ⟨x, hx⟩ := hminus (T.adjoint W - I • (W : H))  set X : T.adjoint.domain := ⟨x, hle.1 x.2⟩ with hX  have hxeq : T.adjoint X = T x := (hle.2 (x := x) (y := X) rfl).symm  have hdiff : T.adjoint (W - X) = I • ((W - X) : H) := by    rw [LinearPMap.map_sub, hxeq, hX, Subtype.coe_mk, smul_sub, sub_eq_sub_iff_sub_eq_sub, hx]  have hker : ∀ w : T.adjoint.domain, T.adjoint w = I • (w : H) → (w : H) = 0 := by    intro w hw    obtain ⟨v, hv⟩ := hplus (w : H)    suffices ⟪↑w, T v + I • v⟫_ℂ = 0 by      exact inner_self_eq_zero.mp (hv ▸ this)    rw [inner_add_right, inner_smul_right, ← adjoint_isFormalAdjoint hdense w v, hw,      inner_smul_left, conj_I]    ring  obtain rfl : w = (x : H) := sub_eq_zero.mp (hker (W - X) hdiff)  exact ⟨hw, x.2, hxeq⟩