case h.a.h
l : Type ?u.20354
m : Type u_1
n : Type u_3
o : Type ?u.20363
l' : Type ?u.20366
m' : Type u_2
n' : Type u_4
o' : Type ?u.20375
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''
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✝
l : Type ?u.20354
m : Type u_1
n : Type u_3
o : Type ?u.20363
l' : Type ?u.20366
m' : Type u_2
n' : Type u_4
o' : Type ?u.20375
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''
⊢ LinearEquiv.trans (reindexLinearEquiv R A e₁ e₂) (reindexLinearEquiv R A e₁' e₂') =
    reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')
ext
no goals
case h.a.h
l : Type ?u.20354
m : Type u_1
n : Type u_3
o : Type ?u.20363
l' : Type ?u.20366
m' : Type u_2
n' : Type u_4
o' : Type ?u.20375
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''
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✝
rfl