[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.239
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : E
h : SameRay ℝ x y
⊢ ‖x + y‖ = ‖x‖ + ‖y‖
[PROOFSTEP]
rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.239
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‖ = ‖a • u‖ + ‖b • u‖
[PROOFSTEP]
rw [← add_smul, norm_smul_of_nonneg (add_nonneg ha hb), norm_smul_of_nonneg ha, norm_smul_of_nonneg hb, add_mul]
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.3876
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : E
h : SameRay ℝ x y
⊢ ‖x - y‖ = |‖x‖ - ‖y‖|
[PROOFSTEP]
rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.3876
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‖ = |‖a • u‖ - ‖b • u‖|
[PROOFSTEP]
wlog hab : b ≤ a with H
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.3876
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.3876}
    [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‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
[PROOFSTEP]
rw [SameRay.sameRay_comm] at h 
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.3876
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.3876}
    [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‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
⊢ ‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
[PROOFSTEP]
rw [norm_sub_rev, abs_sub_comm]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.3876
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.3876}
    [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‖ = |‖a • u‖ - ‖b • u‖|
hab : ¬b ≤ a
⊢ ‖b • u - a • u‖ = |‖b • u‖ - ‖a • u‖|
[PROOFSTEP]
have := @H E _ _ ℝ
[GOAL]
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‖ = |‖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‖ = |‖a • u‖ - ‖b • u‖|
⊢ ‖b • u - a • u‖ = |‖b • u‖ - ‖a • u‖|
[PROOFSTEP]
exact this u b a hb ha h (le_of_not_le hab)
[GOAL]
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‖ = |‖a • u‖ - ‖b • u‖|
[PROOFSTEP]
rw [← sub_nonneg] at hab 
[GOAL]
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‖ = |‖a • u‖ - ‖b • u‖|
[PROOFSTEP]
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 _))]
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.8734
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : E
h : SameRay ℝ x y
⊢ ‖x‖ • y = ‖y‖ • x
[PROOFSTEP]
rcases h.exists_eq_smul with ⟨u, a, b, ha, hb, -, rfl, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.8734
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 = ‖b • u‖ • a • u
[PROOFSTEP]
simp only [norm_smul_of_nonneg, *, mul_smul]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.8734
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 = b • ‖u‖ • a • u
[PROOFSTEP]
rw [smul_comm, smul_comm b, smul_comm a b u]
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
⊢ Set.InjOn Norm.norm {y | SameRay ℝ x y}
[PROOFSTEP]
rintro y hy z hz h
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y✝ : F
hx : x ≠ 0
y : F
hy : y ∈ {y | SameRay ℝ x y}
z : F
hz : z ∈ {y | SameRay ℝ x y}
h : ‖y‖ = ‖z‖
⊢ y = z
[PROOFSTEP]
rcases hy.exists_nonneg_left hx with ⟨r, hr, rfl⟩
[GOAL]
case intro.intro
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
z : F
hz : z ∈ {y | SameRay ℝ x y}
r : ℝ
hr : 0 ≤ r
hy : r • x ∈ {y | SameRay ℝ x y}
h : ‖r • x‖ = ‖z‖
⊢ r • x = z
[PROOFSTEP]
rcases hz.exists_nonneg_left hx with ⟨s, hs, rfl⟩
[GOAL]
case intro.intro.intro.intro
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
r : ℝ
hr : 0 ≤ r
hy : r • x ∈ {y | SameRay ℝ x y}
s : ℝ
hs : 0 ≤ s
hz : s • x ∈ {y | SameRay ℝ x y}
h : ‖r • x‖ = ‖s • x‖
⊢ r • x = s • x
[PROOFSTEP]
rw [norm_smul, norm_smul, mul_left_inj' (norm_ne_zero_iff.2 hx), norm_of_nonneg hr, norm_of_nonneg hs] at h 
[GOAL]
case intro.intro.intro.intro
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
r : ℝ
hr : 0 ≤ r
hy : r • x ∈ {y | SameRay ℝ x y}
s : ℝ
hs : 0 ≤ s
hz : s • x ∈ {y | SameRay ℝ x y}
h : r = s
⊢ r • x = s • x
[PROOFSTEP]
rw [h]
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hy : y ≠ 0
⊢ Set.InjOn Norm.norm {x | SameRay ℝ x y}
[PROOFSTEP]
simpa only [SameRay.sameRay_comm] using norm_injOn_ray_left hy
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
[PROOFSTEP]
rw [inv_smul_eq_iff₀, smul_comm, eq_comm, inv_smul_eq_iff₀, sameRay_iff_norm_smul_eq]
[GOAL]
case ha
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖y‖ ≠ 0
[PROOFSTEP]
rwa [norm_ne_zero_iff]
[GOAL]
case ha
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x‖ ≠ 0
[PROOFSTEP]
rwa [norm_ne_zero_iff]
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx)
[GOAL]
case inl
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
y : F
⊢ SameRay ℝ 0 y ↔ 0 = 0 ∨ y = 0 ∨ ‖0‖⁻¹ • 0 = ‖y‖⁻¹ • y
[PROOFSTEP]
simp [SameRay.zero_left]
[GOAL]
case inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
[PROOFSTEP]
rcases eq_or_ne y 0 with (rfl | hy)
[GOAL]
case inr.inl
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
hx : x ≠ 0
⊢ SameRay ℝ x 0 ↔ x = 0 ∨ 0 = 0 ∨ ‖x‖⁻¹ • x = ‖0‖⁻¹ • 0
[PROOFSTEP]
simp [SameRay.zero_right]
[GOAL]
case inr.inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
[PROOFSTEP]
simp only [sameRay_iff_inv_norm_smul_eq_of_ne hx hy, *, false_or_iff]
[GOAL]
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
h : ‖x‖ = ‖y‖
⊢ SameRay ℝ x y ↔ x = y
[PROOFSTEP]
obtain rfl | hy := eq_or_ne y 0
[GOAL]
case inl
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
h : ‖x‖ = ‖0‖
⊢ SameRay ℝ x 0 ↔ x = 0
[PROOFSTEP]
rw [norm_zero, norm_eq_zero] at h 
[GOAL]
case inl
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
h : x = 0
⊢ SameRay ℝ x 0 ↔ x = 0
[PROOFSTEP]
exact iff_of_true (SameRay.zero_right _) h
[GOAL]
case inr
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
h : ‖x‖ = ‖y‖
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = y
[PROOFSTEP]
exact ⟨fun hxy => norm_injOn_ray_right hy hxy SameRay.rfl h, fun hxy => hxy ▸ SameRay.rfl⟩
