-- Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
theorem tendstoInMeasure_of_tendsto_eLpNorm_top {E} [NormedAddCommGroup E] {f : ι → α → E}
    {g : α → E} {l : Filter ι} (hfg : Tendsto (fun n => eLpNorm (f n - g) ∞ μ) l (𝓝 0)) :
    TendstoInMeasure μ f l g

Proof state:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ‖f x x_1 - g x_1‖ₑ) μ ≤ ENNReal.ofReal δ / 2
n : ι
hn : essSup (fun x => ‖f n x - g x‖ₑ) μ ≤ ENNReal.ofReal δ / 2
hε : 0 < ε
⊢ μ {x | δ ≤ dist (f n x) (g x)} ≤ ε

Tactic:
have : essSup (fun x : α => (‖f n x - g x‖₊ : ℝ≥0∞)) μ < ENNReal.ofReal δ :=
  lt_of_le_of_lt hn
    (ENNReal.half_lt_self (ENNReal.ofReal_pos.2 hδ).ne.symm ENNReal.ofReal_lt_top.ne)

Result:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ‖f x x_1 - g x_1‖ₑ) μ ≤ ENNReal.ofReal δ / 2
n : ι
hn : essSup (fun x => ‖f n x - g x‖ₑ) μ ≤ ENNReal.ofReal δ / 2
hε : 0 < ε
this : essSup (fun x => ↑‖f n x - g x‖₊) μ < ENNReal.ofReal δ
⊢ μ {x | δ ≤ dist (f n x) (g x)} ≤ ε

Proof state:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
hfg : Tendsto (fun n => eLpNorm (f n - g) ⊤ μ) l (𝓝 0)
δ : ℝ
hδ : 0 < δ
⊢ Tendsto (fun i => μ {x | δ ≤ dist (f i x) (g x)}) l (𝓝 0)

Tactic:
simp only [eLpNorm_exponent_top, eLpNormEssSup] at hfg

Result:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
hfg : Tendsto (fun n => essSup (fun x => ‖(f n - g) x‖ₑ) μ) l (𝓝 0)
⊢ Tendsto (fun i => μ {x | δ ≤ dist (f i x) (g x)}) l (𝓝 0)

Proof state:
case h.e_6.h.h
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ‖f x x_1 - g x_1‖ₑ) μ ≤ ENNReal.ofReal δ / 2
n : ι
hn : essSup (fun x => ‖f n x - g x‖ₑ) μ ≤ ENNReal.ofReal δ / 2
hε : 0 < ε
this : essSup (fun x => ↑‖f n x - g x‖₊) μ < ENNReal.ofReal δ
x : α
⊢ δ ≤ dist (f n x) (g x) ↔ δ ≤ ‖f n x - g x‖

Tactic:
rw [← dist_eq_norm (f n x) (g x)]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hε : ε > 0
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ‖(f x - g) x_1‖ₑ) μ ≤ ENNReal.ofReal δ / 2
⊢ ∀ᶠ (x : ι) in l, μ {x_1 | δ ≤ dist (f x x_1) (g x_1)} ≤ ε

Tactic:
refine hfg.mono fun n hn => ?_

Result:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hε : ε > 0
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ‖(f x - g) x_1‖ₑ) μ ≤ ENNReal.ofReal δ / 2
n : ι
hn : essSup (fun x => ‖(f n - g) x‖ₑ) μ ≤ ENNReal.ofReal δ / 2
⊢ μ {x | δ ≤ dist (f n x) (g x)} ≤ ε

Proof state:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
hfg : ∀ ε > 0, ∀ᶠ (x : ι) in l, essSup (fun x_1 => ‖(f x - g) x_1‖ₑ) μ ≤ ε
ε : ℝ≥0∞
hε : ε > 0
⊢ ∀ᶠ (x : ι) in l, μ {x_1 | δ ≤ dist (f x x_1) (g x_1)} ≤ ε

Tactic:
specialize hfg (ENNReal.ofReal δ / 2)
    (ENNReal.div_pos_iff.2 ⟨(ENNReal.ofReal_pos.2 hδ).ne.symm, ENNReal.ofNat_ne_top⟩)

