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 c : Cfg
he_1 : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v'.tail
v₂ : List ℕ
hv₂ : v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail
h₃ : x ∈ eval step (Cfg.ret k v₂)
⊢ 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'.tail))
      (Sum.inl v₂) ∨
    ∃ (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'.tail))
          (Sum.inr a') ∧
        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))
            a')
          v₂
have neg : (Sum.inl v₂ = if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∨
  ∃ (a' : List ℕ),
    (Sum.inr a' = if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∧
      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))
          a')
        v₂
Tactic: simp only [Part.eq_some_iff.2 hv₁, Part.map_some, Part.mem_some_iff]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he_1 : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v'.tail
v₂ : List ℕ
hv₂ : v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail
h₃ : x ∈ eval step (Cfg.ret k v₂)
⊢ (Sum.inl v₂ = if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∨
    ∃ (a' : List ℕ),
      (Sum.inr a' = if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∧
        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))
            a')
          v₂
have pos : v₁.headI = 0 →
  ∀ (hv₂ : Membership.mem (γ := Part (List ℕ)) (pure v₁.tail) v₂),
    Eq (α := List ℕ ⊕ List ℕ) (Sum.inl v₂) (Sum.inl v₁.tail) ∨
      ∃ (a' : List ℕ),
        False ∧
          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))
              a')
            v₂
Tactic: split_ifs at hv₂ ⊢
Cleared hypotheses: hv₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he_1 : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v'.tail
v₂ : List ℕ
hv₂ : v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail
h₃ : x ∈ eval step (Cfg.ret k v₂)
pos :
  v₁.headI = 0 →
    ∀ (hv₂ : Membership.mem (γ := Part (List ℕ)) (pure v₁.tail) v₂),
      Eq (α := List ℕ ⊕ List ℕ) (Sum.inl v₂) (Sum.inl v₁.tail) ∨
        ∃ (a' : List ℕ),
          False ∧
            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))
                a')
              v₂
