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 : SigmaFinite μ
s : Set α
simp_rw :
  Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ i))
    (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s ∩ spanningSets μ i))
simp_rw₁ :
  Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (spanningSets μ i ∩ s))
    (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s ∩ spanningSets μ i))
simp_rw₂ :
  Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ.restrict s : (a : Set α) → ℝ≥0∞) (spanningSets μ i))
    (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s ∩ spanningSets μ i))
⊢ Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s)
    (⨆ (i : ℕ), (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s))
have simp_rw₃ : Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ.restrict (toMeasurable μ s) : (a : Set α) → ℝ≥0∞) (spanningSets μ i))
  (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s ∩ spanningSets μ i))
Tactic: simp_rw [restrict_apply' (measurableSet_spanningSets μ _), Set.inter_comm s,
    ← restrict_apply (measurableSet_spanningSets μ _), ← restrict_toMeasurable_of_sFinite s,
    restrict_apply (measurableSet_spanningSets μ _), Set.inter_comm _ (toMeasurable μ s)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
s : Set α
simp_rw :
  Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ i))
    (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s ∩ spanningSets μ i))
simp_rw₁ :
  Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (spanningSets μ i ∩ s))
    (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s ∩ spanningSets μ i))
simp_rw₂ :
  Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ.restrict s : (a : Set α) → ℝ≥0∞) (spanningSets μ i))
    (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s ∩ spanningSets μ i))
simp_rw₃ :
  Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ.restrict (toMeasurable μ s) : (a : Set α) → ℝ≥0∞) (spanningSets μ i))
    (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s ∩ spanningSets μ i))
⊢ Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s)
    (⨆ (i : ℕ), (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) (toMeasurable μ s))
have simp_rw₄ : Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (spanningSets μ i ∩ toMeasurable μ s))
  (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s ∩ spanningSets μ i))
Tactic: simp_rw [restrict_apply' (measurableSet_spanningSets μ _), Set.inter_comm s,
    ← restrict_apply (measurableSet_spanningSets μ _), ← restrict_toMeasurable_of_sFinite s,
    restrict_apply (measurableSet_spanningSets μ _), Set.inter_comm _ (toMeasurable μ s)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
h's : r < (μ : (a : Set α) → ℝ≥0∞) s
⊢ ∃ (t : Set α),
    MeasurableSet t ∧
      t ⊆ s ∧ r < (μ : (a : Set α) → ℝ≥0∞) t ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have h's₁ : ∃ (i : ℕ), r < (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s
Tactic: rw [← iSup_restrict_spanningSets,
    @lt_iSup_iff _ _ _ r fun i : ℕ => μ.restrict (spanningSets μ i) s] at h's
Cleared hypotheses: h's
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
h's : ∃ (i : ℕ), r < (μ.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s
⊢ ∃ (t : Set α),
    MeasurableSet t ∧
      t ⊆ s ∧ r < (μ : (a : Set α) → ℝ≥0∞) t ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have rcases : ∀ (n : ℕ) (hn : r < (μ.restrict (spanningSets μ n) : (a : Set α) → ℝ≥0∞) s),
  ∃ (t : Set α),
    MeasurableSet t ∧
      t ⊆ s ∧ r < (μ : (a : Set α) → ℝ≥0∞) t ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rcases h's with ⟨n, hn⟩
Cleared hypotheses: h's
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
n : ℕ
hn : r < (μ.restrict (spanningSets μ n) : (a : Set α) → ℝ≥0∞) s
⊢ ∃ (t : Set α),
    MeasurableSet t ∧
      t ⊆ s ∧ r < (μ : (a : Set α) → ℝ≥0∞) t ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have hn₁ : r < (μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ n)
Tactic: simp only [restrict_apply hs] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
n : ℕ
hn : r < (μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ n)
⊢ ∃ (t : Set α),
    MeasurableSet t ∧
      t ⊆ s ∧ r < (μ : (a : Set α) → ℝ≥0∞) t ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have spanningSets : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ n) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine
    ⟨s ∩ spanningSets μ n, hs.inter (measurableSet_spanningSets _ _), inter_subset_left, hn, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hc : S.Countable
