no goals
R : Type ?u.1320421
inst✝¹⁹ : Semiring R
M : Type ?u.1320427
inst✝¹⁸ : AddCommMonoid M
inst✝¹⁷ : Module R M
N : Type ?u.1320459
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : Module R N
P : Type ?u.1320489
inst✝¹⁴ : AddCommMonoid P
inst✝¹³ : Module R P
M' : Type ?u.1320519
inst✝¹² : AddCommGroup M'
inst✝¹¹ : Module R M'
N' : Type ?u.1320907
inst✝¹⁰ : AddCommGroup N'
inst✝⁹ : Module R N'
ι : Type ?u.1321295
ι' : Type ?u.1321298
ι'' : Type ?u.1321301
R' : Type u_1
M'' : Type u_2
M₂'' : Type ?u.1321310
N'' : Type u_3
N₂'' : Type ?u.1321316
inst✝⁸ : CommSemiring R'
inst✝⁷ : AddCommMonoid M''
inst✝⁶ : AddCommMonoid M₂''
inst✝⁵ : AddCommMonoid N''
inst✝⁴ : AddCommMonoid N₂''
inst✝³ : Module R' M''
inst✝² : Module R' M₂''
inst✝¹ : Module R' N''
inst✝ : Module R' N₂''
n : ℕ
f : AlternatingMap R' M'' N'' (Fin (Nat.succ (Nat.succ n)))
m : M''
x : Fin n → M''
⊢ Matrix.vecCons m (Matrix.vecCons m x) 0 = Matrix.vecCons m (Matrix.vecCons m x) 1
simp