case h.h.h.h.h
R : Type u_1
R₁ : Type ?u.1404273
R₂ : Type ?u.1404276
M✝ : Type ?u.1404279
M₁ : Type ?u.1404282
M₂ : Type ?u.1404285
M₁' : Type ?u.1404288
M₂' : Type ?u.1404291
n : Type u_2
m : Type u_3
n' : Type ?u.1404300
m' : Type ?u.1404303
ι : Type ?u.1404306
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m R
i✝¹ : n
i✝ : m
⊢ ↑(comp (↑(comp (↑(toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m)) M) (single i✝¹)) 1) (single i✝)) 1 =
    ↑(comp (↑(comp (↑toLinearMap₂' M) (single i✝¹)) 1) (single i✝)) 1
R : Type u_1
R₁ : Type ?u.1404273
R₂ : Type ?u.1404276
M : Type ?u.1404279
M₁ : Type ?u.1404282
M₂ : Type ?u.1404285
M₁' : Type ?u.1404288
M₂' : Type ?u.1404291
n : Type u_2
m : Type u_3
n' : Type ?u.1404300
m' : Type ?u.1404303
ι : Type ?u.1404306
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
⊢ toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m) = toLinearMap₂'
ext M
no goals
case h.h.h.h.h
R : Type u_1
R₁ : Type ?u.1404273
R₂ : Type ?u.1404276
M✝ : Type ?u.1404279
M₁ : Type ?u.1404282
M₂ : Type ?u.1404285
M₁' : Type ?u.1404288
M₂' : Type ?u.1404291
n : Type u_2
m : Type u_3
n' : Type ?u.1404300
m' : Type ?u.1404303
ι : Type ?u.1404306
inst✝⁸ : CommRing R
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : Module R M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₂
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Fintype m
b₁ : Basis n R M₁
b₂ : Basis m R M₂
M : Matrix n m R
i✝¹ : n
i✝ : m
⊢ ↑(comp (↑(comp (↑(toLinearMap₂ (Pi.basisFun R n) (Pi.basisFun R m)) M) (single i✝¹)) 1) (single i✝)) 1 =
    ↑(comp (↑(comp (↑toLinearMap₂' M) (single i✝¹)) 1) (single i✝)) 1
simp only [Matrix.toLinearMap₂_apply, Matrix.toLinearMap₂'_apply, Pi.basisFun_repr, coe_comp,
  Function.comp_apply]