Compl closure numerical Range subset regularity Domain

lemma compl_closure_numericalRange_subset_regularityDomain (T : H →ₗ.[ℂ] H) :    (_root_.closure (Θ T))ᶜ ⊆ T.regularityDomain := by  intro z hz  by_cases hT : T.domain = ⊥  · refine ⟨1, zero_lt_one, fun ⟨x, hx⟩ ↦ ?_⟩    rw [hT] at hx    simp_all  · use infDist z (Θ T)    constructor    · exact (infDist_pos_iff_notMem_closure <| numericalRange_nonempty hT).mp hz    · intro x      rcases eq_or_ne x 0 with rfl | hx      · simp      · let y : T.domain := ofReal ‖x‖⁻¹ • x        have hy : ‖y‖ = 1 := by simp [y, norm_smul, inv_mul_cancel₀, hx]        have hy' : ‖x‖ ^ 2 * ⟪↑y, T y⟫_ℂ = ⟪↑x, T x⟫_ℂ := by          simp_rw [y, map_smul, SetLike.val_smul, inner_smul_left, inner_smul_right, conj_ofReal,            ← mul_assoc, pow_two, ← ofReal_mul]          field_simp          simp        apply (mul_le_mul_iff_left₀ <| norm_pos_iff.mpr hx).mp        rw [mul_assoc, ← pow_two, mul_comm _ ‖x‖]        calc          _ ≤ ‖z - ⟪↑y, T y⟫_ℂ‖ * ‖x‖ ^ 2 := mul_le_mul_of_nonneg_right            (dist_eq z _ ▸ infDist_le_dist_of_mem ⟨y, hy, rfl⟩) (pow_two_nonneg _)          _ = ‖⟪↑y, T y⟫_ℂ * ‖x‖ ^ 2 - z * ‖x‖ ^ 2‖ := by simp [norm_sub_rev, ← sub_mul]          _ = ‖⟪↑x, T x⟫_ℂ - z * ‖x‖ ^ 2‖ := by rw [mul_comm, hy']          _ = ‖⟪↑x, T x - z • x⟫_ℂ‖ := by simp [inner_sub_right, inner_smul_right]          _ ≤ ‖x‖ * ‖T x - z • x‖ := norm_inner_le_norm _ _