Mem regularity Domain iff

lemma mem_regularityDomain_iff {T : H →ₗ.[ℂ] H} {z : ℂ} :    z ∈ T.regularityDomain ↔ (T - z • 1).toFun.ker = ⊥ ∧ Continuous (𝑅 T z) := by  constructor  · intro ⟨c, hc, h_bound⟩    have h_ker : (T - z • 1).toFun.ker = ⊥ := by      ext x      constructor <;> intro      · have : c * ‖x‖ ≤ 0 → ‖x‖ ≤ 0 := fun h' ↦ nonpos_of_mul_nonpos_right h' hc        specialize h_bound ⟨x, x.2.1⟩        simp_all [sub_apply]      · simp_all    use h_ker    apply LinearMap.continuous_iff_bounded.mpr    refine ⟨c⁻¹, inv_pos.mpr hc, fun ⟨x, hx⟩ ↦ ?_⟩    rw [inverse_domain] at hx    obtain ⟨y, hy⟩ := hx    specialize h_bound ⟨y, y.2.1⟩    simp_all [le_inv_mul_iff₀, sub_apply, inverse_apply_eq h_ker (y := ⟨x, hx⟩) hy]  · intro ⟨h_ker, h_cont⟩    obtain ⟨c, hc, h_bound⟩ := LinearMap.continuous_iff_bounded.mp h_cont    refine ⟨c⁻¹, inv_pos.mpr hc, fun x ↦ ?_⟩    apply (inv_mul_le_iff₀ hc).mpr    have hx : ↑x ∈ (T - z • 1).domain := by simp [sub_domain]    specialize h_bound ⟨(T - z • 1) ⟨x, hx⟩, by simp [inverse_domain]⟩    simp only [toFun_eq_coe, inverse_apply_eq h_ker (x := ⟨x, hx⟩), coe_norm] at h_bound    simp_all [sub_apply]