awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ),
    0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
have h₁ : ∀ (i : ι) (a : α), ε ≤ edist (f i a) (g a) ↔ ε.toReal ≤ dist (f i a) (g a)
Tactic: convert! h ε.toReal (ENNReal.toReal_pos hε.ne' hε_top) with i a
-- 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 : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ),
    0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
i : ι
a : α
⊢ ε ≤ edist (f i a) (g a) ↔ ε.toReal ≤ dist (f i a) (g a)
have h₁ : ε ≤ ENNReal.ofReal (dist (f i a) (g a)) ↔ ε.toReal ≤ dist (f i a) (g a)
Tactic: rw [edist_dist, ENNReal.le_ofReal_iff_toReal_le hε_top (by positivity)]
-- 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 : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ),
    0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
i : ι
a : α
h₁ : ε ≤ ENNReal.ofReal (dist (f i a) (g a)) ↔ ε.toReal ≤ dist (f i a) (g a)
⊢ ε ≤ edist (f i a) (g a) ↔ ε.toReal ≤ dist (f i a) (g a)
have h₂ : ε.toReal ≤ dist (f i a) (g a) ↔ ε.toReal ≤ dist (f i a) (g a)
Tactic: rw [edist_dist, ENNReal.le_ofReal_iff_toReal_le hε_top (by positivity)]
-- 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 : PseudoMetricSpace E
inst_1 : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
have rw : (∀ (ε : ℝ),
    0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)) ↔
  ∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
Tactic: rw [tendstoInMeasure_iff_dist]
-- 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 : PseudoMetricSpace E
inst_1 : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
⊢ (∀ (ε : ℝ),
      0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)) ↔
    ∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
have a : ∀ (ε : ℝ) (hε : 0 < ε),
  Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0) ↔
    Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
Tactic: congr! with ε hε hε_top
-- 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 : SeminormedAddCommGroup E
l : Filter ι
f : ι → α → E
g : α → E
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f i x - g x‖}) l (𝓝 0)
have simp_rw : (∀ (ε : ℝ),
    0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)) ↔
  ∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f i x - g x‖}) l (𝓝 0)
Tactic: simp_rw [tendstoInMeasure_iff_dist, dist_eq_norm_sub]
-- 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 : SeminormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
l : Filter ι
f : ι → α → E
g : α → E
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ ‖f i x - g x‖}) l (𝓝 0)
have rw : (∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f i x - g x‖}) l (𝓝 0)) ↔
  ∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ ‖f i x - g x‖}) l (𝓝 0)
Tactic: rw [tendstoInMeasure_iff_norm]
-- 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 : SeminormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
l : Filter ι
f : ι → α → E
g : α → E
⊢ (∀ (ε : ℝ),
      0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f i x - g x‖}) l (𝓝 0)) ↔
    ∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ ‖f i x - g x‖}) l (𝓝 0)
have a : ∀ (ε : ℝ) (hε : 0 < ε),
  Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f i x - g x‖}) l (𝓝 0) ↔
    Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ ‖f i x - g x‖}) l (𝓝 0)
Tactic: congr! with ε 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 α
inst : EDist E
inst_1 : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ≥0∞),
      0 < ε →
        Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
          l (𝓝 0)
have hfin : ∀ (ε : ℝ≥0∞) (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hfin ε i : μ { x | ε ≤ edist (f i x) (g x) } ≠ ⊤ :=
    measure_ne_top μ {x | ε ≤ edist (f i x) (g 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 α
inst : EDist E
inst_1 : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin :
  ∀ (ε : ℝ≥0∞) (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ≥0∞),
      0 < ε →
        Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
          l (𝓝 0)
have refine_1 : ∀ (h : TendstoInMeasure μ f l g) (ε : ℝ≥0∞) (hε : 0 < ε),
  Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)})) l
    (𝓝 0)
