awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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))
simp_rw₄ :
  Eq (α := ℝ≥0∞) (⨆ (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (spanningSets μ i ∩ toMeasurable μ s))
    (⨆ (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))

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)]

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.measurableSet_spanningSets, Set.inter_comm, MeasureTheory.toMeasurable, MeasureTheory.Measure.restrict_apply', MeasureTheory.Measure.restrict_toMeasurable_of_sFinite
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
h's : r < (μ : (a : Set α) → ℝ≥0∞) 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

Premises used: MeasureTheory.Measure.iSup_restrict_spanningSets, lt_iSup_iff
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
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∞)
⊢ ∃ (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⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
⊢ r < (μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ n)

Tactic:
simp only [restrict_apply hs] at hn

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

Tactic:
⟨s ∩ spanningSets μ n, hs.inter (measurableSet_spanningSets _ _), inter_subset_left, hn, ?_⟩

Premises used: MeasureTheory.measurableSet_spanningSets, Set.inter_subset_left, Inter.inter, And.intro, Exists.intro, MeasureTheory.spanningSets, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : SigmaFinite μ
r : ℝ≥0∞
hs : MeasurableSet s
n : ℕ
hn : r < (μ : (a : Set α) → ℝ≥0∞) (s ∩ MeasureTheory.spanningSets μ n)
spanningSets : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ MeasureTheory.spanningSets μ n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (t : Set α),
    MeasurableSet t ∧
      t ⊆ s ∧ r < (μ : (a : Set α) → ℝ≥0∞) t ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine
    ⟨s ∩ spanningSets μ n, hs.inter (measurableSet_spanningSets _ _), inter_subset_left, hn, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_mono inter_subset_right).trans_lt (measure_spanningSets_lt_top _ _)

Premises used: MeasureTheory.measure_spanningSets_lt_top, MeasureTheory.measure_mono, LE.le.trans_lt, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ spanningSets μ n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact (measure_mono inter_subset_right).trans_lt (measure_spanningSets_lt_top _ _)

Premises used: MeasureTheory.measure_spanningSets_lt_top, MeasureTheory.measure_mono, LE.le.trans_lt, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
C : Set (Set α)
h : μ.FiniteSpanningSetsIn C
⊢ SigmaFinite μ

Tactic:
⟨⟨h.mono <| subset_univ C⟩⟩

Premises used: Set.subset_univ, MeasureTheory.Measure.FiniteSpanningSetsIn.mono, Nonempty.intro, MeasureTheory.SigmaFinite.mk
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
C : Set (Set α)
hA : m0 = generateFrom C
hC : IsPiSystem C
h : μ.FiniteSpanningSetsIn C
h_eq : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ = ν

Tactic:
ext_of_generateFrom_of_iUnion C _ hA hC h.spanning h.set_mem (fun i => (h.finite i).ne) h_eq

Premises used: MeasureTheory.Measure.FiniteSpanningSetsIn.spanning, MeasureTheory.Measure.FiniteSpanningSetsIn.finite, MeasureTheory.Measure.ext_of_generateFrom_of_iUnion, MeasureTheory.Measure.FiniteSpanningSetsIn.set_mem, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
C : Set (Set α)
h : μ.FiniteSpanningSetsIn C
⊢ IsCountablySpanning C

Tactic:
⟨h.set, h.set_mem, h.spanning⟩

Premises used: MeasureTheory.Measure.FiniteSpanningSetsIn.set, MeasureTheory.Measure.FiniteSpanningSetsIn.spanning, And.intro, Exists.intro, IsCountablySpanning, MeasureTheory.Measure.FiniteSpanningSetsIn.set_mem
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
⊢ (fun (x : Set α) ↦ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (∞ : ℝ≥0∞)) ∅

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
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 μ
⊢ 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⟩

Premises used: Iff.mpr, Set.univ, Set.exists_seq_cover_iff_countable, And.intro, Exists.intro, EmptyCollection.emptyCollection
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hc : S.Countable
hμ_1 : ∀ s ∈ S, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hU : ⋃₀ S = univ
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:
⟨⟨⟨fun n => s n, fun _ => trivial, hμ, hs⟩⟩⟩

