awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ∅
i : ℕ
hsi : s i = univ
neg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [← hsi]
-- 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 ∅
i : ℕ
hsi : s i = univ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_spanningSets_lt_top μ i

Premises used: MeasureTheory.measure_spanningSets_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 ∅
i : ℕ
hsi : s i = univ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact measure_spanningSets_lt_top μ i

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

Tactic:
⟨⟨⟨spanningSets μ, fun _ => trivial, fun i => ?_, iUnion_spanningSets μ⟩⟩⟩

Premises used: trivial, MeasureTheory.Measure.FiniteSpanningSetsIn.mk, Nonempty.intro, MeasureTheory.iUnion_spanningSets, MeasureTheory.spanningSets, MeasureTheory.SigmaFinite.mk
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 α
refine : ∀ (i : ℕ), LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (spanningSets μ i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ SigmaFinite (μ.restrict s)

Tactic:
refine ⟨⟨⟨spanningSets μ, fun _ => trivial, fun i => ?_, iUnion_spanningSets μ⟩⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 : ℕ
rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (spanningSets μ i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) (spanningSets μ i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [Measure.restrict_apply (measurableSet_spanningSets μ i)]

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.measurableSet_spanningSets
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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∞) ((μ : (a : Set α) → ℝ≥0∞) (spanningSets μ i ∩ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_mono inter_subset_left).trans_lt (measure_spanningSets_lt_top μ i)

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

Tactic:
exact (measure_mono inter_subset_left).trans_lt (measure_spanningSets_lt_top μ i)

Premises used: MeasureTheory.measure_spanningSets_lt_top, Set.inter_subset_left, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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)
intro : ∀ (val : Fintype ι), SigmaFinite (sum μ)
⊢ SigmaFinite (sum μ)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 ι
⊢ ∀ (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
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 μ)

Tactic:
⟨⟨⟨fun n => ⋂ i, spanningSets (μ i) n, fun _ => trivial, fun n => ?_, ?_⟩⟩⟩

Premises used: trivial, Set.iInter, MeasureTheory.Measure.FiniteSpanningSetsIn.mk, Nonempty.intro, MeasureTheory.spanningSets, MeasureTheory.SigmaFinite.mk
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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∞)
intro₁ : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ (⋂ (i : ι), spanningSets (μ i) n : Set α)) i) univ
⊢ SigmaFinite (sum μ)

Tactic:
refine ⟨⟨⟨fun n => ⋂ i, spanningSets (μ i) n, fun _ => trivial, fun n => ?_, ?_⟩⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 : ℕ
intro :
  ∀ (a : ι),
    Membership.mem (γ := Finset ι) Finset.univ a →
      LT.lt (α := ℝ≥0∞) ((μ a : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), spanningSets (μ i) n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) ((fun (n : ℕ) ↦ (⋂ (i : ι), spanningSets (μ i) n : Set α)) n) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
rw [sum_apply _ (this n), tsum_fintype, ENNReal.sum_lt_top]

Premises used: MeasureTheory.Measure.sum_apply, ENNReal.sum_lt_top, tsum_fintype
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 : ℕ
i : ι
⊢ LT.lt (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), spanningSets (μ i) n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
(measure_mono <| iInter_subset _ i).trans_lt (measure_spanningSets_lt_top (μ i) n)

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

Tactic:
exact (measure_mono <| iInter_subset _ i).trans_lt (measure_spanningSets_lt_top (μ i) n)

Premises used: MeasureTheory.measure_mono, Set.iInter_subset, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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
intro₁ : ∀ (i : ι), Monotone (spanningSets (μ i))
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ (⋂ (i : ι), spanningSets (μ i) n : Set α)) i) univ

Tactic:
rw [iUnion_iInter_of_monotone]

Premises used: Set.iUnion_iInter_of_monotone
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 : ι), univ) univ
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), ⋃ (j : ℕ), spanningSets (μ i) j) univ

Tactic:
simp_rw [iUnion_spanningSets, iInter_univ]

Premises used: Set.iInter_univ, MeasureTheory.iUnion_spanningSets
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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)
⊢ ∀ (i : ι), Monotone (spanningSets (μ i))

Tactic:
fun i => monotone_spanningSets (μ i)

Premises used: MeasureTheory.monotone_spanningSets
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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)
⊢ ∀ (i : ι), Monotone (spanningSets (μ i))

Tactic:
exact fun i => monotone_spanningSets (μ i)

Premises used: MeasureTheory.monotone_spanningSets
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 ν
rw : SigmaFinite.{u_1} (α := α) (m0 := m0) (sum fun (b : Bool) ↦ bif b then μ else ν)
⊢ SigmaFinite (μ + ν)

Tactic:
rw [← sum_cond]

Premises used: MeasureTheory.Measure.sum_cond
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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.{u_1} (α := α) (m0 := m0) (sum fun (b : Bool) ↦ bif b then μ else ν)

