no goals
R : Type u_2
R₁ : Type ?u.133858
R₂ : Type ?u.133861
R₃ : Type ?u.133864
k : Type ?u.133867
S : Type u_1
S₃ : Type ?u.133873
T : Type ?u.133876
M : Type u_4
M₁ : Type ?u.133882
M₂ : Type ?u.133885
M₃ : Type u_3
N₁ : Type ?u.133891
N₂ : Type ?u.133894
N₃ : Type ?u.133897
ι : Type ?u.133900
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₃
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
c : S
x : M
⊢ c • ↑f x = ↑f (↑σ' c • x)
simp