case h
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type ?u.2016127
m : Type u_4
n : Type u_5
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_2
M₂ : Type u_3
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type ?u.2016656
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
f : M₁ →ₗ[R] M₂
x : M₁
i : m
⊢ mulVec (↑(toMatrix v₁ v₂) f) (↑(↑v₁.repr x)) i = ↑(↑v₂.repr (↑f x)) i
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type ?u.2016127
m : Type u_4
n : Type u_5
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_2
M₂ : Type u_3
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type ?u.2016656
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
f : M₁ →ₗ[R] M₂
x : M₁
⊢ mulVec (↑(toMatrix v₁ v₂) f) ↑(↑v₁.repr x) = ↑(↑v₂.repr (↑f x))
ext i
case h
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type ?u.2016127
m : Type u_4
n : Type u_5
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_2
M₂ : Type u_3
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type ?u.2016656
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
f : M₁ →ₗ[R] M₂
x : M₁
i : m
⊢ ↑(↑v₂.repr (↑f (↑(LinearEquiv.symm (Basis.equivFun v₁)) ↑(↑v₁.repr x)))) i = ↑(↑v₂.repr (↑f x)) i
case h
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type ?u.2016127
m : Type u_4
n : Type u_5
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_2
M₂ : Type u_3
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type ?u.2016656
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
f : M₁ →ₗ[R] M₂
x : M₁
i : m
⊢ mulVec (↑(toMatrix v₁ v₂) f) (↑(↑v₁.repr x)) i = ↑(↑v₂.repr (↑f x)) i
rw [← Matrix.toLin'_apply, LinearMap.toMatrix, LinearEquiv.trans_apply, Matrix.toLin'_toMatrix',
  LinearEquiv.arrowCongr_apply, v₂.equivFun_apply]
case h.e_a.h.e_6.h.h.e_6.h
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type ?u.2016127
m : Type u_4
n : Type u_5
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_2
M₂ : Type u_3
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type ?u.2016656
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
f : M₁ →ₗ[R] M₂
x : M₁
i : m
⊢ ↑(LinearEquiv.symm (Basis.equivFun v₁)) ↑(↑v₁.repr x) = x
case h
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type ?u.2016127
m : Type u_4
n : Type u_5
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_2
M₂ : Type u_3
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type ?u.2016656
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
f : M₁ →ₗ[R] M₂
x : M₁
i : m
⊢ ↑(↑v₂.repr (↑f (↑(LinearEquiv.symm (Basis.equivFun v₁)) ↑(↑v₁.repr x)))) i = ↑(↑v₂.repr (↑f x)) i
congr
no goals
case h.e_a.h.e_6.h.h.e_6.h
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type ?u.2016127
m : Type u_4
n : Type u_5
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type u_2
M₂ : Type u_3
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : Module R M₁
inst✝² : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
M₃ : Type ?u.2016656
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
f : M₁ →ₗ[R] M₂
x : M₁
i : m
⊢ ↑(LinearEquiv.symm (Basis.equivFun v₁)) ↑(↑v₁.repr x) = x
exact v₁.equivFun.symm_apply_apply x