awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
inst_1 : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 :
  ∀ (ns : ℕ → ℕ),
    StrictMono ns →
      ∃ (ns' : ℕ → ℕ), StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
ε : ℝ≥0∞
hε : 0 < ε
h2 :
  ¬Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
      atTop (𝓝 0)
δ : ℝ≥0
ns : ℕ → ℕ
hδ : 0 < δ
hns : StrictMono ns
h3 : ∀ (n : ℕ), δ ≤ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)})
obtain :
  ∀ (ns' : ℕ → ℕ),
    StrictMono ns' → ∀ (h6 : ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))), False
⊢ False

Tactic:
obtain ⟨ns', _, h6⟩ := h1 ns hns
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
inst_1 : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 :
  ∀ (ns : ℕ → ℕ),
    StrictMono ns →
      ∃ (ns' : ℕ → ℕ), StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
ε : ℝ≥0∞
hε : 0 < ε
h2 :
  ¬Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
      atTop (𝓝 0)
δ : ℝ≥0
ns : ℕ → ℕ
hδ : 0 < δ
hns : StrictMono ns
h3 : ∀ (n : ℕ), δ ≤ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)})
ns' : ℕ → ℕ
left : StrictMono ns'
h6 : ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
⊢ ∀ (ε : ℝ≥0∞),
    0 < ε →
      Tendsto (β := ℝ≥0)
        (fun (i : ℕ) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns (ns' i)) x) (g x)})) atTop
        (𝓝 0)

Tactic:
have h7 := tendstoInMeasure_iff_tendsto_toNNReal.mp <|
    tendstoInMeasure_of_tendsto_ae (fun n ↦ hf _) h6
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
inst_1 : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 :
  ∀ (ns : ℕ → ℕ),
    StrictMono ns →
      ∃ (ns' : ℕ → ℕ), StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
ε : ℝ≥0∞
hε : 0 < ε
h2 :
  ¬Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
      atTop (𝓝 0)
δ : ℝ≥0
ns : ℕ → ℕ
hδ : 0 < δ
hns : StrictMono ns
h3 : ∀ (n : ℕ), δ ≤ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)})
ns' : ℕ → ℕ
left : StrictMono ns'
h6 : ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
h7 :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      Tendsto (β := ℝ≥0)
        (fun (i : ℕ) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns (ns' i)) x) (g x)})) atTop
        (𝓝 0)
⊢ False

Tactic:
lt_irrefl _ (lt_of_le_of_lt (ge_of_tendsto' (h7 ε hε) (fun n ↦ h3 _)) hδ)

Premises used: lt_of_le_of_lt, lt_irrefl, ge_of_tendsto'
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
inst_1 : IsFiniteMeasure μ
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
g : α → E
h1 :
  ∀ (ns : ℕ → ℕ),
    StrictMono ns →
      ∃ (ns' : ℕ → ℕ), StrictMono ns' ∧ ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
ε : ℝ≥0∞
hε : 0 < ε
h2 :
  ¬Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
      atTop (𝓝 0)
δ : ℝ≥0
ns : ℕ → ℕ
hδ : 0 < δ
hns : StrictMono ns
h3 : ∀ (n : ℕ), δ ≤ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)})
ns' : ℕ → ℕ
left : StrictMono ns'
h6 : ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))
h7 :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      Tendsto (β := ℝ≥0)
        (fun (i : ℕ) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns (ns' i)) x) (g x)})) atTop
        (𝓝 0)
⊢ False

Tactic:
exact lt_irrefl _ (lt_of_le_of_lt (ge_of_tendsto' (h7 ε hε) (fun n ↦ h3 _)) hδ)

Premises used: lt_of_le_of_lt, lt_irrefl, ge_of_tendsto'
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst : SeminormedAddGroup E
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
C p : ℝ≥0∞
bound : ∀ᶠ (i : ι) in u, eLpNorm (f i) p μ ≤ C
h_tendsto : TendstoInMeasure μ f u g
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
obtain :
  ∀ (l : ℕ → ι) (hl : Tendsto l atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (l i) x) atTop (𝓝 (g x))),
    eLpNorm g p μ ≤ C
⊢ eLpNorm g p μ ≤ C

Tactic:
obtain ⟨l, hl⟩ := h_tendsto.exists_seq_tendsto_ae'

Premises used: MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae'
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst : SeminormedAddGroup E
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
C p : ℝ≥0∞
bound : ∀ᶠ (i : ι) in u, eLpNorm (f i) p μ ≤ C
h_tendsto : TendstoInMeasure μ f u g
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
l : ℕ → ι
hl : Tendsto l atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (l i) x) atTop (𝓝 (g x))
⊢ eLpNorm g p μ ≤ C

Tactic:
Lp.eLpNorm_le_of_ae_tendsto (hl.1.eventually bound) (fun n => hf (l n)) hl.2

Premises used: And.right, And.left, Filter.Tendsto.eventually, MeasureTheory.Lp.eLpNorm_le_of_ae_tendsto
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst : SeminormedAddGroup E
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
C p : ℝ≥0∞
bound : ∀ᶠ (i : ι) in u, eLpNorm (f i) p μ ≤ C
h_tendsto : TendstoInMeasure μ f u g
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
l : ℕ → ι
hl : Tendsto l atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (l i) x) atTop (𝓝 (g x))
⊢ eLpNorm g p μ ≤ C

Tactic:
exact Lp.eLpNorm_le_of_ae_tendsto (hl.1.eventually bound) (fun n => hf (l n)) hl.2

Premises used: And.right, And.left, Filter.Tendsto.eventually, MeasureTheory.Lp.eLpNorm_le_of_ae_tendsto
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EMetricSpace E
g h : α → E
f : ι → α → E
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
hg : TendstoInMeasure μ f u g
hh : TendstoInMeasure μ f u h
obtain :
  ∀ (ns : ℕ → ι) (h1 : Tendsto ns atTop u) (h1' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))),
    g =ᶠ[ae μ] h
⊢ g =ᶠ[ae μ] h

Tactic:
obtain ⟨ns, h1, h1'⟩ := hg.exists_seq_tendsto_ae'

Premises used: MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae'
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EMetricSpace E
g h : α → E
f : ι → α → E
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
hg : TendstoInMeasure μ f u g
hh : TendstoInMeasure μ f u h
ns : ℕ → ι
h1 : Tendsto ns atTop u
h1' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
obtain :
  ∀ (ns' : ℕ → ℕ) (h2 : Tendsto ns' atTop atTop)
    (h2' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ (f ∘ ns) (ns' i) x) atTop (𝓝 (h x))), g =ᶠ[ae μ] h
