awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f_2 : List.Vector ℕ n_2 → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
h : Nat.Primrec' f
h_1 : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n + 1)
hf : cf.eval (↑v : List ℕ).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v : List ℕ).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
prim :
  ∀ (x : ℕ),
    (cf.prec cg).eval (x :: (↑v : List ℕ).tail) =
      pure (pure (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) x))
⊢ (cf.prec cg).eval (v.head :: (↑v : List ℕ).tail) =
    pure (pure (Nat.rec (motive := fun (x : ℕ) ↦ ℕ) (f v.tail) (fun (y IH : ℕ) ↦ g (y ::ᵥ IH ::ᵥ v.tail)) v.head))

Tactic:
induction v.head with
        simp [prec, hf, Part.bind_assoc, ← Part.bind_some_eq_map, Part.bind_some, Bind.bind]
      | succ n _ =>
      suffices ∀ a b, a + b = n →
        (n.succ :: 0 ::
          g (n ::ᵥ Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) n ::ᵥ v.tail) ::
              v.val.tail : List ℕ) ∈
          PFun.fix
            (fun v : List ℕ => Part.bind (cg.eval (v.headI :: v.tail.tail))
              (fun x => Part.some (if v.tail.headI = 0
                then Sum.inl
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail : List ℕ)
                else Sum.inr
                  (v.headI.succ :: v.tail.headI.pred :: x.headI :: v.tail.tail.tail))))
            (a :: b :: Nat.rec (f v.tail) (fun y IH => g (y ::ᵥ IH ::ᵥ v.tail)) a :: v.val.tail) by
        have := Part.eq_some_iff.mpr (this _ _ (zero_add _))
        simp_all
      intro a b e
      induction b generalizing a with
      | zero =>
        refine PFun.mem_fix_iff.2 (Or.inl <| Part.eq_some_iff.1 ?_)
        simp only [hg, ← e, Part.bind_some, List.tail_cons, pure]
        rfl
      | succ b IH =>
        refine PFun.mem_fix_iff.2 (Or.inr ⟨_, ?_, IH (a + 1) (by rwa [add_right_comm])⟩)
        simp only [hg, Part.bind_some, List.tail_cons, pure]
        exact Part.mem_some_iff.2 rfl

Premises used: Pure.pure, Iff.mpr, Part.eq_some_iff, Part.bind_some, List.Vector.head, Part.mem_some_iff, Turing.ToPartrec.Code.succ, List.tail_cons, Turing.ToPartrec.Code.prec, Part.bind_some_eq_map, Turing.ToPartrec.Code.zero, Part.bind_assoc, Iff.mp, Bind.bind, Or.inl, PFun.mem_fix_iff, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
m n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
g : Fin n_1 → List.Vector ℕ m →. ℕ
h : Nat.Partrec' f_1
h_1 : ∀ (i : Fin n_1), Nat.Partrec' (g i)
IHf : ∃ (c : Code), ∀ (v : List.Vector ℕ n_1), c.eval (↑v : List ℕ) = pure <$> f_1 v
IHg : ∀ (i : Fin n_1), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ m),
      c.eval (↑v : List ℕ) = pure <$> (fun (v : List.Vector ℕ m) ↦ (Vector.mOfFn fun (i : Fin n_1) ↦ g i v) >>= f_1) v

Tactic:
exists_code.comp IHf IHg

Premises used: Turing.ToPartrec.Code.exists_code.comp
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n : ℕ
f : List.Vector ℕ n →. ℕ
m n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
g : Fin n_1 → List.Vector ℕ m →. ℕ
h : Nat.Partrec' f_1
h_1 : ∀ (i : Fin n_1), Nat.Partrec' (g i)
IHf : ∃ (c : Code), ∀ (v : List.Vector ℕ n_1), c.eval (↑v : List ℕ) = pure <$> f_1 v
IHg : ∀ (i : Fin n_1), ∃ (c : Code), ∀ (v : List.Vector ℕ m), c.eval (↑v : List ℕ) = pure <$> g i v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ m),
      c.eval (↑v : List ℕ) = pure <$> (fun (v : List.Vector ℕ m) ↦ (Vector.mOfFn fun (i : Fin n_1) ↦ g i v) >>= f_1) v

