awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k k' : Cont
v : List ℕ
cons₁ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {v : List ℕ}, stepRet (a_2.then k') v = (stepRet a_2 v).then k') →
      ∀ {v : List ℕ}, stepRet ((Cont.cons₁ a a_1 a_2).then k') v = (stepRet (Cont.cons₁ a a_1 a_2) v).then k'
cons₂ :
  ∀ (a : Code) (a_1 : List ℕ) (a_2 : Cont),
    (∀ {v : List ℕ}, stepRet (a_2.then k') v = (stepRet a_2 v).then k') →
      ∀ {v : List ℕ}, stepNormal a (Cont.cons₂ v (a_2.then k')) a_1 = (stepNormal a (Cont.cons₂ v a_2) a_1).then k'
comp :
  ∀ (a : Code) (a_1 : Cont),
    (∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') →
      ∀ {v : List ℕ}, stepRet ((Cont.comp a a_1).then k') v = (stepRet (Cont.comp a a_1) v).then k'
comp₁ :
  ∀ (a : Code) (a_1 : Cont),
    (∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') →
      ∀ {v : List ℕ}, stepNormal a (a_1.then k') v = (stepNormal a a_1 v).then k'
fix :
  ∀ (a : Code) (a_1 : Cont) (k_ih : ∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') {v : List ℕ},
    stepRet ((Cont.fix a a_1).then k') v = (stepRet (Cont.fix a a_1) v).then k'
fix₁ :
  ∀ (a : Code) (a_1 : Cont) (k_ih : ∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') {v : List ℕ},
    (if v.headI = 0 then (stepRet a_1 v.tail).then k' else stepNormal a (Cont.fix a (a_1.then k')) v.tail) =
      (if v.headI = 0 then stepRet a_1 v.tail else stepNormal a (Cont.fix a a_1) v.tail).then k'
halt : ∀ {v : List ℕ}, stepRet (Cont.halt.then k') v = (stepRet Cont.halt v).then k'
halt₁ : ∀ {v : List ℕ}, stepRet k' v = (Cfg.halt v).then k'
cons₃ :
  ∀ (a : List ℕ) (a_1 : Cont),
    (∀ {v : List ℕ}, stepRet (a_1.then k') v = (stepRet a_1 v).then k') →
      ∀ {v : List ℕ}, stepRet ((Cont.cons₂ a a_1).then k') v = (stepRet (Cont.cons₂ a a_1) v).then k'
⊢ stepRet (k.then k') v = (stepRet k v).then k'

Tactic:
induction k generalizing v with simp only [Cont.then, stepRet, *]
  | cons₁ =>
    rw [← stepNormal_then]
    rfl
  | comp =>
    rw [← stepNormal_then]
  | fix _ _ k_ih =>
    split_ifs
    · rw [← k_ih]
    · rw [← stepNormal_then]
      rfl
  | _ => simp only [Cfg.then]

Premises used: Turing.ToPartrec.Cfg.then, Turing.ToPartrec.stepNormal_then, Turing.ToPartrec.stepRet, Turing.ToPartrec.Cont.then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
c : Code
h : c.Ok
v : List ℕ
rw :
  Eq (α := Part Cfg)
    (do
      let v ← c.eval v
      StateTransition.eval step (Cfg.ret Cont.halt v))
    do
    let a ← c.eval v
    pure (Cfg.halt a)
⊢ StateTransition.eval step (stepNormal c Cont.halt v) = Cfg.halt <$> c.eval v

Tactic:
rw [h, ← bind_pure_comp]

Premises used: LawfulMonad.bind_pure_comp
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
c : Code
h : c.Ok
v : List ℕ
e_a :
  Eq (α := List ℕ → Part Cfg) (fun (v : List ℕ) ↦ StateTransition.eval step (Cfg.ret Cont.halt v)) fun (a : List ℕ) ↦
    pure (Cfg.halt a)
⊢ Eq (α := Part Cfg)
    (do
      let v ← c.eval v
      StateTransition.eval step (Cfg.ret Cont.halt v))
    do
    let a ← c.eval v
    pure (Cfg.halt a)

Tactic:
congr
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
c : Code
h : c.Ok
v : List ℕ
e_a : ∀ (v : List ℕ), StateTransition.eval step (Cfg.ret Cont.halt v) = pure (Cfg.halt v)
⊢ Eq (α := List ℕ → Part Cfg) (fun (v : List ℕ) ↦ StateTransition.eval step (Cfg.ret Cont.halt v)) fun (a : List ℕ) ↦
    pure (Cfg.halt a)

Tactic:
funext v
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
c : Code
h : c.Ok
v_1 v : List ℕ
⊢ StateTransition.eval step (Cfg.ret Cont.halt v) = pure (Cfg.halt v)

Tactic:
Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.single rfl, rfl⟩)

Premises used: Iff.mpr, Part.eq_some_iff, Relation.ReflTransGen.single, StateTransition.mem_eval, And.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
c : Code
h : c.Ok
v_1 v : List ℕ
⊢ StateTransition.eval step (Cfg.ret Cont.halt v) = pure (Cfg.halt v)

Tactic:
exact Part.eq_some_iff.2 (mem_eval.2 ⟨ReflTransGen.single rfl, rfl⟩)

Premises used: Iff.mpr, Part.eq_some_iff, Relation.ReflTransGen.single, StateTransition.mem_eval, And.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
_f fs : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal _f k v = Cfg.ret k' v'
_IHfs : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal fs k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ (k' : Cont) (v' : List ℕ), stepNormal (_f.cons fs) k v = Cfg.ret k' v'

Tactic:
apply IHf
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f _g : Code
_IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal _g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ (k' : Cont) (v' : List ℕ), stepNormal (f.comp _g) k v = Cfg.ret k' v'

Tactic:
apply IHg
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
case :
  ∃ (k' : Cont) (v' : List ℕ),
    (fun (k : Cont) (v : List ℕ) ↦
          (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
              (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI :
            Cfg))
        k v =
      Cfg.ret k' v'
⊢ ∃ (k' : Cont) (v' : List ℕ), stepNormal (f.case g) k v = Cfg.ret k' v'

Tactic:
rw [stepNormal]

Premises used: Turing.ToPartrec.stepNormal
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
case :
  ∃ (k' : Cont) (v' : List ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail) (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail))
        v.headI =
      Cfg.ret k' v'
⊢ ∃ (k' : Cont) (v' : List ℕ),
    (fun (k : Cont) (v : List ℕ) ↦
          (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
              (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI :
            Cfg))
        k v =
      Cfg.ret k' v'

Tactic:
simp only []
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
case :
  ∃ (k' : Cont) (v' : List ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail) (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail))
        0 =
      Cfg.ret k' v'
case₁ :
  ∀ (n : ℕ),
    ∃ (k' : Cont) (v' : List ℕ),
      Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) (n + 1) =
        Cfg.ret k' v'
⊢ ∃ (k' : Cont) (v' : List ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail) (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail))
        v.headI =
      Cfg.ret k' v'

Tactic:
cases v.headI

Premises used: List.headI
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ (k' : Cont) (v' : List ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail) (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail))
        0 =
      Cfg.ret k' v'

Tactic:
apply IHf
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
n : ℕ
⊢ ∃ (k' : Cont) (v' : List ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail) (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail))
        (n + 1) =
      Cfg.ret k' v'

Tactic:
apply IHg
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f g : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v'
IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal g k v = Cfg.ret k' v'
k : Cont
v : List ℕ
case :
  ∃ (k' : Cont) (v' : List ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail) (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail))
        0 =
      Cfg.ret k' v'
case₁ :
  ∀ (n : ℕ),
    ∃ (k' : Cont) (v' : List ℕ),
      Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) (n + 1) =
        Cfg.ret k' v'
case₂ :
  ∃ (k' : Cont) (v' : List ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail) (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail))
        0 =
      Cfg.ret k' v'
case₃ :
  ∀ (n : ℕ),
    ∃ (k' : Cont) (v' : List ℕ),
      Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) (n + 1) =
        Cfg.ret k' v'
⊢ ∃ (k' : Cont) (v' : List ℕ),
    Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail) (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail))
        v.headI =
      Cfg.ret k' v'

Tactic:
cases v.headI <;> [apply IHf; apply IHg]

Premises used: List.headI
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v'
k : Cont
v : List ℕ
⊢ ∃ (k' : Cont) (v' : List ℕ), stepNormal f.fix k v = Cfg.ret k' v'

Tactic:
apply IHf
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k : Cont
v : List ℕ
⊢ ∃ (k' : Cont) (v' : List ℕ), stepNormal Code.zero' k v = Cfg.ret k' v'

Tactic:
⟨_, _, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k : Cont
v : List ℕ
⊢ ∃ (k' : Cont) (v' : List ℕ), stepNormal Code.zero' k v = Cfg.ret k' v'

Tactic:
exact ⟨_, _, rfl⟩
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k : Cont
v : List ℕ
⊢ ∃ (k' : Cont) (v' : List ℕ), stepNormal Code.succ k v = Cfg.ret k' v'

Tactic:
⟨_, _, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k : Cont
v : List ℕ
⊢ ∃ (k' : Cont) (v' : List ℕ), stepNormal Code.succ k v = Cfg.ret k' v'

Tactic:
exact ⟨_, _, rfl⟩
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k : Cont
v : List ℕ
⊢ ∃ (k' : Cont) (v' : List ℕ), stepNormal Code.tail k v = Cfg.ret k' v'

Tactic:
⟨_, _, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
k : Cont
v : List ℕ
⊢ ∃ (k' : Cont) (v' : List ℕ), stepNormal Code.tail k v = Cfg.ret k' v'

Tactic:
exact ⟨_, _, rfl⟩
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
c : Code
k : Cont
v : List ℕ
cons :
  ∀ (_f fs : Code) (IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal _f k v = Cfg.ret k' v')
    (_IHfs : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal fs k v = Cfg.ret k' v') (k : Cont)
    (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (_f.cons fs) k v = Cfg.ret k' v'
comp :
  ∀ (f _g : Code) (_IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v')
    (IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal _g k v = Cfg.ret k' v') (k : Cont)
    (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (f.comp _g) k v = Cfg.ret k' v'
case :
  ∀ (f g : Code) (IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v')
    (IHg : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal g k v = Cfg.ret k' v') (k : Cont)
    (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal (f.case g) k v = Cfg.ret k' v'
fix :
  ∀ (f : Code) (IHf : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f k v = Cfg.ret k' v')
    (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal f.fix k v = Cfg.ret k' v'
zero' : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal Code.zero' k v = Cfg.ret k' v'
succ : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal Code.succ k v = Cfg.ret k' v'
tail : ∀ (k : Cont) (v : List ℕ), ∃ (k' : Cont) (v' : List ℕ), stepNormal Code.tail k v = Cfg.ret k' v'
⊢ ∃ (k' : Cont) (v' : List ℕ), stepNormal c k v = Cfg.ret k' v'

Tactic:
induction c generalizing k v with
  | cons _f fs IHf _IHfs => apply IHf
  | comp f _g _IHf IHg => apply IHg
  | case f g IHf IHg =>
    rw [stepNormal]
    simp only []
    cases v.headI <;> [apply IHf; apply IHg]
  | fix f IHf => apply IHf
  | _ => exact ⟨_, _, rfl⟩

Premises used: Turing.ToPartrec.stepNormal._f, List.headI, Turing.ToPartrec.stepNormal
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
⊢ eval step (stepNormal f (Cont.fix f k) v) = do
    let v ← f.fix.eval v
    eval step (Cfg.ret k v)

Tactic:
Part.ext fun x => ?_

Premises used: Part.ext
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
refine :
  ∀ (x : Cfg),
    x ∈ eval step (stepNormal f (Cont.fix f k) v) ↔
      Membership.mem (γ := Part Cfg)
        (do
          let v ← f.fix.eval v
          eval step (Cfg.ret k v))
        x
⊢ eval step (stepNormal f (Cont.fix f k) v) = do
    let v ← f.fix.eval v
    eval step (Cfg.ret k v)

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

Premises used: Part.ext
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
simp : x ∈ eval step (stepNormal f (Cont.fix f k) v) ↔ ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v) ↔
    Membership.mem (γ := Part Cfg)
      (do
        let v ← f.fix.eval v
        eval step (Cfg.ret k v))
      x

Tactic:
simp only [Part.bind_eq_bind, Part.mem_bind_iff]

Premises used: Part.mem_bind_iff, Part.bind_eq_bind
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
mp : x ∈ eval step (stepNormal f (Cont.fix f k) v) → ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)
mpr : (∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)) → x ∈ eval step (stepNormal f (Cont.fix f k) v)
⊢ x ∈ eval step (stepNormal f (Cont.fix f k) v) ↔ ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)

Tactic:
constructor
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = 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₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
obtain :
  ∀ (v₁ : List ℕ) (hv₁ : v₁ ∈ f.eval v) (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₂)),
    ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)
⊢ ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)

Tactic:
obtain ⟨v₁, hv₁, v₂, hv₂, h₃⟩ :=
        this _ h _ _ (stepNormal_then _ Cont.halt _ _) ReflTransGen.refl

Premises used: Turing.ToPartrec.Cont.halt, Relation.ReflTransGen.refl, Turing.ToPartrec.stepNormal_then
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = 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₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
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₂)
⊢ ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)