Tactic: refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ?_⟩
-- 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 : EDist E
inst_1 : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin :
  ∀ (ε : ℝ≥0∞) (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 :
  ∀ (h : TendstoInMeasure μ f l g) (ε : ℝ≥0∞) (hε : 0 < ε),
    Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)})) l
      (𝓝 0)
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ≥0∞),
      0 < ε →
        Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
          l (𝓝 0)
have refine_2 : ∀
  (h :
    ∀ (ε : ℝ≥0∞),
      0 < ε →
        Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
          l (𝓝 0))
  (ε : ℝ≥0∞) (hε : 0 < ε),
  Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
Tactic: refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
inst_1 : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin :
  ∀ (ε : ℝ≥0∞) (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞) (∞ : ℝ≥0∞)
h : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
⊢ Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)})) l
    (𝓝 0)
have hf : Eq.{u_2 + 1} (α := (i : ι) → ℝ≥0)
  (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
  (ENNReal.toNNReal ∘ fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)})
Tactic: have hf : (fun i => (μ { x | ε ≤ edist (f i x) (g x) }).toNNReal) =
        ENNReal.toNNReal ∘ (fun i ↦ (μ { x | ε ≤ edist (f i x) (g x) })) := rfl
-- 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 : EDist E
inst_1 : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin :
  ∀ (ε : ℝ≥0∞) (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞) (∞ : ℝ≥0∞)
h : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
hf :
  Eq.{u_2 + 1} (α := (i : ι) → ℝ≥0)
    (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
    (ENNReal.toNNReal ∘ fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)})
⊢ Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)})) l
    (𝓝 0)
have refine_1 : Tendsto (fun (x : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x_1 : α | ε ≤ edist (f x x_1) (g x_1)}) l (𝓝 (↑0 : ℝ≥0∞))
Tactic: rw [hf, ENNReal.tendsto_toNNReal_iff' (hfin ε)]
-- 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 : EDist E
inst_1 : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin :
  ∀ (ε : ℝ≥0∞) (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)})) l
        (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
have refine_2 : Tendsto (ENNReal.toNNReal ∘ fun (x : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x_1 : α | ε ≤ edist (f x x_1) (g x_1)}) l
  (𝓝 (ENNReal.toNNReal 0))
Tactic: rw [← ENNReal.tendsto_toNNReal_iff ENNReal.zero_ne_top (hfin ε)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst : PseudoEMetricSpace F
inst_1 : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
⊢ TendstoInMeasure μ (fun (i : ι) ↦ s.indicator (f i)) l (s.indicator g)
have refine_1 : ∀ (ε : ℝ≥0∞) (hε : 0 < ε),
  LE.le.{u_2} (α := ι → ℝ≥0∞) (fun (x : ι) ↦ 0) fun (i : ι) ↦
    (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist ((fun (i : ι) ↦ s.indicator (f i)) i x) (s.indicator g x)}
Tactic: refine fun ε hε => tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds (hg ε hε) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst : PseudoEMetricSpace F
inst_1 : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
refine_1 :
  ∀ (ε : ℝ≥0∞) (hε : 0 < ε),
    LE.le.{u_2} (α := ι → ℝ≥0∞) (fun (x : ι) ↦ 0) fun (i : ι) ↦
      (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist ((fun (i : ι) ↦ s.indicator (f i)) i x) (s.indicator g x)}
⊢ TendstoInMeasure μ (fun (i : ι) ↦ s.indicator (f i)) l (s.indicator g)
have refine_2 : ∀ (ε : ℝ≥0∞) (hε : 0 < ε),
  LE.le.{u_2} (α := ι → ℝ≥0∞)
    (fun (i : ι) ↦
      (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist ((fun (i : ι) ↦ s.indicator (f i)) i x) (s.indicator g x)})
    fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}
Tactic: refine fun ε hε => tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds (hg ε hε) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst : PseudoEMetricSpace F
inst_1 : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
⊢ LE.le.{u_2} (α := ι → ℝ≥0∞)
    (fun (i : ι) ↦
      (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist ((fun (i : ι) ↦ s.indicator (f i)) i x) (s.indicator g x)})
    fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}
