no goals
R : Type u_1
R₁ : Type ?u.1582116
R₂ : Type u_2
R₃ : Type u_5
R₄ : Type ?u.1582125
S : Type ?u.1582128
K : Type ?u.1582131
K₂ : Type ?u.1582134
M : Type u_3
M' : Type ?u.1582140
M₁ : Type ?u.1582143
M₂ : Type u_4
M₃ : Type u_6
M₄ : Type ?u.1582152
N : Type ?u.1582155
N₂ : Type ?u.1582158
ι : Type ?u.1582161
V : Type ?u.1582164
V₂ : Type ?u.1582167
inst✝⁹ : Semiring R
inst✝⁸ : Semiring R₂
inst✝⁷ : Semiring R₃
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : AddCommMonoid M₃
inst✝³ : Module R M
inst✝² : Module R₂ M₂
inst✝¹ : Module R₃ M₃
τ₁₂ : R →+* R₂
τ₂₃ : R₂ →+* R₃
τ₁₃ : R →+* R₃
inst✝ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hg : ker g = ⊥
⊢ ker (comp g f) = ker f
rw [ker_comp, hg, Submodule.comap_bot]