-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
nil :
  ∀ (e : splitAtPred p [] = ([], o, L₂)),
    ReflTransGen
      (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)
      (bif
          match (motive := Option Γ' → Bool → (Γ' → Bool) → Bool) List.head? [], true, p with
          | some x, x_1, f => f x
          | none, y, x => y then
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (List.head? [])
          (update (β := fun (k : K') ↦ List Γ') S k (List.tail []))
      else
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) (List.head? [])
          (update (β := fun (k : K') ↦ List Γ') S k (List.tail [])))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
⊢ ∀ (e : splitAtPred p (S k) = ([], o, L₂)),
    ReflTransGen
      (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)
      (bif
          match (motive := Option Γ' → Bool → (Γ' → Bool) → Bool) (S k).head?, true, p with
          | some x, x_1, f => f x
          | none, y, x => y then
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (S k).head? (update (β := fun (k : K') ↦ List Γ') S k (S k).tail)
      else
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) (S k).head?
          (update (β := fun (k : K') ↦ List Γ') S k (S k).tail))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
have nil₁ : ∀ (a : Γ') (Sk : List Γ') (e : splitAtPred p (a :: Sk) = ([], o, L₂)),
  ReflTransGen
    (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)
    (bif
        match (motive := Option Γ' → Bool → (Γ' → Bool) → Bool) (a :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (a :: Sk).head?
        (update (β := fun (k : K') ↦ List Γ') S k (a :: Sk).tail)
    else
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) (a :: Sk).head?
        (update (β := fun (k : K') ↦ List Γ') S k (a :: Sk).tail))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
Tactic: rcases S k with - | ⟨a, Sk⟩