simp only [norm_norm, norm_div, norm_one, eventually_principal, mem_setOf_eq] at hc ⊢
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 : ℂ) in 𝓟 {s | ε * σ₁ ≤ s.re ∧ s.re ≤ ε * σ₂}, ‖‖𝓜 (fun x => ↑(Ψ x)) x‖‖ ≤ c * ‖1 / ‖x‖‖
⊢ ∀ᶠ (x : ℂ) in 𝓟 {s | σ₁ ≤ s.re ∧ s.re ≤ σ₂}, ‖‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) x‖‖ ≤ c * ‖1 / (ε * ‖x‖ ^ 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‖)
⊢ ∀ (x : ℂ), σ₁ ≤ x.re ∧ x.re ≤ σ₂ → ‖𝓜 (fun x => ↑(Smooth1 Ψ ε x)) x‖ ≤ c * (1 / ‖ε * ‖x‖ ^ 2‖)