awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
rw : μ.withDensityᵥ ((-s).rnDeriv μ) = -μ.withDensityᵥ (s.rnDeriv μ)
⊢ μ.withDensityᵥ ((-s).rnDeriv μ) = μ.withDensityᵥ (-s.rnDeriv μ)
have rw₁ : (-s).singularPart μ + μ.withDensityᵥ ((-s).rnDeriv μ) = (-s).singularPart μ + -μ.withDensityᵥ (s.rnDeriv μ)
Tactic: rw [withDensityᵥ_neg, ← add_right_inj ((-s).singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, singularPart_neg, ← neg_add,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
rw : μ.withDensityᵥ ((-s).rnDeriv μ) = -μ.withDensityᵥ (s.rnDeriv μ)
rw₁ : (-s).singularPart μ + μ.withDensityᵥ ((-s).rnDeriv μ) = (-s).singularPart μ + -μ.withDensityᵥ (s.rnDeriv μ)
⊢ μ.withDensityᵥ ((-s).rnDeriv μ) = μ.withDensityᵥ (-s.rnDeriv μ)
have rw₂ : -s = (-s).singularPart μ + -μ.withDensityᵥ (s.rnDeriv μ)
Tactic: rw [withDensityᵥ_neg, ← add_right_inj ((-s).singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, singularPart_neg, ← neg_add,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
rw : μ.withDensityᵥ ((-s).rnDeriv μ) = -μ.withDensityᵥ (s.rnDeriv μ)
rw₁ : (-s).singularPart μ + μ.withDensityᵥ ((-s).rnDeriv μ) = (-s).singularPart μ + -μ.withDensityᵥ (s.rnDeriv μ)
rw₂ : -s = (-s).singularPart μ + -μ.withDensityᵥ (s.rnDeriv μ)
⊢ μ.withDensityᵥ ((-s).rnDeriv μ) = μ.withDensityᵥ (-s.rnDeriv μ)
have rw₃ : -s = -s.singularPart μ + -μ.withDensityᵥ (s.rnDeriv μ)
Tactic: rw [withDensityᵥ_neg, ← add_right_inj ((-s).singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, singularPart_neg, ← neg_add,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
rw : μ.withDensityᵥ ((-s).rnDeriv μ) = -μ.withDensityᵥ (s.rnDeriv μ)
rw₁ : (-s).singularPart μ + μ.withDensityᵥ ((-s).rnDeriv μ) = (-s).singularPart μ + -μ.withDensityᵥ (s.rnDeriv μ)
rw₂ : -s = (-s).singularPart μ + -μ.withDensityᵥ (s.rnDeriv μ)
rw₃ : -s = -s.singularPart μ + -μ.withDensityᵥ (s.rnDeriv μ)
⊢ μ.withDensityᵥ ((-s).rnDeriv μ) = μ.withDensityᵥ (-s.rnDeriv μ)
have rw₄ : -s = -(s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ))
Tactic: rw [withDensityᵥ_neg, ← add_right_inj ((-s).singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, singularPart_neg, ← neg_add,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
rw : μ.withDensityᵥ ((-s).rnDeriv μ) = -μ.withDensityᵥ (s.rnDeriv μ)
rw₁ : (-s).singularPart μ + μ.withDensityᵥ ((-s).rnDeriv μ) = (-s).singularPart μ + -μ.withDensityᵥ (s.rnDeriv μ)
rw₂ : -s = (-s).singularPart μ + -μ.withDensityᵥ (s.rnDeriv μ)
rw₃ : -s = -s.singularPart μ + -μ.withDensityᵥ (s.rnDeriv μ)
rw₄ : -s = -(s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ))
⊢ μ.withDensityᵥ ((-s).rnDeriv μ) = μ.withDensityᵥ (-s.rnDeriv μ)
have rw₅ : -s = -s
Tactic: rw [withDensityᵥ_neg, ← add_right_inj ((-s).singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, singularPart_neg, ← neg_add,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
⊢ (r • s).rnDeriv μ =ᶠ[ae μ] r • s.rnDeriv μ
have _ : μ.withDensityᵥ ((r • s).rnDeriv μ) = μ.withDensityᵥ (r • s.rnDeriv μ)
Tactic: refine
    Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _)
      ((integrable_rnDeriv _ _).smul r) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
⊢ μ.withDensityᵥ ((r • s).rnDeriv μ) = μ.withDensityᵥ (r • s.rnDeriv μ)
have rw : μ.withDensityᵥ ((r • s).rnDeriv μ) = HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
Tactic: rw [withDensityᵥ_smul (rnDeriv s μ) r, ← add_right_inj ((r • s).singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, singularPart_smul, ← smul_add,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
rw : μ.withDensityᵥ ((r • s).rnDeriv μ) = HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
⊢ μ.withDensityᵥ ((r • s).rnDeriv μ) = μ.withDensityᵥ (r • s.rnDeriv μ)
have rw₁ : (r • s).singularPart μ + μ.withDensityᵥ ((r • s).rnDeriv μ) =
  (r • s).singularPart μ + HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
Tactic: rw [withDensityᵥ_smul (rnDeriv s μ) r, ← add_right_inj ((r • s).singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, singularPart_smul, ← smul_add,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
rw : μ.withDensityᵥ ((r • s).rnDeriv μ) = HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
rw₁ :
  (r • s).singularPart μ + μ.withDensityᵥ ((r • s).rnDeriv μ) =
    (r • s).singularPart μ + HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
⊢ μ.withDensityᵥ ((r • s).rnDeriv μ) = μ.withDensityᵥ (r • s.rnDeriv μ)
have rw₂ : r • s = (r • s).singularPart μ + HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
Tactic: rw [withDensityᵥ_smul (rnDeriv s μ) r, ← add_right_inj ((r • s).singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, singularPart_smul, ← smul_add,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
rw : μ.withDensityᵥ ((r • s).rnDeriv μ) = HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
rw₁ :
  (r • s).singularPart μ + μ.withDensityᵥ ((r • s).rnDeriv μ) =
    (r • s).singularPart μ + HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
rw₂ : r • s = (r • s).singularPart μ + HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
⊢ μ.withDensityᵥ ((r • s).rnDeriv μ) = μ.withDensityᵥ (r • s.rnDeriv μ)
have rw₃ : r • s = r • s.singularPart μ + HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
Tactic: rw [withDensityᵥ_smul (rnDeriv s μ) r, ← add_right_inj ((r • s).singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, singularPart_smul, ← smul_add,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
rw : μ.withDensityᵥ ((r • s).rnDeriv μ) = HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
rw₁ :
  (r • s).singularPart μ + μ.withDensityᵥ ((r • s).rnDeriv μ) =
    (r • s).singularPart μ + HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
rw₂ : r • s = (r • s).singularPart μ + HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
rw₃ : r • s = r • s.singularPart μ + HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
⊢ μ.withDensityᵥ ((r • s).rnDeriv μ) = μ.withDensityᵥ (r • s.rnDeriv μ)
have rw₄ : r • s = r • (s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ))
Tactic: rw [withDensityᵥ_smul (rnDeriv s μ) r, ← add_right_inj ((r • s).singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, singularPart_smul, ← smul_add,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
rw : μ.withDensityᵥ ((r • s).rnDeriv μ) = HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
rw₁ :
  (r • s).singularPart μ + μ.withDensityᵥ ((r • s).rnDeriv μ) =
    (r • s).singularPart μ + HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
rw₂ : r • s = (r • s).singularPart μ + HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
rw₃ : r • s = r • s.singularPart μ + HSMul.hSMul (β := VectorMeasure α ℝ) r (μ.withDensityᵥ (s.rnDeriv μ))
rw₄ : r • s = r • (s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ))
⊢ μ.withDensityᵥ ((r • s).rnDeriv μ) = μ.withDensityᵥ (r • s.rnDeriv μ)
have rw₅ : r • s = r • s
Tactic: rw [withDensityᵥ_smul (rnDeriv s μ) r, ← add_right_inj ((r • s).singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, singularPart_smul, ← smul_add,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
inst_2 : (s + t).HaveLebesgueDecomposition μ
⊢ (s + t).rnDeriv μ =ᶠ[ae μ] s.rnDeriv μ + t.rnDeriv μ
have _ : μ.withDensityᵥ ((s + t).rnDeriv μ) = μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
Tactic: refine
    Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _)
      ((integrable_rnDeriv _ _).add (integrable_rnDeriv _ _)) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
inst_2 : (s + t).HaveLebesgueDecomposition μ
⊢ μ.withDensityᵥ ((s + t).rnDeriv μ) = μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
have rw : (s + t).singularPart μ + μ.withDensityᵥ ((s + t).rnDeriv μ) =
  (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
Tactic: rw [← add_right_inj ((s + t).singularPart μ), singularPart_add_withDensity_rnDeriv_eq,
    withDensityᵥ_add (integrable_rnDeriv _ _) (integrable_rnDeriv _ _), singularPart_add,
    add_assoc, add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
inst_2 : (s + t).HaveLebesgueDecomposition μ
rw :
  (s + t).singularPart μ + μ.withDensityᵥ ((s + t).rnDeriv μ) =
    (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
⊢ μ.withDensityᵥ ((s + t).rnDeriv μ) = μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
have rw₁ : s + t = (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
Tactic: rw [← add_right_inj ((s + t).singularPart μ), singularPart_add_withDensity_rnDeriv_eq,
    withDensityᵥ_add (integrable_rnDeriv _ _) (integrable_rnDeriv _ _), singularPart_add,
    add_assoc, add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
inst_2 : (s + t).HaveLebesgueDecomposition μ
rw :
  (s + t).singularPart μ + μ.withDensityᵥ ((s + t).rnDeriv μ) =
    (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
rw₁ : s + t = (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
⊢ μ.withDensityᵥ ((s + t).rnDeriv μ) = μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
have rw₂ : s + t = (s + t).singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ))
Tactic: rw [← add_right_inj ((s + t).singularPart μ), singularPart_add_withDensity_rnDeriv_eq,
    withDensityᵥ_add (integrable_rnDeriv _ _) (integrable_rnDeriv _ _), singularPart_add,
    add_assoc, add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
inst_2 : (s + t).HaveLebesgueDecomposition μ
rw :
  (s + t).singularPart μ + μ.withDensityᵥ ((s + t).rnDeriv μ) =
    (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
rw₁ : s + t = (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
rw₂ : s + t = (s + t).singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ))
⊢ μ.withDensityᵥ ((s + t).rnDeriv μ) = μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
have rw₃ : s + t = s.singularPart μ + t.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ))
Tactic: rw [← add_right_inj ((s + t).singularPart μ), singularPart_add_withDensity_rnDeriv_eq,
    withDensityᵥ_add (integrable_rnDeriv _ _) (integrable_rnDeriv _ _), singularPart_add,
    add_assoc, add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
inst_2 : (s + t).HaveLebesgueDecomposition μ
rw :
  (s + t).singularPart μ + μ.withDensityᵥ ((s + t).rnDeriv μ) =
    (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
rw₁ : s + t = (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
rw₂ : s + t = (s + t).singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ))
rw₃ : s + t = s.singularPart μ + t.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ))
⊢ μ.withDensityᵥ ((s + t).rnDeriv μ) = μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
have rw₄ : s + t = s.singularPart μ + (t.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ)))
Tactic: rw [← add_right_inj ((s + t).singularPart μ), singularPart_add_withDensity_rnDeriv_eq,
    withDensityᵥ_add (integrable_rnDeriv _ _) (integrable_rnDeriv _ _), singularPart_add,
    add_assoc, add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
inst_2 : (s + t).HaveLebesgueDecomposition μ
rw :
  (s + t).singularPart μ + μ.withDensityᵥ ((s + t).rnDeriv μ) =
    (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
rw₁ : s + t = (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
rw₂ : s + t = (s + t).singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ))
rw₃ : s + t = s.singularPart μ + t.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ))
rw₄ : s + t = s.singularPart μ + (t.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ)))
⊢ μ.withDensityᵥ ((s + t).rnDeriv μ) = μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
have rw₅ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ) + t.singularPart μ)
Tactic: rw [← add_right_inj ((s + t).singularPart μ), singularPart_add_withDensity_rnDeriv_eq,
    withDensityᵥ_add (integrable_rnDeriv _ _) (integrable_rnDeriv _ _), singularPart_add,
    add_assoc, add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
inst_2 : (s + t).HaveLebesgueDecomposition μ
rw :
  (s + t).singularPart μ + μ.withDensityᵥ ((s + t).rnDeriv μ) =
    (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
rw₁ : s + t = (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
rw₂ : s + t = (s + t).singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ))
rw₃ : s + t = s.singularPart μ + t.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ))
rw₄ : s + t = s.singularPart μ + (t.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ)))
rw₅ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ) + t.singularPart μ)
⊢ μ.withDensityᵥ ((s + t).rnDeriv μ) = μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
have rw₆ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + (μ.withDensityᵥ (t.rnDeriv μ) + t.singularPart μ))
Tactic: rw [← add_right_inj ((s + t).singularPart μ), singularPart_add_withDensity_rnDeriv_eq,
    withDensityᵥ_add (integrable_rnDeriv _ _) (integrable_rnDeriv _ _), singularPart_add,
    add_assoc, add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
inst_2 : (s + t).HaveLebesgueDecomposition μ
rw :
  (s + t).singularPart μ + μ.withDensityᵥ ((s + t).rnDeriv μ) =
    (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
rw₁ : s + t = (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
rw₂ : s + t = (s + t).singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ))
rw₃ : s + t = s.singularPart μ + t.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ))
rw₄ : s + t = s.singularPart μ + (t.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ)))
rw₅ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ) + t.singularPart μ)
rw₆ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + (μ.withDensityᵥ (t.rnDeriv μ) + t.singularPart μ))
⊢ μ.withDensityᵥ ((s + t).rnDeriv μ) = μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
have rw₇ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + (t.singularPart μ + μ.withDensityᵥ (t.rnDeriv μ)))
Tactic: rw [← add_right_inj ((s + t).singularPart μ), singularPart_add_withDensity_rnDeriv_eq,
    withDensityᵥ_add (integrable_rnDeriv _ _) (integrable_rnDeriv _ _), singularPart_add,
    add_assoc, add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
inst_2 : (s + t).HaveLebesgueDecomposition μ
rw :
  (s + t).singularPart μ + μ.withDensityᵥ ((s + t).rnDeriv μ) =
    (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
rw₁ : s + t = (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
rw₂ : s + t = (s + t).singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ))
rw₃ : s + t = s.singularPart μ + t.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ))
rw₄ : s + t = s.singularPart μ + (t.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ)))
rw₅ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ) + t.singularPart μ)
rw₆ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + (μ.withDensityᵥ (t.rnDeriv μ) + t.singularPart μ))
rw₇ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + (t.singularPart μ + μ.withDensityᵥ (t.rnDeriv μ)))
⊢ μ.withDensityᵥ ((s + t).rnDeriv μ) = μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
have rw₈ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + t)
Tactic: rw [← add_right_inj ((s + t).singularPart μ), singularPart_add_withDensity_rnDeriv_eq,
    withDensityᵥ_add (integrable_rnDeriv _ _) (integrable_rnDeriv _ _), singularPart_add,
    add_assoc, add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s t : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
inst_1 : t.HaveLebesgueDecomposition μ
inst_2 : (s + t).HaveLebesgueDecomposition μ
rw :
  (s + t).singularPart μ + μ.withDensityᵥ ((s + t).rnDeriv μ) =
    (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
rw₁ : s + t = (s + t).singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
rw₂ : s + t = (s + t).singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ))
rw₃ : s + t = s.singularPart μ + t.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ))
rw₄ : s + t = s.singularPart μ + (t.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ)))
rw₅ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ) + t.singularPart μ)
rw₆ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + (μ.withDensityᵥ (t.rnDeriv μ) + t.singularPart μ))
rw₇ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + (t.singularPart μ + μ.withDensityᵥ (t.rnDeriv μ)))
rw₈ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + t)
⊢ μ.withDensityᵥ ((s + t).rnDeriv μ) = μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
have rw₉ : s + t = s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) + t
Tactic: rw [← add_right_inj ((s + t).singularPart μ), singularPart_add_withDensity_rnDeriv_eq,
    withDensityᵥ_add (integrable_rnDeriv _ _) (integrable_rnDeriv _ _), singularPart_add,
    add_assoc, add_comm (t.singularPart μ), add_assoc, add_comm _ (t.singularPart μ),
    singularPart_add_withDensity_rnDeriv_eq, ← add_assoc,
    singularPart_add_withDensity_rnDeriv_eq]