no goals
ι : Type ?u.1076425
ι' : Type ?u.1076428
R✝ : Type ?u.1076431
R₂ : Type ?u.1076434
K : Type ?u.1076437
M : Type ?u.1076440
M' : Type ?u.1076443
M'' : Type ?u.1076446
V : Type u
V' : Type ?u.1076451
v : ι → M
inst✝⁹ : Ring R✝
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R✝ M
inst✝³ : Module R₂ M
inst✝² : Module R✝ M'
inst✝¹ : Module R✝ M''
c d : R✝
x y : M
b : Basis ι R✝ M
R : Type u_1
inst✝ : Semiring R
⊢ ↑(Basis.finTwoProd R) 0 = (1, 0)
simp [Basis.finTwoProd, LinearEquiv.finTwoArrow]