awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι
δ : ℝ≥0∞
hδ : 0 < δ
hδ_top : δ ≠ ∞
hfg : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ essSup (fun (x : α) ↦ ‖(f n - g) x‖ₑ) μ) l (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | δ ≤ edist (f i x) (g x)}) l (𝓝 0)
have 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)} ≤ ε
Tactic: rw [ENNReal.tendsto_nhds_zero] at hfg ⊢
Cleared hypotheses: hfg
-- 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 ι
δ : ℝ≥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, (μ : (a : Set α) → ℝ≥0∞) {x_1 : α | δ ≤ edist (f x x_1) (g x_1)} ≤ ε
have hfg₁ : ∀ᶠ (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⟩)
Cleared hypotheses: hfg
-- 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 ι
δ : ℝ≥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)} ≤ ε
have refine : ∀ (n : ι) (hn : essSup (fun (x : α) ↦ ‖(f n - g) x‖ₑ) μ ≤ δ / 2),
  (μ : (a : Set α) → ℝ≥0∞) {x : α | δ ≤ edist (f n x) (g x)} ≤ ε
Tactic: refine hfg.mono fun n hn => ?_
-- 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 ι
δ : ℝ≥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
⊢ (μ : (a : Set α) → ℝ≥0∞) {x : α | δ ≤ edist (f n x) (g x)} ≤ ε
have this : 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)
-- 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 ι
δ : ℝ≥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)} ≤ ε
have 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∞)
Tactic: refine ((le_of_eq ?_).trans (ae_lt_of_essSup_lt this).le).trans hε.le
-- 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 ι
δ : ℝ≥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‖ₑ) μ < δ
⊢ 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∞)
have h : ∀ (x : α), δ ≤ edist (f n x) (g x) ↔ x ∉ {x : α | (fun (y : α) ↦ ‖f n y - g y‖ₑ < δ) x}
Tactic: congr with x
-- 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 : 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)
⊢ TendstoInMeasure μ f l g
have pos : ∀ (hp_ne_top : p = ∞), TendstoInMeasure μ f l g
Tactic: by_cases hp_ne_top : p = ∞
-- 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 : 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
⊢ TendstoInMeasure μ f l g
have neg : ∀ (hp_ne_top : ¬p = ∞), TendstoInMeasure μ f l g
Tactic: by_cases hp_ne_top : p = ∞
-- 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 : 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
have hp_ne_zero₁ : Ne (α := ℝ≥0∞) ∞ 0
Tactic: subst hp_ne_top
Cleared hypotheses: p, hp_ne_zero, hfg, hp_ne_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 : 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
⊢ TendstoInMeasure μ f l g
have hfg₁ : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ eLpNorm (f n - g) ∞ μ) l (𝓝 0)
Tactic: subst hp_ne_top
Cleared hypotheses: p, hp_ne_zero, hfg, hp_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : PseudoEMetricSpace β
n : ℕ
j : ι
f : ι → α → β
g : α → β
inst_1 : Preorder ι
x : α
⊢ x ∈ notConvergentSeq f g n j ↔ ∃ k ≥ j, (↑n : ℝ≥0∞)⁻¹ < edist (f k x) (g x)
have 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)
Tactic: simp_rw [notConvergentSeq, Set.mem_iUnion, exists_prop, mem_setOf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
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)
⊢ x ∈ notConvergentSeq f g n j ↔ ∃ k ≥ j, (↑n : ℝ≥0∞)⁻¹ < edist (f k x) (g x)
have 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)
Tactic: simp_rw [notConvergentSeq, Set.mem_iUnion, exists_prop, mem_setOf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
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)
⊢ x ∈ notConvergentSeq f g n j ↔ ∃ k ≥ j, (↑n : ℝ≥0∞)⁻¹ < edist (f k x) (g x)
have 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)
Tactic: simp_rw [notConvergentSeq, Set.mem_iUnion, exists_prop, mem_setOf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (hypothesis)
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∞) (s ∩ ⋂ (j : ι), notConvergentSeq f g n j) : ℝ≥0∞) (0 : ℝ≥0∞)
have hfg₁ : 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
Cleared hypotheses: hfg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
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 ι
n : ℕ
hfg :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ ⋂ (j : ι), notConvergentSeq f g n j) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ ⋂ (j : ι), notConvergentSeq f g n j) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)
Tactic: rw [← nonpos_iff_eq_zero, ← hfg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
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 ι
n : ℕ
hfg :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ ⋂ (j : ι), notConvergentSeq f g n j) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)
have refine : ∀ x ∈ s ∩ ⋂ (j : ι), notConvergentSeq f g n j,
  Membership.mem (γ := Set α) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} x
