no goals
R : Type u_3
R₁ : Type ?u.476879
R₂ : Type u_1
R₃ : Type u_2
R₄ : Type ?u.476888
S : Type ?u.476891
K : Type ?u.476894
K₂ : Type ?u.476897
M : Type u_4
M' : Type ?u.476903
M₁ : Type ?u.476906
M₂ : Type u_5
M₃ : Type u_6
M₄ : Type ?u.476915
N : Type ?u.476918
N₂ : Type ?u.476921
ι : Type ?u.476924
V : Type ?u.476927
V₂ : Type ?u.476930
inst✝¹⁶ : Semiring R
inst✝¹⁵ : Semiring R₂
inst✝¹⁴ : Semiring R₃
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid M₂
inst✝¹¹ : AddCommMonoid M₃
inst✝¹⁰ : AddCommMonoid M'
inst✝⁹ : Module R M
inst✝⁸ : Module R M'
inst✝⁷ : Module R₂ M₂
inst✝⁶ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p✝ p' : Submodule R M
q q' : Submodule R₂ M₂
q₁ q₁' : Submodule R M'
r : R
x y : M
inst✝² : RingHomSurjective σ₁₂
F : Type ?u.477511
sc : SemilinearMapClass F σ₁₂ M M₂
inst✝¹ : RingHomSurjective σ₂₃
inst✝ : RingHomSurjective σ₁₃
f : M →ₛₗ[σ₁₂] M₂
g : M₂ →ₛₗ[σ₂₃] M₃
p : Submodule R M
⊢ ↑(map (LinearMap.comp g f) p) = ↑(map g (map f p))
simp only [← image_comp, map_coe, LinearMap.coe_comp, comp_apply]