apply_fun f using hf
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
hf : Function.Injective ⇑f
p : Submodule R M
x y : ↥p
h : (f.domRestrict p) x = (f.domRestrict p) y
⊢ ↑x = ↑y
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
hf : Function.Injective ⇑f
p : Submodule R M
x y : ↥p
h : (f.domRestrict p) x = (f.domRestrict p) y
⊢ f ↑x = f ↑y