awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
x : α
⊢ edist (f n x) (g x) = ‖(f n - g) x‖ₑ

Tactic:
simp [edist_eq_enorm_sub]

Premises used: edist_eq_enorm_sub
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ (ε ^ p.toReal)⁻¹ ≠ 0

Tactic:
simp [hε_top]
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1
δ : ℝ≥0∞
hδ : δ > 0
n : ι
hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ
⊢ (ε ^ p.toReal)⁻¹ ≠ ∞

Tactic:
simp [hε.ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Tactic:
TendstoInMeasure.congr (fun i => (hf i).ae_eq_mk.symm) hg.ae_eq_mk.symm ?_

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.TendstoInMeasure.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
refine : TendstoInMeasure μ (fun (i : ι) ↦ AEStronglyMeasurable.mk (f i) ⋯) l (AEStronglyMeasurable.mk g hg)
⊢ TendstoInMeasure μ f l g

Tactic:
refine TendstoInMeasure.congr (fun i => (hf i).ae_eq_mk.symm) hg.ae_eq_mk.symm ?_

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.TendstoInMeasure.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
⊢ TendstoInMeasure μ (fun (i : ι) ↦ AEStronglyMeasurable.mk (f i) ⋯) l (AEStronglyMeasurable.mk g hg)

Tactic:
tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable
    hp_ne_zero hp_ne_top (fun i => (hf i).stronglyMeasurable_mk) hg.stronglyMeasurable_mk ?_

Premises used: MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
refine :
  Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ) l
    (𝓝 0)
⊢ TendstoInMeasure μ (fun (i : ι) ↦ AEStronglyMeasurable.mk (f i) ⋯) l (AEStronglyMeasurable.mk g hg)

Tactic:
refine tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable
    hp_ne_zero hp_ne_top (fun i => (hf i).stronglyMeasurable_mk) hg.stronglyMeasurable_mk ?_

Premises used: MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
h : ∀ (n : ι), eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ = eLpNorm (f n - g) p μ
⊢ Eq.{u_2 + 1} (α := (n : ι) → ℝ≥0∞)
    (fun (n : ι) ↦ eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ) fun (n : ι) ↦
    eLpNorm (f n - g) p μ

Tactic:
ext1 n
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
n : ι
⊢ eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ = eLpNorm (f n - g) p μ

Tactic:
eLpNorm_congr_ae (EventuallyEq.sub (hf n).ae_eq_mk.symm hg.ae_eq_mk.symm)

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.eLpNorm_congr_ae, Filter.EventuallyEq.sub, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
n : ι
⊢ eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ = eLpNorm (f n - g) p μ

Tactic:
refine eLpNorm_congr_ae (EventuallyEq.sub (hf n).ae_eq_mk.symm hg.ae_eq_mk.symm)

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.eLpNorm_congr_ae, Filter.EventuallyEq.sub, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
⊢ Eq.{u_2 + 1} (α := (n : ι) → ℝ≥0∞)
    (fun (n : ι) ↦ eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ) fun (n : ι) ↦
    eLpNorm (f n - g) p μ

Tactic:
have : (fun n => eLpNorm ((hf n).mk (f n) - hg.mk g) p μ) = fun n => eLpNorm (f n - g) p μ := by
    ext1 n; refine eLpNorm_congr_ae (EventuallyEq.sub (hf n).ae_eq_mk.symm hg.ae_eq_mk.symm)
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
this :
  Eq.{u_2 + 1} (α := (n : ι) → ℝ≥0∞)
    (fun (n : ι) ↦ eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ) fun (n : ι) ↦
    eLpNorm (f n - g) p μ
rw : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ) l
    (𝓝 0)

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
this :
  Eq.{u_2 + 1} (α := (n : ι) → ℝ≥0∞)
    (fun (n : ι) ↦ eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ) fun (n : ι) ↦
    eLpNorm (f n - g) p μ
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)

Tactic:
hfg
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst : SeminormedAddCommGroup E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ∞
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
l : Filter ι
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
this :
  Eq.{u_2 + 1} (α := (n : ι) → ℝ≥0∞)
    (fun (n : ι) ↦ eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ) fun (n : ι) ↦
    eLpNorm (f n - g) p μ
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)

Tactic:
exact hfg
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst : SeminormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) ∞ μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Tactic:
tendstoInMeasure_of_ne_top fun δ hδ hδ_top ↦ ?_

