awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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 : ℕ → ℕ),
    0 < δ ∧
      StrictMono ns ∧ ∀ (n : ℕ), δ ≤ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)})
have obtain : ∀ (s : Set ℝ≥0) (hs : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) s)
  (h4 : ∃ᶠ (x : ℕ) in atTop, ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x_1 : α | ε ≤ edist (f x x_1) (g x_1)}) ∉ s),
  ∃ (δ : ℝ≥0) (ns : ℕ → ℕ),
    0 < δ ∧
      StrictMono ns ∧ ∀ (n : ℕ), δ ≤ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)})
Tactic: obtain ⟨s, hs, h4⟩ := not_tendsto_iff_exists_frequently_notMem.1 h2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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)
s : Set ℝ≥0
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) s
h4 : ∃ᶠ (x : ℕ) in atTop, ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x_1 : α | ε ≤ edist (f x x_1) (g x_1)}) ∉ s
⊢ ∃ (δ : ℝ≥0) (ns : ℕ → ℕ),
    0 < δ ∧
      StrictMono ns ∧ ∀ (n : ℕ), δ ≤ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)})
have obtain : ∀ (δ : ℝ≥0) (hδ : 0 < δ) (h5 : Set.Iio δ ⊆ s),
  ∃ (δ : ℝ≥0) (ns : ℕ → ℕ),
    0 < δ ∧
      StrictMono ns ∧ ∀ (n : ℕ), δ ≤ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)})
Tactic: obtain ⟨δ, hδ, h5⟩ := NNReal.nhds_zero_basis.mem_iff.1 hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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)
s : Set ℝ≥0
hs : Membership.mem (γ := Filter ℝ≥0) (𝓝 0) s
h4 : ∃ᶠ (x : ℕ) in atTop, ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x_1 : α | ε ≤ edist (f x x_1) (g x_1)}) ∉ s
δ : ℝ≥0
hδ : 0 < δ
h5 : Set.Iio δ ⊆ s
⊢ ∃ (δ : ℝ≥0) (ns : ℕ → ℕ),
    0 < δ ∧
      StrictMono ns ∧ ∀ (n : ℕ), δ ≤ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)})
have obtain : ∀ (ns : ℕ → ℕ) (hns : StrictMono ns)
  (h6 : ∀ (n : ℕ), ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)}) ∉ s),
  ∃ (δ : ℝ≥0) (ns : ℕ → ℕ),
    0 < δ ∧
      StrictMono ns ∧ ∀ (n : ℕ), δ ≤ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)})
Tactic: obtain ⟨ns, hns, h6⟩ := extraction_of_frequently_atTop h4
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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)
⊢ False
have obtain : ∀ (δ : ℝ≥0) (ns : ℕ → ℕ) (hδ : 0 < δ) (hns : StrictMono ns)
  (h3 : ∀ (n : ℕ), δ ≤ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f (ns n) x) (g x)})), False
Tactic: obtain ⟨δ, ns, hδ, hns, h3⟩ : ∃ (δ : ℝ≥0) (ns : ℕ → ℕ), 0 < δ ∧ StrictMono ns ∧
      ∀ n, δ ≤ (μ {x | ε ≤ edist (f (ns n) x) (g x)}).toNNReal := by
    obtain ⟨s, hs, h4⟩ := not_tendsto_iff_exists_frequently_notMem.1 h2
    obtain ⟨δ, hδ, h5⟩ := NNReal.nhds_zero_basis.mem_iff.1 hs
    obtain ⟨ns, hns, h6⟩ := extraction_of_frequently_atTop h4
    exact ⟨δ, ns, hδ, hns, fun n ↦ Set.notMem_Iio.1 (Set.notMem_subset h5 (h6 n))⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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)})
⊢ False
have obtain : ∀ (ns' : ℕ → ℕ),
  StrictMono ns' → ∀ (h6 : ∀ᵐ (ω : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ns' i)) ω) atTop (𝓝 (g ω))), False
Tactic: obtain ⟨ns', _, h6⟩ := h1 ns hns
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
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 ω))
⊢ False
have h7 : ∀ (ε : ℝ≥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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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) μ
⊢ eLpNorm g p μ ≤ C
have obtain : ∀ (l : ℕ → ι) (hl : Tendsto l atTop u ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (l i) x) atTop (𝓝 (g x))),
  eLpNorm g p μ ≤ C
Tactic: obtain ⟨l, hl⟩ := h_tendsto.exists_seq_tendsto_ae'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
⊢ g =ᶠ[ae μ] h
have obtain : ∀ (ns : ℕ → ι) (h1 : Tendsto ns atTop u) (h1' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))),
  g =ᶠ[ae μ] h
Tactic: obtain ⟨ns, h1, h1'⟩ := hg.exists_seq_tendsto_ae'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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))
⊢ g =ᶠ[ae μ] h
have obtain : ∀ (ns' : ℕ → ℕ) (h2 : Tendsto ns' atTop atTop)
  (h2' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ (f ∘ ns) (ns' i) x) atTop (𝓝 (h x))), g =ᶠ[ae μ] h
