awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f : List.Vector ℕ (n_2 + 1) → ℕ
h_1 : 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
h : [f (n ::ᵥ v)].headI = 0
this :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
      (Part.some (Sum.inl ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail))) (Sum.inl v') ∨
    ∃ (a' : List ℕ),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
          (Part.some (Sum.inl ((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'
⊢ v' = n.succ :: (↑v : List ℕ)

Tactic:
simp only [List.headI_cons, exists_false, or_false, Part.mem_some_iff,
          List.tail_cons, false_and, Sum.inl.injEq, reduceCtorEq] at this

Premises used: reduceCtorEq, Part.mem_some_iff, false_and, List.tail_cons, Sum.inl.injEq, List.headI_cons, exists_false, or_false
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f : List.Vector ℕ (n_2 + 1) → ℕ
h_1 : 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
h : [f (n ::ᵥ v)].headI = 0
this : v' = n.succ :: (↑v : List ℕ)
pos :
  ∀
    (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 ℕ)))
        (n.succ :: (↑v : List ℕ)))
    (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_3 : ℕ),
            a'' = n_3 :: (↑v : List ℕ) →
              (∀ m < n_3, ¬f (m ::ᵥ v) = 0) →
                ∃ (a : ℕ),
                  (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧
                    [a] = [(n.succ :: (↑v : List ℕ)).headI.pred]),
    ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [(n.succ :: (↑v : List ℕ)).headI.pred]
⊢ ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]

Tactic:
subst this
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f : List.Vector ℕ (n_2 + 1) → ℕ
h_1 : 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₀ : List ℕ
n : ℕ
hm : ∀ m < n, ¬f (m ::ᵥ v) = 0
h : [f (n ::ᵥ v)].headI = 0
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 ℕ)))
    (n.succ :: (↑v : List ℕ))
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_3 : ℕ),
        a'' = n_3 :: (↑v : List ℕ) →
          (∀ m < n_3, ¬f (m ::ᵥ v) = 0) →
            ∃ (a : ℕ),
              (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [(n.succ :: (↑v : List ℕ)).headI.pred]
⊢ ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [(n.succ :: (↑v : List ℕ)).headI.pred]

Tactic:
⟨_, ⟨h, @hm⟩, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f : List.Vector ℕ (n_2 + 1) → ℕ
h_1 : 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₀ : List ℕ
n : ℕ
hm : ∀ m < n, ¬f (m ::ᵥ v) = 0
h : [f (n ::ᵥ v)].headI = 0
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 ℕ)))
    (n.succ :: (↑v : List ℕ))
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_3 : ℕ),
        a'' = n_3 :: (↑v : List ℕ) →
          (∀ m < n_3, ¬f (m ::ᵥ v) = 0) →
            ∃ (a : ℕ),
              (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [(n.succ :: (↑v : List ℕ)).headI.pred]
⊢ ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [(n.succ :: (↑v : List ℕ)).headI.pred]

Tactic:
exact ⟨_, ⟨h, @hm⟩, rfl⟩
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f : List.Vector ℕ (n_2 + 1) → ℕ
h_1 : 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
h : ¬[f (n ::ᵥ v)].headI = 0
this :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
      (Part.some (Sum.inr ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail))) (Sum.inl v') ∨
    ∃ (a' : List ℕ),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
          (Part.some (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'
⊢ 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 (n.succ :: (↑v : List ℕ)))

Tactic:
simp_all
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f : List.Vector ℕ (n_2 + 1) → ℕ
h_1 : 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
h : ¬[f (n ::ᵥ v)].headI = 0
this :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
      (Part.some (Sum.inr ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail))) (Sum.inl v') ∨
    ∃ (a' : List ℕ),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
          (Part.some (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'
neg : ∀ (m : ℕ) (h' : m < n.succ), ¬f (m ::ᵥ v) = 0
⊢ ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]

Tactic:
refine IH (n.succ::v.val) (by simp_all) _ rfl fun m h' => ?_

Premises used: List.cons, Subtype.val, Nat.succ, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f : List.Vector ℕ (n_2 + 1) → ℕ
h_1 : 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
h_2 : ¬[f (n ::ᵥ v)].headI = 0
this :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
      (Part.some (Sum.inr ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail))) (Sum.inl v') ∨
    ∃ (a' : List ℕ),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
          (Part.some (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'
m : ℕ
h' : m < n.succ
h : m < n
⊢ ¬f (m ::ᵥ v) = 0

Tactic:
hm _ h
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n : ℕ
f : List.Vector ℕ (n + 1) → ℕ
h_1 : 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 ℕ
m : ℕ
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)))
      (m :: (↑v : List ℕ)))
    v'
IH :
  ∀ (a'' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        ((cf.eval (m :: (↑v : List ℕ))).bind fun (y : List ℕ) ↦
          Part.some
            (if y.headI = 0 then Sum.inl ((m :: (↑v : List ℕ)).headI.succ :: (m :: (↑v : List ℕ)).tail)
            else Sum.inr ((m :: (↑v : List ℕ)).headI.succ :: (m :: (↑v : List ℕ)).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]
hm : ∀ m_1 < m, ¬f (m_1 ::ᵥ v) = 0
h : ¬[f (m ::ᵥ v)].headI = 0
this :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
      (Part.some (Sum.inr ((m :: (↑v : List ℕ)).headI.succ :: (m :: (↑v : List ℕ)).tail))) (Sum.inl v') ∨
    ∃ (a' : List ℕ),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
          (Part.some (Sum.inr ((m :: (↑v : List ℕ)).headI.succ :: (m :: (↑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'
h' : m < m.succ
⊢ ¬f (m ::ᵥ v) = 0

Tactic:
h

Premises used: List.headI
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
n_1 : ℕ
f_1 : List.Vector ℕ n_1 →. ℕ
n_2 : ℕ
f : List.Vector ℕ (n_2 + 1) → ℕ
h_1 : 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
h_2 : ¬[f (n ::ᵥ v)].headI = 0
this :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
      (Part.some (Sum.inr ((n :: (↑v : List ℕ)).headI.succ :: (n :: (↑v : List ℕ)).tail))) (Sum.inl v') ∨
    ∃ (a' : List ℕ),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
          (Part.some (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'
m : ℕ
h' : m < n.succ
h : m < n
⊢ ¬f (m ::ᵥ v) = 0

Tactic:
exacts [hm _ h, h]
-- 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)]
n : ℕ
hn : f (n ::ᵥ v) = 0
hm : ∀ {m : ℕ}, m < n → ¬f (m ::ᵥ v) = 0
⊢ ∃ (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 ∧
      pure n = [a.headI.pred]

Tactic:
⟨n.succ::v.1, ?_, rfl⟩

Premises used: List.cons, And.intro, Exists.intro, Subtype.val, Nat.succ, rfl
-- 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)]
n : ℕ
hn : f (n ::ᵥ v) = 0
hm : ∀ {m : ℕ}, m < n → ¬f (m ::ᵥ v) = 0
rfind :
  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 ℕ)))
    (n.succ :: (↑v : List ℕ))
⊢ ∃ (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 ∧
      pure n = [a.headI.pred]

Tactic:
refine ⟨n.succ::v.1, ?_, rfl⟩
-- 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)]
n : ℕ
hn : f (n ::ᵥ v) = 0
hm : ∀ {m : ℕ}, 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 (n.succ :: (↑v : List ℕ)))

Tactic:
simp [hf, hn]
-- 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)]
n : ℕ
hn : f (n ::ᵥ v) = 0
hm : ∀ {m : ℕ}, m < n → ¬f (m ::ᵥ v) = 0
⊢ 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 ℕ)))
    (n.succ :: (↑v : List ℕ))

Tactic:
have : (n.succ::v.1 : List ℕ) ∈
        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))
            (n::v.val) :=
        PFun.mem_fix_iff.2 (Or.inl (by simp [hf, hn]))
-- 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)]
n : ℕ
hn : f (n ::ᵥ v) = 0
hm : ∀ {m : ℕ}, m < n → ¬f (m ::ᵥ v) = 0
this :
  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 ℕ)))
    (n.succ :: (↑v : List ℕ))
rfind :
  ∀ (w : List ℕ)
    (this :
      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 ℕ)))
        w),
    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 ℕ)))
      w
⊢ 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 ℕ)))
    (n.succ :: (↑v : List ℕ))

Tactic:
generalize (n.succ :: v.1 : List ℕ) = w at this ⊢

Premises used: List.cons, Subtype.val, Nat.succ
-- 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)]
w : List ℕ
hm : ∀ {m : ℕ}, m < 0 → ¬f (m ::ᵥ v) = 0
this :
  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 ℕ)))
    w
⊢ 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 ℕ)))
    w

Tactic:
this