hμ : ∀ s ∈ S, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hU : ⋃₀ S = univ
⊢ SigmaFinite μ
have obtain : ∀ (s : ℕ → Set α) (hμ : ∀ (n : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s n) : ℝ≥0∞) (∞ : ℝ≥0∞))
  (hs : Eq.{u_1 + 1} (α := Set α) (⋃ (n : ℕ), s n) univ), SigmaFinite μ
Tactic: obtain ⟨s, hμ, hs⟩ : ∃ s : ℕ → Set α, (∀ n, μ (s n) < ∞) ∧ ⋃ n, s n = univ :=
    (@exists_seq_cover_iff_countable _ (fun x => μ x < ∞) ⟨∅, by simp⟩).2 ⟨S, hc, hμ, hU⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst : SigmaFinite μ
h : ν₁ = ν₂
⊢ μ + ν₁ = μ + ν₂
have rw : μ + ν₂ = μ + ν₂
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst : SigmaFinite μ
⊢ μ + ν₁ = μ + ν₂ ↔ ν₁ = ν₂
have refine : ∀ (h : μ + ν₁ = μ + ν₂), ν₁ = ν₂
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
⊢ ν₁ = ν₂
have rw : ∀ (i : ℕ), ν₁.restrict (spanningSets μ i) = ν₂.restrict (spanningSets μ i)
Tactic: rw [ext_iff_of_iUnion_eq_univ (iUnion_spanningSets μ)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
i : ℕ
⊢ ν₁.restrict (spanningSets μ i) = ν₂.restrict (spanningSets μ i)
have h₁ : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((ν₁.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν₂.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
i : ℕ
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((ν₁.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν₂.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ i) : ℝ≥0∞)
    ((ν₁.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ i) : ℝ≥0∞)
    ((ν₂.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← ENNReal.add_right_inj (measure_mono s.inter_subset_right |>.trans_lt <|
    measure_spanningSets_lt_top μ i).ne]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
i : ℕ
s : Set α
hs : MeasurableSet s
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ i) : ℝ≥0∞)
      ((ν₁.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ i) : ℝ≥0∞)
      ((ν₂.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : ∀ (s : Set α),
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: simp only [ext_iff', coe_add, Pi.add_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst : SigmaFinite μ
⊢ ν₁ + μ = ν₂ + μ ↔ ν₁ = ν₂
have rw : μ + ν₁ = ν₂ + μ ↔ ν₁ = ν₂
Tactic: rw [add_comm _ μ, add_comm _ μ, μ.add_right_inj]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst : SigmaFinite μ
rw : μ + ν₁ = ν₂ + μ ↔ ν₁ = ν₂
⊢ ν₁ + μ = ν₂ + μ ↔ ν₁ = ν₂
have rw₁ : μ + ν₁ = μ + ν₂ ↔ ν₁ = ν₂
Tactic: rw [add_comm _ μ, add_comm _ μ, μ.add_right_inj]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst : SigmaFinite μ
rw : μ + ν₁ = ν₂ + μ ↔ ν₁ = ν₂
rw₁ : μ + ν₁ = μ + ν₂ ↔ ν₁ = ν₂
⊢ ν₁ + μ = ν₂ + μ ↔ ν₁ = ν₂
have rw₂ : ν₁ = ν₂ ↔ ν₁ = ν₂
Tactic: rw [add_comm _ μ, add_comm _ μ, μ.add_right_inj]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Countable α
hμ : ∀ (a : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ SigmaFinite μ
have inl : IsEmpty α → SigmaFinite μ
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Countable α
hμ : ∀ (a : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
inl : IsEmpty α → SigmaFinite μ
⊢ SigmaFinite μ
have inr : Nonempty α → SigmaFinite μ
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Countable α
hμ : ∀ (a : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
h : IsEmpty α
⊢ SigmaFinite μ
have inl : SigmaFinite.{u_1} (α := α) (m0 := m0) 0
Tactic: rw [Subsingleton.elim μ 0]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Countable α
hμ : ∀ (a : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
h : Nonempty α
⊢ SigmaFinite μ
have inr : ∀ (f : ℕ → α) (hf : Surjective f), SigmaFinite μ
Tactic: obtain ⟨f, hf⟩ := exists_surjective_nat α
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
μ : Measure α
⊢ SigmaFinite μ ↔ IsFiniteMeasure μ
have refine : ∀ (h : SigmaFinite μ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine ⟨fun h => ⟨?_⟩, fun h => by infer_instance⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : (i : ℕ) → Set α := spanningSets μ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have hs_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
Tactic: have hs_univ : ⋃ i, s i = Set.univ := iUnion_spanningSets μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : (i : ℕ) → Set α := spanningSets μ
hs_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have hs_meas : ∀ (i : ℕ), MeasurableSet (s i)
Tactic: have hs_meas : ∀ i, MeasurableSet[⊥] (s i) := measurableSet_spanningSets μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : (i : ℕ) → Set α := spanningSets μ
hs_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
hs_meas : ∀ (i : ℕ), MeasurableSet (s i)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have hs_meas₁ : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
Tactic: simp_rw [MeasurableSpace.measurableSet_bot_iff] at hs_meas
Cleared hypotheses: hs_meas
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : (i : ℕ) → Set α := spanningSets μ
hs_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have pos : ∀ (h_univ_empty : Eq.{u_1 + 1} (α := Set α) univ ∅), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: by_cases h_univ_empty : (Set.univ : Set α) = ∅
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : (i : ℕ) → Set α := spanningSets μ
hs_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
pos :
  ∀ (h_univ_empty : Eq.{u_1 + 1} (α := Set α) univ ∅),
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have neg : ∀ (h_univ_empty : ¬Eq.{u_1 + 1} (α := Set α) univ ∅),
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: by_cases h_univ_empty : (Set.univ : Set α) = ∅
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : (i : ℕ) → Set α := spanningSets μ
hs_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : Eq.{u_1 + 1} (α := Set α) univ ∅
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have pos : LT.lt (α := ℝ≥0∞) 0 ∞
Tactic: rw [h_univ_empty, measure_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : (i : ℕ) → Set α := spanningSets μ
hs_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬Eq.{u_1 + 1} (α := Set α) univ ∅
⊢ ∃ (i : ℕ), s i = univ
have by_contra! : ∀ (h_not_univ : ∀ (i : ℕ), s i ≠ univ), False
Tactic: by_contra! h_not_univ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : (i : ℕ) → Set α := spanningSets μ
hs_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬Eq.{u_1 + 1} (α := Set α) univ ∅
h_not_univ : ∀ (i : ℕ), s i ≠ univ
⊢ False
have h_empty : ∀ (i : ℕ), s i = ∅
Tactic: have h_empty : ∀ i, s i = ∅ := by simpa [h_not_univ] using hs_meas
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : (i : ℕ) → Set α := spanningSets μ
hs_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬Eq.{u_1 + 1} (α := Set α) univ ∅
h_not_univ : ∀ (i : ℕ), s i ≠ univ
h_empty : ∀ (i : ℕ), s i = ∅
⊢ False
have hs_univ₁ : Eq.{u_1 + 1} (α := Set α) ∅ univ
Tactic: simp only [h_empty, iUnion_empty] at hs_univ
Cleared hypotheses: hs_univ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : (i : ℕ) → Set α := spanningSets μ
hs_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬Eq.{u_1 + 1} (α := Set α) univ ∅
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have neg : ∀ (i : ℕ) (hsi : s i = univ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: obtain ⟨i, hsi⟩ : ∃ i, s i = Set.univ := by
    by_contra! h_not_univ
    have h_empty : ∀ i, s i = ∅ := by simpa [h_not_univ] using hs_meas
    simp only [h_empty, iUnion_empty] at hs_univ
    exact h_univ_empty hs_univ.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : (i : ℕ) → Set α := spanningSets μ
hs_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
hs_meas : ∀ (i : ℕ), s i = ∅ ∨ s i = univ
h_univ_empty : ¬Eq.{u_1 + 1} (α := Set α) univ ∅
i : ℕ
hsi : s i = univ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have neg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← hsi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 ν : Measure α
s_1 t : Set α
a : α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
⊢ SigmaFinite (μ.restrict s)
have refine : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (spanningSets μ i) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine ⟨⟨⟨spanningSets μ, fun _ => trivial, fun i => ?_, iUnion_spanningSets μ⟩⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 ν : Measure α
s_1 t : Set α
a : α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
i : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (spanningSets μ i) : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (spanningSets μ i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply (measurableSet_spanningSets μ i)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
ι_1 : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst_1 : Finite ι
μ : ι → Measure α
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
⊢ SigmaFinite (sum μ)
have intro : ∀ (val : Fintype ι), SigmaFinite (sum μ)
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι_1 : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst_1 : Finite ι
μ : ι → Measure α
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
val : Fintype ι
⊢ SigmaFinite (sum μ)
have this : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (i : ι), spanningSets (μ i) n)
Tactic: have : ∀ n, MeasurableSet (⋂ i : ι, spanningSets (μ i) n) := fun n =>
    MeasurableSet.iInter fun i => measurableSet_spanningSets (μ i) n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
ι_1 : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst_1 : Finite ι
μ : ι → Measure α
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
val : Fintype ι
this : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (i : ι), spanningSets (μ i) n)
⊢ SigmaFinite (sum μ)
have intro : ∀ (n : ℕ),
  LT.lt (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) ((fun (n : ℕ) ↦ (⋂ (i : ι), spanningSets (μ i) n : Set α)) n) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: refine ⟨⟨⟨fun n => ⋂ i, spanningSets (μ i) n, fun _ => trivial, fun n => ?_, ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
ι_1 : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst_1 : Finite ι
μ : ι → Measure α
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
val : Fintype ι
this : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (i : ι), spanningSets (μ i) n)
intro :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞)
      ((sum μ : (a : Set α) → ℝ≥0∞) ((fun (n : ℕ) ↦ (⋂ (i : ι), spanningSets (μ i) n : Set α)) n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ SigmaFinite (sum μ)
have intro₁ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ (⋂ (i : ι), spanningSets (μ i) n : Set α)) i) univ
Tactic: refine ⟨⟨⟨fun n => ⋂ i, spanningSets (μ i) n, fun _ => trivial, fun n => ?_, ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
ι_1 : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst_1 : Finite ι
μ : ι → Measure α
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
val : Fintype ι
this : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (i : ι), spanningSets (μ i) n)
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) ((fun (n : ℕ) ↦ (⋂ (i : ι), spanningSets (μ i) n : Set α)) n) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
have intro : ∀ (a : ι),
  Membership.mem (γ := Finset ι) Finset.univ a →
    LT.lt (α := ℝ≥0∞) ((μ a : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), spanningSets (μ i) n) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [sum_apply _ (this n), tsum_fintype, ENNReal.sum_lt_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
ι_1 : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst_1 : Finite ι
μ : ι → Measure α
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
val : Fintype ι
this : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (i : ι), spanningSets (μ i) n)
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ (⋂ (i : ι), spanningSets (μ i) n : Set α)) i) univ
have intro : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), ⋃ (j : ℕ), spanningSets (μ i) j) univ
Tactic: rw [iUnion_iInter_of_monotone]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
ι_1 : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst_1 : Finite ι
μ : ι → Measure α
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
val : Fintype ι
this : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (i : ι), spanningSets (μ i) n)
intro : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), ⋃ (j : ℕ), spanningSets (μ i) j) univ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ (⋂ (i : ι), spanningSets (μ i) n : Set α)) i) univ
have intro₁ : ∀ (i : ι), Monotone (spanningSets (μ i))
Tactic: rw [iUnion_iInter_of_monotone]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
ι_1 : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 ν : Measure α
s t : Set α
a : α
ι : Type u_4
inst_1 : Finite ι
μ : ι → Measure α
inst_2 : ∀ (i : ι), SigmaFinite (μ i)
val : Fintype ι
this : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) (⋂ (i : ι), spanningSets (μ i) n)
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), ⋃ (j : ℕ), spanningSets (μ i) j) univ
have intro : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), univ) univ
Tactic: simp_rw [iUnion_spanningSets, iInter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 ν_1 : Measure α
s t : Set α
a : α
μ ν : Measure α
inst_1 : SigmaFinite μ
inst_2 : SigmaFinite ν
⊢ SigmaFinite (μ + ν)
have rw : SigmaFinite.{u_1} (α := α) (m0 := m0) (sum fun (b : Bool) ↦ bif b then μ else ν)
Tactic: rw [← sum_cond]