case h
α : Type u_1
β : Type ?u.19420
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ ↑(toSignedMeasure (r • j)) i = ↑(r • toSignedMeasure j) i
α : Type u_1
β : Type ?u.19420
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
⊢ toSignedMeasure (r • j) = r • toSignedMeasure j
ext1 i hi
no goals
case h
α : Type u_1
β : Type ?u.19420
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ≥0
i : Set α
hi : MeasurableSet i
⊢ ↑(toSignedMeasure (r • j)) i = ↑(r • toSignedMeasure j) i
rw [VectorMeasure.smul_apply, toSignedMeasure, toSignedMeasure,
  toSignedMeasure_sub_apply hi, toSignedMeasure_sub_apply hi, smul_sub, smul_posPart,
  smul_negPart, ← ENNReal.toReal_smul, ← ENNReal.toReal_smul, smul_toOuterMeasure,
  OuterMeasure.coe_smul, Pi.smul_apply, smul_toOuterMeasure, OuterMeasure.coe_smul, Pi.smul_apply]