Tactic:
@sum.sigmaFinite _ _ _ _ _ (Bool.rec ?_ ?_)

Premises used: MeasureTheory.sum.sigmaFinite
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 ν
refine_1 : SigmaFinite (bif false then μ else ν)
refine_2 : SigmaFinite (bif true then μ else ν)
⊢ SigmaFinite.{u_1} (α := α) (m0 := m0) (sum fun (b : Bool) ↦ bif b then μ else ν)

Tactic:
refine @sum.sigmaFinite _ _ _ _ _ (Bool.rec ?_ ?_)

Premises used: MeasureTheory.sum.sigmaFinite
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 (bif false then μ else ν)

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
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 (bif true then μ else ν)

Tactic:
simpa
-- 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 : α
μ : Measure α
inst_1 : SigmaFinite μ
c : ℝ≥0
i : ℕ
simp : HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (spanningSets μ i) : ℝ≥0∞) < ∞
⊢ LT.lt (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) (spanningSets μ i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp only [Measure.coe_smul, Pi.smul_apply, nnreal_smul_coe_apply]

Premises used: MeasureTheory.Measure.coe_smul, MeasureTheory.Measure.nnreal_smul_coe_apply, Pi.smul_apply
-- 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 : α
μ : Measure α
inst_1 : SigmaFinite μ
c : ℝ≥0
i : ℕ
⊢ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (spanningSets μ i) : ℝ≥0∞) < ∞

Tactic:
ENNReal.mul_lt_top ENNReal.coe_lt_top (measure_spanningSets_lt_top μ i)

Premises used: MeasureTheory.measure_spanningSets_lt_top, ENNReal.mul_lt_top, ENNReal.coe_lt_top
-- 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 : α
μ : Measure α
inst_1 : SigmaFinite μ
c : ℝ≥0
i : ℕ
⊢ HMul.hMul (β := ℝ≥0∞) (↑c : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (spanningSets μ i) : ℝ≥0∞) < ∞

Tactic:
exact ENNReal.mul_lt_top ENNReal.coe_lt_top (measure_spanningSets_lt_top μ i)

Premises used: MeasureTheory.measure_spanningSets_lt_top, ENNReal.mul_lt_top, ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ ν : Measure α
s t : Set α
a : α
inst_1 : SigmaFinite (μ.restrict s)
inst_2 : SigmaFinite (μ.restrict t)
⊢ SigmaFinite (μ.restrict (s ∪ t))

Tactic:
sigmaFinite_of_le _ (restrict_union_le _ _)

Premises used: MeasureTheory.Measure.sigmaFinite_of_le, MeasureTheory.Measure.restrict_union_le
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ ν : Measure α
s t : Set α
a : α
inst_1 : SigmaFinite (μ.restrict s)
⊢ SigmaFinite (μ.restrict (s ∩ t))

Tactic:
sigmaFinite_of_le (μ.restrict s) (restrict_mono_ae (ae_of_all _ Set.inter_subset_left))

Premises used: MeasureTheory.Measure.sigmaFinite_of_le, MeasureTheory.Measure.restrict, Set.inter_subset_left, MeasureTheory.Measure.restrict_mono_ae, MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ ν : Measure α
s t : Set α
a : α
inst_1 : SigmaFinite (μ.restrict t)
⊢ SigmaFinite (μ.restrict (s ∩ t))

Tactic:
sigmaFinite_of_le (μ.restrict t) (restrict_mono_ae (ae_of_all _ Set.inter_subset_right))

Premises used: MeasureTheory.Measure.sigmaFinite_of_le, MeasureTheory.Measure.restrict, MeasureTheory.Measure.restrict_mono_ae, MeasureTheory.ae_of_all, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
h : SigmaFinite (m0 := inst) (Measure.map f μ)
n : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) ((fun (n : ℕ) ↦ f ⁻¹' spanningSets (m0 := inst) (Measure.map f μ) n) n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp only [← map_apply_of_aemeasurable hf, measurableSet_spanningSets,
          measure_spanningSets_lt_top]

Premises used: MeasureTheory.measure_spanningSets_lt_top, MeasureTheory.measurableSet_spanningSets, MeasureTheory.Measure.map_apply_of_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
h : SigmaFinite (m0 := inst) (Measure.map f μ)
rw : f ⁻¹' ⋃ (i : ℕ), spanningSets (m0 := inst) (Measure.map f μ) i = univ
rw₁ : f ⁻¹' univ = univ
rw₂ rw₃ : Eq.{u_1 + 1} (α := Set α) univ univ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ f ⁻¹' spanningSets (m0 := inst) (Measure.map f μ) n) i) univ

Tactic:
rw [← preimage_iUnion, iUnion_spanningSets, preimage_univ]

Premises used: MeasureTheory.iUnion_spanningSets, Set.preimage_univ, Set.preimage_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst_1 : SigmaFinite μ
⊢ ∀ (i : ℕ), Membership.mem (γ := Set (Set β)) univ ((fun (n : ℕ) ↦ f '' spanningSets μ n ∪ (range f)ᶜ) i)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst_1 : SigmaFinite μ
refine_1 :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞)
      (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) ((fun (n : ℕ) ↦ f '' spanningSets μ n ∪ (range f)ᶜ) n) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
