Theorem: DMatrix.eq_vecCons (Logic/Vorspiel/Vorspiel.lean)

State before:
n : ℕ
α : Fin (n + 1) → Type u_1
s : (i : Fin (n + 1)) → α i
⊢ s 0 = (s 0 ::> fun i => s i.succ) 0
Tactic:
simp
State after:
no goals

State before:
n : ℕ
α : Fin (n + 1) → Type u_1
s : (i : Fin (n + 1)) → α i
⊢ ∀ (i : Fin n), s i.succ = (s 0 ::> fun i => s i.succ) i.succ
Tactic:
simp
State after:
no goals