awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ (D : Set (Set α)),
    D.Countable ∧
      D ⊆ (supClosure : (a : Set (Set α)) → Set (Set α)) C ∧
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have rcases : ∀ (D : Set (Set α)) (D_count : D.Countable) (DC : D ⊆ C)
  (hD : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∃ (D : Set (Set α)),
    D.Countable ∧
      D ⊆ (supClosure : (a : Set (Set α)) → Set (Set α)) C ∧
        Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rcases h'C with ⟨D, D_count, DC, hD⟩
Cleared hypotheses: h'C
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
⊢ mα = generateFrom ((supClosure : (a : Set (Set α)) → Set (Set α)) C)
have rw : generateFrom C = generateFrom ((supClosure : (a : Set (Set α)) → Set (Set α)) C)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
⊢ generateFrom C = generateFrom ((supClosure : (a : Set (Set α)) → Set (Set α)) C)
have apply : generateFrom ((supClosure : (a : Set (Set α)) → Set (Set α)) C) ≤ generateFrom C
Tactic: apply le_antisymm (generateFrom_mono subset_supClosure)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
⊢ generateFrom ((supClosure : (a : Set (Set α)) → Set (Set α)) C) ≤ generateFrom C
have apply : ∀ (t : Set α)
  (ht : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) t),
  MeasurableSet t