Premises used: MeasureTheory.tendstoInMeasure_of_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst : SeminormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) ∞ μ) l (𝓝 0)
refine :
  ∀ (δ : ℝ≥0∞) (hδ : 0 < δ) (hδ_top : δ ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | δ ≤ edist (f i x) (g x)}) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Tactic:
refine tendstoInMeasure_of_ne_top fun δ hδ hδ_top ↦ ?_

Premises used: MeasureTheory.tendstoInMeasure_of_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst : SeminormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) ∞ μ) l (𝓝 0)
δ : ℝ≥0∞
hδ : 0 < δ
hδ_top : δ ≠ ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ essSup (fun (x : α) ↦ ‖(f n - g) x‖ₑ) μ) l (𝓝 0)

Tactic:
simp only [eLpNorm_exponent_top, eLpNormEssSup] at hfg

Premises used: MeasureTheory.eLpNorm_exponent_top, MeasureTheory.eLpNormEssSup
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst : SeminormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ≥0∞
hδ : 0 < δ
hδ_top : δ ≠ ∞
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ essSup (fun (x : α) ↦ ‖(f n - g) x‖ₑ) μ) l (𝓝 0)
rw :
  ∀ (hfg : ∀ ε > 0, ∀ᶠ (x : ι) in l, essSup (fun (x_1 : α) ↦ ‖(f x - g) x_1‖ₑ) μ ≤ ε),
    ∀ ε > 0, ∀ᶠ (x : ι) in l, (μ : (a : Set α) → ℝ≥0∞) {x_1 : α | δ ≤ edist (f x x_1) (g x_1)} ≤ ε
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | δ ≤ edist (f i x) (g x)}) l (𝓝 0)

Tactic:
rw [ENNReal.tendsto_nhds_zero] at hfg ⊢

Premises used: ENNReal.tendsto_nhds_zero
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst : SeminormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ≥0∞
hδ : 0 < δ
hδ_top : δ ≠ ∞
hfg : ∀ ε > 0, ∀ᶠ (x : ι) in l, essSup (fun (x_1 : α) ↦ ‖(f x - g) x_1‖ₑ) μ ≤ ε
ε : ℝ≥0∞
hε : ε > 0
⊢ ∀ᶠ (x : ι) in l, essSup (fun (x_1 : α) ↦ ‖(f x - g) x_1‖ₑ) μ ≤ δ / 2

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

Premises used: Iff.mpr, ENNReal.ofNat_ne_top, ENNReal.div_pos_iff, HDiv.hDiv, LT.lt.ne', And.intro, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst : SeminormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ≥0∞
hδ : 0 < δ
hδ_top : δ ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hfg : ∀ᶠ (x : ι) in l, essSup (fun (x_1 : α) ↦ ‖(f x - g) x_1‖ₑ) μ ≤ δ / 2
⊢ ∀ᶠ (x : ι) in l, (μ : (a : Set α) → ℝ≥0∞) {x_1 : α | δ ≤ edist (f x x_1) (g x_1)} ≤ ε

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

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst : SeminormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ≥0∞
hδ : 0 < δ
hδ_top : δ ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hfg : ∀ᶠ (x : ι) in l, essSup (fun (x_1 : α) ↦ ‖(f x - g) x_1‖ₑ) μ ≤ δ / 2
refine :
  ∀ (n : ι) (hn : essSup (fun (x : α) ↦ ‖(f n - g) x‖ₑ) μ ≤ δ / 2),
    (μ : (a : Set α) → ℝ≥0∞) {x : α | δ ≤ edist (f n x) (g x)} ≤ ε
⊢ ∀ᶠ (x : ι) in l, (μ : (a : Set α) → ℝ≥0∞) {x_1 : α | δ ≤ edist (f x x_1) (g x_1)} ≤ ε

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

Premises used: Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst : SeminormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ≥0∞
hδ : 0 < δ
hδ_top : δ ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hfg : ∀ᶠ (x : ι) in l, essSup (fun (x_1 : α) ↦ ‖f x x_1 - g x_1‖ₑ) μ ≤ δ / 2
n : ι
hn : essSup (fun (x : α) ↦ ‖f n x - g x‖ₑ) μ ≤ δ / 2
⊢ essSup (fun (x : α) ↦ ‖f n x - g x‖ₑ) μ < δ

