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

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