-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
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₂
a_ih :
  ∀ (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 Γ'
c : Cfg'
h₁ : TrCfg (stepNormal f (Cont.cons₁ fs v k) v) c
h₂ :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (trCont (Cont.cons₁ fs v k)))) none
      (elim (trList v) [] [] (trContStack (Cont.cons₁ fs v k))))
    c
cons :
  TransGen
    (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
      (match (motive :=
          TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ') → Option (TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))) a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (Cont'.cons₁ fs (trCont k))).copy) none
      (elim [] ((trList v).reverseAux []) [] ((some Γ'.consₗ).getD default :: trContStack k)))
    c
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (trNormal f (Cont'.cons₁ fs (trCont k))).copy) none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ')
          (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trList v) [] [] (trContStack k)) stack
            ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.consₗ) s) default : Γ')) s ::
              elim (trList v) [] [] (trContStack k) stack))
          main [])
        rev
        ((update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trList v) [] [] (trContStack k)) stack
              ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.consₗ) s) default : Γ')) s ::
                elim (trList v) [] [] (trContStack k) stack)
              main).reverseAux
          (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k)) (elim (trList v) [] [] (trContStack k)) stack
            ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.consₗ) s) default : Γ')) s ::
              elim (trList v) [] [] (trContStack k) stack)
            rev))))
    c

Tactic:
simp only [TM2.step, Option.mem_def, elim_stack, elim_update_stack, elim_update_main,
      elim_main, elim_rev, elim_update_rev]

Premises used: Turing.PartrecToTM2.K'.elim_update_main, Turing.PartrecToTM2.K'.elim_rev, Turing.PartrecToTM2.K'.elim_main, Turing.TM2.step, Turing.PartrecToTM2.K'.elim_update_stack, Turing.PartrecToTM2.K'.elim_stack, Turing.PartrecToTM2.K'.elim_update_rev, Option.mem_def