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

State before:
n : ℕ
α : Type u
f : Fin (n + 1) → α
⊢ (f 0 :> fun x => f x.succ) = f
Tactic:
funext x
State after:
case h
n : ℕ
α : Type u
f : Fin (n + 1) → α
x : Fin n.succ
⊢ (f 0 :> fun x => f x.succ) x = f x

State before:
case h
n : ℕ
α : Type u
f : Fin (n + 1) → α
x : Fin n.succ
⊢ (f 0 :> fun x => f x.succ) x = f x
Tactic:
cases x using Fin.cases <;> simp
State after:
no goals