no goals
α : Type ?u.261935
R✝ : Type ?u.261938
k : Type ?u.261941
S : Type ?u.261944
M✝ : Type ?u.261947
M₂ : Type ?u.261950
M₃ : Type ?u.261953
ι : Type ?u.261956
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : Zero R
inst✝⁴ : Zero M
inst✝³ : Zero N
inst✝² : SMul R M
inst✝¹ : SMul R N
inst✝ : NoZeroSMulDivisors R N
f : M → N
hf : Injective f
h0 : f 0 = 0
hs : ∀ (c : R) (x : M), f (c • x) = c • f x
x✝¹ : R
x✝ : M
h : x✝¹ • x✝ = 0
⊢ x✝¹ • f x✝ = 0
rw [← hs, h, h0]