Tactic:
have : essSup (fun x : α => ‖f n x - g x‖ₑ) μ < δ :=
    hn.trans_lt (ENNReal.half_lt_self hδ.ne' hδ_top)
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst : SeminormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ≥0∞
hδ : 0 < δ
hδ_top : δ ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hfg : ∀ᶠ (x : ι) in l, essSup (fun (x_1 : α) ↦ ‖f x x_1 - g x_1‖ₑ) μ ≤ δ / 2
n : ι
hn : essSup (fun (x : α) ↦ ‖f n x - g x‖ₑ) μ ≤ δ / 2
this : essSup (fun (x : α) ↦ ‖f n x - g x‖ₑ) μ < δ
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | δ ≤ edist (f n x) (g x)} ≤ ε

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

Premises used: LT.lt.le, Eq.le, LE.le.trans, le_of_eq, ae_lt_of_essSup_lt
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst : SeminormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ≥0∞
hδ : 0 < δ
hδ_top : δ ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hfg : ∀ᶠ (x : ι) in l, essSup (fun (x_1 : α) ↦ ‖f x x_1 - g x_1‖ₑ) μ ≤ δ / 2
n : ι
hn : essSup (fun (x : α) ↦ ‖f n x - g x‖ₑ) μ ≤ δ / 2
this : essSup (fun (x : α) ↦ ‖f n x - g x‖ₑ) μ < δ
refine :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | δ ≤ edist (f n x) (g x)} : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {x : α | (fun (y : α) ↦ ‖f n y - g y‖ₑ < δ) x}ᶜ : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | δ ≤ edist (f n x) (g x)} ≤ ε

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

Premises used: LT.lt.le, Eq.le, LE.le.trans, le_of_eq, ae_lt_of_essSup_lt
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst : SeminormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ≥0∞
hδ : 0 < δ
hδ_top : δ ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hfg : ∀ᶠ (x : ι) in l, essSup (fun (x_1 : α) ↦ ‖f x x_1 - g x_1‖ₑ) μ ≤ δ / 2
n : ι
hn : essSup (fun (x : α) ↦ ‖f n x - g x‖ₑ) μ ≤ δ / 2
this : essSup (fun (x : α) ↦ ‖f n x - g x‖ₑ) μ < δ
h : ∀ (x : α), δ ≤ edist (f n x) (g x) ↔ x ∉ {x : α | (fun (y : α) ↦ ‖f n y - g y‖ₑ < δ) x}
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | δ ≤ edist (f n x) (g x)} : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {x : α | (fun (y : α) ↦ ‖f n y - g y‖ₑ < δ) x}ᶜ : ℝ≥0∞)

Tactic:
congr with x
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
E : Type u_5
inst : SeminormedAddCommGroup E
f : ι → α → E
g : α → E
l : Filter ι
δ : ℝ≥0∞
hδ : 0 < δ
hδ_top : δ ≠ ∞
ε : ℝ≥0∞
hε : ε > 0
hfg : ∀ᶠ (x : ι) in l, essSup (fun (x_1 : α) ↦ ‖f x x_1 - g x_1‖ₑ) μ ≤ δ / 2
n : ι
hn : essSup (fun (x : α) ↦ ‖f n x - g x‖ₑ) μ ≤ δ / 2
this : essSup (fun (x : α) ↦ ‖f n x - g x‖ₑ) μ < δ
x : α
⊢ δ ≤ edist (f n x) (g x) ↔ x ∉ {x : α | (fun (y : α) ↦ ‖f n y - g y‖ₑ < δ) x}

Tactic:
simp [edist_eq_enorm_sub]

Premises used: edist_eq_enorm_sub
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst : NormedAddCommGroup E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
pos : ∀ (hp_ne_top : p = ∞), TendstoInMeasure μ f l g
neg : ∀ (hp_ne_top : ¬p = ∞), TendstoInMeasure μ f l g
⊢ TendstoInMeasure μ f l g

Tactic:
by_cases hp_ne_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst : NormedAddCommGroup E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
hp_ne_top : p = ∞
⊢ Ne (α := ℝ≥0∞) ∞ 0

Tactic:
subst hp_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst : NormedAddCommGroup E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
hp_ne_top : p = ∞
hp_ne_zero₁ : Ne (α := ℝ≥0∞) ∞ 0
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) ∞ μ) l (𝓝 0)

Tactic:
subst hp_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
f : ι → α → E
g : α → E
inst : NormedAddCommGroup E
l : Filter ι
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hp_ne_zero : Ne (α := ℝ≥0∞) ∞ 0
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) ∞ μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Tactic:
tendstoInMeasure_of_tendsto_eLpNorm_top hfg

Premises used: MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_top
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
f : ι → α → E
g : α → E
inst : NormedAddCommGroup E
l : Filter ι
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hp_ne_zero : Ne (α := ℝ≥0∞) ∞ 0
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) ∞ μ) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Tactic:
exact tendstoInMeasure_of_tendsto_eLpNorm_top hfg

