awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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
⊢ (∃ (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
have 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]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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'
⊢ ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ pure a = [v'.headI.pred]
have 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]
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 _ ⟨⟩)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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]
have 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]
Tactic: refine PFun.fixInduction h1 fun v₁ h2 IH => ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
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
⊢ ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
have 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'
Tactic: have := PFun.mem_fix_iff.1 h2
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
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'
⊢ ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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 :
  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'
⊢ ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
have pos : ∀ (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'),
  ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
Tactic: split_ifs at this with h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
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'
⊢ ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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 ℕ)
⊢ ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
have 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]
Tactic: subst this
Cleared hypotheses: v', h2, IH, this
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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'
⊢ ∃ (a : ℕ), (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
have neg : ∀ (m : ℕ) (h' : m < n.succ), ¬f (m ::ᵥ v) = 0
Tactic: refine IH (n.succ::v.val) (by simp_all) _ rfl fun m h' => ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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'
m : ℕ
h' : m < n.succ
⊢ ¬f (m ::ᵥ v) = 0
have neg : ∀ (h : m < n), ¬f (m ::ᵥ v) = 0
Tactic: obtain h | rfl := Nat.lt_succ_iff_lt_or_eq.1 h'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
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]
have 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 ℕ))
Tactic: refine ⟨n.succ::v.1, ?_, rfl⟩