Theorem: Nat.Arith₁.cons (Logic/Vorspiel/Arith.lean)

State before:
n m : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ n → Vector ℕ m
hf : Arith₁ f
hg : Vec g
i : Fin m.succ
⊢ Arith₁ fun v => ((fun v => f v ::ᵥ g v) v).get 0
Tactic:
simp [*]
State after:
no goals

State before:
n m : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ n → Vector ℕ m
hf : Arith₁ f
hg : Vec g
i✝ : Fin m.succ
i : Fin m
⊢ Arith₁ fun v => ((fun v => f v ::ᵥ g v) v).get i.succ
Tactic:
simp [hg i]
State after:
no goals