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

State before:
n✝ : ℕ
α : Type u
n : ℕ
⊢ (0 :> succ) 0 = id 0
Tactic:
simp
State after:
no goals

State before:
n✝ : ℕ
α : Type u
n : ℕ
⊢ ∀ (i : Fin n), (0 :> succ) i.succ = id i.succ
Tactic:
simp
State after:
no goals