awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
h : NeZero μ
inr :
  ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)),
    IsZeroOrProbabilityMeasure (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)
⊢ IsZeroOrProbabilityMeasure (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)
have inr₁ : ∀ (h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)),
  IsZeroOrProbabilityMeasure (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)
Tactic: rcases eq_top_or_lt_top (μ univ) with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
h_1 : NeZero μ
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsZeroOrProbabilityMeasure (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)
have inr : IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := m0) 0
Tactic: simp [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
h_1 : NeZero μ
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsZeroOrProbabilityMeasure (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)
have this : IsFiniteMeasure μ
Tactic: have : IsFiniteMeasure μ := ⟨h⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsZeroOrProbabilityMeasure μ
⊢ μ = 0 ∨ IsProbabilityMeasure μ
have inl : ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)), μ = 0 ∨ IsProbabilityMeasure μ
Tactic: rcases IsZeroOrProbabilityMeasure.measure_univ (μ := μ) with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsZeroOrProbabilityMeasure μ
inl : ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)), μ = 0 ∨ IsProbabilityMeasure μ
⊢ μ = 0 ∨ IsProbabilityMeasure μ
have inr : ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)), μ = 0 ∨ IsProbabilityMeasure μ
Tactic: rcases IsZeroOrProbabilityMeasure.measure_univ (μ := μ) with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
inst_1 : IsZeroOrProbabilityMeasure μ
p : α → Prop
f_1 : β → α
f : α → β
⊢ IsZeroOrProbabilityMeasure (m0 := inst) (Measure.map f μ)
have pos : ∀ (hf : AEMeasurable f μ), IsZeroOrProbabilityMeasure (m0 := inst) (Measure.map f μ)
Tactic: by_cases hf : AEMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
inst_1 : IsZeroOrProbabilityMeasure μ
p : α → Prop
f_1 : β → α
f : α → β
pos : ∀ (hf : AEMeasurable f μ), IsZeroOrProbabilityMeasure (m0 := inst) (Measure.map f μ)
⊢ IsZeroOrProbabilityMeasure (m0 := inst) (Measure.map f μ)
have neg : ∀ (hf : ¬AEMeasurable f μ), IsZeroOrProbabilityMeasure (m0 := inst) (Measure.map f μ)
Tactic: by_cases hf : AEMeasurable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < (μ : (a : Set α) → ℝ≥0∞) s
s_mble : MeasurableSet s
⊢ (μ : (a : Set α) → ℝ≥0∞) sᶜ < 1 - p
have inl : ∀ [IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := m0) 0] (hμs : p < ((0 : Measure α) : (a : Set α) → ℝ≥0∞) s),
  ((0 : Measure α) : (a : Set α) → ℝ≥0∞) sᶜ < 1 - p
Tactic: rcases eq_zero_or_isProbabilityMeasure μ with rfl | h
Cleared hypotheses: μ, inst, hμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < (μ : (a : Set α) → ℝ≥0∞) s
s_mble : MeasurableSet s
inl :
  ∀ [IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := m0) 0] (hμs : p < ((0 : Measure α) : (a : Set α) → ℝ≥0∞) s),
    ((0 : Measure α) : (a : Set α) → ℝ≥0∞) sᶜ < 1 - p
