case intro
m n : ℕ
f : Vector ℕ n →. ℕ
g : Fin n → Vector ℕ m →. ℕ
hf : ∃ c, ∀ (v : Vector ℕ n), eval c ↑v = pure <$> f v
hg✝ : ∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
cg : Code
hg : ∀ (v : Vector ℕ m), eval cg ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
⊢ ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> ((Vector.mOfFn fun i => g i v) >>= f)

m n : ℕ
f : Vector ℕ n →. ℕ
g : Fin n → Vector ℕ m →. ℕ
hf : ∃ c, ∀ (v : Vector ℕ n), eval c ↑v = pure <$> f v
hg : ∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
⊢ ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
m n : ℕ
f : Vector ℕ n →. ℕ
g : Fin n → Vector ℕ m →. ℕ
hf : ∃ c, ∀ (v : Vector ℕ n), eval c ↑v = pure <$> f v
hg : ∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
⊢ ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> ((Vector.mOfFn fun i => g i v) >>= f)
rsuffices ⟨cg, hg⟩ :
  ∃ c : Code, ∀ v : Vector ℕ m, c.eval v.1 = Subtype.val <$> Vector.mOfFn fun i => g i v
m n : ℕ
g : Fin n → Vector ℕ m →. ℕ
hg : ∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
⊢ ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
m n : ℕ
f : Vector ℕ n →. ℕ
g : Fin n → Vector ℕ m →. ℕ
hf : ∃ c, ∀ (v : Vector ℕ n), eval c ↑v = pure <$> f v
hg : ∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
⊢ ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
clear hf f
case zero
m n : ℕ
g✝ : Fin n → Vector ℕ m →. ℕ
hg✝ : ∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g✝ i v
g : Fin Nat.zero → Vector ℕ m →. ℕ
hg : ∀ (i : Fin Nat.zero), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
⊢ ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v

case succ
m n✝ : ℕ
g✝ : Fin n✝ → Vector ℕ m →. ℕ
hg✝ : ∀ (i : Fin n✝), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g✝ i v
n : ℕ
IH :
  ∀ {g : Fin n → Vector ℕ m →. ℕ},
    (∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v) →
      ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
g : Fin (Nat.succ n) → Vector ℕ m →. ℕ
hg : ∀ (i : Fin (Nat.succ n)), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
⊢ ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
m n : ℕ
g : Fin n → Vector ℕ m →. ℕ
hg : ∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
⊢ ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
induction' n with n IH
case intro.intro
m n : ℕ
f : Vector ℕ n →. ℕ
g : Fin n → Vector ℕ m →. ℕ
hg✝ : ∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
cg : Code
hg : ∀ (v : Vector ℕ m), eval cg ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
cf : Code
hf : ∀ (v : Vector ℕ n), eval cf ↑v = pure <$> f v
⊢ ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> ((Vector.mOfFn fun i => g i v) >>= f)
case intro
m n : ℕ
f : Vector ℕ n →. ℕ
g : Fin n → Vector ℕ m →. ℕ
hf : ∃ c, ∀ (v : Vector ℕ n), eval c ↑v = pure <$> f v
hg✝ : ∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
cg : Code
hg : ∀ (v : Vector ℕ m), eval cg ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
⊢ ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> ((Vector.mOfFn fun i => g i v) >>= f)
obtain ⟨cf, hf⟩ := hf
no goals
case intro.intro
m n : ℕ
f : Vector ℕ n →. ℕ
g : Fin n → Vector ℕ m →. ℕ
hg✝ : ∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
cg : Code
hg : ∀ (v : Vector ℕ m), eval cg ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
cf : Code
hf : ∀ (v : Vector ℕ n), eval cf ↑v = pure <$> f v
⊢ ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> ((Vector.mOfFn fun i => g i v) >>= f)
exact
  ⟨cf.comp cg, fun v => by
    simp [hg, hf, map_bind, seq_bind_eq, Function.comp]
    rfl⟩
m n : ℕ
f : Vector ℕ n →. ℕ
g : Fin n → Vector ℕ m →. ℕ
hg✝ : ∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
cg : Code
hg : ∀ (v : Vector ℕ m), eval cg ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
cf : Code
hf : ∀ (v : Vector ℕ n), eval cf ↑v = pure <$> f v
v : Vector ℕ m
⊢ (do
      let x ← Vector.mOfFn fun i => g i v
      pure <$> f x) =
    do
    let a ← Vector.mOfFn fun i => g i v
    pure <$> f a
m n : ℕ
f : Vector ℕ n →. ℕ
g : Fin n → Vector ℕ m →. ℕ
hg✝ : ∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
cg : Code
hg : ∀ (v : Vector ℕ m), eval cg ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
cf : Code
hf : ∀ (v : Vector ℕ n), eval cf ↑v = pure <$> f v
v : Vector ℕ m
⊢ eval (Code.comp cf cg) ↑v = pure <$> ((Vector.mOfFn fun i => g i v) >>= f)
simp [hg, hf, map_bind, seq_bind_eq, Function.comp]
no goals
m n : ℕ
f : Vector ℕ n →. ℕ
g : Fin n → Vector ℕ m →. ℕ
hg✝ : ∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
cg : Code
hg : ∀ (v : Vector ℕ m), eval cg ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
cf : Code
hf : ∀ (v : Vector ℕ n), eval cf ↑v = pure <$> f v
v : Vector ℕ m
⊢ (do
      let x ← Vector.mOfFn fun i => g i v
      pure <$> f x) =
    do
    let a ← Vector.mOfFn fun i => g i v
    pure <$> f a
