awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : (n : ℕ) → Set (Set α)
D_mem : ∀ (n : ℕ), Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (D n)
huD : ∀ (n : ℕ), u n < (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D n)
⊢ Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (⋃ (n : ℕ), D n)
have simp : (∀ (i : ℕ), D i ⊆ C) ∧ ∀ (i : ℕ), (D i).Countable
Tactic: simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : (n : ℕ) → Set (Set α)
D_mem : ∀ (n : ℕ), Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (D n)
huD : ∀ (n : ℕ), u n < (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D n)
⊢ ∃ (D : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
have hD : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (⋃ (n : ℕ), D n)
Tactic: have hD : ⋃ n, D n ∈ {D | D ⊆ C ∧ D.Countable} := by simp; grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : (n : ℕ) → Set (Set α)
D_mem : ∀ (n : ℕ), Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (D n)
huD : ∀ (n : ℕ), u n < (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D n)
hD : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (⋃ (n : ℕ), D n)
⊢ ∃ (D : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
have inr : (μ : (a : Set α) → ℝ≥0∞) (⋃₀ ⋃ (n : ℕ), D n) = m
Tactic: refine ⟨⋃ n, D n, hD, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : (n : ℕ) → Set (Set α)
D_mem : ∀ (n : ℕ), Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (D n)
huD : ∀ (n : ℕ), u n < (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D n)
hD : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (⋃ (n : ℕ), D n)
⊢ (μ : (a : Set α) → ℝ≥0∞) (⋃₀ ⋃ (n : ℕ), D n) = m
have inr : LE.le (α := ℝ≥0∞)
  (⨆ (i : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} i),
      (fun (D : Set (Set α)) ↦ ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) : ℝ≥0∞)) i)
  ((fun (D : Set (Set α)) ↦ ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) : ℝ≥0∞)) (⋃ (n : ℕ), D n))
Tactic: apply le_antisymm (le_biSup (f := fun D ↦ μ (⋃₀ D)) hD)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : (n : ℕ) → Set (Set α)
D_mem : ∀ (n : ℕ), Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (D n)
huD : ∀ (n : ℕ), u n < (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D n)
hD : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (⋃ (n : ℕ), D n)
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (i : Set (Set α)),
      ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} i),
        (fun (D : Set (Set α)) ↦ ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) : ℝ≥0∞)) i)
    ((fun (D : Set (Set α)) ↦ ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) : ℝ≥0∞)) (⋃ (n : ℕ), D n))
have apply : ∀ (n : ℕ),
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D n) : ℝ≥0∞)
    ((fun (D : Set (Set α)) ↦ ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) : ℝ≥0∞)) (⋃ (n : ℕ), D n) : ℝ≥0∞)