⊢ (μ : (a : Set α) → ℝ≥0∞) sᶜ < 1 - p
have inr : ∀ (h : IsProbabilityMeasure μ), (μ : (a : Set α) → ℝ≥0∞) sᶜ < 1 - p
Tactic: rcases eq_zero_or_isProbabilityMeasure μ with rfl | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < (μ : (a : Set α) → ℝ≥0∞) s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ (μ : (a : Set α) → ℝ≥0∞) sᶜ < 1 - p
have inr : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) < 1 - p
Tactic: rw [prob_compl_eq_one_sub s_mble]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < (μ : (a : Set α) → ℝ≥0∞) s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) < 1 - p
have inr : 1 - (1 - p) < (μ : (a : Set α) → ℝ≥0∞) s
Tactic: apply ENNReal.sub_lt_of_sub_lt prob_le_one (Or.inl one_ne_top)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < (μ : (a : Set α) → ℝ≥0∞) s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ 1 - (1 - p) < (μ : (a : Set α) → ℝ≥0∞) s
have h₁ : 1 - (1 - p) = p
Tactic: convert! hμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p ≤ (μ : (a : Set α) → ℝ≥0∞) s
s_mble : MeasurableSet s
⊢ (μ : (a : Set α) → ℝ≥0∞) sᶜ ≤ 1 - p
have inl : ∀ [IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := m0) 0] (hμs : p ≤ ((0 : Measure α) : (a : Set α) → ℝ≥0∞) s),
  ((0 : Measure α) : (a : Set α) → ℝ≥0∞) sᶜ ≤ 1 - p
Tactic: rcases eq_zero_or_isProbabilityMeasure μ with rfl | h
Cleared hypotheses: μ, inst, hμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p ≤ (μ : (a : Set α) → ℝ≥0∞) s
s_mble : MeasurableSet s
inl :
  ∀ [IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := m0) 0] (hμs : p ≤ ((0 : Measure α) : (a : Set α) → ℝ≥0∞) s),
    ((0 : Measure α) : (a : Set α) → ℝ≥0∞) sᶜ ≤ 1 - p
