filter_upwards [self_mem_nhdsWithin, l1] with ε (hε : 0 < ε) (hε' : ε < a / 2)
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
⊢ ∀ᶠ (ε : ℝ) in 𝓝[>] 0,
    ∃ ψ,
      ContDiff ℝ ⊤ ψ ∧
        HasCompactSupport ψ ∧
          closure (Function.support ψ) ⊆ Ioi 0 ∧ (Ico a b).indicator 1 ≤ ψ ∧ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε
case h
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
⊢ ∃ ψ,
    ContDiff ℝ ⊤ ψ ∧
      HasCompactSupport ψ ∧
        closure (Function.support ψ) ⊆ Ioi 0 ∧ (Ico a b).indicator 1 ≤ ψ ∧ ∫ (y : ℝ) in Ioi 0, ψ y ≤ b - a + ε