awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α
rw rw₁ : Eq.{u_1 + 1} (α := Measure α) 0 0
⊢ Eq.{u_1 + 1} (α := Measure α) 0 (sum fun (x : ℕ) ↦ 0)

Tactic:
rw [Measure.sum_zero]

Premises used: MeasureTheory.Measure.sum_zero
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
n : ℕ
⊢ Eq.{u_1 + 1} (α := Measure α) (sfiniteSeq 0 n) 0

Tactic:
bot_unique <| sfiniteSeq_le _ _

Premises used: MeasureTheory.sfiniteSeq_le, bot_unique
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst : Countable ι
m : ι → Measure α
inst_1 : ∀ (n : ι), IsFiniteMeasure (m n)
⊢ ∃ (f : ι → ℕ), Injective f

Tactic:
Countable.exists_injective_nat ι

Premises used: Countable.exists_injective_nat
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst : Countable ι
m : ι → Measure α
inst_1 : ∀ (n : ι), IsFiniteMeasure (m n)
obtain : ∀ (f : ι → ℕ) (hf : Injective f), SFinite (sum m)
⊢ SFinite (sum m)

Tactic:
obtain ⟨f, hf⟩ : ∃ f : ι → ℕ, Function.Injective f := Countable.exists_injective_nat ι

Premises used: Countable.exists_injective_nat
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst : Countable ι
m : ι → Measure α
inst_1 : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
⊢ SFinite (sum m)

Tactic:
⟨_, fun n ↦ ?_, (sum_extend_zero hf m).symm⟩

Premises used: And.intro, MeasureTheory.SFinite.mk, Exists.intro, Eq.symm, MeasureTheory.Measure.sum_extend_zero
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst : Countable ι
m : ι → Measure α
inst_1 : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
refine : ∀ (n : ℕ), IsFiniteMeasure (Function.extend f m 0 n)
⊢ SFinite (sum m)

Tactic:
refine ⟨_, fun n ↦ ?_, (sum_extend_zero hf m).symm⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst : Countable ι
m : ι → Measure α
inst_1 : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
n : ℕ
inl : ∀ (i : ι), IsFiniteMeasure (Function.extend f m 0 (f i))
inr : ∀ (hn : n ∉ range f), IsFiniteMeasure (Function.extend f m 0 n)
⊢ IsFiniteMeasure (Function.extend f m 0 n)

Tactic:
rcases em (n ∈ range f) with ⟨i, rfl⟩ | hn

Premises used: Membership.mem, em, Set.range, rfl
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst : Countable ι
m : ι → Measure α
inst_1 : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
i : ι
inl : IsFiniteMeasure (m i)
⊢ IsFiniteMeasure (Function.extend f m 0 (f i))

Tactic:
rw [hf.extend_apply]

Premises used: Function.Injective.extend_apply
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst : Countable ι
m : ι → Measure α
inst_1 : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
i : ι
⊢ IsFiniteMeasure (m i)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst : Countable ι
m : ι → Measure α
inst_1 : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
n : ℕ
hn : n ∉ range f
inr : IsFiniteMeasure.{u_1} (α := α) (m0 := m0) 0
⊢ IsFiniteMeasure (Function.extend f m 0 n)

