-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
c : Code
k : Cont
v : List ℕ
s : Option Γ'
zero' :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal Code.zero' k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal Code.zero' (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
succ :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal Code.succ k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal Code.succ (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
tail :
  ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal Code.tail k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal Code.tail (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
cons :
  ∀ (f fs : Code)
    (IHf :
      ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
        ∃ (b₂ : Cfg'),
          TrCfg (stepNormal f k v) b₂ ∧
            Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
              (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s
                (elim (trList v) [] [] (trContStack k)))
              b₂),
    (∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
        ∃ (b₂ : Cfg'),
          TrCfg (stepNormal fs k v) b₂ ∧
            Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
              (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal fs (trCont k))) s
                (elim (trList v) [] [] (trContStack k)))
              b₂) →
      ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
        ∃ (b₂ : Cfg'),
          TrCfg (stepNormal (f.cons fs) k v) b₂ ∧
            Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
              (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.cons fs) (trCont k))) s
                (elim (trList v) [] [] (trContStack k)))
              b₂
comp :
  ∀ (f a : Code),
    (∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
        ∃ (b₂ : Cfg'),
          TrCfg (stepNormal f k v) b₂ ∧
            Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
              (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s
                (elim (trList v) [] [] (trContStack k)))
              b₂) →
      ∀
        (IHg :
          ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
            ∃ (b₂ : Cfg'),
              TrCfg (stepNormal a k v) b₂ ∧
                Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
                  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal a (trCont k))) s
                    (elim (trList v) [] [] (trContStack k)))
                  b₂)
        (k : Cont) (v : List ℕ) (s : Option Γ'),
        ∃ (b₂ : Cfg'),
          TrCfg (stepNormal (f.comp a) k v) b₂ ∧
            Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
              (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.comp a) (trCont k))) s
                (elim (trList v) [] [] (trContStack k)))
              b₂
case :
  ∀ (f g : Code)
    (IHf :
      ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
        ∃ (b₂ : Cfg'),
          TrCfg (stepNormal f k v) b₂ ∧
            Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
              (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s
                (elim (trList v) [] [] (trContStack k)))
              b₂)
    (IHg :
      ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
        ∃ (b₂ : Cfg'),
          TrCfg (stepNormal g k v) b₂ ∧
            Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
              (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal g (trCont k))) s
                (elim (trList v) [] [] (trContStack k)))
              b₂)
    (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal (f.case g) k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal (f.case g) (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
fix :
  ∀ (f : Code)
    (IH :
      ∀ (k : Cont) (v : List ℕ) (s : Option Γ'),
        ∃ (b₂ : Cfg'),
          TrCfg (stepNormal f k v) b₂ ∧
            Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
              (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont k))) s
                (elim (trList v) [] [] (trContStack k)))
              b₂)
    (k : Cont) (v : List ℕ) (s : Option Γ'),
    ∃ (b₂ : Cfg'),
      TrCfg (stepNormal f.fix k v) b₂ ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f.fix (trCont k))) s
            (elim (trList v) [] [] (trContStack k)))
          b₂
⊢ ∃ (b₂ : Cfg'),
    TrCfg (stepNormal c k v) b₂ ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal c (trCont k))) s (elim (trList v) [] [] (trContStack k)))
        b₂

Tactic:
induction c generalizing k v s with
  | zero' => refine ⟨_, ⟨s, rfl⟩, TransGen.single ?_⟩; simp
  | succ => refine ⟨_, ⟨none, rfl⟩, head_main_ok.trans succ_ok⟩
  | tail =>
    let o : Option Γ' := List.casesOn v none fun _ _ => some Γ'.cons
    refine ⟨_, ⟨o, rfl⟩, ?_⟩; convert! clear_ok _ using 2
    · simp; rfl
    swap
    refine splitAtPred_eq _ _ (trNat v.headI) _ _ (trNat_natEnd _) ?_
    cases v <;> simp [o]
  | cons f fs IHf _ =>
    obtain ⟨c, h₁, h₂⟩ := IHf (Cont.cons₁ fs v k) v none
    refine ⟨c, h₁, TransGen.head rfl <| (move_ok (by decide) (splitAtPred_false _)).trans ?_⟩
    simp only [TM2.step, Option.mem_def, elim_stack, elim_update_stack, elim_update_main,
      elim_main, elim_rev, elim_update_rev]
    refine (copy_ok _ none [] (trList v).reverse _ _).trans ?_
    convert! h₂ using 2
    simp [List.reverseAux_eq, trContStack]
  | comp f _ _ IHg => exact IHg (Cont.comp f k) v s
  | case f g IHf IHg =>
    rw [stepNormal]
    simp only
    obtain ⟨s', h⟩ := pred_ok _ _ s v _ _
    revert h; rcases v.headI with - | n <;> intro h
    · obtain ⟨c, h₁, h₂⟩ := IHf k _ s'
      exact ⟨_, h₁, h.trans h₂⟩
    · obtain ⟨c, h₁, h₂⟩ := IHg k _ s'
      exact ⟨_, h₁, h.trans h₂⟩
  | fix f IH => apply IH

Premises used: Turing.PartrecToTM2.copy_ok, Turing.PartrecToTM2.trList, Turing.PartrecToTM2.K'.elim_update_main, Turing.PartrecToTM2.K'.elim_rev, Turing.PartrecToTM2.K'.elim_main, Turing.PartrecToTM2.trContStack, Turing.TM2.step, List.reverseAux_eq, Turing.PartrecToTM2.K'.elim_update_stack, Option.none, Turing.PartrecToTM2.splitAtPred_eq, Relation.TransGen.trans, List.reverse, Turing.PartrecToTM2.clear_ok, Turing.PartrecToTM2.pred_ok, List.headI, Turing.PartrecToTM2.K'.elim_stack, Turing.PartrecToTM2.trNat, Turing.ToPartrec.stepNormal, Turing.PartrecToTM2.K'.elim_update_rev, Turing.PartrecToTM2.trNat_natEnd, Option.mem_def, List.nil