Tactic:
⟨v₂, PFun.mem_fix_iff.2 ?_, h₃⟩

Premises used: Iff.mpr, And.intro, Exists.intro, PFun.mem_fix_iff
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = 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₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
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₂)
refine :
  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' : 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') ∧
        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₂
⊢ ∃ a ∈ f.fix.eval v, x ∈ eval step (Cfg.ret k a)

Tactic:
refine ⟨v₂, PFun.mem_fix_iff.2 ?_, h₃⟩
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = 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₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
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₂)
simp :
  Sum.inl v₂ ∈ Part.some (if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∨
    ∃ (a' : List ℕ),
      Sum.inr a' ∈ Part.some (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₂
⊢ 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' : 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') ∧
        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]

Premises used: Iff.mpr, Part.eq_some_iff, Part.map_some
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = 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₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
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₂),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inl v₁.tail)) (Sum.inl v₂) ∨
        ∃ (a' : List ℕ),
          Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inl 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₂
neg :
  ¬v₁.headI = 0 →
    ∀ (hv₂ : v₂ ∈ f.fix.eval v₁.tail),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inr v₁.tail)) (Sum.inl v₂) ∨
        ∃ (a' : List ℕ),
          Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inr 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₂
⊢ Sum.inl v₂ ∈ Part.some (if v₁.headI = 0 then Sum.inl v₁.tail else Sum.inr v₁.tail) ∨
    ∃ (a' : List ℕ),
      Sum.inr a' ∈ Part.some (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:
split_ifs at hv₂ ⊢
-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
f : Code
k : Cont
v : List ℕ
fok : f.Ok
x : Cfg
this :
  ∀ (c : Cfg),
    x ∈ eval step c →
      ∀ (v : List ℕ) (c' : Cfg),
        c = 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₂)
h : x ∈ eval step (stepNormal f (Cont.fix f k) v)
v₁ : List ℕ
hv₁ : v₁ ∈ f.eval v
v₂ : List ℕ
h₃ : x ∈ eval step (Cfg.ret k v₂)
h_1 : v₁.headI = 0
hv₂ : Membership.mem (γ := Part (List ℕ)) (pure v₁.tail) v₂
pos :
  Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inl v₁.tail)) (Sum.inl v₁.tail) ∨
    ∃ (a' : List ℕ),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inl 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₁.tail
⊢ Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inl v₁.tail)) (Sum.inl v₂) ∨
    ∃ (a' : List ℕ),
      Membership.mem (γ := Part (List ℕ ⊕ List ℕ)) (Part.some (Sum.inl 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₂

Tactic:
rw [Part.mem_some_iff.1 hv₂]

Premises used: Part.mem_some_iff, Iff.mp