awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ (r • s).toJordanDecomposition.posPart.HaveLebesgueDecomposition μ
have rw : (r • s.toJordanDecomposition.posPart).HaveLebesgueDecomposition μ
Tactic: rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ≥0
⊢ (r • s).toJordanDecomposition.negPart.HaveLebesgueDecomposition μ
have rw : (r • s.toJordanDecomposition.negPart).HaveLebesgueDecomposition μ
Tactic: rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
⊢ (r • s).HaveLebesgueDecomposition μ
have pos : ∀ (hr : 0 ≤ r), (r • s).HaveLebesgueDecomposition μ
Tactic: by_cases! hr : 0 ≤ r
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
pos : ∀ (hr : 0 ≤ r), (r • s).HaveLebesgueDecomposition μ
⊢ (r • s).HaveLebesgueDecomposition μ
have neg : ∀ (hr : r < 0), (r • s).HaveLebesgueDecomposition μ
Tactic: by_cases! hr : 0 ≤ r
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
hr : 0 ≤ r
⊢ (r • s).HaveLebesgueDecomposition μ
have pos : ∀ (r : ℝ≥0), ((↑r : ℝ) • s).HaveLebesgueDecomposition μ
Tactic: lift r to ℝ≥0 using hr
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
hr : r < 0
⊢ (r • s).toJordanDecomposition.posPart.HaveLebesgueDecomposition μ
have rw : ((-r).toNNReal • s.toJordanDecomposition.negPart).HaveLebesgueDecomposition μ
Tactic: rw [toJordanDecomposition_smul_real, JordanDecomposition.real_smul_posPart_neg _ _ hr]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ_1 : Measure α
s : SignedMeasure α
μ : Measure α
inst : s.HaveLebesgueDecomposition μ
r : ℝ
hr : r < 0
⊢ (r • s).toJordanDecomposition.negPart.HaveLebesgueDecomposition μ
have rw : ((-r).toNNReal • s.toJordanDecomposition.posPart).HaveLebesgueDecomposition μ
Tactic: rw [toJordanDecomposition_smul_real, JordanDecomposition.real_smul_negPart_neg _ _ hr]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ (s.singularPart μ).toJordanDecomposition =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
      negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
      mutuallySingular := ⋯ }
have refine : (s.singularPart μ).toJordanDecomposition.toSignedMeasure =
  { posPart := s.toJordanDecomposition.posPart.singularPart μ,
      negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := sorry, negPart_finite := sorry,
      mutuallySingular := sorry }.toSignedMeasure
Tactic: refine JordanDecomposition.toSignedMeasure_injective ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ (s.singularPart μ).toJordanDecomposition.toSignedMeasure =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
        negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
        mutuallySingular := ⋯ }.toSignedMeasure
have rw : s.singularPart μ =
  { posPart := s.toJordanDecomposition.posPart.singularPart μ,
      negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := sorry, negPart_finite := sorry,
      mutuallySingular := sorry }.toSignedMeasure
Tactic: rw [toSignedMeasure_toJordanDecomposition, singularPart, JordanDecomposition.toSignedMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
rw :
  s.singularPart μ =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
        negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
        mutuallySingular := ⋯ }.toSignedMeasure
⊢ (s.singularPart μ).toJordanDecomposition.toSignedMeasure =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
        negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
        mutuallySingular := ⋯ }.toSignedMeasure
have rw₁ : (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
  { posPart := s.toJordanDecomposition.posPart.singularPart μ,
      negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := sorry, negPart_finite := sorry,
      mutuallySingular := sorry }.toSignedMeasure
Tactic: rw [toSignedMeasure_toJordanDecomposition, singularPart, JordanDecomposition.toSignedMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
rw :
  s.singularPart μ =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
        negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
        mutuallySingular := ⋯ }.toSignedMeasure
rw₁ :
  (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
        negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
        mutuallySingular := ⋯ }.toSignedMeasure
⊢ (s.singularPart μ).toJordanDecomposition.toSignedMeasure =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
        negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
        mutuallySingular := ⋯ }.toSignedMeasure
have rw₂ : (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
  { posPart := s.toJordanDecomposition.posPart.singularPart μ,
          negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := sorry, negPart_finite := sorry,
          mutuallySingular := sorry : JordanDecomposition α }.posPart.toSignedMeasure -
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
          negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := sorry, negPart_finite := sorry,
          mutuallySingular := sorry : JordanDecomposition α }.negPart.toSignedMeasure