have refine_2 : ∀ (n : ι) (x : α)
  (hx : Membership.mem (γ := Set α) {x : α | ε ≤ edist ((fun (i : ι) ↦ s.indicator (f i)) n x) (s.indicator g x)} x),
  Membership.mem (γ := Set α) {x : α | ε ≤ edist (f n x) (g x)} x
Tactic: refine fun n => measure_mono (fun x hx => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst : PseudoEMetricSpace F
inst_1 : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
n : ι
x : α
hx : Membership.mem (γ := Set α) {x : α | ε ≤ edist ((fun (i : ι) ↦ s.indicator (f i)) n x) (s.indicator g x)} x
⊢ Membership.mem (γ := Set α) {x : α | ε ≤ edist (f n x) (g x)} x
have pos : x ∈ s → Membership.mem (γ := Set α) {x : α | ε ≤ edist (f n x) (g x)} x
Tactic: by_cases x ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
ι : Type u_2
m : MeasurableSpace α
μ : Measure α
l : Filter ι
F : Type u_5
inst : PseudoEMetricSpace F
inst_1 : Zero F
f : ι → α → F
g : α → F
hg : TendstoInMeasure μ f l g
s : Set α
ε : ℝ≥0∞
hε : 0 < ε
n : ι
x : α
hx : Membership.mem (γ := Set α) {x : α | ε ≤ edist ((fun (i : ι) ↦ s.indicator (f i)) n x) (s.indicator g x)} x
pos : x ∈ s → Membership.mem (γ := Set α) {x : α | ε ≤ edist (f n x) (g x)} x
⊢ Membership.mem (γ := Set α) {x : α | ε ≤ edist (f n x) (g x)} x
have neg : x ∉ s → Membership.mem (γ := Set α) {x : α | ε ≤ edist (f n x) (g x)} x
Tactic: by_cases x ∈ s
-- 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 : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
this :
  l.EventuallyEq (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f' i x) (g' x)}) fun (i : ι) ↦
    (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f' i x) (g' x)}) l (𝓝 0)
have rw : Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
Tactic: rw [tendsto_congr' this]
-- 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 : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f' i x) (g' x)}) l (𝓝 0)
have i : l.EventuallyEq (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f' i x) (g' x)}) fun (i : ι) ↦
  (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}
Tactic: suffices
    (fun i ↦ μ { x | ε ≤ edist (f' i x) (g' x) }) =ᶠ[l] fun i ↦ μ { x | ε ≤ edist (f i x) (g x) } by
    rw [tendsto_congr' this]
    exact h_tendsto ε hε
-- 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 : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
⊢ l.EventuallyEq (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f' i x) (g' x)}) fun (i : ι) ↦
    (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}
have h : ∀ (i : ι) (h_ae_eq : f i =ᶠ[ae μ] f' i),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f' i x) (g' x)} : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞)
Tactic: filter_upwards [h_left] with i h_ae_eq
-- 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 : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
i : ι
h_ae_eq : f i =ᶠ[ae μ] f' i
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f' i x) (g' x)} : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞)
have h : {x : α | ε ≤ edist (f' i x) (g' x)} =ᶠ[ae μ] {x : α | ε ≤ edist (f i x) (g x)}
Tactic: refine measure_congr ?_
-- 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 : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
i : ι
h_ae_eq : f i =ᶠ[ae μ] f' i
⊢ {x : α | ε ≤ edist (f' i x) (g' x)} =ᶠ[ae μ] {x : α | ε ≤ edist (f i x) (g x)}
have h : ∀ (x : α) (hxf : f i x = f' i x) (hxg : g x = g' x),
  {x : α | ε ≤ edist (f' i x) (g' x)} x = {x : α | ε ≤ edist (f i x) (g x)} x
