no goals
R : Type u_2
R₁ : Type ?u.1593776
R₂ : Type ?u.1593779
R₃ : Type ?u.1593782
R₄ : Type ?u.1593785
S : Type ?u.1593788
K : Type ?u.1593791
K₂ : Type ?u.1593794
M : Type u_3
M'✝ : Type ?u.1593800
M₁ : Type ?u.1593803
M₂ : Type ?u.1593806
M₃ : Type ?u.1593809
M₄ : Type ?u.1593812
N✝ : Type ?u.1593815
N₂ : Type ?u.1593818
ι : Type ?u.1593821
V : Type ?u.1593824
V₂ : Type ?u.1593827
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 τ₁₂ τ₂₃ τ₁₃
M' : Type u_1
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
O : Submodule R M
ϕ : { x // x ∈ O } →ₗ[R] M'
N : Submodule R M
hNO : N ≤ O
⊢ submoduleImage ϕ N = range (comp ϕ (Submodule.ofLe hNO))
rw [submoduleImage, range_comp, Submodule.range_ofLe]