Premises used: MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_top
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst : NormedAddCommGroup E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
hp_ne_top : ¬p = ∞
⊢ TendstoInMeasure μ f l g

Tactic:
tendstoInMeasure_of_tendsto_eLpNorm_of_ne_top hp_ne_zero hp_ne_top hf hg hfg

Premises used: MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_of_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
f : ι → α → E
g : α → E
inst : NormedAddCommGroup E
l : Filter ι
hp_ne_zero : p ≠ 0
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
hg : AEStronglyMeasurable g μ
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
hp_ne_top : ¬p = ∞
⊢ TendstoInMeasure μ f l g

Tactic:
exact tendstoInMeasure_of_tendsto_eLpNorm_of_ne_top hp_ne_zero hp_ne_top hf hg hfg

Premises used: MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm_of_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst : NormedAddCommGroup E
hp : Fact (1 ≤ p)
f : ι → ↥(Lp E p μ)
g : ↥(Lp E p μ)
l : Filter ι
hfg : Tendsto f l (𝓝 g)
⊢ TendstoInMeasure μ (fun (n : ι) ↦ (↑(↑(f n) : α →ₘ[μ] E) : α → E)) l (↑(↑g : α →ₘ[μ] E) : α → E)

Tactic:
tendstoInMeasure_of_tendsto_eLpNorm (zero_lt_one.trans_le hp.elim).ne.symm
    (fun _ => Lp.aestronglyMeasurable _) (Lp.aestronglyMeasurable _)
    ((Lp.tendsto_Lp_iff_tendsto_eLpNorm' _ _).mp hfg)

Premises used: MeasureTheory.Lp.aestronglyMeasurable, MeasureTheory.tendstoInMeasure_of_tendsto_eLpNorm, Ne.symm, zero_lt_one, Fact.elim, LT.lt.trans_le, Iff.mp, MeasureTheory.Lp.tendsto_Lp_iff_tendsto_eLpNorm', LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : PseudoEMetricSpace β
n : ℕ
j : ι
f : ι → α → β
g : α → β
inst_1 : Preorder ι
x : α
simp_rw :
  Membership.mem (γ := Set α) (⋃ (k : ι), ⋃ (_ : j ≤ k), {x : α | (↑n : ℝ≥0∞)⁻¹ < edist (f k x) (g x)}) x ↔
    ∃ k ≥ j, (↑n : ℝ≥0∞)⁻¹ < edist (f k x) (g x)
simp_rw₁ :
  (∃ (i : ι) (_ : j ≤ i), Membership.mem (γ := Set α) {x : α | (↑n : ℝ≥0∞)⁻¹ < edist (f i x) (g x)} x) ↔
    ∃ k ≥ j, (↑n : ℝ≥0∞)⁻¹ < edist (f k x) (g x)
simp_rw₂ :
  (∃ (i : ι), j ≤ i ∧ Membership.mem (γ := Set α) {x : α | (↑n : ℝ≥0∞)⁻¹ < edist (f i x) (g x)} x) ↔
    ∃ k ≥ j, (↑n : ℝ≥0∞)⁻¹ < edist (f k x) (g x)
⊢ x ∈ notConvergentSeq f g n j ↔ ∃ k ≥ j, (↑n : ℝ≥0∞)⁻¹ < edist (f k x) (g x)

Tactic:
simp_rw [notConvergentSeq, Set.mem_iUnion, exists_prop, mem_setOf]

Premises used: Set.mem_iUnion, MeasureTheory.Egorov.notConvergentSeq, exists_prop, Set.mem_setOf
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : PseudoEMetricSpace β
n : ℕ
f : ι → α → β
g : α → β
inst_1 : Preorder ι
⊢ Antitone (notConvergentSeq f g n)

Tactic:
fun _ _ hjk => Set.iUnion₂_mono' fun l hl => ⟨l, le_trans hjk hl, Set.Subset.rfl⟩

Premises used: MeasureTheory.Egorov.notConvergentSeq, Antitone, Set.Subset.rfl, Exists.intro, Set.iUnion₂_mono', le_trans
-- Module: Mathlib.MeasureTheory.Function.Egorov
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Nonempty ι
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
n : ℕ
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)
    (0 : ℝ≥0∞)

Tactic:
simp_rw [EMetric.tendsto_atTop, ae_iff] at hfg

Premises used: EMetric.tendsto_atTop, MeasureTheory.ae_iff