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

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