awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v : List ℕ
IH :
  ∀ (a'' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
        (Sum.inr a'') →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he_1 : v'.tail ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'.tail)
hr : x ∈ eval step (stepRet k v'.tail)
he_2 : v'.tail ∈ f.fix.eval v
he :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
    (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) (Sum.inl v'.tail)
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
have pos : x ∈ eval step (Cfg.ret (Cont.fix f k) v')
Tactic: refine ⟨_, he₁, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v : List ℕ
IH :
  ∀ (a'' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
        (Sum.inr a'') →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he_1 : v'.tail ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'.tail)
hr : x ∈ eval step (stepRet k v'.tail)
he_2 : v'.tail ∈ f.fix.eval v
he :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
    (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) (Sum.inl v'.tail)
⊢ x ∈ eval step (Cfg.ret (Cont.fix f k) v')
have pos : x ∈ eval step (stepRet (Cont.fix f k) v')
Tactic: rw [reaches_eval]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v : List ℕ
IH :
  ∀ (a'' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
        (Sum.inr a'') →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he_1 : v'.tail ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'.tail)
hr : x ∈ eval step (stepRet k v'.tail)
he_2 : v'.tail ∈ f.fix.eval v
he :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
    (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) (Sum.inl v'.tail)
pos : x ∈ eval step (stepRet (Cont.fix f k) v')
⊢ x ∈ eval step (Cfg.ret (Cont.fix f k) v')
have pos₁ : Reaches step (Cfg.ret (Cont.fix f k) v') (stepRet (Cont.fix f k) v')
Tactic: rw [reaches_eval]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v : List ℕ
IH :
  ∀ (a'' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
        (Sum.inr a'') →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he_1 : v'.tail ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'.tail)
hr : x ∈ eval step (stepRet k v'.tail)
he_2 : v'.tail ∈ f.fix.eval v
he :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
    (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) (Sum.inl v'.tail)
⊢ x ∈ eval step (stepRet (Cont.fix f k) v')
have pos : x ∈ eval step (if v'.headI = 0 then stepRet k v'.tail else stepNormal f (Cont.fix f k) v'.tail)
Tactic: rwa [stepRet, if_pos h]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he_1 : v' ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
        (Sum.inr a'') →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v'' : List ℕ
he₁' :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
    (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) (Sum.inr v'')
right :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
      v'')
    v'
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
have mpr : ∀ (v₁ : List ℕ) (he₁ : v₁ ∈ f.eval v) (he₂ : (if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) = Sum.inr v''),
  ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
Tactic: obtain ⟨v₁, he₁, he₂⟩ := (Part.mem_map_iff _).1 he₁'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he_1 : v' ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
        (Sum.inr a'') →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v'' : List ℕ
he₁' :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
    (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) (Sum.inr v'')
right :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
      v'')
    v'
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
he₂ : (if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) = Sum.inr v''
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
have h : ¬v₁.headI = 0
Tactic: split_ifs at he₂ with h
Cleared hypotheses: he₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he_1 : v' ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
        (Sum.inr a'') →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v'' : List ℕ
he₁' :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
    (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) (Sum.inr v'')
right :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
      v'')
    v'
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
he₂ : (if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) = Sum.inr v''
h : ¬v₁.headI = 0
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
have he₃ : Eq (α := List ℕ ⊕ List ℕ) (Sum.inr v₁.tail) (Sum.inr v'')
Tactic: split_ifs at he₂ with h
Cleared hypotheses: he₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he_1 : v' ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
        (Sum.inr a'') →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v'' : List ℕ
he₁' :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
    (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) (Sum.inr v'')
right :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
      v'')
    v'
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
he₂ : Eq (α := List ℕ ⊕ List ℕ) (Sum.inr v₁.tail) (Sum.inr v'')
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
have he₁'₁ : Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
  (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) (Sum.inr v₁.tail)
Tactic: cases he₂
Cleared hypotheses: v'', he₁', right, he₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (hypothesis)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he_1 : v' ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
        (Sum.inr a'') →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v'' : List ℕ
he₁' :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
    (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) (Sum.inr v'')
right :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
      v'')
    v'
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
he₂ : Eq (α := List ℕ ⊕ List ℕ) (Sum.inr v₁.tail) (Sum.inr v'')
he₁'₁ :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
    (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v)) (Sum.inr v₁.tail)
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
have right : Membership.mem (γ := Part (List ℕ))
  (PFun.fix
    (fun (v : List ℕ) ↦ Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
    v₁.tail)
  v'
Tactic: cases he₂
Cleared hypotheses: v'', he₁', right, he₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he_1 : v' ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
        (Sum.inr a'') →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
right :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
      v₁.tail)
    v'
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
have neg : x ∈ eval step (Cfg.ret (Cont.fix f k) v₁)
Tactic: refine ⟨_, he₁, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he_1 : v' ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
        (Sum.inr a'') →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
right :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
      v₁.tail)
    v'
⊢ x ∈ eval step (Cfg.ret (Cont.fix f k) v₁)
have neg : x ∈ eval step (stepRet (Cont.fix f k) v₁)
Tactic: rw [reaches_eval]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he_1 : v' ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
        (Sum.inr a'') →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
right :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
      v₁.tail)
    v'
neg : x ∈ eval step (stepRet (Cont.fix f k) v₁)
⊢ x ∈ eval step (Cfg.ret (Cont.fix f k) v₁)
have neg₁ : Reaches step (Cfg.ret (Cont.fix f k) v₁) (stepRet (Cont.fix f k) v₁)
Tactic: rw [reaches_eval]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he_1 : v' ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
v : List ℕ
he : v' ∈ f.fix.eval v
IH :
  ∀ (a'' : List ℕ),
    Membership.mem (γ := Part (List ℕ ⊕ List ℕ))
        (Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
        (Sum.inr a'') →
      x ∈ eval step (stepNormal f (Cont.fix f k) a'')
v₁ : List ℕ
he₁ : v₁ ∈ f.eval v
h : ¬v₁.headI = 0
right :
  Membership.mem (γ := Part (List ℕ))
    (PFun.fix
      (fun (v : List ℕ) ↦
        Part.map (fun (v : List ℕ) ↦ if v.headI = 0 then Sum.inl v.tail else Sum.inr v.tail) (f.eval v))
      v₁.tail)
    v'
⊢ x ∈ eval step (stepRet (Cont.fix f k) v₁)
have neg : x ∈ eval step (stepNormal f (Cont.fix f k) v₁.tail)
Tactic: rw [stepRet, if_neg h]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ eval step (stepNormal (f.cons fs) k v) = do
    let v ← (f.cons fs).eval v
    eval step (Cfg.ret k v)
have cons : eval step ((fun (k : Cont) (v : List ℕ) ↦ stepNormal f (Cont.cons₁ fs v k) v) k v) = do
  let v ← (f.cons fs).eval v
  eval step (Cfg.ret k v)
Tactic: rw [stepNormal]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun (k : Cont) (v : List ℕ) ↦ stepNormal f (Cont.cons₁ fs v k) v) k v) = do
    let v ← (f.cons fs).eval v
    eval step (Cfg.ret k v)
have cons : Eq (α := Part Cfg)
  (do
    let v_1 ← f.eval v
    eval step (Cfg.ret (Cont.cons₁ fs v k) v_1))
  do
  let v ←
    (fun (v : List ℕ) ↦
          (do
            let n ← f.eval v
            let ns ← fs.eval v
            pure (n.headI :: ns) : Part (List ℕ)))
        v
  eval step (Cfg.ret k v)
Tactic: rw [Code.eval, IHf]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ Eq (α := Part Cfg)
    (do
      let v_1 ← f.eval v
      eval step (Cfg.ret (Cont.cons₁ fs v k) v_1))
    do
    let v ←
      (fun (v : List ℕ) ↦
            (do
              let n ← f.eval v
              let ns ← fs.eval v
              pure (n.headI :: ns) : Part (List ℕ)))
          v
    eval step (Cfg.ret k v)
have cons : Eq (α := Part Cfg)
  (do
    let v_1 ← f.eval v
    eval step (Cfg.ret (Cont.cons₁ fs v k) v_1))
  do
  let x ← f.eval v
  let x_1 ← fs.eval v
  eval step (Cfg.ret k (x.headI :: x_1))
Tactic: simp only [bind_assoc, pure_bind]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ Eq (α := Part Cfg)
    (do
      let v_1 ← f.eval v
      eval step (Cfg.ret (Cont.cons₁ fs v k) v_1))
    do
    let x ← f.eval v
    let x_1 ← fs.eval v
    eval step (Cfg.ret k (x.headI :: x_1))
have cons : Eq (α := List ℕ → Part Cfg) (fun (v_1 : List ℕ) ↦ eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) fun (x : List ℕ) ↦ do
  let x_1 ← fs.eval v
  eval step (Cfg.ret k (x.headI :: x_1))
Tactic: congr
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v : List ℕ
⊢ Eq (α := List ℕ → Part Cfg) (fun (v_1 : List ℕ) ↦ eval step (Cfg.ret (Cont.cons₁ fs v k) v_1)) fun (x : List ℕ) ↦ do
    let x_1 ← fs.eval v
    eval step (Cfg.ret k (x.headI :: x_1))
have cons : ∀ (v_1 : List ℕ),
  eval step (Cfg.ret (Cont.cons₁ fs v k) v_1) = do
    let x ← fs.eval v
    eval step (Cfg.ret k (v_1.headI :: x))
Tactic: funext v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v_1 v : List ℕ
⊢ eval step (Cfg.ret (Cont.cons₁ fs v_1 k) v) = do
    let x ← fs.eval v_1
    eval step (Cfg.ret k (v.headI :: x))
have cons : eval step (stepRet (Cont.cons₁ fs v_1 k) v) = do
  let x ← fs.eval v_1
  eval step (Cfg.ret k (v.headI :: x))
Tactic: rw [reaches_eval]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v_1 v : List ℕ
cons :
  eval step (stepRet (Cont.cons₁ fs v_1 k) v) = do
    let x ← fs.eval v_1
    eval step (Cfg.ret k (v.headI :: x))
⊢ eval step (Cfg.ret (Cont.cons₁ fs v_1 k) v) = do
    let x ← fs.eval v_1
    eval step (Cfg.ret k (v.headI :: x))
have cons₁ : Reaches step (Cfg.ret (Cont.cons₁ fs v_1 k) v) (stepRet (Cont.cons₁ fs v_1 k) v)
Tactic: rw [reaches_eval]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v_1 v : List ℕ
cons :
  eval step (stepRet (Cont.cons₁ fs v_1 k) v) = do
    let x ← fs.eval v_1
    eval step (Cfg.ret k (v.headI :: x))
cons₁ : Reaches step (Cfg.ret (Cont.cons₁ fs v_1 k) v) (stepRet (Cont.cons₁ fs v_1 k) v)
⊢ eval step (Cfg.ret (Cont.cons₁ fs v_1 k) v) = do
    let x ← fs.eval v_1
    eval step (Cfg.ret k (v.headI :: x))
have rw : Cfg
Tactic: rw [reaches_eval]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v_1 v : List ℕ
⊢ eval step (stepRet (Cont.cons₁ fs v_1 k) v) = do
    let x ← fs.eval v_1
    eval step (Cfg.ret k (v.headI :: x))
have cons : Eq (α := Part Cfg)
  (do
    let v_2 ← fs.eval v_1
    eval step (Cfg.ret (Cont.cons₂ v k) v_2))
  do
  let x ← fs.eval v_1
  eval step (Cfg.ret k (v.headI :: x))
Tactic: rw [stepRet, IHfs]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v_1 v : List ℕ
⊢ Eq (α := Part Cfg)
    (do
      let v_2 ← fs.eval v_1
      eval step (Cfg.ret (Cont.cons₂ v k) v_2))
    do
    let x ← fs.eval v_1
    eval step (Cfg.ret k (v.headI :: x))
have cons : Eq (α := List ℕ → Part Cfg) (fun (v_2 : List ℕ) ↦ eval step (Cfg.ret (Cont.cons₂ v k) v_2)) fun (x : List ℕ) ↦
  eval step (Cfg.ret k (v.headI :: x))
Tactic: congr
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v_1 v : List ℕ
⊢ Eq (α := List ℕ → Part Cfg) (fun (v_2 : List ℕ) ↦ eval step (Cfg.ret (Cont.cons₂ v k) v_2)) fun (x : List ℕ) ↦
    eval step (Cfg.ret k (v.headI :: x))
have cons : ∀ (v' : List ℕ), eval step (Cfg.ret (Cont.cons₂ v k) v') = eval step (Cfg.ret k (v.headI :: v'))
Tactic: funext v'
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v_1 v v' : List ℕ
⊢ eval step (Cfg.ret (Cont.cons₂ v k) v') = eval step (Cfg.ret k (v.headI :: v'))
have cons : eval step (Cfg.ret (Cont.cons₂ v k) v') = eval step (stepRet (Cont.cons₂ v k) v')
Tactic: refine Eq.trans (b := eval step (stepRet (Cont.cons₂ v k) v')) ?_ (Eq.symm ?_)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f fs : Code
IHf : f.Ok
IHfs : fs.Ok
k : Cont
v_1 v v' : List ℕ
cons : eval step (Cfg.ret (Cont.cons₂ v k) v') = eval step (stepRet (Cont.cons₂ v k) v')
⊢ eval step (Cfg.ret (Cont.cons₂ v k) v') = eval step (Cfg.ret k (v.headI :: v'))
have cons₁ : eval step (Cfg.ret k (v.headI :: v')) = eval step (stepRet (Cont.cons₂ v k) v')
Tactic: refine Eq.trans (b := eval step (stepRet (Cont.cons₂ v k) v')) ?_ (Eq.symm ?_)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ eval step (stepNormal (f.comp g) k v) = do
    let v ← (f.comp g).eval v
    eval step (Cfg.ret k v)
have comp : eval step ((fun (k : Cont) (v : List ℕ) ↦ stepNormal g (Cont.comp f k) v) k v) = do
  let v ← (f.comp g).eval v
  eval step (Cfg.ret k v)
Tactic: rw [stepNormal]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ eval step ((fun (k : Cont) (v : List ℕ) ↦ stepNormal g (Cont.comp f k) v) k v) = do
    let v ← (f.comp g).eval v
    eval step (Cfg.ret k v)
have comp : Eq (α := Part Cfg)
  (do
    let v ← g.eval v
    eval step (Cfg.ret (Cont.comp f k) v))
  do
  let v ← (fun (v : List ℕ) ↦ g.eval v >>= f.eval) v
  eval step (Cfg.ret k v)
Tactic: rw [Code.eval, IHg]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ Eq (α := Part Cfg)
    (do
      let v ← g.eval v
      eval step (Cfg.ret (Cont.comp f k) v))
    do
    let v ← (fun (v : List ℕ) ↦ g.eval v >>= f.eval) v
    eval step (Cfg.ret k v)
have comp : Eq (α := Part Cfg)
  (do
    let v ← g.eval v
    eval step (Cfg.ret (Cont.comp f k) v))
  do
  let x ← g.eval v
  let v ← f.eval x
  eval step (Cfg.ret k v)
Tactic: simp only [bind_assoc]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ Eq (α := Part Cfg)
    (do
      let v ← g.eval v
      eval step (Cfg.ret (Cont.comp f k) v))
    do
    let x ← g.eval v
    let v ← f.eval x
    eval step (Cfg.ret k v)
have comp : Eq (α := List ℕ → Part Cfg) (fun (v : List ℕ) ↦ eval step (Cfg.ret (Cont.comp f k) v)) fun (x : List ℕ) ↦ do
  let v ← f.eval x
  eval step (Cfg.ret k v)
Tactic: congr
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
⊢ Eq (α := List ℕ → Part Cfg) (fun (v : List ℕ) ↦ eval step (Cfg.ret (Cont.comp f k) v)) fun (x : List ℕ) ↦ do
    let v ← f.eval x
    eval step (Cfg.ret k v)
have comp : ∀ (v : List ℕ),
  eval step (Cfg.ret (Cont.comp f k) v) = do
    let v ← f.eval v
    eval step (Cfg.ret k v)
Tactic: funext v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v_1 v : List ℕ
⊢ eval step (Cfg.ret (Cont.comp f k) v) = do
    let v ← f.eval v
    eval step (Cfg.ret k v)
have comp : eval step (stepRet (Cont.comp f k) v) = do
  let v ← f.eval v
  eval step (Cfg.ret k v)
Tactic: rw [reaches_eval]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v_1 v : List ℕ
comp :
  eval step (stepRet (Cont.comp f k) v) = do
    let v ← f.eval v
    eval step (Cfg.ret k v)
⊢ eval step (Cfg.ret (Cont.comp f k) v) = do
    let v ← f.eval v
    eval step (Cfg.ret k v)
have comp₁ : Reaches step (Cfg.ret (Cont.comp f k) v) (stepRet (Cont.comp f k) v)
Tactic: rw [reaches_eval]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v_1 v : List ℕ
comp :
  eval step (stepRet (Cont.comp f k) v) = do
    let v ← f.eval v
    eval step (Cfg.ret k v)
comp₁ : Reaches step (Cfg.ret (Cont.comp f k) v) (stepRet (Cont.comp f k) v)
⊢ eval step (Cfg.ret (Cont.comp f k) v) = do
    let v ← f.eval v
    eval step (Cfg.ret k v)
have rw : Cfg
Tactic: rw [reaches_eval]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v_1 v : List ℕ
⊢ eval step (stepRet (Cont.comp f k) v) = do
    let v ← f.eval v
    eval step (Cfg.ret k v)
have comp : eval step (stepNormal f k v) = do
  let v ← f.eval v
  eval step (Cfg.ret k v)
Tactic: rw [stepRet, IHf]