no goals
α : Type u_1
β : Type ?u.209886
γ : Type ?u.209889
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : Fin n → α → σ
hf : ∀ (i : Fin n), Computable (f i)
a : α
⊢ (Vector.mOfFn fun i => ↑(f i) a) = (↑fun a => Vector.ofFn fun i => f i a) a
simp