have : ‖𝓜 (fun x ↦ ↑(Ψ x)) (ε * s)‖ ≤ c * (1 / ‖ε * s‖) := by
  refine hc (ε * s) ?_
  simp only [mul_re, ofReal_re, ofReal_im, zero_mul, sub_zero]
  exact ⟨(mul_le_mul_left εpos).mpr hs.1, (mul_le_mul_left εpos).mpr hs.2⟩
case h
𝕂 : 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 ≤ σ₂
⊢ ‖1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖ε * ‖s‖ ^ 2‖)
case h
𝕂 : 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‖)
⊢ ‖1 / s * 𝓜 (fun x => ↑(Ψ x)) (↑ε * s)‖ ≤ c * (1 / ‖ε * ‖s‖ ^ 2‖)