no goals
R : Type ?u.500438
R₁ : Type u_6
R₂ : Type u_1
R₃ : Type u_2
k : Type ?u.500450
S : Type ?u.500453
S₃ : Type ?u.500456
T : Type ?u.500459
M : Type u_5
M₁ : Type ?u.500465
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type ?u.500474
N₂ : Type ?u.500477
N₃ : Type ?u.500480
ι : Type ?u.500483
inst✝¹⁵ : Semiring R₁
inst✝¹⁴ : Semiring R₂
inst✝¹³ : Semiring R₃
inst✝¹² : AddCommMonoid M
inst✝¹¹ : AddCommMonoid M₂
inst✝¹⁰ : AddCommMonoid M₃
inst✝⁹ : AddCommGroup N₁
inst✝⁸ : AddCommGroup N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R₁ M
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
inst✝³ : Module R₁ N₁
inst✝² : Module R₂ N₂
inst✝¹ : Module R₃ N₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
g : M₂ →ₛₗ[σ₂₃] M₃
c : M
⊢ ↑(comp g 0) c = ↑0 c
rw [comp_apply, zero_apply, zero_apply, g.map_zero]