-- Mathlib/MeasureTheory/Decomposition/SignedLebesgue.lean
theorem singularPart_neg (s : SignedMeasure α) (μ : Measure α) :
    (-s).singularPart μ = -s.singularPart μ

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ (-s).toJordanDecomposition.posPart.singularPart μ = s.toJordanDecomposition.negPart.singularPart μ

Tactic:
rw [toJordanDecomposition_neg, JordanDecomposition.neg_posPart]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h₁ :
  ((-s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
⊢ (-s).singularPart μ = -s.singularPart μ

Tactic:
have h₂ :
  ((-s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure := by
  refine toSignedMeasure_congr ?_
  rw [toJordanDecomposition_neg, JordanDecomposition.neg_negPart]

Result:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h₁ :
  ((-s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
h₂ :
  ((-s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure
⊢ (-s).singularPart μ = -s.singularPart μ

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h₁ :
  ((-s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
⊢ ((-s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure

Tactic:
refine toSignedMeasure_congr ?_

Result:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h₁ :
  ((-s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
⊢ (-s).toJordanDecomposition.negPart.singularPart μ = s.toJordanDecomposition.posPart.singularPart μ

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h₁ :
  ((-s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
h₂ :
  ((-s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure
⊢ (-s).singularPart μ = -s.singularPart μ

Tactic:
rw [singularPart, singularPart, neg_sub, h₁, h₂]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h₁ :
  ((-s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
⊢ (-s).toJordanDecomposition.negPart.singularPart μ = s.toJordanDecomposition.posPart.singularPart μ

Tactic:
rw [toJordanDecomposition_neg, JordanDecomposition.neg_negPart]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ (-s).singularPart μ = -s.singularPart μ

Tactic:
have h₁ :
  ((-s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure := by
  refine toSignedMeasure_congr ?_
  rw [toJordanDecomposition_neg, JordanDecomposition.neg_posPart]

Result:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
h₁ :
  ((-s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
⊢ (-s).singularPart μ = -s.singularPart μ

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ ((-s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure

Tactic:
refine toSignedMeasure_congr ?_

Result:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
μ : Measure α
⊢ (-s).toJordanDecomposition.posPart.singularPart μ = s.toJordanDecomposition.negPart.singularPart μ