Tactic:
exact exists_code.comp IHf IHg

Premises used: Turing.ToPartrec.Code.exists_code.comp
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
IHf : ∃ (c : Code), ∀ (v : List.Vector ℕ (n + 1)), c.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ (n + 1) →. ℕ) v
rfind :
  ∀ (cf : Code)
    (hf : ∀ (v : List.Vector ℕ (n + 1)), cf.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ (n + 1) →. ℕ) v),
    ∃ (c : Code),
      ∀ (v : List.Vector ℕ n),
        c.eval (↑v : List ℕ) =
          pure <$> (fun (v : List.Vector ℕ n) ↦ Nat.rfind fun (n_2 : ℕ) ↦ Part.some (decide (f (n_2 ::ᵥ v) = 0))) v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ n),
      c.eval (↑v : List ℕ) =
        pure <$> (fun (v : List.Vector ℕ n) ↦ Nat.rfind fun (n_2 : ℕ) ↦ Part.some (decide (f (n_2 ::ᵥ v) = 0))) v

Tactic:
obtain ⟨cf, hf⟩ := IHf
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
cf : Code
hf : ∀ (v : List.Vector ℕ (n + 1)), cf.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ (n + 1) →. ℕ) v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ n),
      c.eval (↑v : List ℕ) =
        pure <$> (fun (v : List.Vector ℕ n) ↦ Nat.rfind fun (n_2 : ℕ) ↦ Part.some (decide (f (n_2 ::ᵥ v) = 0))) v

Tactic:
⟨rfind cf, fun v => ?_⟩

Premises used: Turing.ToPartrec.Code.rfind, Exists.intro
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
cf : Code
hf : ∀ (v : List.Vector ℕ (n + 1)), cf.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ (n + 1) →. ℕ) v
rfind :
  ∀ (v : List.Vector ℕ n),
    cf.rfind.eval (↑v : List ℕ) =
      pure <$> (fun (v : List.Vector ℕ n) ↦ Nat.rfind fun (n_2 : ℕ) ↦ Part.some (decide (f (n_2 ::ᵥ v) = 0))) v
⊢ ∃ (c : Code),
    ∀ (v : List.Vector ℕ n),
      c.eval (↑v : List ℕ) =
        pure <$> (fun (v : List.Vector ℕ n) ↦ Nat.rfind fun (n_2 : ℕ) ↦ Part.some (decide (f (n_2 ::ᵥ v) = 0))) v

Tactic:
refine ⟨rfind cf, fun v => ?_⟩
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
cf : Code
hf : ∀ (v : List.Vector ℕ (n + 1)), cf.eval (↑v : List ℕ) = pure <$> (↑f : List.Vector ℕ (n + 1) →. ℕ) v
v : List.Vector ℕ n
⊢ ∀ (a : ℕ), cf.eval (↑(a ::ᵥ v) : List ℕ) = pure <$> (↑f : List.Vector ℕ (n + 1) →. ℕ) (a ::ᵥ v)

Tactic:
replace hf := fun a => hf (a ::ᵥ v)
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (↑(a ::ᵥ v) : List ℕ) = pure <$> (↑f : List.Vector ℕ (n + 1) →. ℕ) (a ::ᵥ v)
⊢ ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]

Tactic:
simp only [Part.map_eq_map, Part.map_some, Vector.cons_val, PFun.coe_val,
      show ∀ x, pure x = [x] from fun _ => rfl] at hf ⊢

