-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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₂
⊢ ∃ (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₂
have 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₂
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
Cleared hypotheses: c, k, v, s