⊢ g =ᶠ[ae μ] h

Tactic:
obtain ⟨ns', h2, h2'⟩ := (hh.comp h1).exists_seq_tendsto_ae'

Premises used: MeasureTheory.TendstoInMeasure.comp, MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae'
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EMetricSpace E
g h : α → E
f : ι → α → E
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
hg : TendstoInMeasure μ f u g
hh : TendstoInMeasure μ f u h
ns : ℕ → ι
h1 : Tendsto ns atTop u
h1' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
ns' : ℕ → ℕ
h2 : Tendsto ns' atTop atTop
h2' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ (f ∘ ns) (ns' i) x) atTop (𝓝 (h x))
h₁ :
  ∀ (ω : α) (hg1 : Tendsto (fun (i : ℕ) ↦ f (ns i) ω) atTop (𝓝 (g ω)))
    (hh1 : Tendsto (fun (i : ℕ) ↦ (f ∘ ns) (ns' i) ω) atTop (𝓝 (h ω))), g ω = h ω
⊢ g =ᶠ[ae μ] h

Tactic:
filter_upwards [h1', h2'] with ω hg1 hh1
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EMetricSpace E
g h : α → E
f : ι → α → E
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
hg : TendstoInMeasure μ f u g
hh : TendstoInMeasure μ f u h
ns : ℕ → ι
h1 : Tendsto ns atTop u
h1' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
ns' : ℕ → ℕ
h2 : Tendsto ns' atTop atTop
h2' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ (f ∘ ns) (ns' i) x) atTop (𝓝 (h x))
ω : α
hg1 : Tendsto (fun (i : ℕ) ↦ f (ns i) ω) atTop (𝓝 (g ω))
hh1 : Tendsto (fun (i : ℕ) ↦ (f ∘ ns) (ns' i) ω) atTop (𝓝 (h ω))
⊢ g ω = h ω

Tactic:
tendsto_nhds_unique (hg1.comp h2) hh1

Premises used: Filter.Tendsto.comp, tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EMetricSpace E
g h : α → E
f : ι → α → E
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
hg : TendstoInMeasure μ f u g
hh : TendstoInMeasure μ f u h
ns : ℕ → ι
h1 : Tendsto ns atTop u
h1' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
ns' : ℕ → ℕ
h2 : Tendsto ns' atTop atTop
h2' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ (f ∘ ns) (ns' i) x) atTop (𝓝 (h x))
ω : α
hg1 : Tendsto (fun (i : ℕ) ↦ f (ns i) ω) atTop (𝓝 (g ω))
hh1 : Tendsto (fun (i : ℕ) ↦ (f ∘ ns) (ns' i) ω) atTop (𝓝 (h ω))
⊢ g ω = h ω

Tactic:
exact tendsto_nhds_unique (hg1.comp h2) hh1

Premises used: Filter.Tendsto.comp, tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h_tendsto : TendstoInMeasure μ f u g
obtain :
  ∀ (ns : ℕ → ι) (hns : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))), AEStronglyMeasurable g μ
⊢ AEStronglyMeasurable g μ

Tactic:
obtain ⟨ns, -, hns⟩ := h_tendsto.exists_seq_tendsto_ae'

Premises used: MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae'
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h_tendsto : TendstoInMeasure μ f u g
ns : ℕ → ι
hns : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
⊢ AEStronglyMeasurable g μ

Tactic:
aestronglyMeasurable_of_tendsto_ae atTop (fun n => hf (ns n)) hns

Premises used: aestronglyMeasurable_of_tendsto_ae, Filter.atTop
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
u : Filter ι
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hf : ∀ (n : ι), AEStronglyMeasurable (f n) μ
h_tendsto : TendstoInMeasure μ f u g
ns : ℕ → ι
hns : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
⊢ AEStronglyMeasurable g μ

Tactic:
exact aestronglyMeasurable_of_tendsto_ae atTop (fun n => hf (ns n)) hns

Premises used: aestronglyMeasurable_of_tendsto_ae, Filter.atTop
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
u : Filter ι
inst_3 : u.NeBot
inst_4 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : TendstoInMeasure μ f u g
obtain : ∀ (ns : ℕ → ι) (hns : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))), AEMeasurable g μ
⊢ AEMeasurable g μ

