-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
/-- If a function converges along a filter to a limit `a`, is integrable along this filter, and
all elements of the filter have infinite measure, then the limit has to vanish. -/
lemma IntegrableAtFilter.eq_zero_of_tendsto
    (h : IntegrableAtFilter f l μ) (h' : ∀ s ∈ l, μ s = ∞) {a : E}
    (hf : Tendsto f l (𝓝 a)) : a = 0

Proof state:
case intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
h' : ∀ s ∈ l, μ s = ⊤
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
v : Set α := u ∩ {b | ε < ‖f b‖}
hv : IntegrableOn f v μ
⊢ False

Tactic:
have vl : v ∈ l := inter_mem ul ((tendsto_order.1 hf.norm).1 _ hε)

Result:
case intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
h' : ∀ s ∈ l, μ s = ⊤
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
v : Set α := u ∩ {b | ε < ‖f b‖}
hv : IntegrableOn f v μ
vl : v ∈ l
⊢ False

Proof state:
case intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
h' : ∀ s ∈ l, μ s = ⊤
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
v : Set α := u ∩ {b | ε < ‖f b‖}
⊢ False

Tactic:
have hv : IntegrableOn f v μ := hu.mono_set inter_subset_left

Result:
case intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
h' : ∀ s ∈ l, μ s = ⊤
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
v : Set α := u ∩ {b | ε < ‖f b‖}
hv : IntegrableOn f v μ
⊢ False

Proof state:
case intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
h : IntegrableAtFilter f l μ
h' : ∀ s ∈ l, μ s = ⊤
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
⊢ False

Tactic:
rcases h with ⟨u, ul, hu⟩

Result:
case intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
h' : ∀ s ∈ l, μ s = ⊤
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
⊢ False

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
h : IntegrableAtFilter f l μ
h' : ∀ s ∈ l, μ s = ⊤
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
⊢ False

Tactic:
obtain ⟨ε, εpos, hε⟩ : ∃ (ε : ℝ), 0 < ε ∧ ε < ‖a‖ := exists_between (norm_pos_iff.mpr H)

Result:
case intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
h : IntegrableAtFilter f l μ
h' : ∀ s ∈ l, μ s = ⊤
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
⊢ False

Proof state:
case intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
h' : ∀ s ∈ l, μ s = ⊤
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
v : Set α := u ∩ {b | ε < ‖f b‖}
hv : IntegrableOn f v μ
vl : v ∈ l
this✝ : (μ.restrict v) v < ⊤
this : μ v ≠ ⊤
⊢ False

Tactic:
exact this (h' v vl)

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
h' : ∀ s ∈ l, μ s = ⊤
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
v : Set α := u ∩ {b | ε < ‖f b‖}
hv : IntegrableOn f v μ
vl : v ∈ l
this : (μ.restrict v) v < ⊤
⊢ False

Tactic:
have : μ v ≠ ∞ := ne_of_lt (by simpa only [Measure.restrict_apply_self])

Result:
case intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
h' : ∀ s ∈ l, μ s = ⊤
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
v : Set α := u ∩ {b | ε < ‖f b‖}
hv : IntegrableOn f v μ
vl : v ∈ l
this✝ : (μ.restrict v) v < ⊤
this : μ v ≠ ⊤
⊢ False

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
h' : ∀ s ∈ l, μ s = ⊤
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
v : Set α := u ∩ {b | ε < ‖f b‖}
hv : IntegrableOn f v μ
vl : v ∈ l
this : (μ.restrict v) v < ⊤
⊢ μ v < ⊤

Tactic:
simpa only [Measure.restrict_apply_self]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
h : IntegrableAtFilter f l μ
h' : ∀ s ∈ l, μ s = ⊤
a : E
hf : Tendsto f l (𝓝 a)
⊢ a = 0

Tactic:
by_contra H

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
h : IntegrableAtFilter f l μ
h' : ∀ s ∈ l, μ s = ⊤
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
⊢ False

Proof state:
case intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
h' : ∀ s ∈ l, μ s = ⊤
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
v : Set α := u ∩ {b | ε < ‖f b‖}
hv : IntegrableOn f v μ
vl : v ∈ l
⊢ False

Tactic:
have : μ.restrict v v < ∞ := lt_of_le_of_lt (measure_mono inter_subset_right)
  (Integrable.measure_gt_lt_top hv.norm εpos)

Result:
case intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
h' : ∀ s ∈ l, μ s = ⊤
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
v : Set α := u ∩ {b | ε < ‖f b‖}
hv : IntegrableOn f v μ
vl : v ∈ l
this : (μ.restrict v) v < ⊤
⊢ False

Proof state:
case intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
h' : ∀ s ∈ l, μ s = ⊤
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
⊢ False

Tactic:
let v := u ∩ {b | ε < ‖f b‖}

Result:
case intro.intro.intro.intro
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
μ : Measure α
l : Filter α
h' : ∀ s ∈ l, μ s = ⊤
a : E
hf : Tendsto f l (𝓝 a)
H : ¬a = 0
ε : ℝ
εpos : 0 < ε
hε : ε < ‖a‖
u : Set α
ul : u ∈ l
hu : IntegrableOn f u μ
v : Set α := u ∩ {b | ε < ‖f b‖}
⊢ False