Tactic: filter_upwards [h_ae_eq, h_right] with x hxf hxg
-- 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 : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
i : ι
h_ae_eq : f i =ᶠ[ae μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ {x : α | ε ≤ edist (f' i x) (g' x)} x = {x : α | ε ≤ edist (f i x) (g x)} x
have h : {x : α | ε ≤ edist (f' i x) (g' x)} x ↔ {x : α | ε ≤ edist (f i x) (g x)} x
Tactic: rw [eq_iff_iff]
-- 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 : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
i : ι
h_ae_eq : f i =ᶠ[ae μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ ε ≤ edist (f' i x) (g' x) ↔ ε ≤ edist (f i x) (g x)
have h : ε ≤ edist (f' i x) (g' x) ↔ ε ≤ edist (f i x) (g' x)
Tactic: rw [hxg, hxf]
-- 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 : EDist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
i : ι
h_ae_eq : f i =ᶠ[ae μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
h : ε ≤ edist (f' i x) (g' x) ↔ ε ≤ edist (f i x) (g' x)
⊢ ε ≤ edist (f' i x) (g' x) ↔ ε ≤ edist (f i x) (g x)
have h₁ : ε ≤ edist (f' i x) (g' x) ↔ ε ≤ edist (f' i x) (g' x)
Tactic: rw [hxg, hxf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst_1 : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
⊢ TendstoInMeasure μ f atTop g
have refine : ∀ (ε : ℝ≥0∞) (hε : 0 < ε) (δ : ℝ≥0∞) (hδ : δ > 0),
  ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ δ
Tactic: refine fun ε hε => ENNReal.tendsto_atTop_zero.mpr fun δ hδ => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst_1 : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0∞
hδ : δ > 0
⊢ ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ δ
have pos : ∀ (hδi : δ = ∞), ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ δ
Tactic: by_cases hδi : δ = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst_1 : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0∞
hδ : δ > 0
pos : ∀ (hδi : δ = ∞), ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ δ
⊢ ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ δ
have neg : ∀ (hδi : ¬δ = ∞), ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ δ
Tactic: by_cases hδi : δ = ∞
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst_1 : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0∞
hδ : δ > 0
hδi : ¬δ = ∞
⊢ ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ δ
have neg : ∀ (δ : ℝ≥0) (hδ : (↑δ : ℝ≥0∞) > 0),
  ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ (↑δ : ℝ≥0∞)
Tactic: lift δ to ℝ≥0 using hδi
Cleared hypotheses: δ, hδ, hδi
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (hypothesis)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst_1 : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : (↑δ : ℝ≥0∞) > 0
⊢ ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ (↑δ : ℝ≥0∞)
have hδ₁ : 0 < (↑δ : ℝ)
Tactic: rw [gt_iff_lt, ENNReal.coe_pos, ← NNReal.coe_pos] at hδ
Cleared hypotheses: hδ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConvergenceInMeasure (goal)
Goal:
α : Type u_1
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoEMetricSpace E
f : ℕ → α → E
g : α → E
inst_1 : IsFiniteMeasure μ
hf : ∀ (n : ℕ), Measurable (β := ℝ≥0∞) fun (a : α) ↦ edist (f n a) (g a)
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : 0 < ε
δ : ℝ≥0
hδ : 0 < (↑δ : ℝ)
⊢ ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ (↑δ : ℝ≥0∞)
have neg : ∀ (t : Set α),
  MeasurableSet t →
    ∀ (ht : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal (↑δ : ℝ)) (hunif : TendstoUniformlyOn f g atTop tᶜ),
      ∃ (N : ℕ), ∀ n ≥ N, (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f n x) (g x)} ≤ (↑δ : ℝ≥0∞)
Tactic: obtain ⟨t, _, ht, hunif⟩ :=
    tendstoUniformlyOn_of_ae_tendsto_of_measurable_edist' hf hfg hδ