awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνinter : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (S ∩ T)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ
A : Set α
hA : MeasurableSet A
hsinter : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((s.restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞)
Tactic: rw [restrict_apply hA, ← diff_eq, AEDisjoint.measure_diff_left hsinter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνinter : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (S ∩ T)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ
A : Set α
hA : MeasurableSet A
hsinter : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
rw : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((s.restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A \ (S ∩ T)) : ℝ≥0∞)
Tactic: rw [restrict_apply hA, ← diff_eq, AEDisjoint.measure_diff_left hsinter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνinter : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (S ∩ T)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ
A : Set α
hA : MeasurableSet A
hsinter : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
rw : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞)
rw₁ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A \ (S ∩ T)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((s.restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: rw [restrict_apply hA, ← diff_eq, AEDisjoint.measure_diff_left hsinter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνinter : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (S ∩ T)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ
⊢ s = μ.singularPart ν
have heq' : ∀ (A : Set α),
  MeasurableSet A →
    Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((s.restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: have heq' : ∀ A : Set α, MeasurableSet A → s A = s.restrict (S ∩ T)ᶜ A := by
    intro A hA
    have hsinter : s (A ∩ (S ∩ T)) = 0 := by
      rw [← nonpos_iff_eq_zero]
      exact hS₂ ▸ measure_mono (inter_subset_right.trans inter_subset_left)
    rw [restrict_apply hA, ← diff_eq, AEDisjoint.measure_diff_left hsinter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνinter : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (S ∩ T)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ
heq' :
  ∀ (A : Set α),
    MeasurableSet A →
      Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((s.restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
⊢ s = μ.singularPart ν
have h : ∀ (A : Set α) (hA : MeasurableSet A),
  Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: ext1 A hA
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνinter : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (S ∩ T)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ
heq' :
  ∀ (A : Set α),
    MeasurableSet A →
      Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((s.restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
⊢ Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνinter : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (S ∩ T)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ
heq' :
  ∀ (A : Set α),
    MeasurableSet A →
      Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((s.restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
⊢ Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have hμinter : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have hμinter : μ.singularPart ν (A ∩ (S ∩ T)) = 0 := by
    rw [← nonpos_iff_eq_zero]
    exact hT₂ ▸ measure_mono (inter_subset_right.trans inter_subset_right)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνinter : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (S ∩ T)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ
heq' :
  ∀ (A : Set α),
    MeasurableSet A →
      Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((s.restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
hμinter : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((s.restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: rw [heq' A hA, heq, restrict_apply hA, ← diff_eq, AEDisjoint.measure_diff_left hμinter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνinter : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (S ∩ T)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ
heq' :
  ∀ (A : Set α),
    MeasurableSet A →
      Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((s.restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
hμinter : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
h :
  Eq (α := ℝ≥0∞) ((s.restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) (((μ.singularPart ν).restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
  ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: rw [heq' A hA, heq, restrict_apply hA, ← diff_eq, AEDisjoint.measure_diff_left hμinter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνinter : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (S ∩ T)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ
heq' :
  ∀ (A : Set α),
    MeasurableSet A →
      Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((s.restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
hμinter : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
h :
  Eq (α := ℝ≥0∞) ((s.restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) (((μ.singularPart ν).restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have h₂ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞)
  ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: rw [heq' A hA, heq, restrict_apply hA, ← diff_eq, AEDisjoint.measure_diff_left hμinter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνinter : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (S ∩ T)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ
heq' :
  ∀ (A : Set α),
    MeasurableSet A →
      Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((s.restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
hμinter : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
h :
  Eq (α := ℝ≥0∞) ((s.restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) (((μ.singularPart ν).restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞)
    ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have h₃ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A \ (S ∩ T)) : ℝ≥0∞)
  ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: rw [heq' A hA, heq, restrict_apply hA, ← diff_eq, AEDisjoint.measure_diff_left hμinter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) S : ℝ≥0∞) (0 : ℝ≥0∞)
hS₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
T : Set α
hT₁ : MeasurableSet T
hT₂ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) T : ℝ≥0∞) (0 : ℝ≥0∞)
hT₃ : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) Tᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
hνinter : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (S ∩ T)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ
heq' :
  ∀ (A : Set α),
    MeasurableSet A →
      Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((s.restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
A : Set α
hA : MeasurableSet A
hμinter : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
h :
  Eq (α := ℝ≥0∞) ((s.restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) (((μ.singularPart ν).restrict (S ∩ T)ᶜ : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
h₂ :
  Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)ᶜ) : ℝ≥0∞)
    ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
h₃ :
  Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A \ (S ∩ T)) : ℝ≥0∞)
    ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have h₄ : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: rw [heq' A hA, heq, restrict_apply hA, ← diff_eq, AEDisjoint.measure_diff_left hμinter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
⊢ (r • μ).singularPart ν = r • μ.singularPart ν
have pos : ∀ (hr : r = 0), (r • μ).singularPart ν = r • μ.singularPart ν
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
pos : ∀ (hr : r = 0), (r • μ).singularPart ν = r • μ.singularPart ν
⊢ (r • μ).singularPart ν = r • μ.singularPart ν
have neg : ∀ (hr : ¬r = 0), (r • μ).singularPart ν = r • μ.singularPart ν
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r = 0
⊢ (r • μ).singularPart ν = r • μ.singularPart ν
have pos : (HSMul.hSMul (α := ℝ≥0) 0 μ).singularPart ν = HSMul.hSMul (α := ℝ≥0) 0 (μ.singularPart ν)
Tactic: rw [hr, zero_smul, zero_smul, singularPart_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r = 0
pos : (HSMul.hSMul (α := ℝ≥0) 0 μ).singularPart ν = HSMul.hSMul (α := ℝ≥0) 0 (μ.singularPart ν)
⊢ (r • μ).singularPart ν = r • μ.singularPart ν
have pos₁ : singularPart 0 ν = HSMul.hSMul (α := ℝ≥0) 0 (μ.singularPart ν)
Tactic: rw [hr, zero_smul, zero_smul, singularPart_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r = 0
pos : (HSMul.hSMul (α := ℝ≥0) 0 μ).singularPart ν = HSMul.hSMul (α := ℝ≥0) 0 (μ.singularPart ν)
pos₁ : singularPart 0 ν = HSMul.hSMul (α := ℝ≥0) 0 (μ.singularPart ν)
⊢ (r • μ).singularPart ν = r • μ.singularPart ν
have pos₂ : singularPart 0 ν = 0
Tactic: rw [hr, zero_smul, zero_smul, singularPart_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : r = 0
pos : (HSMul.hSMul (α := ℝ≥0) 0 μ).singularPart ν = HSMul.hSMul (α := ℝ≥0) 0 (μ.singularPart ν)
pos₁ : singularPart 0 ν = HSMul.hSMul (α := ℝ≥0) 0 (μ.singularPart ν)
pos₂ : singularPart 0 ν = 0
⊢ (r • μ).singularPart ν = r • μ.singularPart ν
have pos₃ : Eq.{u_1 + 1} (α := Measure α) 0 0
Tactic: rw [hr, zero_smul, zero_smul, singularPart_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
⊢ (r • μ).singularPart ν = r • μ.singularPart ν
have pos : ∀ (hl : μ.HaveLebesgueDecomposition ν), (r • μ).singularPart ν = r • μ.singularPart ν
Tactic: by_cases hl : HaveLebesgueDecomposition μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
pos : ∀ (hl : μ.HaveLebesgueDecomposition ν), (r • μ).singularPart ν = r • μ.singularPart ν
⊢ (r • μ).singularPart ν = r • μ.singularPart ν
have neg : ∀ (hl : ¬μ.HaveLebesgueDecomposition ν), (r • μ).singularPart ν = r • μ.singularPart ν
Tactic: by_cases hl : HaveLebesgueDecomposition μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : μ.HaveLebesgueDecomposition ν
⊢ (r • μ).singularPart ν = r • μ.singularPart ν
have pos : r • μ = (↑r : ℝ≥0∞) • μ.singularPart ν + ν.withDensity ((↑r : ℝ≥0∞) • μ.rnDeriv ν)
Tactic: refine (eq_singularPart ((measurable_rnDeriv μ ν).const_smul (r : ℝ≥0∞))
          (MutuallySingular.smul r (mutuallySingular_singularPart _ _)) ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : μ.HaveLebesgueDecomposition ν
⊢ r • μ = (↑r : ℝ≥0∞) • μ.singularPart ν + ν.withDensity ((↑r : ℝ≥0∞) • μ.rnDeriv ν)
have pos : r • μ = (↑r : ℝ≥0∞) • μ.singularPart ν + (↑r : ℝ≥0∞) • ν.withDensity (μ.rnDeriv ν)
Tactic: rw [withDensity_smul _ (measurable_rnDeriv _ _), ← smul_add,
      ← haveLebesgueDecomposition_add μ ν, ENNReal.smul_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : μ.HaveLebesgueDecomposition ν
pos : r • μ = (↑r : ℝ≥0∞) • μ.singularPart ν + (↑r : ℝ≥0∞) • ν.withDensity (μ.rnDeriv ν)
⊢ r • μ = (↑r : ℝ≥0∞) • μ.singularPart ν + ν.withDensity ((↑r : ℝ≥0∞) • μ.rnDeriv ν)
have pos₁ : r • μ = (↑r : ℝ≥0∞) • (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν))
Tactic: rw [withDensity_smul _ (measurable_rnDeriv _ _), ← smul_add,
      ← haveLebesgueDecomposition_add μ ν, ENNReal.smul_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
r : ℝ≥0
hr : ¬r = 0
hl : μ.HaveLebesgueDecomposition ν
pos : r • μ = (↑r : ℝ≥0∞) • μ.singularPart ν + (↑r : ℝ≥0∞) • ν.withDensity (μ.rnDeriv ν)
pos₁ : r • μ = (↑r : ℝ≥0∞) • (μ.singularPart ν + ν.withDensity (μ.rnDeriv ν))
⊢ r • μ = (↑r : ℝ≥0∞) • μ.singularPart ν + ν.withDensity ((↑r : ℝ≥0∞) • μ.rnDeriv ν)
have pos₂ : r • μ = (↑r : ℝ≥0∞) • μ
Tactic: rw [withDensity_smul _ (measurable_rnDeriv _ _), ← smul_add,
      ← haveLebesgueDecomposition_add μ ν, ENNReal.smul_def]