no goals
R : Type u_1
R₁ : Type ?u.219990
R₂ : Type ?u.219993
R₃ : Type ?u.219996
k : Type ?u.219999
S : Type u_2
S₃ : Type ?u.220005
T : Type ?u.220008
M : Type ?u.220011
M₁ : Type ?u.220014
M₂ : Type ?u.220017
M₃ : Type u_3
N₁ : Type ?u.220023
N₂ : Type ?u.220026
N₃ : Type ?u.220029
ι : Type ?u.220032
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : AddCommMonoid M₃
inst✝⁵ : AddCommMonoid N₁
inst✝⁴ : AddCommMonoid N₂
inst✝³ : AddCommMonoid N₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module S M₃
σ : R →+* S
fₗ gₗ : M →ₗ[R] M₂
f✝ g✝ : M →ₛₗ[σ] M₃
f g : R →ₛₗ[σ] M₃
h : ↑f 1 = ↑g 1
x : R
⊢ ↑f x = ↑g x
rw [← mul_one x, ← smul_eq_mul, f.map_smulₛₗ, g.map_smulₛₗ, h]