Tactic:
obtain ⟨ns, -, hns⟩ := h_tendsto.exists_seq_tendsto_ae'

Premises used: MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae'
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
u : Filter ι
inst_3 : u.NeBot
inst_4 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : TendstoInMeasure μ f u g
ns : ℕ → ι
hns : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
⊢ AEMeasurable g μ

Tactic:
aemeasurable_of_tendsto_metrizable_ae atTop (fun n => hf (ns n)) hns

Premises used: Filter.atTop, aemeasurable_of_tendsto_metrizable_ae
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
u : Filter ι
inst_3 : u.NeBot
inst_4 : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : TendstoInMeasure μ f u g
ns : ℕ → ι
hns : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))
⊢ AEMeasurable g μ

Tactic:
exact aemeasurable_of_tendsto_metrizable_ae atTop (fun n => hf (ns n)) hns

Premises used: Filter.atTop, aemeasurable_of_tendsto_metrizable_ae
-- 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 ι
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) 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
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 ι
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) 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
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 ι
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
⊢ 1 / ε ^ 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 : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) p μ) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
⊢ Tendsto (fun (b : ι) ↦ 1 / ε ^ p.toReal * eLpNorm (f b - g) p μ ^ p.toReal) l
    (𝓝 (1 / ε ^ p.toReal * HPow.hPow (α := ℝ≥0∞) 0 p.toReal))

