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 α
r : ℝ
hr : r < 0
inr :
  (-r).toNNReal • (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure -
      ((-r).toNNReal • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
inr₁ :
  (-r).toNNReal • (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure -
      (-r).toNNReal • (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
inr₂ :
  -((-r).toNNReal • (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (-r).toNNReal • (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure) =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
inr₃ :
  -((-r).toNNReal •
        ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
          (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)) =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
inr₄ :
  -((↑(-r).toNNReal : ℝ) •
        ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
          (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)) =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
⊢ ((-r).toNNReal • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure -
      ((-r).toNNReal • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
have inr₅ : -(↑(-r).toNNReal : ℝ) •
    ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure) =
  r •
    ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
Tactic: rw [toSignedMeasure_smul, toSignedMeasure_smul, ← neg_sub, ← smul_sub, NNReal.smul_def,
      ← neg_smul, Real.coe_toNNReal _ (le_of_lt (neg_pos.mpr hr)), neg_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
inr :
  (-r).toNNReal • (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure -
      ((-r).toNNReal • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
inr₁ :
  (-r).toNNReal • (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure -
      (-r).toNNReal • (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
inr₂ :
  -((-r).toNNReal • (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (-r).toNNReal • (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure) =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
inr₃ :
  -((-r).toNNReal •
        ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
          (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)) =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
inr₄ :
  -((↑(-r).toNNReal : ℝ) •
        ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
          (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)) =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
inr₅ :
  -(↑(-r).toNNReal : ℝ) •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure) =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
⊢ ((-r).toNNReal • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure -
      ((-r).toNNReal • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
have inr₆ : - -r •
    ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure) =
  r •
    ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
Tactic: rw [toSignedMeasure_smul, toSignedMeasure_smul, ← neg_sub, ← smul_sub, NNReal.smul_def,
      ← neg_smul, Real.coe_toNNReal _ (le_of_lt (neg_pos.mpr hr)), neg_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
⊢ (r • s).singularPart μ = r • s.singularPart μ
have x : 0 ≤ r ∨ r < 0
Tactic: cases le_or_gt 0 r with
  | inl hr =>
    lift r to ℝ≥0 using hr
    exact singularPart_smul_nnreal s μ r
  | inr hr =>
    rw [singularPart, singularPart]
    conv_lhs =>
      congr
      · congr
        · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_posPart_neg _ _ hr, singularPart_smul]
      · congr
        · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_negPart_neg _ _ hr, singularPart_smul]
    rw [toSignedMeasure_smul, toSignedMeasure_smul, ← neg_sub, ← smul_sub, NNReal.smul_def,
      ← neg_smul, Real.coe_toNNReal _ (le_of_lt (neg_pos.mpr hr)), neg_neg]
-- 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 μ
⊢ (s + t).singularPart μ = s.singularPart μ + t.singularPart μ
have _ : s + t = s.singularPart μ + t.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
Tactic: refine
    (eq_singularPart _ (s.rnDeriv μ + t.rnDeriv μ)
        ((mutuallySingular_singularPart s μ).add_left (mutuallySingular_singularPart t μ))
        ?_).symm
-- 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 μ
⊢ s + t = s.singularPart μ + t.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
have rw : s + t = s.singularPart μ + t.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ))
Tactic: rw [withDensityᵥ_add (integrable_rnDeriv s μ) (integrable_rnDeriv t μ), 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 μ
rw : s + t = s.singularPart μ + t.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ))
⊢ s + t = s.singularPart μ + t.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
have rw₁ : s + t = s.singularPart μ + (t.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ)))
Tactic: rw [withDensityᵥ_add (integrable_rnDeriv s μ) (integrable_rnDeriv t μ), 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 μ
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 μ)))
⊢ s + t = s.singularPart μ + t.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
have rw₂ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + μ.withDensityᵥ (t.rnDeriv μ) + t.singularPart μ)
Tactic: rw [withDensityᵥ_add (integrable_rnDeriv s μ) (integrable_rnDeriv t μ), 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 μ
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 μ)
⊢ s + t = s.singularPart μ + t.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
have rw₃ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + (μ.withDensityᵥ (t.rnDeriv μ) + t.singularPart μ))
Tactic: rw [withDensityᵥ_add (integrable_rnDeriv s μ) (integrable_rnDeriv t μ), 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 μ
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 μ))
⊢ s + t = s.singularPart μ + t.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
have rw₄ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + (t.singularPart μ + μ.withDensityᵥ (t.rnDeriv μ)))
Tactic: rw [withDensityᵥ_add (integrable_rnDeriv s μ) (integrable_rnDeriv t μ), 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 μ
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 μ)))
⊢ s + t = s.singularPart μ + t.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
have rw₅ : s + t = s.singularPart μ + (μ.withDensityᵥ (s.rnDeriv μ) + t)
Tactic: rw [withDensityᵥ_add (integrable_rnDeriv s μ) (integrable_rnDeriv t μ), 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 μ
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)
⊢ s + t = s.singularPart μ + t.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
have rw₆ : s + t = s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) + t
Tactic: rw [withDensityᵥ_add (integrable_rnDeriv s μ) (integrable_rnDeriv t μ), 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 μ
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)
rw₆ : s + t = s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) + t
⊢ s + t = s.singularPart μ + t.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ + t.rnDeriv μ)
have rw₇ : s + t = s + t
Tactic: rw [withDensityᵥ_add (integrable_rnDeriv s μ) (integrable_rnDeriv t μ), 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 μ
⊢ (s - t).singularPart μ = s.singularPart μ - t.singularPart μ
have rw : (s + -t).singularPart μ = s.singularPart μ - t.singularPart μ
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, singularPart_add, singularPart_neg]
-- 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 μ
rw : (s + -t).singularPart μ = s.singularPart μ - t.singularPart μ
⊢ (s - t).singularPart μ = s.singularPart μ - t.singularPart μ
have rw₁ : (s + -t).singularPart μ = s.singularPart μ + -t.singularPart μ
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, singularPart_add, singularPart_neg]
-- 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 μ
rw : (s + -t).singularPart μ = s.singularPart μ - t.singularPart μ
rw₁ : (s + -t).singularPart μ = s.singularPart μ + -t.singularPart μ
⊢ (s - t).singularPart μ = s.singularPart μ - t.singularPart μ
have rw₂ : s.singularPart μ + (-t).singularPart μ = s.singularPart μ + -t.singularPart μ
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, singularPart_add, singularPart_neg]
-- 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 μ
rw : (s + -t).singularPart μ = s.singularPart μ - t.singularPart μ
rw₁ : (s + -t).singularPart μ = s.singularPart μ + -t.singularPart μ
rw₂ : s.singularPart μ + (-t).singularPart μ = s.singularPart μ + -t.singularPart μ
⊢ (s - t).singularPart μ = s.singularPart μ - t.singularPart μ
have rw₃ : s.singularPart μ + -t.singularPart μ = s.singularPart μ + -t.singularPart μ
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, singularPart_add, singularPart_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
f' : α → ℝ := AEStronglyMeasurable.mk f ⋯
⊢ s = t + μ.withDensityᵥ f'
have h : μ.withDensityᵥ f' = μ.withDensityᵥ f
Tactic: convert! hadd using 2
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
f' : α → ℝ := AEStronglyMeasurable.mk f ⋯
⊢ f =ᶠ[ae μ] s.rnDeriv μ
have hadd' : s = t + μ.withDensityᵥ f'
Tactic: have hadd' : s = t + μ.withDensityᵥ f' := by
    convert! hadd using 2
    exact WithDensityᵥEq.congr_ae hfi.1.ae_eq_mk.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