Tactic: obtain ⟨ns', h2, h2'⟩ := (hh.comp h1).exists_seq_tendsto_ae'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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))
⊢ g =ᶠ[ae μ] h
have h₁ : ∀ (ω : α) (hg1 : Tendsto (fun (i : ℕ) ↦ f (ns i) ω) atTop (𝓝 (g ω)))
  (hh1 : Tendsto (fun (i : ℕ) ↦ (f ∘ ns) (ns' i) ω) atTop (𝓝 (h ω))), g ω = h ω
Tactic: filter_upwards [h1', h2'] with ω hg1 hh1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
⊢ AEStronglyMeasurable g μ
have obtain : ∀ (ns : ℕ → ι) (hns : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))), AEStronglyMeasurable g μ
Tactic: obtain ⟨ns, -, hns⟩ := h_tendsto.exists_seq_tendsto_ae'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
⊢ AEMeasurable g μ
have obtain : ∀ (ns : ℕ → ι) (hns : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns i) x) atTop (𝓝 (g x))), AEMeasurable g μ
Tactic: obtain ⟨ns, -, hns⟩ := h_tendsto.exists_seq_tendsto_ae'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
have refine : ∀ (ε : ℝ≥0∞) (hε : 0 < ε) (hε_top : ε ≠ ∞),
  Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
Tactic: refine tendstoInMeasure_of_ne_top fun ε hε hε_top ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
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 (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
have hfg₁ : 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'])
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
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 (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
have hfg₁ : 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
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
have 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
Tactic: rw [ENNReal.tendsto_nhds_zero] at hfg ⊢
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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)} ≤ δ
have refine : ∀ (n : ι) (hn : 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal ≤ δ),
  (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ δ
Tactic: refine (hfg δ hδ).mono fun n hn => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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)} ≤ δ
have refine : (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal
Tactic: refine le_trans ?_ hn
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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)} ≤ 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal
have rw : HMul.hMul (β := ℝ≥0∞) (ε ^ p.toReal) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} : ℝ≥0∞) ≤
  eLpNorm (f n - g) p μ ^ p.toReal
Tactic: rw [one_div, ← ENNReal.inv_mul_le_iff, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal
have h1 : (ε ^ p.toReal)⁻¹ ≠ 0
Tactic: rw [one_div, ← ENNReal.inv_mul_le_iff, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ 1 / ε ^ p.toReal * eLpNorm (f n - g) p μ ^ p.toReal
have h2 : (ε ^ p.toReal)⁻¹ ≠ ∞
Tactic: rw [one_div, ← ENNReal.inv_mul_le_iff, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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 : α | ε ≤ edist (f n x) (g x)} : ℝ≥0∞) ≤
    eLpNorm (f n - g) p μ ^ p.toReal
have h : ∀ (x : α), edist (f n x) (g x) = ‖(f n - g) x‖ₑ
Tactic: convert!
      mul_meas_ge_le_pow_eLpNorm' μ hp_ne_zero hp_ne_top ((hf n).sub hg).aestronglyMeasurable ε
      using 6
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
have refine : TendstoInMeasure μ (fun (i : ι) ↦ AEStronglyMeasurable.mk (f i) sorry) l (AEStronglyMeasurable.mk g hg)
Tactic: refine TendstoInMeasure.congr (fun i => (hf i).ae_eq_mk.symm) hg.ae_eq_mk.symm ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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)
have refine : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (AEStronglyMeasurable.mk (f n) sorry - AEStronglyMeasurable.mk g hg) p μ) l (𝓝 0)
Tactic: refine tendstoInMeasure_of_tendsto_eLpNorm_of_stronglyMeasurable
    hp_ne_zero hp_ne_top (fun i => (hf i).stronglyMeasurable_mk) hg.stronglyMeasurable_mk ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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 μ
have h : ∀ (n : ι), eLpNorm (AEStronglyMeasurable.mk (f n) sorry - AEStronglyMeasurable.mk g hg) p μ = eLpNorm (f n - g) p μ
Tactic: ext1 n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
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)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (AEStronglyMeasurable.mk (f n) ⋯ - AEStronglyMeasurable.mk g hg) p μ) l
    (𝓝 0)
have this : Eq.{u_2 + 1} (α := (n : ι) → ℝ≥0∞)
  (fun (n : ι) ↦ eLpNorm (AEStronglyMeasurable.mk (f n) sorry - 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
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
have refine : ∀ (δ : ℝ≥0∞) (hδ : 0 < δ) (hδ_top : δ ≠ ∞),
  Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | δ ≤ edist (f i x) (g x)}) l (𝓝 0)
Tactic: refine tendstoInMeasure_of_ne_top fun δ hδ hδ_top ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
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 (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | δ ≤ edist (f i x) (g x)}) l (𝓝 0)
have hfg₁ : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ essSup (fun (x : α) ↦ ‖(f n - g) x‖ₑ) μ) l (𝓝 0)
Tactic: simp only [eLpNorm_exponent_top, eLpNormEssSup] at hfg
Cleared hypotheses: hfg