Premises used: List.Vector.cons_val, PFun.coe_val, Part.map_eq_map, Part.map_some, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
⊢ cf.rfind.eval (↑v : List ℕ) = Part.map pure (Nat.rfind fun (n_2 : ℕ) ↦ Part.some (decide (f (n_2 ::ᵥ v) = 0)))

Tactic:
Part.ext fun x => ?_

Premises used: Part.ext
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
rfind :
  ∀ (x : List ℕ),
    x ∈ cf.rfind.eval (↑v : List ℕ) ↔
      Membership.mem (γ := Part (List ℕ))
        (Part.map pure (Nat.rfind fun (n_2 : ℕ) ↦ Part.some (decide (f (n_2 ::ᵥ v) = 0)))) x
⊢ cf.rfind.eval (↑v : List ℕ) = Part.map pure (Nat.rfind fun (n_2 : ℕ) ↦ Part.some (decide (f (n_2 ::ᵥ v) = 0)))

Tactic:
refine Part.ext fun x => ?_

Premises used: Part.ext
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
x : List ℕ
rfind :
  (∃ (a : List ℕ),
      Membership.mem (γ := Part (List ℕ))
          (PFun.fix
            (fun (v : List ℕ) ↦
              (cf.eval v).bind fun (y : List ℕ) ↦
                Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
            (0 :: (↑v : List ℕ)))
          a ∧
        x = [a.headI.pred]) ↔
    ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = x
⊢ x ∈ cf.rfind.eval (↑v : List ℕ) ↔
    Membership.mem (γ := Part (List ℕ))
      (Part.map pure (Nat.rfind fun (n_2 : ℕ) ↦ Part.some (decide (f (n_2 ::ᵥ v) = 0)))) x

Tactic:
simp only [rfind, Part.bind_eq_bind, Part.pure_eq_some, Part.bind_some,
      cons_eval, comp_eval, fix_eval, tail_eval, succ_eval, zero'_eval,
      List.headI_cons, pred_eval, Part.map_some, false_eq_decide_iff,
      Part.mem_bind_iff, Part.mem_map_iff, Nat.mem_rfind,
      List.tail_cons, true_eq_decide_iff, Part.mem_some_iff, Part.map_bind]

Premises used: Part.mem_bind_iff, Turing.ToPartrec.Code.comp_eval, Part.map_bind, Turing.ToPartrec.Code.pred_eval, Part.bind_some, Part.mem_some_iff, Turing.ToPartrec.Code.zero'_eval, Turing.ToPartrec.Code.tail_eval, Nat.mem_rfind, false_eq_decide_iff, List.tail_cons, List.headI_cons, Turing.ToPartrec.Code.cons_eval, Turing.ToPartrec.Code.rfind, Part.map_some, Turing.ToPartrec.Code.succ_eval, Turing.ToPartrec.Code.fix_eval, Part.mem_map_iff, Part.pure_eq_some, Part.bind_eq_bind, true_eq_decide_iff
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
x : List ℕ
rfind :
  (∃ (a : List ℕ),
      Membership.mem (γ := Part (List ℕ))
          (PFun.fix
            (fun (v : List ℕ) ↦
              (cf.eval v).bind fun (y : List ℕ) ↦
                Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
            (0 :: (↑v : List ℕ)))
          a ∧
        x = [a.headI.pred]) →
    ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = x
rfind₁ :
  (∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = x) →
    ∃ (a : List ℕ),
      Membership.mem (γ := Part (List ℕ))
          (PFun.fix
            (fun (v : List ℕ) ↦
              (cf.eval v).bind fun (y : List ℕ) ↦
                Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
            (0 :: (↑v : List ℕ)))
          a ∧
        x = [a.headI.pred]
⊢ (∃ (a : List ℕ),
      Membership.mem (γ := Part (List ℕ))
          (PFun.fix
            (fun (v : List ℕ) ↦
              (cf.eval v).bind fun (y : List ℕ) ↦
                Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
            (0 :: (↑v : List ℕ)))
          a ∧
        x = [a.headI.pred]) ↔
    ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = x

Tactic:
constructor
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
v' : List ℕ
h1 :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: (↑v : List ℕ)))
    v'
this :
  ∀ (v₁ : List ℕ),
    Membership.mem (γ := Part (List ℕ))
        (PFun.fix
          (fun (v : List ℕ) ↦
            (cf.eval v).bind fun (y : List ℕ) ↦
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          v₁)
        v' →
      ∀ (n_2 : ℕ),
        v₁ = n_2 :: (↑v : List ℕ) →
          (∀ m < n_2, ¬f (m ::ᵥ v) = 0) →
            ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
⊢ ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = [v'.headI.pred]

Tactic:
exact this _ h1 0 rfl (by rintro _ ⟨⟩)

Premises used: OfNat.ofNat, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
v' : List ℕ
h1 :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (0 :: (↑v : List ℕ)))
    v'
rfind :
  ∀ (v₁ : List ℕ),
    Membership.mem (γ := Part (List ℕ))
        (PFun.fix
          (fun (v : List ℕ) ↦
            (cf.eval v).bind fun (y : List ℕ) ↦
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          v₁)
        v' →
      ∀ (n_2 : ℕ),
        v₁ = n_2 :: (↑v : List ℕ) →
          (∀ m < n_2, ¬f (m ::ᵥ v) = 0) →
            ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
⊢ ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = [v'.headI.pred]

Tactic:
suffices ∀ v₁ : List ℕ, v' ∈ PFun.fix
        (fun v => (cf.eval v).bind fun y => Part.some <|
          if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail)
            else Sum.inr (v.headI.succ :: v.tail)) v₁ →
        ∀ n, (v₁ = n :: v.val) → (∀ m < n, ¬f (m ::ᵥ v) = 0) →
          ∃ a : ℕ,
            (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
        by exact this _ h1 0 rfl (by rintro _ ⟨⟩)
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
v' v₀ : List ℕ
h1 :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      v₀)
    v'
⊢ ∀ (n_2 : ℕ),
    v₀ = n_2 :: (↑v : List ℕ) →
      (∀ m < n_2, ¬f (m ::ᵥ v) = 0) →
        ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]

Tactic:
PFun.fixInduction h1 fun v₁ h2 IH => ?_

Premises used: PFun.fixInduction
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
v' v₀ : List ℕ
h1 :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      v₀)
    v'
rfind :
  ∀ (v₁ : List ℕ)
    (h2 :
      Membership.mem (γ := Part (List ℕ))
        (PFun.fix
          (fun (v : List ℕ) ↦
            (cf.eval v).bind fun (y : List ℕ) ↦
              Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
          v₁)
        v')
    (IH :
      ∀ (a'' : List ℕ),
        Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
            ((cf.eval v₁).bind fun (y : List ℕ) ↦
              Part.some
                (if y.headI = 0 then Sum.inl (v₁.headI.succ :: v₁.tail) else Sum.inr (v₁.headI.succ :: v₁.tail)))
            (Sum.inr a'') →
          ∀ (n_2 : ℕ),
            a'' = n_2 :: (↑v : List ℕ) →
              (∀ m < n_2, ¬f (m ::ᵥ v) = 0) →
                ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred])
    (n_2 : ℕ),
    v₁ = n_2 :: (↑v : List ℕ) →
      (∀ m < n_2, ¬f (m ::ᵥ v) = 0) →
        ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
⊢ ∀ (n_2 : ℕ),
    v₀ = n_2 :: (↑v : List ℕ) →
      (∀ m < n_2, ¬f (m ::ᵥ v) = 0) →
        ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]

Tactic:
refine PFun.fixInduction h1 fun v₁ h2 IH => ?_
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f : List.Vector ℕ (n_2 + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n_2 + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n_2
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
v' v₀ : List ℕ
n : ℕ
h2 :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (n :: (↑v : List ℕ)))
    v'
IH :
  ∀ (a'' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        ((cf.eval (n :: (↑v : List ℕ))).bind fun (y : List ℕ) ↦
          Part.some
            (if y.headI = 0 then Sum.inl ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)
            else Sum.inr ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)))
        (Sum.inr a'') →
      ∀ (n : ℕ),
        a'' = n :: (↑v : List ℕ) →
          (∀ m < n, ¬f (m ::ᵥ v) = 0) →
            ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
hm : ∀ m < n, ¬f (m ::ᵥ v) = 0
⊢ Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
      ((cf.eval (n :: (↑v : List ℕ))).bind fun (y : List ℕ) ↦
        Part.some
          (if y.headI = 0 then Sum.inl ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)
          else Sum.inr ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)))
      (Sum.inl v') ∨
    ∃ (a' : List ℕ),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
          ((cf.eval (n :: (↑v : List ℕ))).bind fun (y : List ℕ) ↦
            Part.some
              (if y.headI = 0 then Sum.inl ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)
              else Sum.inr ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)))
          (Sum.inr a') ∧
        Membership.mem (γ := Part (List ℕ))
          (PFun.fix
            (fun (v : List ℕ) ↦
              (cf.eval v).bind fun (y : List ℕ) ↦
                Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
            a')
          v'

Tactic:
have := PFun.mem_fix_iff.1 h2
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f : List.Vector ℕ (n_2 + 1) → ℕ
h : Nat.Partrec' (↑f : List.Vector ℕ (n_2 + 1) →. ℕ)
cf : Code
v : List.Vector ℕ n_2
hf : ∀ (a : ℕ), cf.eval (a :: (↑v : List ℕ)) = Part.some [f (a ::ᵥ v)]
v' v₀ : List ℕ
n : ℕ
h2 :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        (cf.eval v).bind fun (y : List ℕ) ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (n :: (↑v : List ℕ)))
    v'
IH :
  ∀ (a'' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        ((cf.eval (n :: (↑v : List ℕ))).bind fun (y : List ℕ) ↦
          Part.some
            (if y.headI = 0 then Sum.inl ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)
            else Sum.inr ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)))
        (Sum.inr a'') →
      ∀ (n : ℕ),
        a'' = n :: (↑v : List ℕ) →
          (∀ m < n, ¬f (m ::ᵥ v) = 0) →
            ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
hm : ∀ m < n, ¬f (m ::ᵥ v) = 0
this :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
      ((cf.eval (n :: (↑v : List ℕ))).bind fun (y : List ℕ) ↦
        Part.some
          (if y.headI = 0 then Sum.inl ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)
          else Sum.inr ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)))
      (Sum.inl v') ∨
    ∃ (a' : List ℕ),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
          ((cf.eval (n :: (↑v : List ℕ))).bind fun (y : List ℕ) ↦
            Part.some
              (if y.headI = 0 then Sum.inl ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)
              else Sum.inr ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)))
          (Sum.inr a') ∧
        Membership.mem (γ := Part (List ℕ))
          (PFun.fix
            (fun (v : List ℕ) ↦
              (cf.eval v).bind fun (y : List ℕ) ↦
                Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
            a')
          v'
⊢ Sum.inl v' ∈
      Part.some
        (if [f (n ::ᵥ v)].headI = 0 then Sum.inl ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)
        else Sum.inr ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)) ∨
    ∃ (a' : List ℕ),
      Sum.inr a' ∈
          Part.some
            (if [f (n ::ᵥ v)].headI = 0 then Sum.inl ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)
            else Sum.inr ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail)) ∧
        Membership.mem (γ := Part (List ℕ))
          (PFun.fix
            (fun (v : List ℕ) ↦
              (cf.eval v).bind fun (y : List ℕ) ↦
                Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
            a')
          v'

Tactic:
simp only [hf, Part.bind_some] at this

Premises used: Part.bind_some