-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Config (goal)
Goal:
f g : Code
IHf : f.Ok
IHg : g.Ok
k : Cont
v : List ℕ
case :
  eval step
      (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
        (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) 0) =
    do
    let v ←
      Nat.rec (motive := fun (x : ℕ) ↦ Part (List ℕ)) (f.eval v.tail)
          (fun (y : ℕ) (x : Part (List ℕ)) ↦ g.eval (y :: v.tail)) 0
    eval step (Cfg.ret k v)
case₁ :
  ∀ (n : ℕ),
    eval step
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) (n + 1)) =
      do
      let v ←
        Nat.rec (motive := fun (x : ℕ) ↦ Part (List ℕ)) (f.eval v.tail)
            (fun (y : ℕ) (x : Part (List ℕ)) ↦ g.eval (y :: v.tail)) (n + 1)
      eval step (Cfg.ret k v)
case₂ :
  eval step
      (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
        (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) 0) =
    do
    let v ←
      Nat.rec (motive := fun (x : ℕ) ↦ Part (List ℕ)) (f.eval v.tail)
          (fun (y : ℕ) (x : Part (List ℕ)) ↦ g.eval (y :: v.tail)) 0
    eval step (Cfg.ret k v)
case₃ :
  ∀ (n : ℕ),
    eval step
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) (n + 1)) =
      do
      let v ←
        Nat.rec (motive := fun (x : ℕ) ↦ Part (List ℕ)) (f.eval v.tail)
            (fun (y : ℕ) (x : Part (List ℕ)) ↦ g.eval (y :: v.tail)) (n + 1)
      eval step (Cfg.ret k v)
case₄ :
  eval step
      (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
        (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) 0) =
    do
    let v ←
      Nat.rec (motive := fun (x : ℕ) ↦ Part (List ℕ)) (f.eval v.tail)
          (fun (y : ℕ) (x : Part (List ℕ)) ↦ g.eval (y :: v.tail)) 0
    eval step (Cfg.ret k v)
case₅ :
  ∀ (n : ℕ),
    eval step
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) (n + 1)) =
      do
      let v ←
        Nat.rec (motive := fun (x : ℕ) ↦ Part (List ℕ)) (f.eval v.tail)
            (fun (y : ℕ) (x : Part (List ℕ)) ↦ g.eval (y :: v.tail)) (n + 1)
      eval step (Cfg.ret k v)
case₆ :
  eval step
      (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
        (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) 0) =
    do
    let v ←
      Nat.rec (motive := fun (x : ℕ) ↦ Part (List ℕ)) (f.eval v.tail)
          (fun (y : ℕ) (x : Part (List ℕ)) ↦ g.eval (y :: v.tail)) 0
    eval step (Cfg.ret k v)
case₇ :
  ∀ (n : ℕ),
    eval step
        (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
          (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) (n + 1)) =
      do
      let v ←
        Nat.rec (motive := fun (x : ℕ) ↦ Part (List ℕ)) (f.eval v.tail)
            (fun (y : ℕ) (x : Part (List ℕ)) ↦ g.eval (y :: v.tail)) (n + 1)
      eval step (Cfg.ret k v)
case₈ : eval step (stepNormal f k v.tail) = (f.eval v.tail).bind fun (v : List ℕ) ↦ eval step (Cfg.ret k v)
⊢ eval step
      (Nat.rec (motive := fun (x : ℕ) ↦ Cfg) (stepNormal f k v.tail)
        (fun (y : ℕ) (x : Cfg) ↦ stepNormal g k (y :: v.tail)) v.headI) =
    do
    let v ←
      Nat.rec (motive := fun (x : ℕ) ↦ Part (List ℕ)) (f.eval v.tail)
          (fun (y : ℕ) (x : Part (List ℕ)) ↦ g.eval (y :: v.tail)) v.headI
    eval step (Cfg.ret k v)
have case₉ : ∀ (n : ℕ),
  eval step (stepNormal g k (n :: v.tail)) = (g.eval (n :: v.tail)).bind fun (v : List ℕ) ↦ eval step (Cfg.ret k v)
Tactic: cases v.headI <;> simp only [Nat.rec_zero, Part.bind_eq_bind] <;> [apply IHf; apply IHg]