Theorem: LinearEquiv.map_trans (Matroid/ForMathlib/LinearAlgebra/Submodule.lean)

State before:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
e₁₂ : M₁ ≃ₗ[R] M₂
e₂₃ : M₂ ≃ₗ[R] M₃
U : Submodule R M₁
⊢ Submodule.map (e₁₂ ≪≫ₗ e₂₃) U = Submodule.map e₂₃ (Submodule.map e₁₂ U)
Tactic:
rw [← LinearEquiv.map_coe,  LinearEquiv.coe_trans, Submodule.map_comp]
State after:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
e₁₂ : M₁ ≃ₗ[R] M₂
e₂₃ : M₂ ≃ₗ[R] M₃
U : Submodule R M₁
⊢ Submodule.map (↑e₂₃) (Submodule.map (↑e₁₂) U) = Submodule.map e₂₃ (Submodule.map e₁₂ U)

State before:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
e₁₂ : M₁ ≃ₗ[R] M₂
e₂₃ : M₂ ≃ₗ[R] M₃
U : Submodule R M₁
⊢ Submodule.map (↑e₂₃) (Submodule.map (↑e₁₂) U) = Submodule.map e₂₃ (Submodule.map e₁₂ U)
Tactic:
rfl
State after:
no goals