filter_upwards [Ioo_mem_nhdsWithin_Ioi' (by linarith : (0 : ℝ) < a)] with c hc
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] 0, ‖f x‖ ≤ 0
case h
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
ha : 0 < a
fSupp : Function.support f ⊆ Icc a b
c : ℝ
hc : c ∈ Ioo 0 a
⊢ ‖f c‖ ≤ 0