awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hs : s ⟂ₘ ν
hadd : μ = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
⊢ ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
have hsing : μ.singularPart ν ⟂ₘ ν
Tactic: obtain ⟨hmeas, hsing, hadd'⟩ := haveLebesgueDecomposition_spec μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hs : s ⟂ₘ ν
hadd : μ = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
⊢ ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
have hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
Tactic: obtain ⟨hmeas, hsing, hadd'⟩ := haveLebesgueDecomposition_spec μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hs : s ⟂ₘ ν
hadd : μ = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hsing : μ.singularPart ν ⟂ₘ ν
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
⊢ ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
have obtain : ∀ (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∞)), ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
Tactic: obtain ⟨⟨S, hS₁, hS₂, hS₃⟩, ⟨T, hT₁, hT₂, hT₃⟩⟩ := hs, hsing
Cleared hypotheses: hs, hsing
-- 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 : μ = 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∞)
⊢ ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
have rw : ∀ (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∞)), ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
Tactic: rw [hadd'] at hadd
Cleared hypotheses: hadd, this, hmeas, hadd', S, hS₁, hS₂, hS₃, T, hT₁, hT₂, hT₃
-- 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∞)
⊢ ν.withDensity f = ν.withDensity (μ.rnDeriv ν)
have hνinter : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (S ∩ T)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have hνinter : ν (S ∩ T)ᶜ = 0 := by
    rw [compl_inter]
    refine nonpos_iff_eq_zero.1 (le_trans (measure_union_le _ _) ?_)
    rw [hT₃, hS₃, add_zero]
-- 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∞)
⊢ (ν.withDensity f).restrict (S ∩ T) = (ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T)
have h : ∀ (A : Set α) (hA : MeasurableSet A),
  Eq (α := ℝ≥0∞) (((ν.withDensity f).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) : (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∞)
A : Set α
hA : MeasurableSet A
⊢ Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((s : (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∞)
A : Set α
hA : MeasurableSet A
⊢ Eq (α := ℝ≥0∞) (((ν.withDensity f).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have hs : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have hs : s (A ∩ (S ∩ T)) = 0 := by
      rw [← nonpos_iff_eq_zero]
      exact hS₂ ▸ measure_mono (inter_subset_right.trans inter_subset_left)
-- 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∞)
A : Set α
hA : MeasurableSet A
hs : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ 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∞)
A : Set α
hA : MeasurableSet A
hs : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((ν.withDensity f).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have hsing : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have hsing : μ.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∞)
A : Set α
hA : MeasurableSet A
hs : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
hsing : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((ν.withDensity f).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
  (((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
Tactic: rw [restrict_apply hA, restrict_apply hA, ← add_zero (ν.withDensity f (A ∩ (S ∩ T))), ← hs, ←
      add_apply, add_comm, ← hadd, add_apply, hsing, zero_add]
-- 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∞)
A : Set α
hA : MeasurableSet A
hs : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
hsing : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
h :
  Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
    (((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((ν.withDensity f).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
  ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
Tactic: rw [restrict_apply hA, restrict_apply hA, ← add_zero (ν.withDensity f (A ∩ (S ∩ T))), ← hs, ←
      add_apply, add_comm, ← hadd, add_apply, hsing, zero_add]
-- 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∞)
A : Set α
hA : MeasurableSet A
hs : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
hsing : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
h :
  Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
    (((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
    ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((ν.withDensity f).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have h₂ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞) =
  (ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T))
Tactic: rw [restrict_apply hA, restrict_apply hA, ← add_zero (ν.withDensity f (A ∩ (S ∩ T))), ← hs, ←
      add_apply, add_comm, ← hadd, add_apply, hsing, zero_add]
-- 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∞)
A : Set α
hA : MeasurableSet A
hs : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
hsing : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
h :
  Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
    (((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
    ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
h₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞) =
    (ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T))
⊢ Eq (α := ℝ≥0∞) (((ν.withDensity f).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have h₃ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
    ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) =
  (ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T))
Tactic: rw [restrict_apply hA, restrict_apply hA, ← add_zero (ν.withDensity f (A ∩ (S ∩ T))), ← hs, ←
      add_apply, add_comm, ← hadd, add_apply, hsing, zero_add]
-- 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∞)
A : Set α
hA : MeasurableSet A
hs : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
hsing : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
h :
  Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
    (((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
    ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
h₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞) =
    (ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T))
h₃ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
      ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) =
    (ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T))
⊢ Eq (α := ℝ≥0∞) (((ν.withDensity f).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have h₄ : Eq (α := ℝ≥0∞) ((ν.withDensity f + s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
  ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
Tactic: rw [restrict_apply hA, restrict_apply hA, ← add_zero (ν.withDensity f (A ∩ (S ∩ T))), ← hs, ←
      add_apply, add_comm, ← hadd, add_apply, hsing, zero_add]
-- 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∞)
A : Set α
hA : MeasurableSet A
hs : Eq (α := ℝ≥0∞) ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
hsing : Eq (α := ℝ≥0∞) ((μ.singularPart ν : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞)
h :
  Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
    (((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
h₁ :
  Eq (α := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
    ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
h₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) (0 : ℝ≥0∞) =
    (ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T))
h₃ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
      ((s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞) =
    (ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T))
h₄ :
  Eq (α := ℝ≥0∞) ((ν.withDensity f + s : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
    ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((ν.withDensity f).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
    (((ν.withDensity (μ.rnDeriv ν)).restrict (S ∩ T) : (a : Set α) → ℝ≥0∞) A : ℝ≥0∞)
have h₅ : Eq (α := ℝ≥0∞) ((s + ν.withDensity f : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
  ((ν.withDensity (μ.rnDeriv ν) : (a : Set α) → ℝ≥0∞) (A ∩ (S ∩ T)) : ℝ≥0∞)
Tactic: rw [restrict_apply hA, restrict_apply hA, ← add_zero (ν.withDensity f (A ∩ (S ∩ T))), ← hs, ←
      add_apply, add_comm, ← hadd, add_apply, hsing, zero_add]