Tactic: refine measure_mono fun x => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
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 ι
n : ℕ
hfg :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
x : α
⊢ x ∈ s ∩ ⋂ (j : ι), notConvergentSeq f g n j →
    Membership.mem (γ := Set α) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} x
have simp : (x ∈ s ∧ ∀ (i : ι), ∃ k ≥ i, (↑n : ℝ≥0∞)⁻¹ < edist (f k x) (g x)) →
  Membership.mem (γ := Set α) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} x
Tactic: simp only [Set.mem_inter_iff, Set.mem_iInter, mem_notConvergentSeq_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
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 ι
n : ℕ
hfg :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
x : α
⊢ (x ∈ s ∧ ∀ (i : ι), ∃ k ≥ i, (↑n : ℝ≥0∞)⁻¹ < edist (f k x) (g x)) →
    Membership.mem (γ := Set α) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} x
have push : (x ∈ s ∧ ∀ (i : ι), ∃ k ≥ i, (↑n : ℝ≥0∞)⁻¹ < edist (f k x) (g x)) →
  Membership.mem (γ := Set α) {a : α | a ∈ s ∧ ∃ ε > 0, ∀ (N : ι), ∃ n ≥ N, ε ≤ edist (f n a) (g a)} x
Tactic: push Not
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
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 ι
n : ℕ
hfg :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
x : α
hmem : x ∈ s
hx : ∀ (i : ι), ∃ k ≥ i, (↑n : ℝ≥0∞)⁻¹ < edist (f k x) (g x)
⊢ Membership.mem (γ := Set α) {a : α | a ∈ s ∧ ∃ ε > 0, ∀ (N : ι), ∃ n ≥ N, ε ≤ edist (f n a) (g a)} x
have refine : ∀ (N : ι), ∃ n_1 ≥ N, (↑n : ℝ≥0∞)⁻¹ ≤ edist (f n_1 x) (g x)
Tactic: refine ⟨hmem, (n : ℝ≥0∞)⁻¹, by simp, fun N => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
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 ι
n : ℕ
hfg :
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬(a ∈ s → ∀ ε > 0, ∃ (N : ι), ∀ n ≥ N, edist (f n a) (g a) < ε)} : ℝ≥0∞)
    (0 : ℝ≥0∞)
x : α
hmem : x ∈ s
hx : ∀ (i : ι), ∃ k ≥ i, (↑n : ℝ≥0∞)⁻¹ < edist (f k x) (g x)
N : ι
⊢ ∃ n_1 ≥ N, (↑n : ℝ≥0∞)⁻¹ ≤ edist (f n_1 x) (g x)
have obtain : ∀ (n_1 : ι) (hn₁ : n_1 ≥ N) (hn₂ : (↑n : ℝ≥0∞)⁻¹ < edist (f n_1 x) (g x)),
  ∃ n_2 ≥ N, (↑n : ℝ≥0∞)⁻¹ ≤ edist (f n_2 x) (g x)
Tactic: obtain ⟨n, hn₁, hn₂⟩ := hx N
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Countable ι
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
n : ℕ
⊢ Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)
have inl : ∀ (h : IsEmpty ι),
  Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)
Tactic: rcases isEmpty_or_nonempty ι with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Countable ι
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
n : ℕ
inl :
  ∀ (h : IsEmpty ι),
    Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)
have inr : ∀ (h : Nonempty ι),
  Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)
Tactic: rcases isEmpty_or_nonempty ι with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Countable ι
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
n : ℕ
h : IsEmpty ι
⊢ Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)
have this : Eq.{u_3 + 1} (α := (j : ι) → ℝ≥0∞) (fun (j : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j)) fun (j : ι) ↦
  0
Tactic: have : (fun j => μ (s ∩ notConvergentSeq f g n j)) = fun j => 0 := by
      simp only [eq_iff_true_of_subsingleton]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Countable ι
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
n : ℕ
h : IsEmpty ι
this :
  Eq.{u_3 + 1} (α := (j : ι) → ℝ≥0∞) (fun (j : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j))
    fun (j : ι) ↦ 0
