have hεx : x⁻¹ < ε := by apply (inv_lt hε hx).mp hxε
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
⊢ (Ioi x⁻¹).indicator (fun y => Ψ y) t - (Ioi 0).indicator (fun y => Ψ y) t = 0
case h.h.hf.hp
n : ℕ
A a b c d u x✝ y t✝ σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : Integrable Ψ volume
hplus : closure (Function.support Ψ) ⊆ Ioi 0
ε : ℝ
hε : ε > 0
hh : ∀ ⦃y : ℝ⦄, dist y 0 < ε → Ψ y = 0
x : ℝ
hxε : ε⁻¹ < x
l1 : Integrable ((Ioi x⁻¹).indicator fun x => Ψ x) volume
l2 : Integrable ((Ioi 0).indicator fun x => Ψ x) volume
t : ℝ
hε' : 0 < ε⁻¹
hx : 0 < x
hx' : 0 < x⁻¹
hεx : x⁻¹ < ε
⊢ (Ioi x⁻¹).indicator (fun y => Ψ y) t - (Ioi 0).indicator (fun y => Ψ y) t = 0