⊢ (Sum.inl v₂ = if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∨
    ∃ (a' : List ℕ),
      (Sum.inr a' = if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∧
        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))
            a')
          v₂
have neg : ¬v₁.headI = 0 →
  ∀ (hv₂ : v₂ ∈ f.fix.eval v₁.tail),
    False ∨
      ∃ (a' : List ℕ),
        Eq (α := List ℕ ⊕ List ℕ) (Sum.inr a') (Sum.inr v₁.tail) ∧
          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))
              a')
            v₂
Tactic: split_ifs at hv₂ ⊢
Cleared hypotheses: hv₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he_1 : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v'.tail
v₂ : List ℕ
hv₂ : v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail
h₃ : x ∈ eval step (Cfg.ret k v₂)
⊢ (Sum.inl v₂ = if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∨
    ∃ (a' : List ℕ),
      (Sum.inr a' = if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∧
        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))
            a')
          v₂
have pos : v₁.headI = 0 →
  ∀ (hv₂ : Membership.mem (γ := Part (List ℕ)) (pure v₁.tail) v₂),
    Eq (α := List ℕ ⊕ List ℕ) (Sum.inl v₂) (Sum.inl v₁.tail) ∨
      ∃ (a' : List ℕ),
        False ∧
          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))
              a')
            v₂
Tactic: split_ifs at hv₂ ⊢ <;> [exact Or.inl (congr_arg Sum.inl (Part.mem_some_iff.1 hv₂));
          exact Or.inr ⟨_, rfl, hv₂⟩]
Cleared hypotheses: hv₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v_1 : List ℕ
fok : f.Ok
x c : Cfg
he_1 : x ∈ eval step c
v v' : List ℕ
IH :
  ∀ (a' : Cfg),
    step (stepRet (Cont.fix f k) v') = some a' →
      ∀ (v : List ℕ) (c' : Cfg),
        a' = c'.then (Cont.fix f k) →
          Reaches step (stepNormal f Cont.halt v) c' →
            ∃ v₁ ∈ f.eval v,
              ∃ v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail, x ∈ eval step (Cfg.ret k v₂)
hr : Reaches step (stepNormal f Cont.halt v) (Cfg.halt v')
h₁ : v' ∈ f.eval v
h₂_1 : Cfg.halt v' ∈ eval step (Cfg.ret Cont.halt v')
h₂ : Cfg.halt v' ∈ eval step (stepRet Cont.halt v')
he : ¬v'.headI = 0
h : x ∈ eval step (stepNormal f (Cont.fix f k) v'.tail)
k₀ : Cont
v₀ : List ℕ
e₀ : stepNormal f Cont.halt v'.tail = Cfg.ret k₀ v₀
e₁ : stepNormal f (Cont.fix f k) v'.tail = Cfg.ret (k₀.then (Cont.fix f k)) v₀
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v'.tail
v₂ : List ℕ
hv₂ : v₂ ∈ if v₁.headI = 0 then pure v₁.tail else f.fix.eval v₁.tail
h₃ : x ∈ eval step (Cfg.ret k v₂)
pos :
  v₁.headI = 0 →
    ∀ (hv₂ : Membership.mem (γ := Part (List ℕ)) (pure v₁.tail) v₂),
      Eq (α := List ℕ ⊕ List ℕ) (Sum.inl v₂) (Sum.inl v₁.tail) ∨
        ∃ (a' : List ℕ),
          False ∧
            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))
                a')
              v₂
⊢ (Sum.inl v₂ = if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∨
    ∃ (a' : List ℕ),
      (Sum.inr a' = if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∧
        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))
            a')
          v₂
have neg : ¬v₁.headI = 0 →
  ∀ (hv₂ : v₂ ∈ f.fix.eval v₁.tail),
    False ∨
      ∃ (a' : List ℕ),
        Eq (α := List ℕ ⊕ List ℕ) (Sum.inr a') (Sum.inr v₁.tail) ∧
          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))
              a')
            v₂
Tactic: split_ifs at hv₂ ⊢ <;> [exact Or.inl (congr_arg Sum.inl (Part.mem_some_iff.1 hv₂));
          exact Or.inr ⟨_, rfl, hv₂⟩]
Cleared hypotheses: hv₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he : v' ∈ f.fix.eval v
hr : x ∈ eval step (Cfg.ret k v')
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v)
have mpr : ∀ (hr : x ∈ eval step (stepRet k v')), x ∈ eval step (stepNormal f (Cont.fix f k) v)
Tactic: rw [reaches_eval] at hr
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he : v' ∈ f.fix.eval v
hr : x ∈ eval step (Cfg.ret k v')
mpr : ∀ (hr : x ∈ eval step (stepRet k v')), x ∈ eval step (stepNormal f (Cont.fix f k) v)
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v)
have mpr₁ : Reaches step (Cfg.ret k v') (stepRet k v')
Tactic: rw [reaches_eval] at hr
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
v' : List ℕ
he : v' ∈ f.fix.eval v
hr_1 : x ∈ eval step (Cfg.ret k v')
hr : x ∈ eval step (stepRet k v')
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v)
have mpr : ∀ (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'')),
  x ∈ eval step (stepNormal f (Cont.fix f k) v)
Tactic: refine PFun.fixInduction he fun v (he : v' ∈ f.fix.eval v) IH => ?_
-- 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'')
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v)
have mpr : ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
Tactic: rw [fok, Part.bind_eq_bind, Part.mem_bind_iff]
-- 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'')
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
have mpr : ∀
  (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')),
  ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
Tactic: obtain he | ⟨v'', he₁', _⟩ := PFun.mem_fix_iff.1 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'')
mpr :
  ∀
    (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')),
    ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
have mpr₁ : ∀ (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'')),
  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)
Tactic: obtain he | ⟨v'', he₁', _⟩ := PFun.mem_fix_iff.1 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_2 : 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'')
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')
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
have mpr : ∀ (v'_1 : List ℕ) (he₁ : v'_1 ∈ f.eval v)
  (he₂ : (if v'_1.headI = 0 then Sum.inl v'_1.tail else Sum.inr v'_1.tail) = Sum.inl 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'_1 : List ℕ
he_1 : v'_1 ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'_1)
hr : x ∈ eval step (stepRet k v'_1)
v : List ℕ
he_2 : v'_1 ∈ 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'')
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'_1)
v' : List ℕ
he₁ : v' ∈ f.eval v
he₂ : (if v'.headI = 0 then Sum.inl v'.tail else Sum.inr v'.tail) = Sum.inl v'_1
⊢ ∃ 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'_1 : List ℕ
he_1 : v'_1 ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'_1)
hr : x ∈ eval step (stepRet k v'_1)
v : List ℕ
he_2 : v'_1 ∈ 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'')
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'_1)
v' : List ℕ
he₁ : v' ∈ f.eval v
he₂ : (if v'.headI = 0 then Sum.inl v'.tail else Sum.inr v'.tail) = Sum.inl v'_1
h : v'.headI = 0
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
have he₃ : Eq (α := List ℕ ⊕ List ℕ) (Sum.inl v'.tail) (Sum.inl v'_1)
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'_1 : List ℕ
he_1 : v'_1 ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'_1)
hr : x ∈ eval step (stepRet k v'_1)
v : List ℕ
he_2 : v'_1 ∈ 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'')
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'_1)
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he₂ : Eq (α := List ℕ ⊕ List ℕ) (Sum.inl v'.tail) (Sum.inl v'_1)
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
have he₃ : v'.tail ∈ f.fix.eval v_1
Tactic: cases he₂
Cleared hypotheses: v'_1, he_1, hr_1, hr, he_2, he, 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'_1 : List ℕ
he_1 : v'_1 ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'_1)
hr : x ∈ eval step (stepRet k v'_1)
v : List ℕ
he_2 : v'_1 ∈ 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'')
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'_1)
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he₂ : Eq (α := List ℕ ⊕ List ℕ) (Sum.inl v'.tail) (Sum.inl v'_1)
he₃ : v'.tail ∈ f.fix.eval v_1
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
have hr₁ : x ∈ eval step (Cfg.ret k v'.tail)
Tactic: cases he₂
Cleared hypotheses: v'_1, he_1, hr_1, hr, he_2, he, 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'_1 : List ℕ
he_1 : v'_1 ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'_1)
hr : x ∈ eval step (stepRet k v'_1)
v : List ℕ
he_2 : v'_1 ∈ 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'')
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'_1)
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he₂ : Eq (α := List ℕ ⊕ List ℕ) (Sum.inl v'.tail) (Sum.inl v'_1)
he₃ : v'.tail ∈ f.fix.eval v_1
hr₁ : x ∈ eval step (Cfg.ret k v'.tail)
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
have hr₂ : x ∈ eval step (stepRet k v'.tail)
Tactic: cases he₂
Cleared hypotheses: v'_1, he_1, hr_1, hr, he_2, he, 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'_1 : List ℕ
he_1 : v'_1 ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'_1)
hr : x ∈ eval step (stepRet k v'_1)
v : List ℕ
he_2 : v'_1 ∈ 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'')
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'_1)
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he₂ : Eq (α := List ℕ ⊕ List ℕ) (Sum.inl v'.tail) (Sum.inl v'_1)
he₃ : v'.tail ∈ f.fix.eval v_1
hr₁ : x ∈ eval step (Cfg.ret k v'.tail)
hr₂ : x ∈ eval step (stepRet k v'.tail)
⊢ ∃ a ∈ f.eval v, x ∈ eval step (Cfg.ret (Cont.fix f k) a)
have he₄ : v'.tail ∈ f.fix.eval v
Tactic: cases he₂
Cleared hypotheses: v'_1, he_1, hr_1, hr, he_2, he, 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'_1 : List ℕ
he_1 : v'_1 ∈ f.fix.eval v_1
hr_1 : x ∈ eval step (Cfg.ret k v'_1)
hr : x ∈ eval step (stepRet k v'_1)
v : List ℕ
he_2 : v'_1 ∈ 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'')
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'_1)
v' : List ℕ
he₁ : v' ∈ f.eval v
h : v'.headI = 0
he₂ : Eq (α := List ℕ ⊕ List ℕ) (Sum.inl v'.tail) (Sum.inl v'_1)
he₃ : v'.tail ∈ f.fix.eval v_1
hr₁ : x ∈ eval step (Cfg.ret k v'.tail)
hr₂ : x ∈ eval step (stepRet k v'.tail)
he₄ : v'.tail ∈ f.fix.eval 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.inl v'.tail)
Tactic: cases he₂
Cleared hypotheses: v'_1, he_1, hr_1, hr, he_2, he, he₂