⊢ Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)
have inl : Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ 0) atTop (𝓝 0)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
inst : PseudoEMetricSpace β
μ : Measure α
s : Set α
f : ι → α → β
g : α → β
inst_1 : SemilatticeSup ι
inst_2 : Countable ι
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
n : ℕ
h : Nonempty ι
⊢ Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j)) atTop (𝓝 0)
have inr : Tendsto (β := ℝ≥0∞) (fun (j : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j) : ℝ≥0∞)) atTop
  (𝓝 ((μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s ∩ notConvergentSeq f g n i)) : Filter ℝ≥0∞)
Tactic: rw [← measure_inter_notConvergentSeq_eq_zero hfg n, Set.inter_iInter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
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 ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
n : ℕ
⊢ ∃ (j : ι), (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)
have have : ∀ (N : ι)
  (hN :
    ∀ n_1 ≥ N,
      Membership.mem (α := ℝ≥0∞)
        (Icc (0 - ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)) (0 + ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)))
        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n n_1) : ℝ≥0∞)),
  ∃ (j : ι), (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)
Tactic: have ⟨N, hN⟩ := (ENNReal.tendsto_atTop ENNReal.zero_ne_top).1
    (measure_notConvergentSeq_tendsto_zero hf hsm hs hfg n) (.ofReal (ε * 2⁻¹ ^ n))
      (by positivity)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (hypothesis)
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 ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
n : ℕ
N : ι
hN :
  ∀ n_1 ≥ N,
    Membership.mem (α := ℝ≥0∞)
      (Icc (0 - ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)) (0 + ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)))
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n n_1) : ℝ≥0∞)
⊢ ∃ (j : ι), (μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n j) ≤ ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)
have hN₁ : ∀ n_1 ≥ N,
  Membership.mem (α := ℝ≥0∞)
    (Icc (0 - ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)) (ENNReal.ofReal (ε * HPow.hPow (α := ℝ) 2⁻¹ n)))
    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ notConvergentSeq f g n n_1) : ℝ≥0∞)
Tactic: rw [zero_add] at hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
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 ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
⊢ (μ : (a : Set α) → ℝ≥0∞) (iUnionNotConvergentSeq (s := s) hε hf hsm hs hfg) ≤ ENNReal.ofReal ε
have refine : ∑' (a : ℕ), ENNReal.ofReal (ε / 2 * HPow.hPow (α := ℝ) 2⁻¹ a) ≤ ENNReal.ofReal ε
Tactic: refine le_trans (measure_iUnion_le _) (le_trans
    (ENNReal.tsum_le_tsum <| notConvergentSeqLTIndex_spec (half_pos hε) hf hsm hs hfg) ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
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 ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
⊢ ∑' (a : ℕ), ENNReal.ofReal (ε / 2 * HPow.hPow (α := ℝ) 2⁻¹ a) ≤ ENNReal.ofReal ε
have simp_rw : ∑' (a : ℕ), ENNReal.ofReal (ε / 2) * ENNReal.ofReal (HPow.hPow (α := ℝ) 2⁻¹ a) ≤ ENNReal.ofReal ε
Tactic: simp_rw [ENNReal.ofReal_mul (half_pos hε).le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
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 ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
⊢ ∑' (a : ℕ), ENNReal.ofReal (ε / 2) * ENNReal.ofReal (HPow.hPow (α := ℝ) 2⁻¹ a) ≤ ENNReal.ofReal ε
have hf_nonneg : ∀ (n : ℕ), 0 ≤ HPow.hPow (α := ℝ) 2⁻¹ n
Tactic: rw [ENNReal.tsum_mul_left, ← ENNReal.ofReal_tsum_of_nonneg, inv_eq_one_div, tsum_geometric_two,
    ← ENNReal.ofReal_mul (half_pos hε).le, div_mul_cancel₀ ε two_ne_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.Egorov (goal)
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 ι
inst_3 : Countable ι
hε : 0 < ε
hf : ∀ (n : ι), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hsm : MeasurableSet s
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Tendsto (fun (n : ι) ↦ f n x) atTop (𝓝 (g x))
hf_nonneg : ∀ (n : ℕ), 0 ≤ HPow.hPow (α := ℝ) 2⁻¹ n
⊢ ∑' (a : ℕ), ENNReal.ofReal (ε / 2) * ENNReal.ofReal (HPow.hPow (α := ℝ) 2⁻¹ a) ≤ ENNReal.ofReal ε
have hf₁ : Summable (HPow.hPow (α := ℝ) 2⁻¹)
Tactic: rw [ENNReal.tsum_mul_left, ← ENNReal.ofReal_tsum_of_nonneg, inv_eq_one_div, tsum_geometric_two,
    ← ENNReal.ofReal_mul (half_pos hε).le, div_mul_cancel₀ ε two_ne_zero]