-- Module: Mathlib.Computability.TuringMachine.Config
Goal:
c : Code
k k' : Cont
v : List ℕ
cons :
  ∀ (c c' : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'),
    (∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k') →
      ∀ (k : Cont) (v : List ℕ), stepNormal (c.cons c') (k.then k') v = (stepNormal (c.cons c') k v).then k'
cons₁ :
  ∀ (c c' : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k'),
    (∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k') →
      ∀ (k : Cont) (v : List ℕ),
        stepNormal c (Cont.cons₁ c' v (k.then k')) v = (stepNormal c (Cont.cons₁ c' v k) v).then k'
comp :
  ∀ (c c' : Code),
    (∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k') →
      ∀ (ih' : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k') (k : Cont)
        (v : List ℕ), stepNormal (c.comp c') (k.then k') v = (stepNormal (c.comp c') k v).then k'
comp₁ :
  ∀ (c c' : Code),
    (∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k') →
      ∀ (ih' : ∀ (k : Cont) (v : List ℕ), stepNormal c' (k.then k') v = (stepNormal c' k v).then k') (k : Cont)
        (v : List ℕ), stepNormal c' (Cont.comp c (k.then k')) v = (stepNormal c' (Cont.comp c k) v).then k'
case :
  ∀ (a a_1 : Code),
    (∀ (k : Cont) (v : List ℕ), stepNormal a (k.then k') v = (stepNormal a k v).then k') →
      (∀ (k : Cont) (v : List ℕ), stepNormal a_1 (k.then k') v = (stepNormal a_1 k v).then k') →
        ∀ (k : Cont) (v : List ℕ), stepNormal (a.case a_1) (k.then k') v = (stepNormal (a.case a_1) k v).then k'
case₁ :
  ∀ (a a_1 : Code),
    (∀ (k : Cont) (v : List ℕ), stepNormal a (k.then k') v = (stepNormal a k v).then k') →
      (∀ (k : Cont) (v : List ℕ), stepNormal a_1 (k.then k') v = (stepNormal a_1 k v).then k') →
        ∀ (k : Cont) (v : List ℕ),
          Nat.rec (motive := fun (x : ℕ) ↦ Cfg) ((stepNormal a k v.tail).then k')
              (fun (y : ℕ) (x : Cfg) ↦ (stepNormal a_1 k (y :: v.tail)).then k') v.headI =
            Cfg.then
              (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal a k v.tail)
                (fun (y : ℕ) (x : Cfg) ↦ stepNormal a_1 k (y :: v.tail)) v.headI)
              k'
fix :
  ∀ (c : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k') (k : Cont)
    (v : List ℕ), stepNormal c.fix (k.then k') v = (stepNormal c.fix k v).then k'
fix₁ :
  ∀ (c : Code) (ih : ∀ (k : Cont) (v : List ℕ), stepNormal c (k.then k') v = (stepNormal c k v).then k') (k : Cont)
    (v : List ℕ), stepNormal c (Cont.fix c (k.then k')) v = (stepNormal c (Cont.fix c k) v).then k'
zero' : ∀ (k : Cont) (v : List ℕ), stepNormal Code.zero' (k.then k') v = (stepNormal Code.zero' k v).then k'
zero'₁ : ∀ (k : Cont) (v : List ℕ), Cfg.ret (k.then k') (0 :: v) = (Cfg.ret k (0 :: v)).then k'
succ : ∀ (k : Cont) (v : List ℕ), stepNormal Code.succ (k.then k') v = (stepNormal Code.succ k v).then k'
succ₁ : ∀ (k : Cont) (v : List ℕ), Cfg.ret (k.then k') [v.headI.succ] = (Cfg.ret k [v.headI.succ]).then k'
tail : ∀ (k : Cont) (v : List ℕ), stepNormal Code.tail (k.then k') v = (stepNormal Code.tail k v).then k'
tail₁ : ∀ (k : Cont) (v : List ℕ), Cfg.ret (k.then k') v.tail = (Cfg.ret k v.tail).then k'
⊢ stepNormal c (k.then k') v = (stepNormal c k v).then k'

Tactic:
induction c generalizing k v with simp only [stepNormal, *]
  | cons c c' ih _ => rw [← ih, Cont.then]
  | comp c c' _ ih' => rw [← ih', Cont.then]
  | case => cases v.headI <;> simp only [Nat.rec_zero]
  | fix c ih => rw [← ih, Cont.then]
  | _ => simp only [Cfg.then]

Premises used: Nat.rec_zero, Turing.ToPartrec.Cfg.then, List.headI, Turing.ToPartrec.stepNormal, Turing.ToPartrec.Cont.then