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

State before:
f : ℕ → ℕ
hf : Arith₁ fun v => f (v.get 0)
n : ℕ
g : Vector ℕ n → ℕ
hg : Arith₁ g
⊢ ∀ (i : Vector ℕ n), f ((ofFn fun i_1 => g i).get 0) = f (g i)
Tactic:
simp
State after:
no goals