α : Type u_1
β : Type ?u.622814
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
h₁ :
  toSignedMeasure (Measure.singularPart (toJordanDecomposition (-s)).posPart μ) =
    toSignedMeasure (Measure.singularPart (toJordanDecomposition s).negPart μ)
⊢ singularPart (-s) μ = -singularPart s μ
α : Type u_1
β : Type ?u.622814
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
⊢ singularPart (-s) μ = -singularPart s μ
have h₁ :
  ((-s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure =
    (s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure := by
  refine' toSignedMeasure_congr _
  rw [toJordanDecomposition_neg, JordanDecomposition.neg_posPart]
α : Type u_1
β : Type ?u.622814
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
h₁ :
  toSignedMeasure (Measure.singularPart (toJordanDecomposition (-s)).posPart μ) =
    toSignedMeasure (Measure.singularPart (toJordanDecomposition s).negPart μ)
h₂ :
  toSignedMeasure (Measure.singularPart (toJordanDecomposition (-s)).negPart μ) =
    toSignedMeasure (Measure.singularPart (toJordanDecomposition s).posPart μ)
⊢ singularPart (-s) μ = -singularPart s μ
α : Type u_1
β : Type ?u.622814
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
h₁ :
  toSignedMeasure (Measure.singularPart (toJordanDecomposition (-s)).posPart μ) =
    toSignedMeasure (Measure.singularPart (toJordanDecomposition s).negPart μ)
⊢ singularPart (-s) μ = -singularPart s μ
have h₂ :
  ((-s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure =
    (s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure := by
  refine' toSignedMeasure_congr _
  rw [toJordanDecomposition_neg, JordanDecomposition.neg_negPart]
no goals
α : Type u_1
β : Type ?u.622814
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
h₁ :
  toSignedMeasure (Measure.singularPart (toJordanDecomposition (-s)).posPart μ) =
    toSignedMeasure (Measure.singularPart (toJordanDecomposition s).negPart μ)
h₂ :
  toSignedMeasure (Measure.singularPart (toJordanDecomposition (-s)).negPart μ) =
    toSignedMeasure (Measure.singularPart (toJordanDecomposition s).posPart μ)
⊢ singularPart (-s) μ = -singularPart s μ
rw [singularPart, singularPart, neg_sub, h₁, h₂]
α : Type u_1
β : Type ?u.622814
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
⊢ Measure.singularPart (toJordanDecomposition (-s)).posPart μ = Measure.singularPart (toJordanDecomposition s).negPart μ
α : Type u_1
β : Type ?u.622814
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
⊢ toSignedMeasure (Measure.singularPart (toJordanDecomposition (-s)).posPart μ) =
    toSignedMeasure (Measure.singularPart (toJordanDecomposition s).negPart μ)
refine' toSignedMeasure_congr _
no goals
α : Type u_1
β : Type ?u.622814
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
⊢ Measure.singularPart (toJordanDecomposition (-s)).posPart μ = Measure.singularPart (toJordanDecomposition s).negPart μ
rw [toJordanDecomposition_neg, JordanDecomposition.neg_posPart]
α : Type u_1
β : Type ?u.622814
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
h₁ :
  toSignedMeasure (Measure.singularPart (toJordanDecomposition (-s)).posPart μ) =
    toSignedMeasure (Measure.singularPart (toJordanDecomposition s).negPart μ)
⊢ Measure.singularPart (toJordanDecomposition (-s)).negPart μ = Measure.singularPart (toJordanDecomposition s).posPart μ
α : Type u_1
β : Type ?u.622814
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
h₁ :
  toSignedMeasure (Measure.singularPart (toJordanDecomposition (-s)).posPart μ) =
    toSignedMeasure (Measure.singularPart (toJordanDecomposition s).negPart μ)
⊢ toSignedMeasure (Measure.singularPart (toJordanDecomposition (-s)).negPart μ) =
    toSignedMeasure (Measure.singularPart (toJordanDecomposition s).posPart μ)
refine' toSignedMeasure_congr _
no goals
α : Type u_1
β : Type ?u.622814
m : MeasurableSpace α
μ✝ ν : Measure α
s✝ t s : SignedMeasure α
μ : Measure α
h₁ :
  toSignedMeasure (Measure.singularPart (toJordanDecomposition (-s)).posPart μ) =
    toSignedMeasure (Measure.singularPart (toJordanDecomposition s).negPart μ)
⊢ Measure.singularPart (toJordanDecomposition (-s)).negPart μ = Measure.singularPart (toJordanDecomposition s).posPart μ
rw [toJordanDecomposition_neg, JordanDecomposition.neg_negPart]