case pos
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : 0 ≤ r
⊢ toJordanDecomposition (r • s) = r • toJordanDecomposition s

case neg
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ toJordanDecomposition (r • s) = r • toJordanDecomposition s
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
⊢ toJordanDecomposition (r • s) = r • toJordanDecomposition s
by_cases hr : 0 ≤ r
no goals
case pos
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : 0 ≤ r
⊢ toJordanDecomposition (r • s) = r • toJordanDecomposition s
exact toJordanDecomposition_smul_real_nonneg s r hr
case neg.posPart
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ (toJordanDecomposition (r • s)).posPart = (r • toJordanDecomposition s).posPart

case neg.negPart
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ (toJordanDecomposition (r • s)).negPart = (r • toJordanDecomposition s).negPart
case neg
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ toJordanDecomposition (r • s) = r • toJordanDecomposition s
ext1
case neg.posPart.hr
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ 0 ≤ -r

case neg.posPart.hr
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ 0 ≤ -r
case neg.posPart
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ (toJordanDecomposition (r • s)).posPart = (r • toJordanDecomposition s).posPart
rw [real_smul_posPart_neg _ _ (not_le.1 hr),
  show r • s = -(-r • s) by rw [neg_smul, neg_neg], toJordanDecomposition_neg, neg_posPart,
  toJordanDecomposition_smul_real_nonneg, ← smul_negPart, real_smul_nonneg]
no goals
case neg.posPart.hr
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ 0 ≤ -r

case neg.posPart.hr
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ 0 ≤ -r
all_goals exact Left.nonneg_neg_iff.2 (le_of_lt (not_le.1 hr))
no goals
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ r • s = -(-r • s)
rw [neg_smul, neg_neg]
no goals
case neg.posPart.hr
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ 0 ≤ -r
exact Left.nonneg_neg_iff.2 (le_of_lt (not_le.1 hr))
case neg.negPart.hr
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ 0 ≤ -r

case neg.negPart.hr
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ 0 ≤ -r
case neg.negPart
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ (toJordanDecomposition (r • s)).negPart = (r • toJordanDecomposition s).negPart
rw [real_smul_negPart_neg _ _ (not_le.1 hr),
  show r • s = -(-r • s) by rw [neg_smul, neg_neg], toJordanDecomposition_neg, neg_negPart,
  toJordanDecomposition_smul_real_nonneg, ← smul_posPart, real_smul_nonneg]
no goals
case neg.negPart.hr
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ 0 ≤ -r

case neg.negPart.hr
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ 0 ≤ -r
all_goals exact Left.nonneg_neg_iff.2 (le_of_lt (not_le.1 hr))
no goals
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ r • s = -(-r • s)
rw [neg_smul, neg_neg]
no goals
case neg.negPart.hr
α : Type u_1
β : Type ?u.79282
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ 0 ≤ -r
exact Left.nonneg_neg_iff.2 (le_of_lt (not_le.1 hr))