⊢ (μ : (a : Set α) → ℝ≥0∞) sᶜ ≤ 1 - p
have inr : ∀ (h : IsProbabilityMeasure μ), (μ : (a : Set α) → ℝ≥0∞) sᶜ ≤ 1 - p
Tactic: rcases eq_zero_or_isProbabilityMeasure μ with rfl | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsZeroOrProbabilityMeasure μ
⊢ HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = μ
have inl : ∀ (h : μ = 0), HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = μ
Tactic: rcases eq_zero_or_isProbabilityMeasure μ with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Probability (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsZeroOrProbabilityMeasure μ
inl : ∀ (h : μ = 0), HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = μ
⊢ HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = μ
have inr : ∀ (h : IsProbabilityMeasure μ), HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = μ
Tactic: rcases eq_zero_or_isProbabilityMeasure μ with h | h
-- 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 β
μ ν : Measure α
s t : Set α
a : α
⊢ Eq.{u_1 + 1} (α := Measure α) 0 (sum fun (x : ℕ) ↦ 0)
have rw : Eq.{u_1 + 1} (α := Measure α) 0 0
Tactic: rw [Measure.sum_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst : Countable ι
m : ι → Measure α
inst_1 : ∀ (n : ι), IsFiniteMeasure (m n)
⊢ SFinite (sum m)
have obtain : ∀ (f : ι → ℕ) (hf : Injective f), SFinite (sum m)
Tactic: obtain ⟨f, hf⟩ : ∃ f : ι → ℕ, Function.Injective f := Countable.exists_injective_nat ι
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
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)
have refine : ∀ (n : ℕ), IsFiniteMeasure (Function.extend f m 0 n)
Tactic: refine ⟨_, fun n ↦ ?_, (sum_extend_zero hf m).symm⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst : Countable ι
m : ι → Measure α
inst_1 : ∀ (n : ι), IsFiniteMeasure (m n)
f : ι → ℕ
hf : Injective f
n : ℕ
⊢ IsFiniteMeasure (Function.extend f m 0 n)
have inl : ∀ (i : ι), IsFiniteMeasure (Function.extend f m 0 (f i))
Tactic: rcases em (n ∈ range f) with ⟨i, rfl⟩ | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
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))
⊢ IsFiniteMeasure (Function.extend f m 0 n)
have inr : ∀ (hn : n ∉ range f), IsFiniteMeasure (Function.extend f m 0 n)
Tactic: rcases em (n ∈ range f) with ⟨i, rfl⟩ | hn
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
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 (Function.extend f m 0 (f i))
have inl : IsFiniteMeasure (m i)
Tactic: rw [hf.extend_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
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 (Function.extend f m 0 n)
have inr : IsFiniteMeasure.{u_1} (α := α) (m0 := m0) 0
Tactic: rw [Function.extend_apply' _ _ _ hn, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
ι : Type u_3
m0 : MeasurableSpace α
inst : Countable ι
m : ι → Measure α
inst_1 : ∀ (n : ι), IsFiniteMeasure (m n)
⊢ SFinite (sum m)
have obtain : ∀ (f : ι → ℕ) (hf : Injective f), 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
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)
have obtain₁ : ∀ (f : ι → ℕ) (hf : Injective f) (n : ℕ), IsFiniteMeasure (Function.extend f m 0 n)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
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)
⊢ SFinite (sum m)
have inl : ∀ (f : ι → ℕ) (hf : Injective f) (i : ι), IsFiniteMeasure (Function.extend f m 0 (f i))
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
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))
⊢ SFinite (sum m)
have inr : ∀ (f : ι → ℕ) (hf : Injective f) (n : ℕ) (hn : n ∉ range f), IsFiniteMeasure (Function.extend f m 0 n)
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
-- 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 β
μ ν : Measure α
s t : Set α
a : α
inst_1 : Countable ι
m : ι → Measure α
inst_2 : ∀ (n : ι), SFinite (m n)
⊢ SFinite.{u_1} (α := α) (m0 := m0) (sum fun (i : ι) ↦ m i)
have simp_rw : SFinite.{u_1} (α := α) (m0 := m0) (sum fun (p : ι × ℕ) ↦ sfiniteSeq (m p.1) p.2)
Tactic: simp_rw [← sum_sfiniteSeq (m _), Measure.sum_sum]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
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 ν
⊢ SFinite (μ + ν)
have this : ∀ (b : Bool), SFinite (bif b then μ else ν)
Tactic: have : ∀ b : Bool, SFinite (cond b μ ν) := by simp [*]
-- 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 β
μ ν : Measure α
s_1 t : Set α
a : α
inst_1 : SFinite μ
s : Set α
⊢ μ.restrict s = sum fun (n : ℕ) ↦ (sfiniteSeq μ n).restrict s
have rw : μ.restrict s = (sum (sfiniteSeq μ)).restrict s
Tactic: rw [← restrict_sum_of_countable, sum_sfiniteSeq]
-- 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 β
μ ν : Measure α
s_1 t : Set α
a : α
inst_1 : SFinite μ
s : Set α
rw : μ.restrict s = (sum (sfiniteSeq μ)).restrict s
⊢ μ.restrict s = sum fun (n : ℕ) ↦ (sfiniteSeq μ n).restrict s
have rw₁ : μ.restrict s = μ.restrict s
Tactic: rw [← restrict_sum_of_countable, sum_sfiniteSeq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
⊢ ∃ (ν : Measure α), IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ
have 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 ν ∧ μ ≪ ν ∧ ν ≪ μ
Tactic: rcases ENNReal.exists_pos_tsum_mul_lt_of_countable top_ne_zero (sfiniteSeq μ · univ)
    fun _ ↦ measure_ne_top _ _ with ⟨c, hc₀, hc⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
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∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (∑' (i : ℕ), (sfiniteSeq μ i : (a : Set α) → ℝ≥0∞) s) 0
Tactic: rw [← sum_sfiniteSeq μ, sum_apply_of_countable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
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∞)
have 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
Tactic: conv_rhs => rw [← sum_sfiniteSeq μ, sum_apply_of_countable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
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∞)) ∞
⊢ ∃ (ν : Measure α), IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ
have 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∞)
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']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
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 ν ∧ μ ≪ ν ∧ ν ≪ μ
have refine : LT.lt (α := ℝ≥0∞) (((sum fun (n : ℕ) ↦ c n • sfiniteSeq μ n : Measure α) : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine ⟨.sum fun n ↦ c n • sfiniteSeq μ n, ⟨?_⟩, fun _ ↦ this.1, fun _ ↦ this.2⟩
-- 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 t : Set α
a : α
μ : Measure α
h : SigmaFinite μ
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (⋯.some.set (C := univ) n)) : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (sorry.some.set (C := univ) n) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [measure_toMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), spanningSets μ i) univ
have simp_rw : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), accumulate (μ.toFiniteSpanningSetsIn.set (C := {s : Set α | MeasurableSet s})) i)
  univ
