simp only [Complex.norm_eq_abs, norm_mul, Real.norm_eq_abs, norm_pow, Complex.abs_abs, one_div,
mul_inv_rev, abs_ofReal]
case h.e'_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
this : ‖𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖↑ε * s‖)
⊢ c * (1 / ‖ε * ‖s‖ ^ 2‖) = 1 / ‖s‖ * (c * (1 / ‖↑ε * s‖))
case h.e'_4
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
diffΨ : ContDiff ℝ 1 Ψ
suppΨ : Function.support Ψ ⊆ Icc (1 / 2) 2
σ₁ σ₂ : ℝ
σ₁pos : 0 < σ₁
ε : ℝ
εpos : 0 < ε
c : ℝ
hc : ∀ (x : ℂ), ε * σ₁ ≤ x.re ∧ x.re ≤ ε * σ₂ → ‖𝓜 (fun x => ↑(Ψ x)) x‖ ≤ c * (1 / ‖x‖)
s : ℂ
hs : σ₁ ≤ s.re ∧ s.re ≤ σ₂
this : ‖𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖↑ε * s‖)
⊢ c * ((Complex.abs s ^ 2)⁻¹ * |ε|⁻¹) = (Complex.abs s)⁻¹ * (c * ((Complex.abs s)⁻¹ * |ε|⁻¹))