case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.4436
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
⊢ ‖a • u - b • u‖ = abs (‖a • u‖ - ‖b • u‖)
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.4436
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : E
h : SameRay ℝ x y
⊢ ‖x - y‖ = abs (‖x‖ - ‖y‖)
rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.4436
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
H :
  ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type ?u.4436}
    [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (u : E) (a b : ℝ),
    0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = abs (‖a • u‖ - ‖b • u‖)
hab : ¬b ≤ a
⊢ ‖a • u - b • u‖ = abs (‖a • u‖ - ‖b • u‖)

E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.4436
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
hab : b ≤ a
⊢ ‖a • u - b • u‖ = abs (‖a • u‖ - ‖b • u‖)
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.4436
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
⊢ ‖a • u - b • u‖ = abs (‖a • u‖ - ‖b • u‖)
wlog hab : b ≤ a with H
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
hab✝ : b ≤ a
hab : 0 ≤ a - b
⊢ ‖a • u - b • u‖ = abs (‖a • u‖ - ‖b • u‖)
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
hab : b ≤ a
⊢ ‖a • u - b • u‖ = abs (‖a • u‖ - ‖b • u‖)
rw [← sub_nonneg] at hab
no goals
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
hab✝ : b ≤ a
hab : 0 ≤ a - b
⊢ ‖a • u - b • u‖ = abs (‖a • u‖ - ‖b • u‖)
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 _))]
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.4436
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (b • u) (a • u)
H :
  ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type ?u.4436}
    [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (u : E) (a b : ℝ),
    0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = abs (‖a • u‖ - ‖b • u‖)
hab : ¬b ≤ a
⊢ ‖a • u - b • u‖ = abs (‖a • u‖ - ‖b • u‖)
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.4436
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (a • u) (b • u)
H :
  ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type ?u.4436}
    [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (u : E) (a b : ℝ),
    0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = abs (‖a • u‖ - ‖b • u‖)
hab : ¬b ≤ a
⊢ ‖a • u - b • u‖ = abs (‖a • u‖ - ‖b • u‖)
rw [SameRay.sameRay_comm] at h
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.4436
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (b • u) (a • u)
H :
  ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type ?u.4436}
    [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (u : E) (a b : ℝ),
    0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = abs (‖a • u‖ - ‖b • u‖)
hab : ¬b ≤ a
⊢ ‖b • u - a • u‖ = abs (‖b • u‖ - ‖a • u‖)
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.4436
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (b • u) (a • u)
H :
  ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type ?u.4436}
    [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (u : E) (a b : ℝ),
    0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = abs (‖a • u‖ - ‖b • u‖)
hab : ¬b ≤ a
⊢ ‖a • u - b • u‖ = abs (‖a • u‖ - ‖b • u‖)
rw [norm_sub_rev, abs_sub_comm]
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (b • u) (a • u)
H :
  ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type}
    [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (u : E) (a b : ℝ),
    0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = abs (‖a • u‖ - ‖b • u‖)
hab : ¬b ≤ a
this :
  ∀ [inst : NormedAddCommGroup ℝ] [inst : NormedSpace ℝ ℝ] (u : E) (a b : ℝ),
    0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = abs (‖a • u‖ - ‖b • u‖)
⊢ ‖b • u - a • u‖ = abs (‖b • u‖ - ‖a • u‖)
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.4436
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (b • u) (a • u)
H :
  ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type ?u.4436}
    [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (u : E) (a b : ℝ),
    0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = abs (‖a • u‖ - ‖b • u‖)
hab : ¬b ≤ a
⊢ ‖b • u - a • u‖ = abs (‖b • u‖ - ‖a • u‖)
have := @H E _ _ ℝ
no goals
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
u : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
h : SameRay ℝ (b • u) (a • u)
H :
  ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type}
    [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] (u : E) (a b : ℝ),
    0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = abs (‖a • u‖ - ‖b • u‖)
hab : ¬b ≤ a
this :
  ∀ [inst : NormedAddCommGroup ℝ] [inst : NormedSpace ℝ ℝ] (u : E) (a b : ℝ),
    0 ≤ a → 0 ≤ b → SameRay ℝ (a • u) (b • u) → b ≤ a → ‖a • u - b • u‖ = abs (‖a • u‖ - ‖b • u‖)
⊢ ‖b • u - a • u‖ = abs (‖b • u‖ - ‖a • u‖)
exact this u b a hb ha h (le_of_not_le hab)