no goals
R : Type u_1
R₁ : Type ?u.1578452
R₂ : Type u_2
R₃ : Type u_3
R₄ : Type ?u.1578461
S : Type ?u.1578464
K : Type ?u.1578467
K₂ : Type ?u.1578470
M : Type u_4
M' : Type ?u.1578476
M₁ : Type ?u.1578479
M₂ : Type u_5
M₃ : Type u_6
M₄ : Type ?u.1578488
N : Type ?u.1578491
N₂ : Type ?u.1578494
ι : Type ?u.1578497
V : Type ?u.1578500
V₂ : Type ?u.1578503
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 τ₁₂ τ₂₃ τ₁₃
inst✝² : RingHomSurjective τ₁₂
inst✝¹ : RingHomSurjective τ₂₃
inst✝ : RingHomSurjective τ₁₃
f : M →ₛₗ[τ₁₂] M₂
g : M₂ →ₛₗ[τ₂₃] M₃
hf : range f = ⊤
⊢ range (comp g f) = range g
rw [range_comp, hf, Submodule.map_top]