-- Mathlib/Analysis/Normed/Module/Ray.lean
theorem norm_sub (h : SameRay ℝ x y) : ‖x - y‖ = |‖x‖ - ‖y‖|

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
hab : b ≤ a
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|

Tactic:
rw [← sub_nonneg] at hab

Result:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
hab : 0 ≤ a - b
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|

Proof state:
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (b • u) (a • u)
H : ∀ (a b : ℝ), 0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
⊢ ‖b • u - a • u‖ = |‖b • u‖ - ‖a • u‖|

Tactic:
exact H b a hb ha h (le_of_not_le hab)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|

Tactic:
wlog hab : b ≤ a generalizing a b with H

Result:
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
H : ∀ (a b : ℝ), 0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|

E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
hab : b ≤ a
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|

Proof state:
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (b • u) (a • u)
H : ∀ (a b : ℝ), 0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|

Tactic:
rw [norm_sub_rev, abs_sub_comm]

Result:
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (b • u) (a • u)
H : ∀ (a b : ℝ), 0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
⊢ ‖b • u - a • u‖ = |‖b • u‖ - ‖a • u‖|

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x y : E
h : SameRay ℝ x y
⊢ ‖x - y‖ = |‖x‖ - ‖y‖|

Tactic:
rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
hab : 0 ≤ a - b
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|

Tactic:
rw [← sub_smul, norm_smul_of_nonneg hab, norm_smul_of_nonneg ha, norm_smul_of_nonneg hb, ←
  sub_mul, abs_of_nonneg (mul_nonneg hab (norm_nonneg _))]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
H : ∀ (a b : ℝ), 0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|

Tactic:
rw [SameRay.sameRay_comm] at h

Result:
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (b • u) (a • u)
H : ∀ (a b : ℝ), 0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|