simp [h5, l4.ne, Icc_subset_Ioi_iff l4.le, l5]
case h.intro.intro.intro.intro.intro.refine_1
n : ℕ
A a b c d u x y t σ' : ℝ
ψ✝ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
ha : 0 < a
hab : a < b
l1 : Iio (a / 2) ∈ 𝓝[>] 0
ε : ℝ
hε : 0 < ε
hε' : ε < a / 2
l2 : a - ε / 2 < a
l3 : b < b + ε / 2
ψ : ℝ → ℝ
h1 : ContDiff ℝ ⊤ ψ
h2 : HasCompactSupport ψ
h3 : (Icc a b).indicator 1 ≤ ψ
h4 : ψ ≤ (Ioo (a - ε / 2) (b + ε / 2)).indicator 1
h5 : Function.support ψ = Ioo (a - ε / 2) (b + ε / 2)
l4 : a - ε / 2 < b + ε / 2
l5 : ε / 2 < a
⊢ closure (Function.support ψ) ⊆ Ioi 0
no goals