Tactic: apply generateFrom_le (fun t ht ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
⊢ Dense (X := MeasuredSets μ) (SetLike.coe ⁻¹' C)
have rw : ∀ (x : MeasuredSets μ), ∀ r > 0, (Metric.eball x r ∩ SetLike.coe ⁻¹' C).Nonempty
Tactic: rw [EMetric.dense_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
⊢ (Metric.eball s ε ∩ SetLike.coe ⁻¹' C).Nonempty
have rcases : ∀ (t : Set α) (tC : t ∈ C) (ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε),
  (Metric.eball s ε ∩ SetLike.coe ⁻¹' C).Nonempty
Tactic: rcases exists_measure_symmDiff_lt_of_generateFrom_isSetRing hC h'C h s.2 εpos with ⟨t, tC, ht⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε
⊢ MeasurableSet t
have rw : MeasurableSet t
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε
⊢ (Metric.eball s ε ∩ SetLike.coe ⁻¹' C).Nonempty
have t_meas : MeasurableSet t
Tactic: have t_meas : MeasurableSet t := by rw [h]; exact measurableSet_generateFrom tC
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε
t_meas : MeasurableSet t
⊢ (Metric.eball s ε ∩ SetLike.coe ⁻¹' C).Nonempty
have refine : Subtype.mk (p := fun (s : Set α) ↦ MeasurableSet s) t t_meas ∈ Metric.eball s ε
Tactic: refine ⟨⟨t, t_meas⟩, ?_, tC⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
⊢ Dense (X := MeasuredSets μ) (SetLike.coe ⁻¹' (supClosure : (a : Set (Set α)) → Set (Set α)) C)
have rw : ∀ (x : MeasuredSets μ),
  ∀ r > 0, (Metric.eball x r ∩ SetLike.coe ⁻¹' (supClosure : (a : Set (Set α)) → Set (Set α)) C).Nonempty
Tactic: rw [EMetric.dense_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
⊢ (Metric.eball s ε ∩ SetLike.coe ⁻¹' (supClosure : (a : Set (Set α)) → Set (Set α)) C).Nonempty
have rcases : ∀ (t : Set α)
  (tC : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) t)
  (ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε),
  (Metric.eball s ε ∩ SetLike.coe ⁻¹' (supClosure : (a : Set (Set α)) → Set (Set α)) C).Nonempty
Tactic: rcases exists_measure_symmDiff_lt_of_generateFrom_isSetSemiring hC h'C h s.2 εpos
    with ⟨t, tC, ht⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
t : Set α
tC : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) t
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε
⊢ (Metric.eball s ε ∩ SetLike.coe ⁻¹' (supClosure : (a : Set (Set α)) → Set (Set α)) C).Nonempty
have refine : MeasurableSet t
Tactic: refine ⟨⟨t, ?_⟩, by simpa [MeasuredSets.edist_def] using ht, tC⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetSemiring C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : MeasuredSets μ
ε : ℝ≥0∞
εpos : ε > 0
t : Set α
tC : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) t
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ (↑s : Set α)) < ε
⊢ MeasurableSet t
have rw : MeasurableSet t
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ht : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
hst : univ ⊆ s ∪ t
⊢ μ ⟂ₘ ν
have right : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (toMeasurable μ s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: use toMeasurable μ s, measurableSet_toMeasurable _ _, (measure_toMeasurable _).trans hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ht : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
hst : univ ⊆ s ∪ t
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (toMeasurable μ s)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have right : ∀ (x : α) (hx : x ∈ (toMeasurable μ s)ᶜ) (hxs : x ∈ s), x ∈ toMeasurable μ s
Tactic: refine measure_mono_null (fun x hx => (hst trivial).resolve_left fun hxs => hx ?_) ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : μ = 0
⊢ μ ⟂ₘ μ
have rw : @MutuallySingular.{u_1} α m0 0 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ μ ⟂ₘ μ ↔ μ = 0
have refine : μ ⟂ₘ μ → μ = 0
Tactic: refine ⟨?_, fun h ↦ by (rw [h]; exact zero_left)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμs_compl : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ = 0
have rwa : ∀ (this : μ = 0), μ = 0
Tactic: rwa [measure_univ_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμs_compl : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ = 0
have suffices : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: suffices μ Set.univ = 0 by rwa [measure_univ_eq_zero] at this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμs_compl : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← Set.union_compl_self s, measure_union disjoint_compl_right hs.compl, hμs, hμs_compl,
    add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμs_compl : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) = 0
Tactic: rw [← Set.union_compl_self s, measure_union disjoint_compl_right hs.compl, hμs, hμs_compl,
    add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμs_compl : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) = 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₂ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) = 0
Tactic: rw [← Set.union_compl_self s, measure_union disjoint_compl_right hs.compl, hμs, hμs_compl,
    add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμs_compl : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) = 0
rw₂ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) = 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₃ : HAdd.hAdd (α := ℝ≥0∞) 0 0 = 0
Tactic: rw [← Set.union_compl_self s, measure_union disjoint_compl_right hs.compl, hμs, hμs_compl,
    add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hμs_compl : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ sᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) = 0
rw₂ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) = 0
rw₃ : HAdd.hAdd (α := ℝ≥0∞) 0 0 = 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₄ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [← Set.union_compl_self s, measure_union disjoint_compl_right hs.compl, hμs, hμs_compl,
    add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst : Countable ι
μ : ι → Measure α
⊢ sum μ ⟂ₘ ν ↔ ∀ (i : ι), μ i ⟂ₘ ν
have refine : ∀ (H : ∀ (i : ι), μ i ⟂ₘ ν), sum μ ⟂ₘ ν
Tactic: refine ⟨fun h i => h.mono (le_sum _ _) le_rfl, fun H => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst : Countable ι
μ : ι → Measure α
H : ∀ (i : ι), μ i ⟂ₘ ν
⊢ sum μ ⟂ₘ ν
have choose : ∀ (s : (i : ι) → Set α) (hsm : ∀ (i : ι), MeasurableSet (s i))
  (hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞))
  (hsν : ∀ (i : ι), Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)), sum μ ⟂ₘ ν
Tactic: choose s hsm hsμ hsν using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst : Countable ι
μ : ι → Measure α
s : (i : ι) → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsν : ∀ (i : ι), Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ sum μ ⟂ₘ ν
have refine_1 : Eq (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨⋂ i, s i, MeasurableSet.iInter hsm, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst : Countable ι
μ : ι → Measure α
s : (i : ι) → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsν : ∀ (i : ι), Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
refine_1 : Eq (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ sum μ ⟂ₘ ν
have refine_2 : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨⋂ i, s i, MeasurableSet.iInter hsm, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst : Countable ι
μ : ι → Measure α
s : (i : ι) → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsν : ∀ (i : ι), Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((sum μ : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i) : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_1 : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (⋂ (b : ι), s b) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [sum_apply _ (MeasurableSet.iInter hsm), ENNReal.tsum_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
ν : Measure α
ι : Type u_2
inst : Countable ι
μ : ι → Measure α
s : (i : ι) → Set α
hsm : ∀ (i : ι), MeasurableSet (s i)
hsμ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ i : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞) (0 : ℝ≥0∞)
hsν : ∀ (i : ι), Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋂ (i : ι), s i)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
have refine_2 : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), (s i)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rwa [compl_iInter, measure_iUnion_null_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ ν : Measure α
⊢ μ₁ + μ₂ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
have rw : (sum fun (b : Bool) ↦ bif b then μ₁ else μ₂) ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
Tactic: rw [← sum_cond, sum_left, Bool.forall_bool, cond, cond, and_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ ν : Measure α
rw : (sum fun (b : Bool) ↦ bif b then μ₁ else μ₂) ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
⊢ μ₁ + μ₂ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
have rw₁ : (∀ (i : Bool), (bif i then μ₁ else μ₂) ⟂ₘ ν) ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
Tactic: rw [← sum_cond, sum_left, Bool.forall_bool, cond, cond, and_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ ν : Measure α
rw : (sum fun (b : Bool) ↦ bif b then μ₁ else μ₂) ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
rw₁ : (∀ (i : Bool), (bif i then μ₁ else μ₂) ⟂ₘ ν) ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
⊢ μ₁ + μ₂ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
have rw₂ : (bif false then μ₁ else μ₂) ⟂ₘ ν ∧ (bif true then μ₁ else μ₂) ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
Tactic: rw [← sum_cond, sum_left, Bool.forall_bool, cond, cond, and_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ ν : Measure α
rw : (sum fun (b : Bool) ↦ bif b then μ₁ else μ₂) ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
rw₁ : (∀ (i : Bool), (bif i then μ₁ else μ₂) ⟂ₘ ν) ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
rw₂ : (bif false then μ₁ else μ₂) ⟂ₘ ν ∧ (bif true then μ₁ else μ₂) ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
⊢ μ₁ + μ₂ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
have rw₃ : (bif false then μ₁ else μ₂) ⟂ₘ ν ∧ μ₁ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
Tactic: rw [← sum_cond, sum_left, Bool.forall_bool, cond, cond, and_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ ν : Measure α
rw : (sum fun (b : Bool) ↦ bif b then μ₁ else μ₂) ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
rw₁ : (∀ (i : Bool), (bif i then μ₁ else μ₂) ⟂ₘ ν) ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
rw₂ : (bif false then μ₁ else μ₂) ⟂ₘ ν ∧ (bif true then μ₁ else μ₂) ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
rw₃ : (bif false then μ₁ else μ₂) ⟂ₘ ν ∧ μ₁ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
⊢ μ₁ + μ₂ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
have rw₄ : μ₂ ⟂ₘ ν ∧ μ₁ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
Tactic: rw [← sum_cond, sum_left, Bool.forall_bool, cond, cond, and_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ ν : Measure α
rw : (sum fun (b : Bool) ↦ bif b then μ₁ else μ₂) ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
rw₁ : (∀ (i : Bool), (bif i then μ₁ else μ₂) ⟂ₘ ν) ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
rw₂ : (bif false then μ₁ else μ₂) ⟂ₘ ν ∧ (bif true then μ₁ else μ₂) ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
rw₃ : (bif false then μ₁ else μ₂) ⟂ₘ ν ∧ μ₁ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
rw₄ : μ₂ ⟂ₘ ν ∧ μ₁ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
⊢ μ₁ + μ₂ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
have rw₅ : μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν ↔ μ₁ ⟂ₘ ν ∧ μ₂ ⟂ₘ ν
Tactic: rw [← sum_cond, sum_left, Bool.forall_bool, cond, cond, and_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
⊢ μ.restrict s ⟂ₘ ν
have refine : Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) h.nullSet : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨h.nullSet, h.measurableSet_nullSet, ?_, h.measure_compl_nullSet⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) h.nullSet : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (h.nullSet ∩ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply h.measurableSet_nullSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h_ac : μ ≪ ν
h_ms : μ ⟂ₘ ν
⊢ μ = 0
have rw : μ ⟂ₘ μ
Tactic: rw [← Measure.MutuallySingular.self_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
⊢ μ ≪ ν₁
have refine : ∀ (s : Set α) (hs : MeasurableSet s) (hs_zero : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine AbsolutelyContinuous.mk fun s hs hs_zero ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
s : Set α
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := h_ms.nullSet
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have ht : MeasurableSet t
Tactic: have ht : MeasurableSet t := h_ms.measurableSet_nullSet
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
s : Set α
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := h_ms.nullSet
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have htμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have htμ : μ t = 0 := h_ms.measure_nullSet
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MutuallySingular (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν₁ ν₂ : Measure α
h : μ ≪ ν₁ + ν₂
h_ms : μ ⟂ₘ ν₂
s : Set α
hs : MeasurableSet s
hs_zero : Eq (α := ℝ≥0∞) ((ν₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
t : Set α := h_ms.nullSet
ht : MeasurableSet t
htμ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have htν₂ : Eq (α := ℝ≥0∞) ((ν₂ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have htν₂ : ν₂ tᶜ = 0 := h_ms.measure_compl_nullSet