-- Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
theorem tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable (hp_ne_zero : p ≠ 0)
    (hp_ne_top : p ≠ ∞) (hf : ∀ n, StronglyMeasurable (f n)) (hg : StronglyMeasurable g)
    {l : Filter ι} (hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)) :
    TendstoInMeasure μ f l g

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ ENNReal.ofReal (ε ^ p.toReal) ≠ 0 ∨ eLpNorm (f n - g) p μ ^ p.toReal ≠ 0

Tactic:
rw [Ne, ENNReal.ofReal_eq_zero, not_le]

Result:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ 0 < ε ^ p.toReal ∨ eLpNorm (f n - g) p μ ^ p.toReal ≠ 0

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Tactic:
intro ε hε

Result:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun i => μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ ENNReal.ofReal (ε ^ p.toReal) * μ {x | ε ≤ dist (f n x) (g x)} ≤ eLpNorm (f n - g) p μ ^ p.toReal

Tactic:
rw [← ENNReal.ofReal_rpow_of_pos hε]

Result:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ ENNReal.ofReal ε ^ p.toReal * μ {x | ε ≤ dist (f n x) (g x)} ≤ eLpNorm (f n - g) p μ ^ p.toReal

Proof state:
case h.e'_3.h.e'_6.h.e'_6.h.e'_2.h.a
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
x✝ : α
⊢ ENNReal.ofReal ε ≤ ‖f n x✝ - g x✝‖ₑ ↔ ENNReal.ofReal ε ≤ ↑‖(f n - g) x✝‖₊

Tactic:
exact Iff.rfl

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ 0 < ε ^ p.toReal ∨ eLpNorm (f n - g) p μ ^ p.toReal ≠ 0

Tactic:
exact Or.inl (Real.rpow_pos_of_pos hε _)

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ μ {x | ε ≤ dist (f n x) (g x)} ≤ δ

Tactic:
refine le_trans ?_ hn

Result:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ μ {x | ε ≤ dist (f n x) (g x)} ≤ ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f n - g) p μ ^ p.toReal

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
hfg : Tendsto (fun n => eLpNorm (f n - g) p μ) l (𝓝 0)
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun i => μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)

Tactic:
replace hfg := ENNReal.Tendsto.const_mul
  (Tendsto.ennrpow_const p.toReal hfg) (Or.inr <| @ENNReal.ofReal_ne_top (1 / ε ^ p.toReal))

Result:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg :
  Tendsto (fun b => ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f b - g) p μ ^ p.toReal) l
    (𝓝 (ENNReal.ofReal (1 / ε ^ p.toReal) * 0 ^ p.toReal))
⊢ Tendsto (fun i => μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg : Tendsto (fun b => ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f b - g) p μ ^ p.toReal) l (𝓝 0)
⊢ Tendsto (fun i => μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)

Tactic:
rw [ENNReal.tendsto_nhds_zero] at hfg ⊢

Result:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : ι → α → E
g : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ
hε : 0 < ε
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, ENNReal.ofReal (1 / ε ^ p.toReal) * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
⊢ ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, μ {x_1 | ε ≤ dist (f x x_1) (g x_1)} ≤ ε_1