no goals
α : Type u_1
β : Type ?u.86482
inst✝ : MeasurableSpace α
s : SignedMeasure α
j : JordanDecomposition α
h : s = toSignedMeasure j
⊢ toJordanDecomposition s = j
rw [h, toJordanDecomposition_toSignedMeasure]