Theorem: Matrix.vecCons_succ (Logic/Vorspiel/Vorspiel.lean)

State before:
n : ℕ
α : Type u
α✝ : Type u_1
a : α✝
s : Fin n → α✝
i : Fin n
⊢ (a :> s) i.succ = s i
Tactic:
simp
State after:
no goals