awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
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∞)
⊢ (∀ (n : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ n) : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
nth_rw 2 [show s = ⋃ n, s ∩ spanningSets μ n by
      rw [← inter_iUnion, iUnion_spanningSets, inter_univ]]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
rw 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∞)
⊢ (∀ (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:
rw [measure_iUnion_null_iff]

Premises used: MeasureTheory.measure_iUnion_null_iff
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
contrapose! :
  (∀ (n : ℕ), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ n) : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (∃ (n : ℕ), LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ n) : ℝ≥0∞)) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
contrapose!
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
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∞)
⊢ (∀ (n : ℕ), LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ n) : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [nonpos_iff_eq_zero, ← forall_measure_inter_isCountablySpanning_eq_zero
    (isCountablySpanning_spanningSets μ)]

Premises used: MeasureTheory.Measure.forall_measure_inter_isCountablySpanning_eq_zero, MeasureTheory.isCountablySpanning_spanningSets, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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∞)) ↔
    ∀ t ∈ range (spanningSets μ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_4
inst : MeasurableSpace α
μ : Measure α
ε : ℝ≥0∞
ε_pos : 0 < ε
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.Finite.{u_4} (α := ι) {i : ι | ε ≤ (μ : (a : Set α) → ℝ≥0∞) (As i)}

Tactic:
ENNReal.finite_const_le_of_tsum_ne_top
    (ne_top_of_le_ne_top Union_As_finite (tsum_meas_le_meas_iUnion_of_disjoint₀ μ As_mble As_disj))
    ε_pos.ne'

Premises used: ENNReal.finite_const_le_of_tsum_ne_top, LT.lt.ne', ne_top_of_le_ne_top, MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint₀
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_4
inst : MeasurableSpace α
μ : Measure α
ε : ℝ≥0∞
ε_pos : 0 < ε
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint on As)
Union_As_finite : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), As i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Set.Finite.{u_4} (α := ι) {i : ι | ε ≤ (μ : (a : Set α) → ℝ≥0∞) (As i)}

Tactic:
finite_const_le_meas_of_disjoint_iUnion₀ μ ε_pos (fun i ↦ (As_mble i).nullMeasurableSet)
    (fun _ _ h ↦ Disjoint.aedisjoint (As_disj h)) Union_As_finite

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion₀, Disjoint.aedisjoint
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : MeasurableSingletonClass α
s : Set α
hs : s.Infinite
h' : ∃ (ε : ℝ≥0∞), ε ≠ 0 ∧ ∀ x ∈ s, ε ≤ (μ : (a : Set α) → ℝ≥0∞) {x}
ε : ℝ≥0∞
hne_1 : ε ≠ 0
hε : ∀ x ∈ s, ε ≤ (μ : (a : Set α) → ℝ≥0∞) {x}
this : Infinite.{u_1 + 1} (↑s : Type u_1)
x y : (↑s : Type u_1)
hne : x ≠ y
⊢ onFun (β := Set α) Disjoint (fun (x : (↑s : Type u_1)) ↦ {(↑x : α)}) x y

Tactic:
simpa [Subtype.val_inj]

Premises used: Subtype.val_inj
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : MeasurableSingletonClass α
s : Set α
hs : s.Infinite
h' : ∃ (ε : ℝ≥0∞), ε ≠ 0 ∧ ∀ x ∈ s, ε ≤ (μ : (a : Set α) → ℝ≥0∞) {x}
ε : ℝ≥0∞
hne : ε ≠ 0
hε : ∀ x ∈ s, ε ≤ (μ : (a : Set α) → ℝ≥0∞) {x}
this : Infinite.{u_1 + 1} (↑s : Type u_1)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (x : (↑s : Type u_1)), {(↑x : α)}) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 :
  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
⊢ Set.Countable.{u_4} (α := ι) {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}

Tactic:
set posmeas := { i : ι | 0 < μ (As i) } with posmeas_def
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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∞)}
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
⊢ posmeas.Countable

Tactic:
rcases exists_seq_strictAnti_tendsto' (zero_lt_one : (0 : ℝ≥0∞) < 1) with
    ⟨as, _, as_mem, as_lim⟩

