-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem toJordanDecomposition_smul_real (s : SignedMeasure α) (r : ℝ) :
    (r • s).toJordanDecomposition = r • s.toJordanDecomposition

Proof state:
case neg.negPart.hr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ 0 ≤ -r

case neg.negPart.hr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ 0 ≤ -r

Tactic:
all_goals exact Left.nonneg_neg_iff.2 (le_of_lt (not_le.1 hr))

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ r • s = -(-r • s)

Tactic:
rw [neg_smul, neg_neg]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition

Tactic:
ext1

Result:
case neg.posPart
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ (r • s).toJordanDecomposition.posPart = (r • s.toJordanDecomposition).posPart

case neg.negPart
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ (r • s).toJordanDecomposition.negPart = (r • s.toJordanDecomposition).negPart

Proof state:
case neg.posPart.hr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ 0 ≤ -r

case neg.posPart.hr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ 0 ≤ -r

Tactic:
all_goals exact Left.nonneg_neg_iff.2 (le_of_lt (not_le.1 hr))

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : 0 ≤ r
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition

Tactic:
exact toJordanDecomposition_smul_real_nonneg s r hr

Result:
no goals

Proof state:
case neg.posPart.hr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ 0 ≤ -r

Tactic:
exact Left.nonneg_neg_iff.2 (le_of_lt (not_le.1 hr))

Result:
no goals

Proof state:
case neg.posPart
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ (r • s).toJordanDecomposition.posPart = (r • s.toJordanDecomposition).posPart

Tactic:
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]

Result:
case neg.posPart.hr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ 0 ≤ -r

case neg.posPart.hr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ 0 ≤ -r

Proof state:
case neg.negPart.hr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ 0 ≤ -r

Tactic:
exact Left.nonneg_neg_iff.2 (le_of_lt (not_le.1 hr))

Result:
no goals

Proof state:
case neg.negPart
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ (r • s).toJordanDecomposition.negPart = (r • s.toJordanDecomposition).negPart

Tactic:
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]

Result:
case neg.negPart.hr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ 0 ≤ -r

case neg.negPart.hr
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ 0 ≤ -r

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition

Tactic:
by_cases hr : 0 ≤ r

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

case neg
α : Type u_1
inst✝ : MeasurableSpace α
s : SignedMeasure α
r : ℝ
hr : ¬0 ≤ r
⊢ (r • s).toJordanDecomposition = r • s.toJordanDecomposition