Is Unbounded orthogonal closure sub range

lemma IsUnbounded.orthogonal_closure_sub_range [CompleteSpace H]    {T : H →ₗ.[ℂ] H} (hT : T.IsUnbounded) (z : ℂ) :    (T.closure - z • 1).toFun.rangeᗮ      = (T† - conj z • 1).toFun.ker.map (T† - conj z • 1).domain.subtype := by  have h_adj : (T.closure - z • 1)† = T† - conj z • 1 := by    have hC : Continuous (z • 1 : H →ₗ.[ℂ] H) := Continuous.const_smul (by fun_prop) _    rw [hT.hasDenseDomain.closure.adjoint_sub_continuous hC le_top, hT.adjoint_closure_eq_adjoint]    rcases eq_zero_or_neZero z with rfl | hz    · simp    · simp [hz.ne]  refine h_adj ▸ HasDenseDomain.orthogonal_range ?_  exact hT.hasDenseDomain.mono (by simp [sub_domain, T.le_closure.1])