Premises used: exists_seq_strictAnti_tendsto', zero_lt_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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)}
n : ℕ
simp :
  Eq.{u_4 + 1} (α := Set ι) {i : ι | as n ≤ (μ : (a : Set α) → ℝ≥0∞) (As i)}
    ((fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (As i)) ⁻¹' Ici (as n))
⊢ fairmeas n = (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (As i)) ⁻¹' Ici (as n)

Tactic:
simp only [fairmeas]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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)}
n : ℕ
⊢ Eq.{u_4 + 1} (α := Set ι) {i : ι | as n ≤ (μ : (a : Set α) → ℝ≥0∞) (As i)}
    ((fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (As i)) ⁻¹' Ici (as n))

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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)}
⊢ ∀ (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
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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)}
fairmeas_eq : ∀ (n : ℕ), fairmeas n = (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) (As i)) ⁻¹' Ici (as n)
⊢ posmeas = ⋃ (n : ℕ), fairmeas n

Tactic:
simpa only [fairmeas_eq, posmeas_def, ← preimage_iUnion,
      iUnion_Ici_eq_Ioi_of_lt_of_tendsto (fun n => (as_mem n).1) as_lim]

Premises used: iUnion_Ici_eq_Ioi_of_lt_of_tendsto, And.left, Set.preimage_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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

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]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
rw : Set.Countable.{u_4} (α := ι) (⋃ (n : ℕ), fairmeas n)
⊢ posmeas.Countable

Tactic:
rw [countable_union]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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)

Tactic:
countable_iUnion fun n => Finite.countable ?_

Premises used: Set.countable_iUnion, Set.Finite.countable
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
refine : ∀ (n : ℕ), (fairmeas n).Finite
⊢ Set.Countable.{u_4} (α := ι) (⋃ (n : ℕ), fairmeas n)

Tactic:
refine countable_iUnion fun n => Finite.countable ?_

Premises used: Set.countable_iUnion, Set.Finite.countable
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
n : ℕ
⊢ (fairmeas n).Finite

Tactic:
finite_const_le_meas_of_disjoint_iUnion₀ μ (as_mem n).1 As_mble As_disj Union_As_finite

Premises used: And.left, MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion₀
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
n : ℕ
⊢ (fairmeas n).Finite

Tactic:
exact finite_const_le_meas_of_disjoint_iUnion₀ μ (as_mem n).1 As_mble As_disj Union_As_finite

Premises used: And.left, MeasureTheory.Measure.finite_const_le_meas_of_disjoint_iUnion₀
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_4
x : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), MeasurableSet (As i)
As_disj : Pairwise (Disjoint 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∞)}

Tactic:
countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀ μ (fun i ↦ (As_mble i).nullMeasurableSet)
    ((fun _ _ h ↦ Disjoint.aedisjoint (As_disj h))) Union_As_finite

Premises used: MeasurableSet.nullMeasurableSet, Disjoint.aedisjoint, MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top₀
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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)
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∞)}
⊢ Set.Countable.{u_4} (α := ι) {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}

Tactic:
rw [← sum_sfiniteSeq μ] at As_disj As_mble ⊢

Premises used: MeasureTheory.sum_sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
by_contra :
  ∀ (con : i ∉ ⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}),
    False
⊢ Membership.mem (γ := Set ι)
    (⋃ (n : ℕ), {i : ι | LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((sfiniteSeq μ n : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞)}) i

Tactic:
by_contra con
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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∞)}
⊢ ∀ (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 *

Premises used: Set.mem_iUnion, not_exists, Set.mem_setOf_eq, not_lt, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
hs : NullMeasurableSet (As i) (sum (sfiniteSeq μ))
⊢ False

Tactic:
rw [sum_apply₀] at hi

Premises used: MeasureTheory.Measure.sum_apply₀
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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∞)
⊢ LT.lt (α := ℝ≥0∞) 0 (∑' (i : ℕ), 0)

Tactic:
simp_rw [con] at hi
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 : ι
con : ∀ (x_1 : ℕ), Eq (α := ℝ≥0∞) ((sfiniteSeq μ x_1 : (a : Set α) → ℝ≥0∞) (As i) : ℝ≥0∞) (0 : ℝ≥0∞)
hi : LT.lt (α := ℝ≥0∞) 0 (∑' (i : ℕ), 0)
⊢ False

Tactic:
simp at hi
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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∞)
⊢ NullMeasurableSet (As i) (sum (sfiniteSeq μ))

Tactic:
As_mble i
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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∞)
⊢ NullMeasurableSet (As i) (sum (sfiniteSeq μ))

Tactic:
exact As_mble i
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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)
⊢ 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