Tactic: apply le_of_tendsto' u_lim (fun n ↦ (huD n).le.trans ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
hm : ⊥ < m
u : ℕ → ℝ≥0∞
u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m
u_lim : Tendsto u atTop (𝓝 m)
D : (n : ℕ) → Set (Set α)
D_mem : ∀ (n : ℕ), Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (D n)
huD : ∀ (n : ℕ), u n < (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D n)
hD : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (⋃ (n : ℕ), D n)
n : ℕ
x : α
hx : x ∈ ⋃₀ D n
⊢ Membership.mem (γ := Set α) (⋃₀ ⋃ (n : ℕ), D n) x
have simp : ∀ (hx : ∃ t ∈ D n, x ∈ t), ∃ (t : Set α), (∃ (i : ℕ), t ∈ D i) ∧ x ∈ t
Tactic: simp at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
⊢ ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᶠ[ae μ] ⋃₀ D
have obtain : ∀ (D : Set (Set α)) (D_mem : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D)
  (hD : (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m), ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᶠ[ae μ] ⋃₀ D
Tactic: obtain ⟨D, D_mem, hD⟩ : ∃ D ∈ {D : Set (Set α) | D ⊆ C ∧ D.Countable}, μ (⋃₀ D) = m := by
    rcases eq_bot_or_bot_lt m with hm | hm
    · exact ⟨∅, by simp, by simp [hm]⟩
    obtain ⟨u, -, u_mem, u_lim⟩ :
        ∃ u : ℕ → ℝ≥0∞, StrictMono u ∧ (∀ n, u n ∈ Ioo 0 m) ∧ Tendsto u atTop (𝓝 m) :=
      exists_seq_strictMono_tendsto' hm
    have A n : ∃ D ∈ {D : Set (Set α) | D ⊆ C ∧ D.Countable}, u n < μ (⋃₀ D) :=
      lt_biSup_iff.1 (u_mem n).2
    choose! D D_mem huD using A
    have hD : ⋃ n, D n ∈ {D | D ⊆ C ∧ D.Countable} := by simp; grind
    refine ⟨⋃ n, D n, hD, ?_⟩
    apply le_antisymm (le_biSup (f := fun D ↦ μ (⋃₀ D)) hD)
    apply le_of_tendsto' u_lim (fun n ↦ (huD n).le.trans ?_)
    exact measure_mono (fun x hx ↦ by simp at hx ⊢; grind)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
D : Set (Set α)
D_mem : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D
hD : (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
⊢ ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᶠ[ae μ] ⋃₀ D
have refine : ∀ (s : Set α) (hs : s ∈ C), s ∪ ⋃₀ D =ᶠ[ae μ] ⋃₀ D
Tactic: refine ⟨D, by grind, by grind, fun s hs ↦ union_ae_eq_right_iff_ae_subset.mp ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
D : Set (Set α)
D_mem : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D
hD : (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
s : Set α
hs : s ∈ C
⊢ s ∪ ⋃₀ D =ᶠ[ae μ] ⋃₀ D
have symm : ⋃₀ D =ᶠ[ae μ] s ∪ ⋃₀ D
Tactic: symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
D : Set (Set α)
D_mem : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D
hD : (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
s : Set α
hs : s ∈ C
⊢ ⋃₀ D =ᶠ[ae μ] s ∪ ⋃₀ D
have h₂ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ ⋃₀ D) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) : ℝ≥0∞)
Tactic: apply ae_eq_of_ae_subset_of_measure_ge subset_union_right.eventuallyLE
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
D : Set (Set α)
D_mem : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D
hD : (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
s : Set α
hs : s ∈ C
h₂ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ ⋃₀ D) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) : ℝ≥0∞)
⊢ ⋃₀ D =ᶠ[ae μ] s ∪ ⋃₀ D
have hsm : NullMeasurableSet (⋃₀ D) μ
Tactic: apply ae_eq_of_ae_subset_of_measure_ge subset_union_right.eventuallyLE
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
D : Set (Set α)
D_mem : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D
hD : (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
s : Set α
hs : s ∈ C
h₂ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ ⋃₀ D) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) : ℝ≥0∞)
hsm : NullMeasurableSet (⋃₀ D) μ
⊢ ⋃₀ D =ᶠ[ae μ] s ∪ ⋃₀ D
have ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ ⋃₀ D) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply ae_eq_of_ae_subset_of_measure_ge subset_union_right.eventuallyLE
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
D : Set (Set α)
D_mem : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D
hD : (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
s : Set α
hs : s ∈ C
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ ⋃₀ D) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) : ℝ≥0∞)
have h₂ : (μ : (a : Set α) → ℝ≥0∞) (⋃₀ (D ∪ {s})) ≤ m
Tactic: rw [hD, show s ∪ ⋃₀ D = ⋃₀ (D ∪ {s}) by simp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
m : ℝ≥0∞ :=
  ⨆ (D : Set (Set α)),
    ⨆ (_ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D),
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
D : Set (Set α)
D_mem : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D
hD : (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
s : Set α
hs : s ∈ C
⊢ (μ : (a : Set α) → ℝ≥0∞) (⋃₀ (D ∪ {s})) ≤ m
have h₂ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (D ∪ {s})
Tactic: apply le_biSup (f := fun D ↦ μ (⋃₀ D))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
⊢ ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᶠ[ae μ] ⋃₀ D
have A : ∀ (n : ℕ), ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᶠ[ae (sfiniteSeq μ n)] ⋃₀ D
Tactic: have A n : ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᵐ[sfiniteSeq μ n] (⋃₀ D) :=
    exists_ae_subset_biUnion_countable_of_isFiniteMeasure hC
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
A : ∀ (n : ℕ), ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᶠ[ae (sfiniteSeq μ n)] ⋃₀ D
⊢ ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᶠ[ae μ] ⋃₀ D
have choose : ∀ (D : (n : ℕ) → Set (Set α)) (DC : ∀ (n : ℕ), D n ⊆ C) (D_count : ∀ (n : ℕ), (D n).Countable)
  (hD : ∀ (n : ℕ), ∀ s ∈ C, s ≤ᶠ[ae (sfiniteSeq μ n)] ⋃₀ D n), ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᶠ[ae μ] ⋃₀ D
Tactic: choose D DC D_count hD using A
Cleared hypotheses: A
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
D : (n : ℕ) → Set (Set α)
DC : ∀ (n : ℕ), D n ⊆ C
D_count : ∀ (n : ℕ), (D n).Countable
hD : ∀ (n : ℕ), ∀ s ∈ C, s ≤ᶠ[ae (sfiniteSeq μ n)] ⋃₀ D n
⊢ ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᶠ[ae μ] ⋃₀ D
have refine : ∀ (s : Set α) (hs : s ∈ C), s ≤ᶠ[ae μ] ⋃₀ ⋃ (n : ℕ), D n
Tactic: refine ⟨⋃ n, D n, by simp [DC], by simp [D_count], fun s hs ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
D : (n : ℕ) → Set (Set α)
DC : ∀ (n : ℕ), D n ⊆ C
D_count : ∀ (n : ℕ), (D n).Countable
hD : ∀ (n : ℕ), ∀ s ∈ C, s ≤ᶠ[ae (sfiniteSeq μ n)] ⋃₀ D n
s : Set α
hs : s ∈ C
⊢ s ≤ᶠ[ae μ] ⋃₀ ⋃ (n : ℕ), D n
have rw : s ≤ᶠ[ae (sum (sfiniteSeq μ))] ⋃₀ ⋃ (n : ℕ), D n
Tactic: rw [← sum_sfiniteSeq μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
D : (n : ℕ) → Set (Set α)
DC : ∀ (n : ℕ), D n ⊆ C
D_count : ∀ (n : ℕ), (D n).Countable
hD : ∀ (n : ℕ), ∀ s ∈ C, s ≤ᶠ[ae (sfiniteSeq μ n)] ⋃₀ D n
s : Set α
hs : s ∈ C
⊢ s ≤ᶠ[ae (sum (sfiniteSeq μ))] ⋃₀ ⋃ (n : ℕ), D n
have apply : ∀ (n : ℕ), ⋃₀ D n ≤ᶠ[ae (sfiniteSeq μ n)] ⋃₀ ⋃ (n : ℕ), D n
Tactic: apply ae_sum_iff.2 (fun n ↦ (hD n s hs).trans ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
D : (n : ℕ) → Set (Set α)
DC : ∀ (n : ℕ), D n ⊆ C
D_count : ∀ (n : ℕ), (D n).Countable
hD : ∀ (n : ℕ), ∀ s ∈ C, s ≤ᶠ[ae (sfiniteSeq μ n)] ⋃₀ D n
s : Set α
hs : s ∈ C
n : ℕ
x : α
hx : x ∈ ⋃₀ D n
⊢ Membership.mem (γ := Set α) (⋃₀ ⋃ (n : ℕ), D n) x
have simp : ∀ (hx : ∃ t ∈ D n, x ∈ t), ∃ (t : Set α), (∃ (i : ℕ), t ∈ D i) ∧ x ∈ t
Tactic: simp at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
have simp_rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: simp_rw [w, measure_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
⊢ ∃ t' ⊇ t,
    MeasurableSet t' ∧
      ∀ (u : Set α),
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
have hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hw : ∀ n, μ (w n) < ∞ := by
      intro n
      simp_rw [w, measure_toMeasurable]
      exact (h'v n).lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ t' ⊇ t,
    MeasurableSet t' ∧
      ∀ (u : Set α),
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
have ht' : let t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n);
t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
Tactic: set t' := ⋃ n, toMeasurable μ (t ∩ disjointed w n) with ht'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
⊢ t ⊆ ⋃ (n : ℕ), t ∩ disjointed w n
have rw : t ⊆ ⋃ (i : ℕ), t ∩ w i
Tactic: rw [← inter_iUnion, iUnion_disjointed, inter_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
x : α
hx : x ∈ t
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), t ∩ w i) x
have rcases : ∀ (n : ℕ) (hn : x ∈ v n), Membership.mem (γ := Set α) (⋃ (i : ℕ), t ∩ w i) x
Tactic: rcases mem_iUnion.1 (hv hx) with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
x : α
hx : x ∈ t
n : ℕ
hn : x ∈ v n
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), t ∩ w i) x
have refine : x ∈ t ∩ w n
Tactic: refine mem_iUnion.2 ⟨n, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
x : α
hx : x ∈ t
n : ℕ
hn : x ∈ v n
⊢ x ∈ t ∩ w n
have this : x ∈ t ∩ v n
Tactic: have : x ∈ t ∩ v n := ⟨hx, hn⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
⊢ ∃ t' ⊇ t,
    MeasurableSet t' ∧
      ∀ (u : Set α),
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
have tt' : t ⊆ t'
Tactic: have tt' : t ⊆ t' :=
      calc
        t ⊆ ⋃ n, t ∩ disjointed w n := by
          rw [← inter_iUnion, iUnion_disjointed, inter_iUnion]
          intro x hx
          rcases mem_iUnion.1 (hv hx) with ⟨n, hn⟩
          refine mem_iUnion.2 ⟨n, ?_⟩
          have : x ∈ t ∩ v n := ⟨hx, hn⟩
          exact ⟨hx, subset_toMeasurable μ _ this⟩
        _ ⊆ ⋃ n, toMeasurable μ (t ∩ disjointed w n) :=
          iUnion_mono fun n => subset_toMeasurable _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
v : ℕ → Set α
hv : t ⊆ ⋃ (n : ℕ), v n
h'v : ∀ (n : ℕ), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
w : (n : ℕ) → Set α := fun (n : ℕ) ↦ toMeasurable μ (t ∩ v n)
hw : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)
t' : Set α := ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
ht' : t' = ⋃ (n : ℕ), toMeasurable μ (t ∩ disjointed w n)
tt' : t ⊆ t'
⊢ ∃ t' ⊇ t,
    MeasurableSet t' ∧
      ∀ (u : Set α),
        MeasurableSet u →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
have refine : ∀ (u : Set α) (hu : MeasurableSet u),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
Tactic: refine ⟨t', tt', MeasurableSet.iUnion fun n => measurableSet_toMeasurable μ _, fun u hu => ?_⟩