rfl
no goals
case zero
m n : ℕ
g✝ : Fin n → Vector ℕ m →. ℕ
hg✝ : ∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g✝ i v
g : Fin Nat.zero → Vector ℕ m →. ℕ
hg : ∀ (i : Fin Nat.zero), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
⊢ ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
exact ⟨nil, fun v => by simp [Vector.mOfFn, Bind.bind]; rfl⟩
m n : ℕ
g✝ : Fin n → Vector ℕ m →. ℕ
hg✝ : ∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g✝ i v
g : Fin Nat.zero → Vector ℕ m →. ℕ
hg : ∀ (i : Fin Nat.zero), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
v : Vector ℕ m
⊢ Part.some [] = Subtype.val <$> Part.some Vector.nil
m n : ℕ
g✝ : Fin n → Vector ℕ m →. ℕ
hg✝ : ∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g✝ i v
g : Fin Nat.zero → Vector ℕ m →. ℕ
hg : ∀ (i : Fin Nat.zero), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
v : Vector ℕ m
⊢ eval nil ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
simp [Vector.mOfFn, Bind.bind]
no goals
m n : ℕ
g✝ : Fin n → Vector ℕ m →. ℕ
hg✝ : ∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g✝ i v
g : Fin Nat.zero → Vector ℕ m →. ℕ
hg : ∀ (i : Fin Nat.zero), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
v : Vector ℕ m
⊢ Part.some [] = Subtype.val <$> Part.some Vector.nil
rfl
case succ.intro
m n✝ : ℕ
g✝ : Fin n✝ → Vector ℕ m →. ℕ
hg✝ : ∀ (i : Fin n✝), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g✝ i v
n : ℕ
IH :
  ∀ {g : Fin n → Vector ℕ m →. ℕ},
    (∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v) →
      ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
g : Fin (Nat.succ n) → Vector ℕ m →. ℕ
hg : ∀ (i : Fin (Nat.succ n)), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
cg : Code
hg₁ : ∀ (v : Vector ℕ m), eval cg ↑v = pure <$> g 0 v
⊢ ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
case succ
m n✝ : ℕ
g✝ : Fin n✝ → Vector ℕ m →. ℕ
hg✝ : ∀ (i : Fin n✝), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g✝ i v
n : ℕ
IH :
  ∀ {g : Fin n → Vector ℕ m →. ℕ},
    (∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v) →
      ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
g : Fin (Nat.succ n) → Vector ℕ m →. ℕ
hg : ∀ (i : Fin (Nat.succ n)), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
⊢ ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
obtain ⟨cg, hg₁⟩ := hg 0
case succ.intro.intro
m n✝ : ℕ
g✝ : Fin n✝ → Vector ℕ m →. ℕ
hg✝ : ∀ (i : Fin n✝), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g✝ i v
n : ℕ
IH :
  ∀ {g : Fin n → Vector ℕ m →. ℕ},
    (∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v) →
      ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
g : Fin (Nat.succ n) → Vector ℕ m →. ℕ
hg : ∀ (i : Fin (Nat.succ n)), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
cg : Code
hg₁ : ∀ (v : Vector ℕ m), eval cg ↑v = pure <$> g 0 v
cl : Code
hl : ∀ (v : Vector ℕ m), eval cl ↑v = Subtype.val <$> Vector.mOfFn fun i => g (Fin.succ i) v
⊢ ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
case succ.intro
m n✝ : ℕ
g✝ : Fin n✝ → Vector ℕ m →. ℕ
hg✝ : ∀ (i : Fin n✝), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g✝ i v
n : ℕ
IH :
  ∀ {g : Fin n → Vector ℕ m →. ℕ},
    (∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v) →
      ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
g : Fin (Nat.succ n) → Vector ℕ m →. ℕ
hg : ∀ (i : Fin (Nat.succ n)), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
cg : Code
hg₁ : ∀ (v : Vector ℕ m), eval cg ↑v = pure <$> g 0 v
⊢ ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
obtain ⟨cl, hl⟩ := IH fun i => hg i.succ
no goals
m n✝ : ℕ
g✝ : Fin n✝ → Vector ℕ m →. ℕ
hg✝ : ∀ (i : Fin n✝), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g✝ i v
n : ℕ
IH :
  ∀ {g : Fin n → Vector ℕ m →. ℕ},
    (∀ (i : Fin n), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v) →
      ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = Subtype.val <$> Vector.mOfFn fun i => g i v
g : Fin (Nat.succ n) → Vector ℕ m →. ℕ
hg : ∀ (i : Fin (Nat.succ n)), ∃ c, ∀ (v : Vector ℕ m), eval c ↑v = pure <$> g i v
cg : Code
hg₁ : ∀ (v : Vector ℕ m), eval cg ↑v = pure <$> g 0 v
cl : Code
hl : ∀ (v : Vector ℕ m), eval cl ↑v = Subtype.val <$> Vector.mOfFn fun i => g (Fin.succ i) v
v : Vector ℕ m
⊢ (do
      let x ← g 0 v
      let x_1 ← Vector.mOfFn fun i => g (Fin.succ i) v
      Part.some (List.headI (pure x) :: ↑x_1)) =
    do
    let a ← g 0 v
    let a_1 ← Vector.mOfFn fun i => g (Fin.succ i) v
    Subtype.val <$> Part.some (a ::ᵥ a_1)
rfl