no goals
R : Type u_2
inst✝⁶ : StrictOrderedCommSemiring R
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module R N
ι : Type ?u.44462
inst✝¹ : DecidableEq ι
x y z : M
F : Type u_1
inst✝ : LinearMapClass F R M N
f : F
hf : Function.Injective ↑f
⊢ SameRay R (↑f x) (↑f y) ↔ SameRay R x y
simp only [SameRay, map_zero, ← hf.eq_iff, map_smul]