simp[hg, hf]
case mp.intro.intro
k : ℕ
c✝ : Code k
f✝ : Vector ℕ k →. ℕ
m✝ n✝ : ℕ
c : Code n✝
d : Fin n✝ → Code m✝
f : Vector ℕ n✝ →. ℕ
g : Fin n✝ → Vector ℕ m✝ →. ℕ
a✝¹ : c.eval f
a✝ : ∀ (i : Fin n✝), (d i).eval (g i)
ihf : ∀ (y : ℕ) (v : Fin n✝ → ℕ), (Semiformula.Evalfm ℕ (y :> v)) (codeAux c) ↔ f (Vector.ofFn v) = Part.some y
ihg :
  ∀ (i : Fin n✝) (y : ℕ) (v : Fin m✝ → ℕ),
    (Semiformula.Evalfm ℕ (y :> v)) (codeAux (d i)) ↔ g i (Vector.ofFn v) = Part.some y
y : ℕ
v : Fin m✝ → ℕ
e : Fin n✝ → ℕ
hf✝ : (Semiformula.Eval (standardModel ℕ) ![] (y :> fun i => e i)) (codeAux c)
hg✝ : ∀ (i : Fin n✝), (Semiformula.Eval (standardModel ℕ) ![] (e i :> fun i => v i)) (codeAux (d i))
hf : f (Vector.ofFn e) = Part.some y
hg : ∀ (i : Fin n✝), g i (Vector.ofFn v) = Part.some (e i)
⊢ (Vector.mOfFn fun i => g i (Vector.ofFn v)).bind f = Part.some y
no goals