case inl
E : Type ?u.245331
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
h : ‖x‖ = ‖0‖
⊢ SameRay ℝ x 0 ↔ x = 0

case inr
E : Type ?u.245331
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
h : ‖x‖ = ‖y‖
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = y
E : Type ?u.245331
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
h : ‖x‖ = ‖y‖
⊢ SameRay ℝ x y ↔ x = y
obtain rfl | hy := eq_or_ne y 0
case inl
E : Type ?u.245331
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
h : x = 0
⊢ SameRay ℝ x 0 ↔ x = 0
case inl
E : Type ?u.245331
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
h : ‖x‖ = ‖0‖
⊢ SameRay ℝ x 0 ↔ x = 0
rw [norm_zero, norm_eq_zero] at h
no goals
case inl
E : Type ?u.245331
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : F
h : x = 0
⊢ SameRay ℝ x 0 ↔ x = 0
exact iff_of_true (SameRay.zero_right _) h
no goals
case inr
E : Type ?u.245331
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
h : ‖x‖ = ‖y‖
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = y
exact ⟨fun hxy => norm_injOn_ray_right hy hxy SameRay.rfl h, fun hxy => hxy ▸ SameRay.rfl⟩