by_cases ht : t ∈ Ioc 0 x⁻¹ <;> simp [ht]
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⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
⊢ -(Ioc 0 x⁻¹).indicator Ψ t = 0
case pos
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⁻¹ < ε
l3 : Ioi 0 = Ioc 0 x⁻¹ ∪ Ioi x⁻¹
l4 : Disjoint (Ioc 0 x⁻¹) (Ioi x⁻¹)
l5 : (Ioc 0 x⁻¹ ∪ Ioi x⁻¹).indicator Ψ = fun a => (Ioc 0 x⁻¹).indicator Ψ a + (Ioi x⁻¹).indicator Ψ a
ht : t ∈ Ioc 0 x⁻¹
⊢ Ψ t = 0