no goals
E : Type ?u.229888
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_1
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y
rw [inv_smul_eq_iff₀, smul_comm, eq_comm, inv_smul_eq_iff₀, sameRay_iff_norm_smul_eq] <;>
  rwa [norm_ne_zero_iff]