l : Type ?u.22310
m : Type u_1
n : Type u_3
o : Type ?u.22319
l' : Type ?u.22322
m' : Type u_2
n' : Type u_4
o' : Type ?u.22331
m'' : Type u_5
n'' : Type u_6
R : Type u_8
A : Type u_7
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₂'))
l : Type ?u.22310
m : Type u_1
n : Type u_3
o : Type ?u.22319
l' : Type ?u.22322
m' : Type u_2
n' : Type u_4
o' : Type ?u.22331
m'' : Type u_5
n'' : Type u_6
R : Type u_8
A : Type u_7
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₂'))
rw [← reindexLinearEquiv_trans]
no goals
l : Type ?u.22310
m : Type u_1
n : Type u_3
o : Type ?u.22319
l' : Type ?u.22322
m' : Type u_2
n' : Type u_4
o' : Type ?u.22331
m'' : Type u_5
n'' : Type u_6
R : Type u_8
A : Type u_7
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₂'))
rfl