no goals
R : Type ?u.248225
R₁ : Type u_6
R₂ : Type u_3
R₃ : Type u_4
k : Type ?u.248237
S : Type ?u.248240
S₃ : Type ?u.248243
T : Type ?u.248246
M : Type ?u.248249
M₁ : Type u_5
M₂ : Type u_1
M₃ : Type u_2
N₁ : Type ?u.248261
N₂ : Type ?u.248264
N₃ : Type ?u.248267
ι : Type ?u.248270
inst✝⁹ : Semiring R
inst✝⁸ : Semiring S
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₂] M₂
f' : M₂ →ₛₗ[σ₂₃] M₃
g' : M₁ →ₛₗ[σ₁₂] M₂
hf : Injective ↑f
h : comp f g = comp f g'
x : M₁
⊢ ↑f (↑g x) = ↑f (↑g' x)
rw [← comp_apply, h, comp_apply]