case a.h
ι : Type u_1
ι' : Type u_4
κ : Type ?u.637514
κ' : Type ?u.637517
R : Type u_2
M : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
R₂ : Type ?u.637710
M₂ : Type ?u.637713
inst✝⁴ : CommRing R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
N : Type ?u.638458
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
b✝ : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
i✝ x✝ : ι'
⊢ toMatrix (reindex b e) v i✝ x✝ = submatrix (toMatrix b v) (↑e.symm) _root_.id i✝ x✝
ι : Type u_1
ι' : Type u_4
κ : Type ?u.637514
κ' : Type ?u.637517
R : Type u_2
M : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
R₂ : Type ?u.637710
M₂ : Type ?u.637713
inst✝⁴ : CommRing R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
N : Type ?u.638458
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
b✝ : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ toMatrix (reindex b e) v = submatrix (toMatrix b v) (↑e.symm) _root_.id
ext
no goals
case a.h
ι : Type u_1
ι' : Type u_4
κ : Type ?u.637514
κ' : Type ?u.637517
R : Type u_2
M : Type u_3
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
R₂ : Type ?u.637710
M₂ : Type ?u.637713
inst✝⁴ : CommRing R₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i : ι
j : ι'
N : Type ?u.638458
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
b✝ : Basis ι R M
b' : Basis ι' R M
c : Basis κ R N
c' : Basis κ' R N
f : M →ₗ[R] N
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
i✝ x✝ : ι'
⊢ toMatrix (reindex b e) v i✝ x✝ = submatrix (toMatrix b v) (↑e.symm) _root_.id i✝ x✝
simp only [Basis.toMatrix_apply, Basis.repr_reindex, Matrix.submatrix_apply, id.def,
  Finsupp.mapDomain_equiv_apply]