no goals
ι : Type ?u.1086687
ι' : Type ?u.1086690
R✝ : Type ?u.1086693
R₂ : Type ?u.1086696
K : Type ?u.1086699
M : Type ?u.1086702
M' : Type ?u.1086705
M'' : Type ?u.1086708
V : Type u
V' : Type ?u.1086713
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) 1 = (0, 1)
simp [Basis.finTwoProd, LinearEquiv.finTwoArrow]