Tactic: rw [toSignedMeasure_toJordanDecomposition, singularPart, JordanDecomposition.toSignedMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ (s.singularPart μ).totalVariation =
    s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ
have this : (s.singularPart μ).toJordanDecomposition =
  { posPart := s.toJordanDecomposition.posPart.singularPart μ,
    negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := sorry, negPart_finite := sorry,
    mutuallySingular := sorry }
Tactic: have :
    (s.singularPart μ).toJordanDecomposition =
      ⟨s.toJordanDecomposition.posPart.singularPart μ,
        s.toJordanDecomposition.negPart.singularPart μ, singularPart_mutuallySingular s μ⟩ := by
    refine JordanDecomposition.toSignedMeasure_injective ?_
    rw [toSignedMeasure_toJordanDecomposition, singularPart, JordanDecomposition.toSignedMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
this :
  (s.singularPart μ).toJordanDecomposition =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
      negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
      mutuallySingular := ⋯ }
⊢ (s.singularPart μ).totalVariation =
    s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ
have rw : (s.singularPart μ).toJordanDecomposition.posPart + (s.singularPart μ).toJordanDecomposition.negPart =
  s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ
Tactic: rw [totalVariation, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
this :
  (s.singularPart μ).toJordanDecomposition =
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
      negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := ⋯, negPart_finite := ⋯,
      mutuallySingular := ⋯ }
rw :
  (s.singularPart μ).toJordanDecomposition.posPart + (s.singularPart μ).toJordanDecomposition.negPart =
    s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ
⊢ (s.singularPart μ).totalVariation =
    s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ
have rw₁ : { posPart := s.toJordanDecomposition.posPart.singularPart μ, negPart := s.toJordanDecomposition.negPart.singularPart μ,
        posPart_finite := sorry, negPart_finite := sorry, mutuallySingular := sorry : JordanDecomposition α }.posPart +
    { posPart := s.toJordanDecomposition.posPart.singularPart μ,
        negPart := s.toJordanDecomposition.negPart.singularPart μ, posPart_finite := sorry, negPart_finite := sorry,
        mutuallySingular := sorry : JordanDecomposition α }.negPart =
  s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ
Tactic: rw [totalVariation, this]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ s.singularPart μ ⟂ᵥ μ.toENNRealVectorMeasure
have rw : s.toJordanDecomposition.posPart.singularPart μ + s.toJordanDecomposition.negPart.singularPart μ ⟂ₘ μ
Tactic: rw [mutuallySingular_ennreal_iff, singularPart_totalVariation,
    VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Integrable (s.rnDeriv μ) μ
have refine_1 : Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ
Tactic: refine Integrable.sub ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
refine_1 : Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ
⊢ Integrable (s.rnDeriv μ) μ
have refine_2 : Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ
Tactic: refine Integrable.sub ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ
have refine_1 : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
refine_1 : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ
have refine_1₁ : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal) μ
have refine_1 : Measurable (β := ℝ) fun (x : α) ↦ (s.toJordanDecomposition.posPart.rnDeriv μ x).toReal
Tactic: apply Measurable.aestronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ
have refine_2 : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
refine_2 : AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ
⊢ Integrable (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ
have refine_2₁ : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal) μ
have refine_2 : Measurable (β := ℝ) fun (x : α) ↦ (s.toJordanDecomposition.negPart.rnDeriv μ x).toReal
Tactic: apply Measurable.aestronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
| s
have rw : s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
Tactic: rw [← toSignedMeasure_toJordanDecomposition s, JordanDecomposition.toSignedMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = s
have conv_rhs : s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) =
  s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
Tactic: conv_rhs =>
    rw [← toSignedMeasure_toJordanDecomposition s, JordanDecomposition.toSignedMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
have rw : (s.toJordanDecomposition.posPart.singularPart μ +
        μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)).toSignedMeasure -
    (μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ) +
        s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
  s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
Tactic: rw [singularPart, rnDeriv_def,
    withDensityᵥ_sub' (integrable_toReal_of_lintegral_ne_top _ _)
      (integrable_toReal_of_lintegral_ne_top _ _),
    withDensityᵥ_toReal, withDensityᵥ_toReal, sub_eq_add_neg, sub_eq_add_neg,
    add_comm (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure, ← add_assoc,
    add_assoc (-(s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure),
    ← toSignedMeasure_add, add_comm, ← add_assoc, ← neg_add, ← toSignedMeasure_add, add_comm,
    ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
rw :
  (s.toJordanDecomposition.posPart.singularPart μ +
          μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)).toSignedMeasure -
      (μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ) +
          s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
⊢ s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
have hfm : AEMeasurable (s.toJordanDecomposition.negPart.rnDeriv μ) μ
Tactic: rw [singularPart, rnDeriv_def,
    withDensityᵥ_sub' (integrable_toReal_of_lintegral_ne_top _ _)
      (integrable_toReal_of_lintegral_ne_top _ _),
    withDensityᵥ_toReal, withDensityᵥ_toReal, sub_eq_add_neg, sub_eq_add_neg,
    add_comm (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure, ← add_assoc,
    add_assoc (-(s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure),
    ← toSignedMeasure_add, add_comm, ← add_assoc, ← neg_add, ← toSignedMeasure_add, add_comm,
    ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
rw :
  (s.toJordanDecomposition.posPart.singularPart μ +
          μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)).toSignedMeasure -
      (μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ) +
          s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
hfm : AEMeasurable (s.toJordanDecomposition.negPart.rnDeriv μ) μ
⊢ s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
have hf : ∫⁻ (x : α), s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ∞
Tactic: rw [singularPart, rnDeriv_def,
    withDensityᵥ_sub' (integrable_toReal_of_lintegral_ne_top _ _)
      (integrable_toReal_of_lintegral_ne_top _ _),
    withDensityᵥ_toReal, withDensityᵥ_toReal, sub_eq_add_neg, sub_eq_add_neg,
    add_comm (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure, ← add_assoc,
    add_assoc (-(s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure),
    ← toSignedMeasure_add, add_comm, ← add_assoc, ← neg_add, ← toSignedMeasure_add, add_comm,
    ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
rw :
  (s.toJordanDecomposition.posPart.singularPart μ +
          μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)).toSignedMeasure -
      (μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ) +
          s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
hfm : AEMeasurable (s.toJordanDecomposition.negPart.rnDeriv μ) μ
hf : ∫⁻ (x : α), s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ∞
⊢ s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
have hfm₁ : AEMeasurable (s.toJordanDecomposition.posPart.rnDeriv μ) μ
Tactic: rw [singularPart, rnDeriv_def,
    withDensityᵥ_sub' (integrable_toReal_of_lintegral_ne_top _ _)
      (integrable_toReal_of_lintegral_ne_top _ _),
    withDensityᵥ_toReal, withDensityᵥ_toReal, sub_eq_add_neg, sub_eq_add_neg,
    add_comm (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure, ← add_assoc,
    add_assoc (-(s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure),
    ← toSignedMeasure_add, add_comm, ← add_assoc, ← neg_add, ← toSignedMeasure_add, add_comm,
    ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
rw :
  (s.toJordanDecomposition.posPart.singularPart μ +
          μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)).toSignedMeasure -
      (μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ) +
          s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
hfm : AEMeasurable (s.toJordanDecomposition.negPart.rnDeriv μ) μ
hf : ∫⁻ (x : α), s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ∞
hfm₁ : AEMeasurable (s.toJordanDecomposition.posPart.rnDeriv μ) μ
⊢ s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
have hf₁ : ∫⁻ (x : α), s.toJordanDecomposition.posPart.rnDeriv μ x ∂μ ≠ ∞
Tactic: rw [singularPart, rnDeriv_def,
    withDensityᵥ_sub' (integrable_toReal_of_lintegral_ne_top _ _)
      (integrable_toReal_of_lintegral_ne_top _ _),
    withDensityᵥ_toReal, withDensityᵥ_toReal, sub_eq_add_neg, sub_eq_add_neg,
    add_comm (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure, ← add_assoc,
    add_assoc (-(s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure),
    ← toSignedMeasure_add, add_comm, ← add_assoc, ← neg_add, ← toSignedMeasure_add, add_comm,
    ← sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
⊢ (s.toJordanDecomposition.posPart.singularPart μ +
          μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)).toSignedMeasure -
      (μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ) +
          s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
have h : s.toJordanDecomposition.posPart =
  s.toJordanDecomposition.posPart.singularPart μ + μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)
Tactic: convert! rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : SignedMeasure α
inst : s.HaveLebesgueDecomposition μ
h :
  s.toJordanDecomposition.posPart =
    s.toJordanDecomposition.posPart.singularPart μ + μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)
⊢ (s.toJordanDecomposition.posPart.singularPart μ +
          μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)).toSignedMeasure -
      (μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ) +
          s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
have h₁ : s.toJordanDecomposition.negPart =
  μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ) + s.toJordanDecomposition.negPart.singularPart μ
Tactic: convert! rfl