Ball subset regularity Domain

lemma ball_subset_regularityDomain    {T : H →ₗ.[ℂ] H} {z : ℂ} {c : ℝ} (h : IsLowerBound T z c) : ball z c ⊆ T.regularityDomain := by  intro z' hzc  refine ⟨c - ‖z - z'‖, by simp_all [dist_eq, norm_sub_rev], fun x ↦ ?_⟩  calc    _ = c * ‖x‖ - ‖(z - z') • x‖ := by simp [sub_mul, norm_smul]    _ ≤ ‖T x - z • x‖ - ‖(z - z') • x‖ := by linarith [h x]    _ ≤ ‖T x - z • x + (z - z') • x‖ := norm_sub_le_norm_add _ _    _ = ‖T x - z' • x‖ := by simp [sub_smul]