awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
simp : ∀ (hx : ∃ t ∈ D n, x ∈ t), ∃ (t : Set α), (∃ (i : ℕ), t ∈ D i) ∧ x ∈ t
⊢ Membership.mem (γ := Set α) (⋃₀ ⋃ (n : ℕ), D n) x

Tactic:
simp at hx ⊢
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 : ∃ t ∈ D n, x ∈ t
⊢ ∃ (t : Set α), (∃ (i : ℕ), t ∈ D i) ∧ x ∈ t

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 : ℕ
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D n) : ℝ≥0∞)
    ((fun (D : Set (Set α)) ↦ ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) : ℝ≥0∞)) (⋃ (n : ℕ), D n) : ℝ≥0∞)

Tactic:
exact measure_mono (fun x hx ↦ by simp at hx ⊢; grind)

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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)
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
⊢ ∃ 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)

Premises used: Set
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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.Countable

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
refine : ∀ (s : Set α) (hs : s ∈ C), s ∪ ⋃₀ D =ᶠ[ae μ] ⋃₀ D
⊢ ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᶠ[ae μ] ⋃₀ D

Tactic:
refine ⟨D, by grind, by grind, fun s hs ↦ union_ae_eq_right_iff_ae_subset.mp ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
symm : ⋃₀ D =ᶠ[ae μ] s ∪ ⋃₀ D
⊢ s ∪ ⋃₀ D =ᶠ[ae μ] ⋃₀ D

Tactic:
symm
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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) μ
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ ⋃₀ D) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ⋃₀ D =ᶠ[ae μ] s ∪ ⋃₀ D

Tactic:
apply ae_eq_of_ae_subset_of_measure_ge subset_union_right.eventuallyLE

Premises used: Set.subset_union_right, HasSubset.Subset.eventuallyLE, MeasureTheory.ae_eq_of_ae_subset_of_measure_ge
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 = ⋃₀ (D ∪ {s})

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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₂ : (μ : (a : Set α) → ℝ≥0∞) (⋃₀ (D ∪ {s})) ≤ m
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ ⋃₀ D) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) : ℝ≥0∞)

Tactic:
rw [hD, show s ∪ ⋃₀ D = ⋃₀ (D ∪ {s}) by simp]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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₂ : Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (D ∪ {s})
⊢ (μ : (a : Set α) → ℝ≥0∞) (⋃₀ (D ∪ {s})) ≤ m

Tactic:
apply le_biSup (f := fun D ↦ μ (⋃₀ D))

Premises used: Set.sUnion, le_biSup, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
⊢ Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} (D ∪ {s})

Tactic:
simp [D_mem.2, insert_subset_iff, hs, D_mem.1]

Premises used: Set.insert_subset_iff, And.right, And.left
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
⊢ ∀ t ∈ D, MeasurableSet t

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
⊢ NullMeasurableSet (⋃₀ D) μ

Tactic:
exact (MeasurableSet.sUnion D_mem.2 (by grind)).nullMeasurableSet

Premises used: MeasurableSet.sUnion, MeasurableSet.nullMeasurableSet, And.right
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ ⋃₀ D) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
C : Set (Set α)
hC : ∀ s ∈ C, MeasurableSet s
⊢ ∀ (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
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
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
⊢ ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᶠ[ae μ] ⋃₀ D

Tactic:
choose D DC D_count hD using A
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
⊢ ⋃ (n : ℕ), D n ⊆ C

Tactic:
simp [DC]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
⊢ Set.Countable.{u_1} (α := Set α) (⋃ (n : ℕ), D n)

Tactic:
simp [D_count]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
refine : ∀ (s : Set α) (hs : s ∈ C), s ≤ᶠ[ae μ] ⋃₀ ⋃ (n : ℕ), D n
⊢ ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᶠ[ae μ] ⋃₀ D

Tactic:
refine ⟨⋃ n, D n, by simp [DC], by simp [D_count], fun s hs ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
rw : s ≤ᶠ[ae (sum (sfiniteSeq μ))] ⋃₀ ⋃ (n : ℕ), D n
⊢ s ≤ᶠ[ae μ] ⋃₀ ⋃ (n : ℕ), D n

Tactic:
rw [← sum_sfiniteSeq μ]

Premises used: MeasureTheory.sum_sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
apply : ∀ (n : ℕ), ⋃₀ D n ≤ᶠ[ae (sfiniteSeq μ n)] ⋃₀ ⋃ (n : ℕ), D n
⊢ s ≤ᶠ[ae (sum (sfiniteSeq μ))] ⋃₀ ⋃ (n : ℕ), D n

Tactic:
apply ae_sum_iff.2 (fun n ↦ (hD n s hs).trans ?_)

Premises used: Iff.mpr, MeasureTheory.Measure.ae_sum_iff, Filter.EventuallyLE.trans
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
simp : ∀ (hx : ∃ t ∈ D n, x ∈ t), ∃ (t : Set α), (∃ (i : ℕ), t ∈ D i) ∧ x ∈ t
⊢ Membership.mem (γ := Set α) (⋃₀ ⋃ (n : ℕ), D n) x

Tactic:
simp at hx ⊢
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 : ∃ t ∈ D n, x ∈ t
⊢ ∃ (t : Set α), (∃ (i : ℕ), t ∈ D i) ∧ x ∈ t

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 : ℕ
⊢ ⋃₀ D n ≤ᶠ[ae (sfiniteSeq μ n)] ⋃₀ ⋃ (n : ℕ), D n

Tactic:
exact HasSubset.Subset.eventuallyLE (fun x hx ↦ by simp at hx ⊢; grind)

Premises used: HasSubset.Subset.eventuallyLE
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 : ℕ
simp_rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (w n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp_rw [w, measure_toMeasurable]

Premises used: MeasureTheory.measure_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(h'v n).lt_top

Premises used: Ne.lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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∞) (t ∩ v n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact (h'v n).lt_top

Premises used: Ne.lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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∞)

Tactic:
have hw : ∀ n, μ (w n) < ∞ := by
      intro n
      simp_rw [w, measure_toMeasurable]
      exact (h'v n).lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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∞)
⊢ 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'
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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)
rw : t ⊆ ⋃ (i : ℕ), t ∩ w i
⊢ t ⊆ ⋃ (n : ℕ), t ∩ disjointed w n

Tactic:
rw [← inter_iUnion, iUnion_disjointed, inter_iUnion]

Premises used: iUnion_disjointed, Set.inter_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
rcases : ∀ (n : ℕ) (hn : x ∈ v n), Membership.mem (γ := Set α) (⋃ (i : ℕ), t ∩ w i) x
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), t ∩ w i) x

Tactic:
rcases mem_iUnion.1 (hv hx) with ⟨n, hn⟩

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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

Tactic:
mem_iUnion.2 ⟨n, ?_⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
refine : x ∈ t ∩ w n
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), t ∩ w i) x

Tactic:
refine mem_iUnion.2 ⟨n, ?_⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 ∩ v n

Tactic:
have : x ∈ t ∩ v n := ⟨hx, hn⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
this : x ∈ t ∩ v n
⊢ x ∈ t ∩ w n

Tactic:
⟨hx, subset_toMeasurable μ _ this⟩

Premises used: Set.Mem, setOf, Set.inter, MeasureTheory.subset_toMeasurable, And.intro