f' : α → ℝ := AEStronglyMeasurable.mk f ⋯
hadd' : s = t + μ.withDensityᵥ f'
⊢ f =ᶠ[ae μ] s.rnDeriv μ
have this : s.HaveLebesgueDecomposition μ
Tactic: have := haveLebesgueDecomposition_mk μ hfi.1.measurable_mk htμ hadd'
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
f' : α → ℝ := AEStronglyMeasurable.mk f ⋯
hadd' : s = t + μ.withDensityᵥ f'
this : s.HaveLebesgueDecomposition μ
⊢ f =ᶠ[ae μ] s.rnDeriv μ
have refine : μ.withDensityᵥ (s.rnDeriv μ) = μ.withDensityᵥ f
Tactic: refine (Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _) hfi ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
f' : α → ℝ := AEStronglyMeasurable.mk f ⋯
hadd' : s = t + μ.withDensityᵥ f'
this : s.HaveLebesgueDecomposition μ
⊢ μ.withDensityᵥ (s.rnDeriv μ) = μ.withDensityᵥ f
have rw : t + μ.withDensityᵥ (s.rnDeriv μ) = t + μ.withDensityᵥ f
Tactic: rw [← add_right_inj t, ← hadd, eq_singularPart _ f htμ hadd,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
f' : α → ℝ := AEStronglyMeasurable.mk f ⋯
hadd' : s = t + μ.withDensityᵥ f'
this : s.HaveLebesgueDecomposition μ
rw : t + μ.withDensityᵥ (s.rnDeriv μ) = t + μ.withDensityᵥ f
⊢ μ.withDensityᵥ (s.rnDeriv μ) = μ.withDensityᵥ f
have rw₁ : t + μ.withDensityᵥ (s.rnDeriv μ) = s
Tactic: rw [← add_right_inj t, ← hadd, eq_singularPart _ f htμ hadd,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
f' : α → ℝ := AEStronglyMeasurable.mk f ⋯
hadd' : s = t + μ.withDensityᵥ f'
this : s.HaveLebesgueDecomposition μ
rw : t + μ.withDensityᵥ (s.rnDeriv μ) = t + μ.withDensityᵥ f
rw₁ : t + μ.withDensityᵥ (s.rnDeriv μ) = s
⊢ μ.withDensityᵥ (s.rnDeriv μ) = μ.withDensityᵥ f
have rw₂ : s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = s
Tactic: rw [← add_right_inj t, ← hadd, eq_singularPart _ f htμ hadd,
    singularPart_add_withDensity_rnDeriv_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : SignedMeasure α
f : α → ℝ
hfi : Integrable f μ
htμ : t ⟂ᵥ μ.toENNRealVectorMeasure
hadd : s = t + μ.withDensityᵥ f
f' : α → ℝ := AEStronglyMeasurable.mk f ⋯
hadd' : s = t + μ.withDensityᵥ f'
this : s.HaveLebesgueDecomposition μ
rw : t + μ.withDensityᵥ (s.rnDeriv μ) = t + μ.withDensityᵥ f
rw₁ : t + μ.withDensityᵥ (s.rnDeriv μ) = s
rw₂ : s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = s
⊢ μ.withDensityᵥ (s.rnDeriv μ) = μ.withDensityᵥ f
have rw₃ : s = s
Tactic: rw [← add_right_inj t, ← hadd, eq_singularPart _ f htμ hadd,
    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 μ
⊢ (-s).rnDeriv μ =ᶠ[ae μ] -s.rnDeriv μ
have _ : μ.withDensityᵥ ((-s).rnDeriv μ) = μ.withDensityᵥ (-s.rnDeriv μ)
Tactic: refine
    Integrable.ae_eq_of_withDensityᵥ_eq (integrable_rnDeriv _ _) (integrable_rnDeriv _ _).neg ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
⊢ μ.withDensityᵥ ((-s).rnDeriv μ) = μ.withDensityᵥ (-s.rnDeriv μ)
have rw : μ.withDensityᵥ ((-s).rnDeriv μ) = -μ.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]