Iio subset regularity Domain

lemma Iio_subset_regularityDomain {m : ℝ} (h : m ∈ lowerBounds (Θᵣₑ T)) :    ofReal '' Iio m ⊆ T.regularityDomain := by  intro z ⟨r, hr, hrz⟩  refine ⟨m - r, sub_pos.mpr hr, fun x ↦ ?_⟩  rcases eq_zero_or_neZero x with rfl | hx  · simp  · obtain ⟨s, hs, hs'⟩ := hT.numericalRange_eq ▸ mem_numericalRange hx.ne    apply h at hs    have hsr : r < s := lt_of_lt_of_le hr hs    refine le_of_mul_le_mul_right ?_ (norm_pos_iff.mpr hx.ne)    calc      _ = (m - r) * ‖x‖ ^ 2 := by rw [mul_assoc, pow_two]      _ ≤ (s - r) * ‖x‖ ^ 2 := by nlinarith      _ = ‖s * ‖x‖ ^ 2 - r * ‖x‖ ^ 2‖ := by simp [← sub_mul, abs_of_pos, sub_pos, hsr]      _ = ‖(s : ℂ) * ‖x‖ ^ 2 - r * ‖x‖ ^ 2‖ := by simp [← ofReal_pow, ← ofReal_mul, ← ofReal_sub]      _ = ‖⟪↑x, T x⟫_ℂ - r * ‖x‖ ^ 2‖ := by simp [hs', mul_comm, hx.ne]      _ = ‖⟪↑x, T x - z • x⟫_ℂ‖ := by simp [inner_sub_right, inner_smul_right, hrz]      _ ≤ ‖T x - z • x‖ * ‖x‖ := mul_comm _ ‖x‖ ▸ norm_inner_le_norm _ _