Result:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hε : ε > 0
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ‖(f x - g) x_1‖ₑ) μ ≤ ENNReal.ofReal δ / 2
⊢ ∀ᶠ (x : ι) in l, μ {x_1 | δ ≤ dist (f x x_1) (g x_1)} ≤ ε

Proof state:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ‖f x x_1 - g x_1‖ₑ) μ ≤ ENNReal.ofReal δ / 2
n : ι
hn : essSup (fun x => ‖f n x - g x‖ₑ) μ ≤ ENNReal.ofReal δ / 2
hε : 0 < ε
this : essSup (fun x => ↑‖f n x - g x‖₊) μ < ENNReal.ofReal δ
⊢ μ {x | δ ≤ dist (f n x) (g x)} = μ {x | (fun y => ↑‖f n y - g y‖₊ < ENNReal.ofReal δ) x}ᶜ

Tactic:
congr with x

Result:
case h.e_6.h.h
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ‖f x x_1 - g x_1‖ₑ) μ ≤ ENNReal.ofReal δ / 2
n : ι
hn : essSup (fun x => ‖f n x - g x‖ₑ) μ ≤ ENNReal.ofReal δ / 2
hε : 0 < ε
this : essSup (fun x => ↑‖f n x - g x‖₊) μ < ENNReal.ofReal δ
x : α
⊢ x ∈ {x | δ ≤ dist (f n x) (g x)} ↔ x ∈ {x | (fun y => ↑‖f n y - g y‖₊ < ENNReal.ofReal δ) x}ᶜ

Proof state:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
hfg : Tendsto (fun n => eLpNorm (f n - g) ⊤ μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Tactic:
intro δ hδ

Result:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
hfg : Tendsto (fun n => eLpNorm (f n - g) ⊤ μ) l (𝓝 0)
δ : ℝ
hδ : 0 < δ
⊢ Tendsto (fun i => μ {x | δ ≤ dist (f i x) (g x)}) l (𝓝 0)

Proof state:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hε : ε > 0
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ‖(f x - g) x_1‖ₑ) μ ≤ ENNReal.ofReal δ / 2
n : ι
hn : essSup (fun x => ‖(f n - g) x‖ₑ) μ ≤ ENNReal.ofReal δ / 2
⊢ μ {x | δ ≤ dist (f n x) (g x)} ≤ ε

Tactic:
simp only [gt_iff_lt, zero_tsub, zero_le, zero_add, Set.mem_Icc,
  Pi.sub_apply] at *

Result:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ‖f x x_1 - g x_1‖ₑ) μ ≤ ENNReal.ofReal δ / 2
n : ι
hn : essSup (fun x => ‖f n x - g x‖ₑ) μ ≤ ENNReal.ofReal δ / 2
hε : 0 < ε
⊢ μ {x | δ ≤ dist (f n x) (g x)} ≤ ε

Proof state:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ‖f x x_1 - g x_1‖ₑ) μ ≤ ENNReal.ofReal δ / 2
n : ι
hn : essSup (fun x => ‖f n x - g x‖ₑ) μ ≤ ENNReal.ofReal δ / 2
hε : 0 < ε
this : essSup (fun x => ↑‖f n x - g x‖₊) μ < ENNReal.ofReal δ
⊢ μ {x | δ ≤ dist (f n x) (g x)} ≤ ε

Tactic:
refine ((le_of_eq ?_).trans (ae_lt_of_essSup_lt this).le).trans hε.le

Result:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst✝ : NormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ
hδ : 0 < δ
ε : ℝ≥0∞
hfg : ∀ᶠ (x : ι) in l, essSup (fun x_1 => ‖f x x_1 - g x_1‖ₑ) μ ≤ ENNReal.ofReal δ / 2
n : ι
hn : essSup (fun x => ‖f n x - g x‖ₑ) μ ≤ ENNReal.ofReal δ / 2
hε : 0 < ε
this : essSup (fun x => ↑‖f n x - g x‖₊) μ < ENNReal.ofReal δ
⊢ μ {x | δ ≤ dist (f n x) (g x)} = μ {x | (fun y => ↑‖f n y - g y‖₊ < ENNReal.ofReal δ) x}ᶜ