refine_2 : Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), (fun (n : ℕ) ↦ f '' spanningSets μ n ∪ (range f)ᶜ) i) univ
⊢ SigmaFinite (m0 := inst) (Measure.map f μ)

Tactic:
refine ⟨fun n ↦ f '' (spanningSets μ n) ∪ (Set.range f)ᶜ, by simp, fun n ↦ ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst_1 : SigmaFinite μ
n : ℕ
refine_1 :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' spanningSets μ n ∪ f ⁻¹' (range f)ᶜ) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞)
    (((Measure.map f μ : Measure β) : (a : Set β) → ℝ≥0∞) ((fun (n : ℕ) ↦ f '' spanningSets μ n ∪ (range f)ᶜ) n) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
rw [hf.map_apply, Set.preimage_union]

Premises used: Set.preimage_union, MeasurableEmbedding.map_apply
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst_1 : SigmaFinite μ
n : ℕ
refine_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (spanningSets μ n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' f '' spanningSets μ n ∪ f ⁻¹' (range f)ᶜ) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp only [Set.preimage_compl, Set.preimage_range, Set.compl_univ, Set.union_empty,
      Set.preimage_image_eq _ hf.injective]

Premises used: Set.union_empty, Set.preimage_range, Set.compl_univ, MeasurableEmbedding.injective, Set.preimage_image_eq, Set.preimage_compl
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst_1 : SigmaFinite μ
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (spanningSets μ n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_spanningSets_lt_top μ n

Premises used: MeasureTheory.measure_spanningSets_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst_1 : SigmaFinite μ
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (spanningSets μ n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact measure_spanningSets_lt_top μ n

Premises used: MeasureTheory.measure_spanningSets_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
hf : MeasurableEmbedding f
inst_1 : SigmaFinite μ
refine_2 : (⋃ (i : ℕ), f '' spanningSets μ i) ∪ (range f)ᶜ = univ
refine_2₁ : (f '' ⋃ (i : ℕ), spanningSets μ i) ∪ (range f)ᶜ = univ
refine_2₂ : f '' univ ∪ (range f)ᶜ = univ
refine_2₃ : range f ∪ (range f)ᶜ = univ
refine_2₄ refine_2₅ : Eq.{u_2 + 1} (α := Set β) univ univ
⊢ Eq.{u_2 + 1} (α := Set β) (⋃ (i : ℕ), (fun (n : ℕ) ↦ f '' spanningSets μ n ∪ (range f)ᶜ) i) univ

Tactic:
rw [← Set.iUnion_union, ← Set.image_iUnion, iUnion_spanningSets,
      Set.image_univ, Set.union_compl_self]

Premises used: Set.image_univ, Set.iUnion_union, Set.union_compl_self, Set.image_iUnion, MeasureTheory.iUnion_spanningSets
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α ≃ᵐ β
inst_1 : SigmaFinite μ
⊢ SigmaFinite.{u_2} (α := β) (m0 := inst) (Measure.map (⇑f : (a : α) → β) μ)

Tactic:
f.measurableEmbedding.sigmaFinite_map

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEmbedding.sigmaFinite_map
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
P : α → Prop
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∀ᵐ (x : α) ∂μ.restrict s, P x
n : ℕ
⊢ ∀ᵐ (x : α) ∂μ.restrict (spanningSets (μ + ν) n), P x

Tactic:
have := h
      (spanningSets (μ + ν) n) (measurableSet_spanningSets _ _)
      ((self_le_add_right _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
      ((self_le_add_left _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
P : α → Prop
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∀ᵐ (x : α) ∂μ.restrict s, P x
n : ℕ
this : ∀ᵐ (x : α) ∂μ.restrict (spanningSets (μ + ν) n), P x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x

Tactic:
(ae_restrict_iff' (measurableSet_spanningSets _ _)).mp this

Premises used: MeasureTheory.measurableSet_spanningSets, Iff.mp, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
P : α → Prop
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∀ᵐ (x : α) ∂μ.restrict s, P x
n : ℕ
this : ∀ᵐ (x : α) ∂μ.restrict (spanningSets (μ + ν) n), P x
⊢ ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x

Tactic:
exact (ae_restrict_iff' (measurableSet_spanningSets _ _)).mp this

Premises used: MeasureTheory.measurableSet_spanningSets, Iff.mp, MeasureTheory.ae_restrict_iff'