Tactic: simp_rw [spanningSets, iUnion_accumulate, μ.toFiniteSpanningSetsIn.spanning]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
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
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), spanningSets μ i) univ
have simp_rw₁ : Eq.{u_1 + 1} (α := Set α) (⋃ (x : ℕ), μ.toFiniteSpanningSetsIn.set (C := {s : Set α | MeasurableSet s}) x) univ
Tactic: simp_rw [spanningSets, iUnion_accumulate, μ.toFiniteSpanningSetsIn.spanning]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite ν
⊢ (sum fun (n : ℕ) ↦ μ.restrict (disjointed (spanningSets ν) n)) = μ
have rw : μ.restrict (⋃ (i : ℕ), disjointed (spanningSets ν) i) = μ
Tactic: rw [← restrict_iUnion (disjoint_disjointed _)
      (MeasurableSet.disjointed (measurableSet_spanningSets _)),
    iUnion_disjointed, iUnion_spanningSets, restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite ν
rw : μ.restrict (⋃ (i : ℕ), disjointed (spanningSets ν) i) = μ
⊢ (sum fun (n : ℕ) ↦ μ.restrict (disjointed (spanningSets ν) n)) = μ
have rw₁ : μ.restrict (⋃ (i : ℕ), spanningSets ν i) = μ
Tactic: rw [← restrict_iUnion (disjoint_disjointed _)
      (MeasurableSet.disjointed (measurableSet_spanningSets _)),
    iUnion_disjointed, iUnion_spanningSets, restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite ν
rw : μ.restrict (⋃ (i : ℕ), disjointed (spanningSets ν) i) = μ
rw₁ : μ.restrict (⋃ (i : ℕ), spanningSets ν i) = μ
⊢ (sum fun (n : ℕ) ↦ μ.restrict (disjointed (spanningSets ν) n)) = μ
have rw₂ : μ.restrict univ = μ
Tactic: rw [← restrict_iUnion (disjoint_disjointed _)
      (MeasurableSet.disjointed (measurableSet_spanningSets _)),
    iUnion_disjointed, iUnion_spanningSets, restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite ν
rw : μ.restrict (⋃ (i : ℕ), disjointed (spanningSets ν) i) = μ
rw₁ : μ.restrict (⋃ (i : ℕ), spanningSets ν i) = μ
rw₂ : μ.restrict univ = μ
⊢ (sum fun (n : ℕ) ↦ μ.restrict (disjointed (spanningSets ν) n)) = μ
have rw₃ : μ = μ
Tactic: rw [← restrict_iUnion (disjoint_disjointed _)
      (MeasurableSet.disjointed (measurableSet_spanningSets _)),
    iUnion_disjointed, iUnion_spanningSets, restrict_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ ν : Measure α
s t : Set α
a : α
inst_1 : SigmaFinite μ
⊢ SFinite μ
have this : ∀ (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)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
⊢ s = ⋃ (n : ℕ), s ∩ spanningSets μ n
have rw : s = s ∩ ⋃ (i : ℕ), spanningSets μ i
Tactic: rw [← inter_iUnion, iUnion_spanningSets, inter_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.SFinite (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : SigmaFinite μ
s : Set α
rw : s = s ∩ ⋃ (i : ℕ), spanningSets μ i
⊢ s = ⋃ (n : ℕ), s ∩ spanningSets μ n
have rw₁ : s = s ∩ univ
Tactic: rw [← inter_iUnion, iUnion_spanningSets, inter_univ]