awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
⊢ μ.withDensity (((↑r : ℝ≥0∞) • ν).rnDeriv μ) = (↑r : ℝ≥0∞) • μ.withDensity (ν.rnDeriv μ)
have suffices : (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
Tactic: suffices (r • ν).singularPart μ + withDensity μ (rnDeriv (r • ν) μ)
        = (r • ν).singularPart μ + r • withDensity μ (rnDeriv ν μ) by
      rwa [Measure.add_right_inj] at this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
⊢ (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
have rw : r • ν = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
Tactic: rw [← (r • ν).haveLebesgueDecomposition_add μ, singularPart_smul, ← smul_add,
      ← ν.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
rw : r • ν = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
⊢ (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
have rw₁ : r • ν = r • ν.singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
Tactic: rw [← (r • ν).haveLebesgueDecomposition_add μ, singularPart_smul, ← smul_add,
      ← ν.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
rw : r • ν = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
rw₁ : r • ν = r • ν.singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
⊢ (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
have rw₂ : r • ν = r • (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ))
Tactic: rw [← (r • ν).haveLebesgueDecomposition_add μ, singularPart_smul, ← smul_add,
      ← ν.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
rw : r • ν = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
rw₁ : r • ν = r • ν.singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
rw₂ : r • ν = r • (ν.singularPart μ + μ.withDensity (ν.rnDeriv μ))
⊢ (r • ν).singularPart μ + μ.withDensity ((r • ν).rnDeriv μ) = (r • ν).singularPart μ + r • μ.withDensity (ν.rnDeriv μ)
have rw₃ : r • ν = r • ν
Tactic: rw [← (r • ν).haveLebesgueDecomposition_add μ, singularPart_smul, ← smul_add,
      ← ν.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ ∞
⊢ (r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ
have h : (r.toNNReal • ν).rnDeriv μ =ᶠ[ae μ] r.toNNReal • ν.rnDeriv μ
Tactic: have h : (r.toNNReal • ν).rnDeriv μ =ᵐ[μ] r.toNNReal • ν.rnDeriv μ :=
    rnDeriv_smul_left' ν μ r.toNNReal
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
have refine : ν.rnDeriv (r • μ) =ᶠ[ae (r • μ)] r⁻¹ • ν.rnDeriv μ
Tactic: refine (absolutelyContinuous_smul <| ENNReal.coe_ne_zero.2 hr).ae_le
    (?_ : ν.rnDeriv (r • μ) =ᵐ[r • μ] r⁻¹ • ν.rnDeriv μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν.rnDeriv (r • μ) =ᶠ[ae (r • μ)] r⁻¹ • ν.rnDeriv μ
have rw : (r • μ).withDensity (ν.rnDeriv (r • μ)) = (r • μ).withDensity (r⁻¹ • ν.rnDeriv μ)
Tactic: rw [← withDensity_eq_iff_of_sigmaFinite]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
rw : (r • μ).withDensity (ν.rnDeriv (r • μ)) = (r • μ).withDensity (r⁻¹ • ν.rnDeriv μ)
⊢ ν.rnDeriv (r • μ) =ᶠ[ae (r • μ)] r⁻¹ • ν.rnDeriv μ
have hf : AEMeasurable (ν.rnDeriv (r • μ)) (r • μ)
Tactic: rw [← withDensity_eq_iff_of_sigmaFinite]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
rw : (r • μ).withDensity (ν.rnDeriv (r • μ)) = (r • μ).withDensity (r⁻¹ • ν.rnDeriv μ)
hf : AEMeasurable (ν.rnDeriv (r • μ)) (r • μ)
⊢ ν.rnDeriv (r • μ) =ᶠ[ae (r • μ)] r⁻¹ • ν.rnDeriv μ
have hg : AEMeasurable (r⁻¹ • ν.rnDeriv μ) (r • μ)
Tactic: rw [← withDensity_eq_iff_of_sigmaFinite]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
⊢ ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv ((↑r : ℝ≥0∞) • μ)) =
    ((↑r : ℝ≥0∞) • μ).withDensity ((↑r⁻¹ : ℝ≥0∞) • ν.rnDeriv μ)
have rw : ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv ((↑r : ℝ≥0∞) • μ)) =
  (↑r⁻¹ : ℝ≥0∞) • ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv μ)
Tactic: rw [withDensity_smul _ (measurable_rnDeriv _ _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
this :
  ν.singularPart (r • μ) + (r • μ).withDensity (ν.rnDeriv (r • μ)) =
    ν.singularPart (r • μ) + r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)
⊢ ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv ((↑r : ℝ≥0∞) • μ)) =
    (↑r⁻¹ : ℝ≥0∞) • ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv μ)
have rwa : ∀ (this : (r • μ).withDensity (ν.rnDeriv (r • μ)) = r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)),
  ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv ((↑r : ℝ≥0∞) • μ)) =
    (↑r⁻¹ : ℝ≥0∞) • ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv μ)
Tactic: rwa [add_right_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
⊢ ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv ((↑r : ℝ≥0∞) • μ)) =
    (↑r⁻¹ : ℝ≥0∞) • ((↑r : ℝ≥0∞) • μ).withDensity (ν.rnDeriv μ)
have suffices : ν.singularPart (r • μ) + (r • μ).withDensity (ν.rnDeriv (r • μ)) =
  ν.singularPart (r • μ) + r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)
Tactic: suffices ν.singularPart (r • μ) + withDensity (r • μ) (rnDeriv ν (r • μ))
        = ν.singularPart (r • μ) + r⁻¹ • withDensity (r • μ) (rnDeriv ν μ) by
      rwa [add_right_inj] at this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0
hr : r ≠ 0
⊢ ν.singularPart (r • μ) + (r • μ).withDensity (ν.rnDeriv (r • μ)) =
    ν.singularPart (r • μ) + r⁻¹ • (r • μ).withDensity (ν.rnDeriv μ)
have rw : ν = ν.singularPart μ + μ.withDensity (ν.rnDeriv μ)
Tactic: rw [← ν.haveLebesgueDecomposition_add (r • μ), singularPart_smul_right _ _ _ hr,
      ENNReal.smul_def r, withDensity_smul_measure, ← ENNReal.smul_def, ← smul_assoc,
      smul_eq_mul, inv_mul_cancel₀ hr, one_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
⊢ ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ
have refine : r.toNNReal ≠ 0
Tactic: refine rnDeriv_smul_right' ν μ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
⊢ r.toNNReal ≠ 0
have rw : ¬(r = 0 ∨ r = ∞)
Tactic: rw [ne_eq, ENNReal.toNNReal_eq_zero_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
⊢ ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
have h : ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ
Tactic: have h : ν.rnDeriv (r.toNNReal • μ) =ᵐ[μ] r.toNNReal⁻¹ • ν.rnDeriv μ := by
    refine rnDeriv_smul_right' ν μ ?_
    rw [ne_eq, ENNReal.toNNReal_eq_zero_iff]
    simp [hr, hr_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
h : ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ
⊢ ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
have rwa : ∀ (h : ν.rnDeriv ((↑r.toNNReal : ℝ≥0∞) • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ),
  ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
Tactic: rwa [ENNReal.smul_def, ENNReal.coe_toNNReal hr_ne_top,
    ← ENNReal.toNNReal_inv, ENNReal.smul_def, ENNReal.coe_toNNReal (ENNReal.inv_ne_top.mpr hr)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
h : ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ
rwa :
  ∀ (h : ν.rnDeriv ((↑r.toNNReal : ℝ≥0∞) • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ),
    ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
⊢ ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
have rwa₁ : ∀ (h : ν.rnDeriv (r • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ), ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
Tactic: rwa [ENNReal.smul_def, ENNReal.coe_toNNReal hr_ne_top,
    ← ENNReal.toNNReal_inv, ENNReal.smul_def, ENNReal.coe_toNNReal (ENNReal.inv_ne_top.mpr hr)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
h : ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ
rwa :
  ∀ (h : ν.rnDeriv ((↑r.toNNReal : ℝ≥0∞) • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ),
    ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
rwa₁ : ∀ (h : ν.rnDeriv (r • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ), ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
⊢ ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
have rwa₂ : ∀ (h : ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹.toNNReal • ν.rnDeriv μ), ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
Tactic: rwa [ENNReal.smul_def, ENNReal.coe_toNNReal hr_ne_top,
    ← ENNReal.toNNReal_inv, ENNReal.smul_def, ENNReal.coe_toNNReal (ENNReal.inv_ne_top.mpr hr)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
h : ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ
rwa :
  ∀ (h : ν.rnDeriv ((↑r.toNNReal : ℝ≥0∞) • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ),
    ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
rwa₁ : ∀ (h : ν.rnDeriv (r • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ), ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
rwa₂ : ∀ (h : ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹.toNNReal • ν.rnDeriv μ), ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
⊢ ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
have rwa₃ : ∀ (h : ν.rnDeriv (r • μ) =ᶠ[ae μ] (↑r⁻¹.toNNReal : ℝ≥0∞) • ν.rnDeriv μ), ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
Tactic: rwa [ENNReal.smul_def, ENNReal.coe_toNNReal hr_ne_top,
    ← ENNReal.toNNReal_inv, ENNReal.smul_def, ENNReal.coe_toNNReal (ENNReal.inv_ne_top.mpr hr)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst : SigmaFinite ν
inst_1 : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ 0
hr_ne_top : r ≠ ∞
h : ν.rnDeriv (r.toNNReal • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ
rwa :
  ∀ (h : ν.rnDeriv ((↑r.toNNReal : ℝ≥0∞) • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ),
    ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
rwa₁ : ∀ (h : ν.rnDeriv (r • μ) =ᶠ[ae μ] r.toNNReal⁻¹ • ν.rnDeriv μ), ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
rwa₂ : ∀ (h : ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹.toNNReal • ν.rnDeriv μ), ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
rwa₃ :
  ∀ (h : ν.rnDeriv (r • μ) =ᶠ[ae μ] (↑r⁻¹.toNNReal : ℝ≥0∞) • ν.rnDeriv μ), ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
⊢ ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
have rwa₄ : ∀ (h : ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ), ν.rnDeriv (r • μ) =ᶠ[ae μ] r⁻¹ • ν.rnDeriv μ
Tactic: rwa [ENNReal.smul_def, ENNReal.coe_toNNReal hr_ne_top,
    ← ENNReal.toNNReal_inv, ENNReal.smul_def, ENNReal.coe_toNNReal (ENNReal.inv_ne_top.mpr hr)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
⊢ (ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ
have rw : μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
Tactic: rw [← withDensity_eq_iff_of_sigmaFinite]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
rw : μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
⊢ (ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ
have hf : AEMeasurable ((ν₁ + ν₂).rnDeriv μ) μ
Tactic: rw [← withDensity_eq_iff_of_sigmaFinite]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
rw : μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
hf : AEMeasurable ((ν₁ + ν₂).rnDeriv μ) μ
⊢ (ν₁ + ν₂).rnDeriv μ =ᶠ[ae μ] ν₁.rnDeriv μ + ν₂.rnDeriv μ
have hg : AEMeasurable (ν₁.rnDeriv μ + ν₂.rnDeriv μ) μ
Tactic: rw [← withDensity_eq_iff_of_sigmaFinite]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
this :
  (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
⊢ μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
have rwa : ∀ (this : μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)),
  μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
Tactic: rwa [add_right_inj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
⊢ μ.withDensity ((ν₁ + ν₂).rnDeriv μ) = μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
have suffices : (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
  (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
Tactic: suffices (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ)
        = (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ) by
      rwa [add_right_inj] at this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
⊢ (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
have rw : ν₁ + ν₂ = (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
Tactic: rw [← (ν₁ + ν₂).haveLebesgueDecomposition_add μ, singularPart_add,
      withDensity_add_left (measurable_rnDeriv _ _), add_assoc,
      add_comm (ν₂.singularPart μ), add_assoc, add_comm _ (ν₂.singularPart μ),
      ← ν₂.haveLebesgueDecomposition_add μ, ← add_assoc, ← ν₁.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
rw : ν₁ + ν₂ = (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
⊢ (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
have rw₁ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
Tactic: rw [← (ν₁ + ν₂).haveLebesgueDecomposition_add μ, singularPart_add,
      withDensity_add_left (measurable_rnDeriv _ _), add_assoc,
      add_comm (ν₂.singularPart μ), add_assoc, add_comm _ (ν₂.singularPart μ),
      ← ν₂.haveLebesgueDecomposition_add μ, ← add_assoc, ← ν₁.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
rw : ν₁ + ν₂ = (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rw₁ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
⊢ (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
have rw₂ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ))
Tactic: rw [← (ν₁ + ν₂).haveLebesgueDecomposition_add μ, singularPart_add,
      withDensity_add_left (measurable_rnDeriv _ _), add_assoc,
      add_comm (ν₂.singularPart μ), add_assoc, add_comm _ (ν₂.singularPart μ),
      ← ν₂.haveLebesgueDecomposition_add μ, ← add_assoc, ← ν₁.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
rw : ν₁ + ν₂ = (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rw₁ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rw₂ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ))
⊢ (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
have rw₃ : ν₁ + ν₂ = ν₁.singularPart μ + (ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ)))
Tactic: rw [← (ν₁ + ν₂).haveLebesgueDecomposition_add μ, singularPart_add,
      withDensity_add_left (measurable_rnDeriv _ _), add_assoc,
      add_comm (ν₂.singularPart μ), add_assoc, add_comm _ (ν₂.singularPart μ),
      ← ν₂.haveLebesgueDecomposition_add μ, ← add_assoc, ← ν₁.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
rw : ν₁ + ν₂ = (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rw₁ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rw₂ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ))
rw₃ : ν₁ + ν₂ = ν₁.singularPart μ + (ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ)))
⊢ (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
have rw₄ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ) + ν₂.singularPart μ)
Tactic: rw [← (ν₁ + ν₂).haveLebesgueDecomposition_add μ, singularPart_add,
      withDensity_add_left (measurable_rnDeriv _ _), add_assoc,
      add_comm (ν₂.singularPart μ), add_assoc, add_comm _ (ν₂.singularPart μ),
      ← ν₂.haveLebesgueDecomposition_add μ, ← add_assoc, ← ν₁.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
rw : ν₁ + ν₂ = (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rw₁ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rw₂ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ))
rw₃ : ν₁ + ν₂ = ν₁.singularPart μ + (ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ)))
rw₄ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ) + ν₂.singularPart μ)
⊢ (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
have rw₅ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + (μ.withDensity (ν₂.rnDeriv μ) + ν₂.singularPart μ))
Tactic: rw [← (ν₁ + ν₂).haveLebesgueDecomposition_add μ, singularPart_add,
      withDensity_add_left (measurable_rnDeriv _ _), add_assoc,
      add_comm (ν₂.singularPart μ), add_assoc, add_comm _ (ν₂.singularPart μ),
      ← ν₂.haveLebesgueDecomposition_add μ, ← add_assoc, ← ν₁.haveLebesgueDecomposition_add μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
ν₁ ν₂ μ : Measure α
inst : SigmaFinite ν₁
inst_1 : SigmaFinite ν₂
inst_2 : SigmaFinite μ
rw : ν₁ + ν₂ = (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rw₁ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
rw₂ : ν₁ + ν₂ = ν₁.singularPart μ + ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ))
rw₃ : ν₁ + ν₂ = ν₁.singularPart μ + (ν₂.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ)))
rw₄ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + μ.withDensity (ν₂.rnDeriv μ) + ν₂.singularPart μ)
rw₅ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + (μ.withDensity (ν₂.rnDeriv μ) + ν₂.singularPart μ))
⊢ (ν₁ + ν₂).singularPart μ + μ.withDensity ((ν₁ + ν₂).rnDeriv μ) =
    (ν₁ + ν₂).singularPart μ + μ.withDensity (ν₁.rnDeriv μ + ν₂.rnDeriv μ)
have rw₆ : ν₁ + ν₂ = ν₁.singularPart μ + (μ.withDensity (ν₁.rnDeriv μ) + (ν₂.singularPart μ + μ.withDensity (ν₂.rnDeriv μ)))
Tactic: rw [← (ν₁ + ν₂).haveLebesgueDecomposition_add μ, singularPart_add,
      withDensity_add_left (measurable_rnDeriv _ _), add_assoc,
      add_comm (ν₂.singularPart μ), add_assoc, add_comm _ (ν₂.singularPart μ),
      ← ν₂.haveLebesgueDecomposition_add μ, ← add_assoc, ← ν₁.haveLebesgueDecomposition_add μ]