[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
l' : Type u_5
m' : Type u_6
n' : Type u_7
o' : Type u_8
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
⊢ LinearEquiv.trans (reindexLinearEquiv R A e₁ e₂) (reindexLinearEquiv R A e₁' e₂') =
    reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')
[PROOFSTEP]
ext
[GOAL]
case h.a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
l' : Type u_5
m' : Type u_6
n' : Type u_7
o' : Type u_8
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
x✝¹ : Matrix m n A
i✝ : m''
x✝ : n''
⊢ ↑(LinearEquiv.trans (reindexLinearEquiv R A e₁ e₂) (reindexLinearEquiv R A e₁' e₂')) x✝¹ i✝ x✝ =
    ↑(reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')) x✝¹ i✝ x✝
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
l' : Type u_5
m' : Type u_6
n' : Type u_7
o' : Type u_8
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
⊢ ↑(reindexLinearEquiv R A e₁' e₂') ∘ ↑(reindexLinearEquiv R A e₁ e₂) =
    ↑(reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂'))
[PROOFSTEP]
rw [← reindexLinearEquiv_trans]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
l' : Type u_5
m' : Type u_6
n' : Type u_7
o' : Type u_8
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst✝² : Semiring R
inst✝¹ : AddCommMonoid A
inst✝ : Module R A
e₁ : m ≃ m'
e₂ : n ≃ n'
e₁' : m' ≃ m''
e₂' : n' ≃ n''
⊢ ↑(reindexLinearEquiv R A e₁' e₂') ∘ ↑(reindexLinearEquiv R A e₁ e₂) =
    ↑(LinearEquiv.trans (reindexLinearEquiv R A e₁ e₂) (reindexLinearEquiv R A e₁' e₂'))
[PROOFSTEP]
rfl
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
l' : Type u_5
m' : Type u_6
n' : Type u_7
o' : Type u_8
m'' : Type u_9
n'' : Type u_10
R : Type u_11
A : Type u_12
inst✝⁴ : CommSemiring R
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
e : m ≃ n
src✝ : Matrix m m R ≃ₗ[R] Matrix n n R := reindexLinearEquiv R R e e
r : R
⊢ toFun
      { toFun := ↑(reindex e e), invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
        right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
      (↑(algebraMap R (Matrix m m R)) r) =
    ↑(algebraMap R (Matrix n n R)) r
[PROOFSTEP]
simp [algebraMap, Algebra.toRingHom, submatrix_smul _ 1]
