no goals
R : Type u_1
inst✝⁹ : CommSemiring R
l : Type ?u.2864957
m : Type ?u.2864960
n : Type ?u.2864963
inst✝⁸ : Fintype n
inst✝⁷ : Fintype m
inst✝⁶ : DecidableEq n
M₁ : Type ?u.2864981
M₂ : Type ?u.2864984
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.2865486
inst✝¹ : AddCommMonoid M₃
inst✝ : Module R M₃
v₃ : Basis l R M₃
a b c d : R
x : R × R
⊢ ↑(↑(toLin (Basis.finTwoProd R) (Basis.finTwoProd R)) (↑of ![![a, b], ![c, d]])) x =
    (a * x.fst + b * x.snd, c * x.fst + d * x.snd)
simp [Matrix.toLin_apply, Matrix.mulVec, Matrix.dotProduct, (Prod.smul_mk)]