Tactic:
rw [Function.extend_apply' _ _ _ hn, Pi.zero_apply]

Premises used: Pi.zero_apply, Function.extend_apply'
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst : Countable ι
m : ι → Measure α
inst_1 : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
n : ℕ
hn : n ∉ range f
⊢ IsFiniteMeasure.{u_1} (α := α) (m0 := m0) 0

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst : Countable ι
m : ι → Measure α
inst_1 : ∀ (n : ι), IsFiniteMeasure (m n)
obtain : ∀ (f : ι → ℕ) (hf : Injective f), SFinite (sum m)
obtain₁ : ∀ (f : ι → ℕ) (hf : Injective f) (n : ℕ), IsFiniteMeasure (Function.extend f m 0 n)
inl : ∀ (f : ι → ℕ) (hf : Injective f) (i : ι), IsFiniteMeasure (Function.extend f m 0 (f i))
inr inr₁ : ∀ (f : ι → ℕ) (hf : Injective f) (n : ℕ) (hn : n ∉ range f), IsFiniteMeasure (Function.extend f m 0 n)
⊢ SFinite (sum m)

Tactic:
classical
  obtain ⟨f, hf⟩ : ∃ f : ι → ℕ, Function.Injective f := Countable.exists_injective_nat ι
  refine ⟨_, fun n ↦ ?_, (sum_extend_zero hf m).symm⟩
  rcases em (n ∈ range f) with ⟨i, rfl⟩ | hn
  · rw [hf.extend_apply]
    infer_instance
  · rw [Function.extend_apply' _ _ _ hn, Pi.zero_apply]
    infer_instance

Premises used: Pi.zero_apply, Countable.exists_injective_nat, rfl
-- 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 : Countable ι
m : ι → Measure α
inst_2 : ∀ (n : ι), SFinite (m n)
simp_rw : SFinite.{u_1} (α := α) (m0 := m0) (sum fun (p : ι × ℕ) ↦ sfiniteSeq (m p.1) p.2)
⊢ SFinite.{u_1} (α := α) (m0 := m0) (sum fun (i : ι) ↦ m i)

Tactic:
simp_rw [← sum_sfiniteSeq (m _), Measure.sum_sum]

Premises used: MeasureTheory.Measure.sum_sum, MeasureTheory.sum_sfiniteSeq
-- 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 : Countable ι
m : ι → Measure α
inst_2 : ∀ (n : ι), SFinite (m n)
⊢ SFinite.{u_1} (α := α) (m0 := m0) (sum fun (p : ι × ℕ) ↦ sfiniteSeq (m p.1) p.2)

Tactic:
apply sfinite_sum_of_countable

Premises used: MeasureTheory.sfinite_sum_of_countable
-- 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 : SFinite μ
inst_2 : SFinite ν
⊢ ∀ (b : Bool), SFinite (bif b then μ else ν)

Tactic:
simp [*]
-- 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 : SFinite μ
inst_2 : SFinite ν
⊢ ∀ (b : Bool), SFinite (bif b then μ else ν)

Tactic:
have : ∀ b : Bool, SFinite (cond b μ ν) := by simp [*]
-- 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 : SFinite μ
inst_2 : SFinite ν
this : ∀ (b : Bool), SFinite (bif b then μ else ν)
⊢ SFinite (μ + ν)

Tactic:
simpa using (inferInstance : SFinite (.sum (cond · μ ν)))

Premises used: inferInstance
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ ν : Measure α
s_1 t : Set α
a : α
inst_1 : SFinite μ
s : Set α
rw : μ.restrict s = (sum (sfiniteSeq μ)).restrict s
rw₁ rw₂ : μ.restrict s = μ.restrict s
⊢ μ.restrict s = sum fun (n : ℕ) ↦ (sfiniteSeq μ n).restrict s

Tactic:
rw [← restrict_sum_of_countable, sum_sfiniteSeq]

Premises used: MeasureTheory.Measure.restrict_sum_of_countable, MeasureTheory.sum_sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
rcases :
  ∀ (c : ℕ → ℝ≥0) (hc₀ : ∀ (i : ℕ), 0 < c i)
    (hc :
      LT.lt (α := ℝ≥0∞)
        (∑' (i : ℕ), HMul.hMul (α := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (↑(c i) : ℝ≥0∞)) ∞),
    ∃ (ν : Measure α), IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ
⊢ ∃ (ν : Measure α), IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ

Tactic:
rcases ENNReal.exists_pos_tsum_mul_lt_of_countable top_ne_zero (sfiniteSeq μ · univ)
    fun _ ↦ measure_ne_top _ _ with ⟨c, hc₀, hc⟩

Premises used: Set.univ, MeasureTheory.measure_ne_top, ENNReal.exists_pos_tsum_mul_lt_of_countable, ENNReal.top_ne_zero, DFunLike.coe, MeasureTheory.sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc :
  LT.lt (α := ℝ≥0∞)
    (∑' (i : ℕ), HMul.hMul (α := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (↑(c i) : ℝ≥0∞)) ∞
s : Set α
rw : Eq (α := ℝ≥0∞) (∑' (i : ℕ), (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s) 0
| Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← sum_sfiniteSeq μ, sum_apply_of_countable]

Premises used: MeasureTheory.Measure.sum_apply_of_countable, MeasureTheory.sum_sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc :
  LT.lt (α := ℝ≥0∞)
    (∑' (i : ℕ), HMul.hMul (α := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (↑(c i) : ℝ≥0∞)) ∞
s : Set α
conv_rhs :
  Eq (α := ℝ≥0∞) (((sum fun (n : ℕ) ↦ c n • sfiniteSeq μ n : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) (∑' (i : ℕ), (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s) 0
⊢ Eq (α := ℝ≥0∞) (((sum fun (n : ℕ) ↦ c n • sfiniteSeq μ n : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
conv_rhs => rw [← sum_sfiniteSeq μ, sum_apply_of_countable]

Premises used: MeasureTheory.Measure.sum_apply_of_countable, MeasureTheory.sum_sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc :
  LT.lt (α := ℝ≥0∞)
    (∑' (i : ℕ), HMul.hMul (α := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (↑(c i) : ℝ≥0∞)) ∞
s : Set α
⊢ Eq (α := ℝ≥0∞) (((sum fun (n : ℕ) ↦ c n • sfiniteSeq μ n : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) (∑' (i : ℕ), (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s) 0

Tactic:
simp [(hc₀ _).ne']

Premises used: LT.lt.ne'
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc :
  LT.lt (α := ℝ≥0∞)
    (∑' (i : ℕ), HMul.hMul (α := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (↑(c i) : ℝ≥0∞)) ∞
⊢ ∀ {s : Set α},
    Eq (α := ℝ≥0∞) (((sum fun (n : ℕ) ↦ c n • sfiniteSeq μ n : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have {s : Set α} : sum (fun n ↦ c n • sfiniteSeq μ n) s = 0 ↔ μ s = 0 := by
    conv_rhs => rw [← sum_sfiniteSeq μ, sum_apply_of_countable]
    simp [(hc₀ _).ne']
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc :
  LT.lt (α := ℝ≥0∞)
    (∑' (i : ℕ), HMul.hMul (α := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (↑(c i) : ℝ≥0∞)) ∞
this :
  ∀ {s : Set α},
    Eq (α := ℝ≥0∞) (((sum fun (n : ℕ) ↦ c n • sfiniteSeq μ n : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (ν : Measure α), IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ

Tactic:
⟨.sum fun n ↦ c n • sfiniteSeq μ n, ⟨?_⟩, fun _ ↦ this.1, fun _ ↦ this.2⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Iff.mp, MeasureTheory.IsFiniteMeasure.mk, HSMul.hSMul, MeasureTheory.Measure.sum, MeasureTheory.sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc :
  LT.lt (α := ℝ≥0∞)
    (∑' (i : ℕ), HMul.hMul (α := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (↑(c i) : ℝ≥0∞)) ∞
this :
  ∀ {s : Set α},
    Eq (α := ℝ≥0∞) (((sum fun (n : ℕ) ↦ c n • sfiniteSeq μ n : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
refine :
  LT.lt (α := ℝ≥0∞) (((sum fun (n : ℕ) ↦ c n • sfiniteSeq μ n : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (ν : Measure α), IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ

Tactic:
refine ⟨.sum fun n ↦ c n • sfiniteSeq μ n, ⟨?_⟩, fun _ ↦ this.1, fun _ ↦ this.2⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc :
  LT.lt (α := ℝ≥0∞)
    (∑' (i : ℕ), HMul.hMul (α := ℝ≥0∞) ((sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (↑(c i) : ℝ≥0∞)) ∞
this :
  ∀ {s : Set α},
    Eq (α := ℝ≥0∞) (((sum fun (n : ℕ) ↦ c n • sfiniteSeq μ n : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (((sum fun (n : ℕ) ↦ c n • sfiniteSeq μ n : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simpa [mul_comm] using hc

Premises used: mul_comm
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ SigmaFinite μ ↔ Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn univ)

Tactic:
⟨fun h => h.1, fun h => ⟨h⟩⟩

Premises used: Iff.intro, MeasureTheory.SigmaFinite.out', MeasureTheory.SigmaFinite.mk
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : SigmaFinite μ
⊢ Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn univ)

Tactic:
h.1

Premises used: MeasureTheory.SigmaFinite.out'
-- 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 α
h : SigmaFinite μ
n : ℕ
rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋯.some.set (C := univ) n) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (⋯.some.set (C := univ) n)) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [measure_toMeasurable]

Premises used: MeasureTheory.measure_toMeasurable
-- 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 α
h : SigmaFinite μ
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋯.some.set (C := univ) n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
h.out.some.finite n

Premises used: Nonempty.some, MeasureTheory.Measure.FiniteSpanningSetsIn.finite, MeasureTheory.SigmaFinite.out
-- 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 α
h : SigmaFinite μ
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋯.some.set (C := univ) n) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact h.out.some.finite n

Premises used: Nonempty.some, MeasureTheory.Measure.FiniteSpanningSetsIn.finite, MeasureTheory.SigmaFinite.out
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
⊢ Monotone (spanningSets μ)

Tactic:
monotone_accumulate

Premises used: Set.monotone_accumulate, MeasureTheory.spanningSets
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
m n : ℕ
hmn : m ≤ n
⊢ spanningSets μ m ⊆ spanningSets μ n

Tactic:
monotone_spanningSets _ hmn

Premises used: MeasureTheory.monotone_spanningSets
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
i : ℕ
⊢ MeasurableSet (spanningSets μ i)

Tactic:
MeasurableSet.iUnion fun j => MeasurableSet.iUnion fun _ => μ.toFiniteSpanningSetsIn.set_mem j

Premises used: Set.accumulate, MeasureTheory.Measure.toFiniteSpanningSetsIn, MeasurableSet.iUnion, MeasureTheory.spanningSets, MeasureTheory.Measure.FiniteSpanningSetsIn.set_mem
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
i : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (spanningSets μ i) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_biUnion_lt_top (finite_le_nat i) fun j _ => μ.toFiniteSpanningSetsIn.finite j

Premises used: MeasureTheory.measure_biUnion_lt_top, Set.Mem, MeasureTheory.Measure.FiniteSpanningSetsIn.finite, Set.accumulate, MeasureTheory.Measure.toFiniteSpanningSetsIn, MeasureTheory.spanningSets, Set.finite_le_nat
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
simp_rw :
  Eq.{u_1 + 1} (α := Set α)
    (⋃ (i : ℕ), accumulate (μ.toFiniteSpanningSetsIn.set (C := {s : Set α | MeasurableSet s})) i) univ
simp_rw₁ :
  Eq.{u_1 + 1} (α := Set α) (⋃ (x : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set α | MeasurableSet s}) x) univ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), spanningSets μ i) univ

Tactic:
simp_rw [spanningSets, iUnion_accumulate, μ.toFiniteSpanningSetsIn.spanning]

Premises used: Set.iUnion_accumulate, MeasureTheory.Measure.FiniteSpanningSetsIn.spanning, MeasureTheory.Measure.toFiniteSpanningSetsIn, MeasureTheory.spanningSets
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
⊢ IsCountablySpanning (range (spanningSets μ))

Tactic:
⟨spanningSets μ, mem_range_self, iUnion_spanningSets μ⟩

Premises used: Set.mem_range_self, MeasureTheory.iUnion_spanningSets, And.intro, Exists.intro, IsCountablySpanning, MeasureTheory.spanningSets
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
⊢ Measurable (spanningSetsIndex μ)

Tactic:
measurable_find _ <| measurableSet_spanningSets μ

Premises used: MeasureTheory.measurableSet_spanningSets, MeasureTheory.spanningSetsIndex, measurable_find
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
n : ℕ
⊢ spanningSetsIndex μ ⁻¹' {n} = disjointed (spanningSets μ) n

Tactic:
preimage_find_eq_disjointed _ _ _

Premises used: MeasureTheory.spanningSetsIndex, preimage_find_eq_disjointed
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
x : α
n : ℕ
⊢ x ∈ spanningSetsIndex μ ⁻¹' {n} ↔ x ∈ disjointed (spanningSets μ) n

Tactic:
Set.ext_iff.1 (preimage_spanningSetsIndex_singleton μ n) x

Premises used: MeasureTheory.preimage_spanningSetsIndex_singleton, Iff.mp, Set.ext_iff
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
x : α
n : ℕ
⊢ spanningSetsIndex μ x = n ↔ x ∈ disjointed (spanningSets μ) n

Tactic:
convert! Set.ext_iff.1 (preimage_spanningSetsIndex_singleton μ n) x

Premises used: MeasureTheory.preimage_spanningSetsIndex_singleton, Iff.mp, Set.ext_iff
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
x : α
⊢ x ∈ disjointed (spanningSets μ) (spanningSetsIndex μ x)

Tactic:
(spanningSetsIndex_eq_iff μ).1 rfl

Premises used: MeasureTheory.spanningSetsIndex_eq_iff, Iff.mp, rfl
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
x : α
⊢ x ∈ spanningSets μ (spanningSetsIndex μ x)

Tactic:
disjointed_subset _ _ (mem_disjointed_spanningSetsIndex μ x)

Premises used: MeasureTheory.mem_disjointed_spanningSetsIndex, disjointed_subset
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
x : α
n : ℕ
hn : spanningSetsIndex μ x ≤ n
⊢ x ∈ spanningSets μ n

Tactic:
monotone_spanningSets μ hn (mem_spanningSetsIndex μ x)

Premises used: MeasureTheory.monotone_spanningSets, MeasureTheory.mem_spanningSetsIndex
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
x : α
⊢ ∀ᶠ (n : ℕ) in atTop, x ∈ spanningSets μ n

Tactic:
eventually_atTop.2 ⟨spanningSetsIndex μ x, fun _ => mem_spanningSets_of_index_le μ x⟩

Premises used: Iff.mpr, MeasureTheory.spanningSetsIndex, Exists.intro, MeasureTheory.mem_spanningSets_of_index_le, Filter.eventually_atTop
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
a : α
inst : SigmaFinite μ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_lt_top_mono (singleton_subset_iff.2 <| mem_spanningSetsIndex ..)
    (measure_spanningSets_lt_top _ _)

Premises used: Iff.mpr, Set.singleton_subset_iff, MeasureTheory.measure_spanningSets_lt_top, MeasureTheory.measure_lt_top_mono, MeasureTheory.mem_spanningSetsIndex
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite ν
rw : μ.restrict (⋃ (i : ℕ), disjointed (spanningSets ν) i) = μ
rw₁ : μ.restrict (⋃ (i : ℕ), spanningSets ν i) = μ
rw₂ : μ.restrict univ = μ
rw₃ rw₄ : μ = μ
⊢ (sum fun (n : ℕ) ↦ μ.restrict (disjointed (spanningSets ν) n)) = μ

Tactic:
rw [← restrict_iUnion (disjoint_disjointed _)
      (MeasurableSet.disjointed (measurableSet_spanningSets _)),
    iUnion_disjointed, iUnion_spanningSets, restrict_univ]

Premises used: iUnion_disjointed, MeasureTheory.Measure.restrict_iUnion, MeasureTheory.measurableSet_spanningSets, MeasureTheory.iUnion_spanningSets, MeasurableSet.disjointed, disjoint_disjointed, MeasureTheory.Measure.restrict_univ
-- 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 μ
⊢ ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (disjointed (spanningSets μ) n) : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
have : ∀ n, Fact (μ (disjointed (spanningSets μ) n) < ∞) :=
    fun n ↦ ⟨(measure_mono (disjointed_subset _ _)).trans_lt (measure_spanningSets_lt_top μ n)⟩
-- 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 μ
this : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (disjointed (spanningSets μ) n) : ℝ≥0∞) (∞ : ℝ≥0∞))
n : ℕ
⊢ IsFiniteMeasure.{u_1} (α := α) (m0 := m0) ((fun (n : ℕ) ↦ μ.restrict (disjointed (spanningSets μ) n)) n)

Tactic:
infer_instance
-- 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 μ
this : ∀ (n : ℕ), Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (disjointed (spanningSets μ) n) : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ SFinite μ

Tactic:
exact ⟨⟨fun n ↦ μ.restrict (disjointed (spanningSets μ) n), fun n ↦ by infer_instance,
    (sum_restrict_disjointed_spanningSets μ μ).symm⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
rw : s = s ∩ ⋃ (i : ℕ), spanningSets μ i
rw₁ : s = s ∩ univ
rw₂ rw₃ : s = s
⊢ s = ⋃ (n : ℕ), s ∩ spanningSets μ n

Tactic:
rw [← inter_iUnion, iUnion_spanningSets, inter_univ]

Premises used: Set.inter_univ, MeasureTheory.iUnion_spanningSets, Set.inter_iUnion