no goals
ι : Type u_1
ι' : Type u_2
κ : Type ?u.369990
κ' : Type u_3
R : Type u_4
M : Type u_5
inst✝¹³ : CommSemiring R
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module R M
R₂ : Type ?u.370186
M₂ : Type ?u.370189
inst✝¹⁰ : CommRing R₂
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
N : Type u_6
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
inst✝⁵ : Fintype ι'
inst✝⁴ : Fintype κ
inst✝³ : Fintype κ'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
⊢ ↑(toLin b c') (↑(toMatrix b' c') f ⬝ Basis.toMatrix b' ↑b) = ↑(toLin b c') (↑(toMatrix b c') f)
rw [toLin_toMatrix, toLin_mul b b' c', toLin_toMatrix, b'.toLin_toMatrix, comp_id]