Theorem: Nat.unvector_vecToNat (Logic/Vorspiel/Vorspiel.lean)

State before:
n : ℕ
v : Fin n → ℕ
⊢ unvector (vecToNat v) = v
Tactic:
induction n <;> simp[*, Nat.unvector, vecToNat, Matrix.empty_eq]
State after:
case succ
n n✝ : ℕ
a✝ : ∀ (v : Fin n✝ → ℕ), unvector (vecToNat v) = v
v : Fin (n✝ + 1) → ℕ
⊢ v 0 :> v ∘ Fin.succ = v

State before:
case succ
n n✝ : ℕ
a✝ : ∀ (v : Fin n✝ → ℕ), unvector (vecToNat v) = v
v : Fin (n✝ + 1) → ℕ
⊢ v 0 :> v ∘ Fin.succ = v
Tactic:
exact funext (fun i => i.cases (by simp[Matrix.empty_eq]) (by simp[Matrix.empty_eq]))
State after:
no goals

State before:
n n✝ : ℕ
a✝ : ∀ (v : Fin n✝ → ℕ), unvector (vecToNat v) = v
v : Fin (n✝ + 1) → ℕ
i : Fin n✝.succ
⊢ (v 0 :> v ∘ Fin.succ) 0 = v 0
Tactic:
simp[Matrix.empty_eq]
State after:
no goals

State before:
n n✝ : ℕ
a✝ : ∀ (v : Fin n✝ → ℕ), unvector (vecToNat v) = v
v : Fin (n✝ + 1) → ℕ
i : Fin n✝.succ
⊢ ∀ (i : Fin n✝), (v 0 :> v ∘ Fin.succ) i.succ = v i.succ
Tactic:
simp[Matrix.empty_eq]
State after:
no goals