awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
rw : s = s ∩ ⋃ (i : ℕ), spanningSets μ i
rw₁ : s = s ∩ univ
⊢ s = ⋃ (n : ℕ), s ∩ spanningSets μ n
have rw₂ : s = s
Tactic: rw [← inter_iUnion, iUnion_spanningSets, inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
⊢ (∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ n) : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have nth_rw : (∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ n) : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s ∩ spanningSets μ n) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: nth_rw 2 [show s = ⋃ n, s ∩ spanningSets μ n by
      rw [← inter_iUnion, iUnion_spanningSets, inter_univ]]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
⊢ (∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ n) : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (n : ℕ), s ∩ spanningSets μ n) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : (∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ n) : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
  ∀ (i : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ i) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [measure_iUnion_null_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
⊢ (∃ (n : ℕ), LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ n) : ℝ≥0∞)) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have contrapose! : (∀ (n : ℕ), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ n) : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
⊢ (∀ (n : ℕ), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ n) : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : (∀ (n : ℕ), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ n) : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
  ∀ t ∈ range (spanningSets μ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [nonpos_iff_eq_zero, ← forall_measure_inter_isCountablySpanning_eq_zero
    (isCountablySpanning_spanningSets μ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
Union_As_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Set.Countable.{u_4} (α := ι) {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
have set : let posmeas : Set ι := {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)};
∀ (posmeas_def : posmeas = {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}),
  posmeas.Countable
Tactic: set posmeas := { i : ι | 0 < μ (As i) } with posmeas_def
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
Union_As_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞) (∞ : ℝ≥0∞)
posmeas : Set ι := {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
posmeas_def : posmeas = {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
⊢ posmeas.Countable
have rcases : ∀ (as : ℕ → ℝ≥0∞),
  StrictAnti as →
    ∀ (as_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (as n)) (as_lim : Tendsto as atTop (𝓝 0)),
      posmeas.Countable
Tactic: rcases exists_seq_strictAnti_tendsto' (zero_lt_one : (0 : ℝ≥0∞) < 1) with
    ⟨as, _, as_mem, as_lim⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
Union_As_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞) (∞ : ℝ≥0∞)
posmeas : Set ι := {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
posmeas_def : posmeas = {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
as : ℕ → ℝ≥0∞
left : StrictAnti as
as_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (as n)
as_lim : Tendsto as atTop (𝓝 0)
fairmeas : (n : ℕ) → Set ι := fun (n : ℕ) ↦ {i : ι | as n ≤ (μ : (a : Set α) → ℝ≥0∞) (As i)}
⊢ posmeas = ⋃ (n : ℕ), fairmeas n
have fairmeas_eq : ∀ (n : ℕ), fairmeas n = (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (As i)) ⁻¹' Ici (as n)
Tactic: have fairmeas_eq : ∀ n, fairmeas n = (fun i => μ (As i)) ⁻¹' Ici (as n) := fun n => by
      simp only [fairmeas]
      rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
Union_As_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞) (∞ : ℝ≥0∞)
posmeas : Set ι := {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
posmeas_def : posmeas = {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
as : ℕ → ℝ≥0∞
left : StrictAnti as
as_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (as n)
as_lim : Tendsto as atTop (𝓝 0)
fairmeas : (n : ℕ) → Set ι := fun (n : ℕ) ↦ {i : ι | as n ≤ (μ : (a : Set α) → ℝ≥0∞) (As i)}
⊢ posmeas.Countable
have countable_union : posmeas = ⋃ (n : ℕ), fairmeas n
Tactic: have countable_union : posmeas = ⋃ n, fairmeas n := by
    have fairmeas_eq : ∀ n, fairmeas n = (fun i => μ (As i)) ⁻¹' Ici (as n) := fun n => by
      simp only [fairmeas]
      rfl
    simpa only [fairmeas_eq, posmeas_def, ← preimage_iUnion,
      iUnion_Ici_eq_Ioi_of_lt_of_tendsto (fun n => (as_mem n).1) as_lim]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
Union_As_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞) (∞ : ℝ≥0∞)
posmeas : Set ι := {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
posmeas_def : posmeas = {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
as : ℕ → ℝ≥0∞
left : StrictAnti as
as_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (as n)
as_lim : Tendsto as atTop (𝓝 0)
fairmeas : (n : ℕ) → Set ι := fun (n : ℕ) ↦ {i : ι | as n ≤ (μ : (a : Set α) → ℝ≥0∞) (As i)}
countable_union : posmeas = ⋃ (n : ℕ), fairmeas n
⊢ posmeas.Countable
have rw : Set.Countable.{u_4} (α := ι) (⋃ (n : ℕ), fairmeas n)
Tactic: rw [countable_union]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
Union_As_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞) (∞ : ℝ≥0∞)
posmeas : Set ι := {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
posmeas_def : posmeas = {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
as : ℕ → ℝ≥0∞
left : StrictAnti as
as_mem : ∀ (n : ℕ), Membership.mem (γ := Set ℝ≥0∞) (Ioo 0 1) (as n)
as_lim : Tendsto as atTop (𝓝 0)
fairmeas : (n : ℕ) → Set ι := fun (n : ℕ) ↦ {i : ι | as n ≤ (μ : (a : Set α) → ℝ≥0∞) (As i)}
countable_union : posmeas = ⋃ (n : ℕ), fairmeas n
⊢ Set.Countable.{u_4} (α := ι) (⋃ (n : ℕ), fairmeas n)
have refine : ∀ (n : ℕ), (fairmeas n).Finite
Tactic: refine countable_iUnion fun n => Finite.countable ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
⊢ Set.Countable.{u_4} (α := ι) {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
have rw : ∀ (As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ)))
  (As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)),
  Set.Countable.{u_4} (α := ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
Tactic: rw [← sum_sfiniteSeq μ] at As_disj As_mble ⊢
Cleared hypotheses: As_mble, As_disj
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
hi :
  Membership.mem (γ := Set ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)} i
⊢ Membership.mem (γ := Set ι)
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}) i
have by_contra : ∀ (con : i ∉ ⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}),
  False
Tactic: by_contra con
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
hi :
  Membership.mem (γ := Set ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)} i
con : i ∉ ⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
⊢ False
have con₁ : ∀ (x_1 : ℕ), Eq (α := ℝ≥0∞) ((sfiniteSeq μ x_1 : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp only [mem_iUnion, mem_setOf_eq, not_exists, not_lt, nonpos_iff_eq_zero] at *
Cleared hypotheses: con
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
hi : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)
con : ∀ (x_1 : ℕ), Eq (α := ℝ≥0∞) ((sfiniteSeq μ x_1 : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False
have rw : ∀ (hi : LT.lt (α := ℝ≥0∞) 0 (∑' (i_1 : ℕ), (sfiniteSeq μ i_1 : (a : Set α) → ℝ≥0∞) (As i)))
  (con : ∀ (x_1 : ℕ), Eq (α := ℝ≥0∞) ((sfiniteSeq μ x_1 : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞) (0 : ℝ≥0∞)), False
Tactic: rw [sum_apply₀] at hi
Cleared hypotheses: hi, con
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
hi : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)
con : ∀ (x_1 : ℕ), Eq (α := ℝ≥0∞) ((sfiniteSeq μ x_1 : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞) (0 : ℝ≥0∞)
rw :
  ∀ (hi : LT.lt (α := ℝ≥0∞) 0 (∑' (i_1 : ℕ), (sfiniteSeq μ i_1 : (a : Set α) → ℝ≥0∞) (As i)))
    (con : ∀ (x_1 : ℕ), Eq (α := ℝ≥0∞) ((sfiniteSeq μ x_1 : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞) (0 : ℝ≥0∞)), False
⊢ False
have hs : NullMeasurableSet (As i) (sum (sfiniteSeq μ))
Tactic: rw [sum_apply₀] at hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
i : ι
hi : LT.lt (α := ℝ≥0∞) 0 (∑' (i_1 : ℕ), (sfiniteSeq μ i_1 : (a : Set α) → ℝ≥0∞) (As i))
con : ∀ (x_1 : ℕ), Eq (α := ℝ≥0∞) ((sfiniteSeq μ x_1 : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False
have hi₁ : LT.lt (α := ℝ≥0∞) 0 (∑' (i : ℕ), 0)
Tactic: simp_rw [con] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
⊢ Set.Countable.{u_4} (α := ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
have obs : Subset.{u_4} (α := Set ι)
  {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
  (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})
Tactic: have obs : { i : ι | 0 < sum (sfiniteSeq μ) (As i) }
      ⊆ ⋃ n, { i : ι | 0 < sfiniteSeq μ n (As i) } := by
    intro i hi
    by_contra con
    simp only [mem_iUnion, mem_setOf_eq, not_exists, not_lt, nonpos_iff_eq_zero] at *
    rw [sum_apply₀] at hi
    · simp_rw [con] at hi
      simp at hi
    · exact As_mble i
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs :
  Subset.{u_4} (α := Set ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})
⊢ Set.Countable.{u_4} (α := ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
have apply : Set.Countable.{u_4} (α := ι)
  (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})
Tactic: apply Countable.mono obs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs :
  Subset.{u_4} (α := Set ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})
⊢ Set.Countable.{u_4} (α := ι)
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})
have refine : ∀ (n : ℕ),
  Set.Countable.{u_4} (α := ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
Tactic: refine countable_iUnion fun n ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs :
  Subset.{u_4} (α := Set ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})
n : ℕ
⊢ Set.Countable.{u_4} (α := ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
have As_mble₁ : ∀ (i : ι), NullMeasurableSet (As i) (sfiniteSeq μ n)
Tactic: apply countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs :
  Subset.{u_4} (α := Set ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})
n : ℕ
As_mble₁ : ∀ (i : ι), NullMeasurableSet (As i) (sfiniteSeq μ n)
⊢ Set.Countable.{u_4} (α := ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
have As_disj₁ : Pairwise (AEDisjoint (sfiniteSeq μ n) on As)
Tactic: apply countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) (sum (sfiniteSeq μ))
As_disj : Pairwise (AEDisjoint (sum (sfiniteSeq μ)) on As)
obs :
  Subset.{u_4} (α := Set ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sum (sfiniteSeq μ) : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)})
n : ℕ
As_mble₁ : ∀ (i : ι), NullMeasurableSet (As i) (sfiniteSeq μ n)
As_disj₁ : Pairwise (AEDisjoint (sfiniteSeq μ n) on As)
⊢ Set.Countable.{u_4} (α := ι)
    {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}
have Union_As_finite : Ne (α := ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_4
β : Type u_5
x : MeasurableSpace α
μ : Measure α
inst : SFinite μ
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass β
g : α → β
g_mble : NullMeasurable g μ
⊢ Set.Countable.{u_5} (α := β)
    {t : β | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | g a = t} : ℝ≥0∞)}
have level_sets_disjoint : Pairwise.{u_5} (α := β) (onFun.{u_5 + 1, u_4 + 1, 1} (β := Set α) Disjoint fun (t : β) ↦ {a : α | g a = t})
Tactic: have level_sets_disjoint : Pairwise (Disjoint on fun t : β => { a : α | g a = t }) :=
    fun s t hst => Disjoint.preimage g (disjoint_singleton.mpr hst)
-- 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 α)),
    Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
have inl : ∀ (hm : m = ⊥),
  ∃ (D : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
Tactic: rcases eq_bot_or_bot_lt m with hm | hm
-- 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)
inl :
  ∀ (hm : m = ⊥),
    ∃ (D : Set (Set α)),
      Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
        (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
⊢ ∃ (D : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
have inr : ∀ (hm : ⊥ < m),
  ∃ (D : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
Tactic: rcases eq_bot_or_bot_lt m with hm | hm
-- 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
⊢ ∃ (D : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
have inr : ∀ (u : ℕ → ℝ≥0∞) (u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 m) (u_lim : Tendsto u atTop (𝓝 m)),
  ∃ (D : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
Tactic: 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
-- 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 : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
have A : ∀ (n : ℕ),
  ∃ (D : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
      u n < (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
Tactic: have A n : ∃ D ∈ {D : Set (Set α) | D ⊆ C ∧ D.Countable}, u n < μ (⋃₀ D) :=
      lt_biSup_iff.1 (u_mem n).2
-- 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)
A :
  ∀ (n : ℕ),
    ∃ (D : Set (Set α)),
      Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
        u n < (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)
⊢ ∃ (D : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {D : Set (Set α) | D ⊆ C ∧ D.Countable} D ∧
      (μ : (a : Set α) → ℝ≥0∞) (⋃₀ D) = m
have inr : ∀ (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
Tactic: choose! D D_mem huD using A
Cleared hypotheses: A