Premises used: trivial, MeasureTheory.Measure.FiniteSpanningSetsIn.mk, Nonempty.intro, MeasureTheory.SigmaFinite.mk
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
S : Set (Set α)
hc : S.Countable
hμ_1 : ∀ s ∈ S, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
hU : ⋃₀ S = univ
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:
exact ⟨⟨⟨fun n => s n, fun _ => trivial, hμ, hs⟩⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
ν μ : Measure α
hs : SigmaFinite μ
h : ν ≤ μ
⊢ SigmaFinite ν

Tactic:
⟨hs.out.map <| FiniteSpanningSetsIn.ofLE h⟩

Premises used: MeasureTheory.Measure.FiniteSpanningSetsIn.ofLE, MeasureTheory.SigmaFinite.out, Nonempty.map, MeasureTheory.SigmaFinite.mk
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst : SigmaFinite μ
h : ν₁ = ν₂
rw rw₁ : μ + ν₂ = μ + ν₂
⊢ μ + ν₁ = μ + ν₂

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst : SigmaFinite μ
refine : ∀ (h : μ + ν₁ = μ + ν₂), ν₁ = ν₂
⊢ μ + ν₁ = μ + ν₂ ↔ ν₁ = ν₂

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
rw : ∀ (i : ℕ), ν₁.restrict (spanningSets μ i) = ν₂.restrict (spanningSets μ i)
⊢ ν₁ = ν₂

Tactic:
rw [ext_iff_of_iUnion_eq_univ (iUnion_spanningSets μ)]