Tactic:
replace hfg := ENNReal.Tendsto.const_mul (a := 1 / ε ^ p.toReal)
    (Tendsto.ennrpow_const p.toReal hfg) (Or.inr <| by simp [hε.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 : ι), StronglyMeasurable (f n)
hg : StronglyMeasurable g
l : Filter ι
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
hfg :
  Tendsto (fun (b : ι) ↦ 1 / ε ^ p.toReal * eLpNorm (f b - g) p μ ^ p.toReal) l
    (𝓝 (1 / ε ^ p.toReal * HPow.hPow (α := ℝ≥0∞) 0 p.toReal))
⊢ Tendsto (β := ℝ≥0∞) (fun (b : ι) ↦ 1 / ε ^ p.toReal * eLpNorm (f b - g) p μ ^ p.toReal) l (𝓝 0)

Tactic:
simp only [mul_zero,
    ENNReal.zero_rpow_of_pos (ENNReal.toReal_pos hp_ne_zero hp_ne_top)] at hfg

Premises used: ENNReal.zero_rpow_of_pos, MulZeroClass.mul_zero, ENNReal.toReal_pos
-- 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 : Tendsto (β := ℝ≥0∞) (fun (b : ι) ↦ 1 / ε ^ p.toReal * eLpNorm (f b - g) p μ ^ p.toReal) l (𝓝 0)
rw :
  ∀ (hfg : ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, 1 / ε ^ p.toReal * eLpNorm (f x - g) p μ ^ p.toReal ≤ ε_1),
    ∀ ε_1 > 0, ∀ᶠ (x : ι) in l, (μ : (a : Set α) → ℝ≥0∞) {x_1 : α | ε ≤ edist (f x x_1) (g x_1)} ≤ ε_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
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
⊢ ∀ᶠ (x : ι) in l, (μ : (a : Set α) → ℝ≥0∞) {x_1 : α | ε ≤ edist (f x x_1) (g x_1)} ≤ δ

Tactic:
(hfg δ hδ).mono fun n hn => ?_

Premises used: Filter.Eventually.mono
-- 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
refine :
  ∀ (n : ι) (hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ),
    (μ : (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 δ hδ).mono fun n hn => ?_

Premises used: Filter.Eventually.mono
-- 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 ≤ δ
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ δ

Tactic:
le_trans ?_ hn

Premises used: le_trans
-- 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 ≤ δ
refine :
  (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ δ

Tactic:
refine le_trans ?_ hn

Premises used: le_trans
-- 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 ≤ δ
rw :
  HMul.hMul (β := ℝ≥0∞) (ε ^ p.toReal) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} : ℝ≥0∞) ≤
    eLpNorm (f n - g) p μ ^ p.toReal
h1 : (ε ^ p.toReal)⁻¹ ≠ 0
h2 : (ε ^ p.toReal)⁻¹ ≠ ∞
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal

Tactic:
rw [one_div, ← ENNReal.inv_mul_le_iff, inv_inv]

Premises used: ENNReal.inv_mul_le_iff, inv_inv, one_div
-- 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 ≤ δ
⊢ HMul.hMul (β := ℝ≥0∞) (ε ^ p.toReal) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖(f n - g) x‖ₑ} : ℝ≥0∞) ≤
    eLpNorm (f n - g) p μ ^ p.toReal

Tactic:
mul_meas_ge_le_pow_eLpNorm' μ hp_ne_zero hp_ne_top ((hf n).sub hg).aestronglyMeasurable ε

Premises used: MeasureTheory.mul_meas_ge_le_pow_eLpNorm', MeasureTheory.StronglyMeasurable.sub, MeasureTheory.StronglyMeasurable.aestronglyMeasurable
-- 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 ≤ δ
h : ∀ (x : α), edist (f n x) (g x) = ‖(f n - g) x‖ₑ
⊢ HMul.hMul (β := ℝ≥0∞) (ε ^ p.toReal) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} : ℝ≥0∞) ≤
    eLpNorm (f n - g) p μ ^ p.toReal

Tactic:
convert!
      mul_meas_ge_le_pow_eLpNorm' μ hp_ne_zero hp_ne_top ((hf n).sub hg).aestronglyMeasurable ε
      using 6

Premises used: MeasureTheory.mul_meas_ge_le_pow_eLpNorm', MeasureTheory.StronglyMeasurable.sub, MeasureTheory.StronglyMeasurable.aestronglyMeasurable