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 : ℝ≥0
a : (r • s).toJordanDecomposition.negPart.singularPart μ
| ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
have a₁ : r • s.toJordanDecomposition.negPart.singularPart μ
Tactic: · congr
      rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
have a : ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure
Tactic: congr
    · congr
      · rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart, singularPart_smul]
    · congr
      rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
a : ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
have a₁ : ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
Tactic: congr
    · congr
      · rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart, singularPart_smul]
    · congr
      rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
⊢ ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    (r • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (r • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
have conv_lhs : ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
  (r • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    (r • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
Tactic: conv_lhs =>
    congr
    · congr
      · rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart, singularPart_smul]
    · congr
      rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ≥0
conv_lhs :
  ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    (r • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (r • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
⊢ ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    (r • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      (r • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
have conv_lhs₁ : (r • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    (r • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
  (r • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    (r • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
Tactic: conv_lhs =>
    congr
    · congr
      · rw [toJordanDecomposition_smul, JordanDecomposition.smul_posPart, singularPart_smul]
    · congr
      rw [toJordanDecomposition_smul, JordanDecomposition.smul_negPart, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : 0 ≤ r
⊢ (r • s).singularPart μ = r • s.singularPart μ
have inl : ∀ (r : ℝ≥0), ((↑r : ℝ) • s).singularPart μ = (↑r : ℝ) • s.singularPart μ
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 α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
have a : ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
a : ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
have a₁ : ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure
have a : (r • s).toJordanDecomposition.posPart.singularPart μ
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
| (r • s).toJordanDecomposition.posPart.singularPart μ
have a : (-r).toNNReal • s.toJordanDecomposition.negPart.singularPart μ
Tactic: rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_posPart_neg _ _ hr, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
| (r • s).toJordanDecomposition.posPart.singularPart μ
have a : (r • s.toJordanDecomposition).posPart.singularPart μ
Tactic: · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_posPart_neg _ _ hr, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
a : (r • s.toJordanDecomposition).posPart.singularPart μ
| (r • s).toJordanDecomposition.posPart.singularPart μ
have a₁ : ((-r).toNNReal • s.toJordanDecomposition.negPart).singularPart μ
Tactic: · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_posPart_neg _ _ hr, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
a : (r • s.toJordanDecomposition).posPart.singularPart μ
a₁ : ((-r).toNNReal • s.toJordanDecomposition.negPart).singularPart μ
| (r • s).toJordanDecomposition.posPart.singularPart μ
have a₂ : (-r).toNNReal • s.toJordanDecomposition.negPart.singularPart μ
Tactic: · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_posPart_neg _ _ hr, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure
have a : (r • s).toJordanDecomposition.posPart.singularPart μ
Tactic: congr
        · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_posPart_neg _ _ hr, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
| ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
have a : (r • s).toJordanDecomposition.negPart.singularPart μ
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
| (r • s).toJordanDecomposition.negPart.singularPart μ
have a : (-r).toNNReal • s.toJordanDecomposition.posPart.singularPart μ
Tactic: rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_negPart_neg _ _ hr, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
| (r • s).toJordanDecomposition.negPart.singularPart μ
have a : (r • s.toJordanDecomposition).negPart.singularPart μ
Tactic: · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_negPart_neg _ _ hr, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
a : (r • s.toJordanDecomposition).negPart.singularPart μ
| (r • s).toJordanDecomposition.negPart.singularPart μ
have a₁ : ((-r).toNNReal • s.toJordanDecomposition.posPart).singularPart μ
Tactic: · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_negPart_neg _ _ hr, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
a : (r • s.toJordanDecomposition).negPart.singularPart μ
a₁ : ((-r).toNNReal • s.toJordanDecomposition.posPart).singularPart μ
| (r • s).toJordanDecomposition.negPart.singularPart μ
have a₂ : (-r).toNNReal • s.toJordanDecomposition.posPart.singularPart μ
Tactic: · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_negPart_neg _ _ hr, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
| ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
have a : (r • s).toJordanDecomposition.negPart.singularPart μ
Tactic: congr
        · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_negPart_neg _ _ hr, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
| ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
have a : (r • s).toJordanDecomposition.negPart.singularPart μ
Tactic: · congr
        · rw [toJordanDecomposition_smul_real,
            JordanDecomposition.real_smul_negPart_neg _ _ hr, singularPart_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
have a : ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure
Tactic: 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
a : ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure
| ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
    ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
have a₁ : ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
Tactic: 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
⊢ ((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
      ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    r •
      ((s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure -
        (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure)
have 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)
Tactic: 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
r : ℝ
hr : r < 0
⊢ ((-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.negPart.singularPart μ).toSignedMeasure -
    ((-r).toNNReal • s.toJordanDecomposition.posPart.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)
⊢ ((-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.negPart.singularPart μ).toSignedMeasure -
    (-r).toNNReal • (s.toJordanDecomposition.posPart.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)
⊢ ((-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 -
      (-r).toNNReal • (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)
⊢ ((-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)
⊢ ((-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]