Premises used: MeasureTheory.iUnion_spanningSets, MeasureTheory.Measure.ext_iff_of_iUnion_eq_univ
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
i : ℕ
h₁ :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((ν₁.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((ν₂.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ν₁.restrict (spanningSets μ i) = ν₂.restrict (spanningSets μ i)

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
i : ℕ
s : Set α
hs : MeasurableSet s
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∞)
⊢ Eq (α := ℝ≥0∞) ((ν₁.restrict (spanningSets μ i) : (a : Set α) → ℝ≥0∞) s : ℝ≥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]

Premises used: MeasureTheory.measure_spanningSets_lt_top, ENNReal.add_right_inj, MeasureTheory.measure_mono, LE.le.trans_lt, Set.inter_subset_right, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst : SigmaFinite μ
h : μ + ν₁ = μ + ν₂
i : ℕ
s : Set α
hs : MeasurableSet s
⊢ ∀ (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

Premises used: MeasureTheory.Measure.coe_add, Pi.add_apply, MeasureTheory.Measure.ext_iff'
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst : SigmaFinite μ
i : ℕ
s : Set α
hs : MeasurableSet s
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∞)
⊢ 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:
simp [hs, h]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
inst : SigmaFinite μ
rw : μ + ν₁ = ν₂ + μ ↔ ν₁ = ν₂
rw₁ : μ + ν₁ = μ + ν₂ ↔ ν₁ = ν₂
rw₂ rw₃ : ν₁ = ν₂ ↔ ν₁ = ν₂
⊢ ν₁ + μ = ν₂ + μ ↔ ν₁ = ν₂

Tactic:
rw [add_comm _ μ, add_comm _ μ, μ.add_right_inj]

Premises used: MeasureTheory.Measure.add_right_inj, add_comm
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 ν : Measure α
s t : Set α
a : α
_m0 : MeasurableSpace α
μ : Measure α
inst_1 : IsFiniteMeasure μ
⊢ SigmaFinite μ

Tactic:
⟨⟨⟨fun _ => univ, fun _ => trivial, fun _ => measure_lt_top μ _, iUnion_const _⟩⟩⟩

Premises used: trivial, MeasureTheory.measure_lt_top, Set.univ, MeasureTheory.Measure.FiniteSpanningSetsIn.mk, Set.iUnion_const, Nonempty.intro, MeasureTheory.SigmaFinite.mk
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Countable α
hμ : ∀ (a : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
inl : IsEmpty α → SigmaFinite μ
inr : Nonempty α → SigmaFinite μ
⊢ SigmaFinite μ

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Countable α
hμ : ∀ (a : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
h : IsEmpty α
inl : SigmaFinite.{u_1} (α := α) (m0 := m0) 0
⊢ SigmaFinite μ

Tactic:
rw [Subsingleton.elim μ 0]

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Countable α
hμ : ∀ (a : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
h : IsEmpty α
⊢ SigmaFinite.{u_1} (α := α) (m0 := m0) 0

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Countable α
hμ : ∀ (a : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
h : Nonempty α
inr : ∀ (f : ℕ → α) (hf : Surjective f), SigmaFinite μ
⊢ SigmaFinite μ

Tactic:
obtain ⟨f, hf⟩ := exists_surjective_nat α

Premises used: exists_surjective_nat
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Countable α
hμ : ∀ (a : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
h : Nonempty α
f : ℕ → α
hf : Surjective f
⊢ ∀ (i : ℕ), Membership.mem (γ := Set (Set α)) univ ((fun (n : ℕ) ↦ ({f n} : Set α)) i)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Countable α
hμ : ∀ (a : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
h : Nonempty α
f : ℕ → α
hf : Surjective f
⊢ ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (n : ℕ) ↦ ({f n} : Set α)) i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simpa [hf.forall] using hμ

Premises used: Function.Surjective.forall
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Countable α
hμ : ∀ (a : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
h : Nonempty α
f : ℕ → α
hf : Surjective f
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ ({f n} : Set α)) i) univ

Tactic:
simp [hf.range_eq]

Premises used: Function.Surjective.range_eq
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : Countable α
hμ : ∀ (a : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)
h : Nonempty α
f : ℕ → α
hf : Surjective f
⊢ SigmaFinite μ

Tactic:
exact ⟨⟨⟨fun n ↦ {f n}, by simp, by simpa [hf.forall] using hμ, by simp [hf.range_eq]⟩⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
μ : Measure α
h : IsFiniteMeasure μ
⊢ SigmaFinite μ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
μ : Measure α
refine : ∀ (h : SigmaFinite μ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ SigmaFinite μ ↔ IsFiniteMeasure μ

Tactic:
refine ⟨fun h => ⟨?_⟩, fun h => by infer_instance⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
μ : Measure α
h : SigmaFinite μ
⊢ SigmaFinite μ

Tactic:
haveI : SigmaFinite μ := h
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : (i : ℕ) → Set α := spanningSets μ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ

Tactic:
have hs_univ : ⋃ i, s i = Set.univ := iUnion_spanningSets μ
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : (i : ℕ) → Set α := spanningSets μ
hs_univ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), s i) univ
⊢ ∀ (i : ℕ), MeasurableSet (s i)

Tactic:
have hs_meas : ∀ i, MeasurableSet[⊥] (s i) := measurableSet_spanningSets μ
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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)
⊢ ∀ (i : ℕ), s i = ∅ ∨ s i = univ

Tactic:
simp_rw [MeasurableSpace.measurableSet_bot_iff] at hs_meas

Premises used: MeasurableSpace.measurableSet_bot_iff
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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∞)
neg :
  ∀ (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∞)

Tactic:
by_cases h_univ_empty : (Set.univ : Set α) = ∅

Premises used: Set.univ
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 ∅
pos : LT.lt (α := ℝ≥0∞) 0 ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [h_univ_empty, measure_empty]

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

Tactic:
ENNReal.zero_ne_top.lt_top

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

Tactic:
exact ENNReal.zero_ne_top.lt_top

Premises used: ENNReal.zero_ne_top, Ne.lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 ∅
by_contra! : ∀ (h_not_univ : ∀ (i : ℕ), s i ≠ univ), False
⊢ ∃ (i : ℕ), s i = univ

Tactic:
by_contra! h_not_univ
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
⊢ ∀ (i : ℕ), s i = ∅

Tactic:
simpa [h_not_univ] using hs_meas
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
⊢ ∀ (i : ℕ), s i = ∅

Tactic:
have h_empty : ∀ i, s i = ∅ := by simpa [h_not_univ] using hs_meas
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 = ∅
⊢ Eq.{u_1 + 1} (α := Set α) ∅ univ

Tactic:
simp only [h_empty, iUnion_empty] at hs_univ

Premises used: Set.iUnion_empty
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : (i : ℕ) → Set α := spanningSets μ
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 = ∅
hs_univ : Eq.{u_1 + 1} (α := Set α) ∅ univ
⊢ False

Tactic:
h_univ_empty hs_univ.symm

Premises used: Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
μ : Measure α
h this : SigmaFinite μ
s : (i : ℕ) → Set α := spanningSets μ
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 = ∅
hs_univ : Eq.{u_1 + 1} (α := Set α) ∅ univ
⊢ False

Tactic:
exact h_univ_empty hs_univ.symm

Premises used: Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 ∅
neg : ∀ (i : ℕ) (hsi : s i = univ), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ 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

Premises used: Set.univ