-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'} (e : splitAtPred p (S k₁) = (L₁, o, L₂)),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.move p k₁ k₂ q)) s S)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o
        (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) k₂ (L₁.reverseAux (S k₂))))
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k₁) = (a :: L₁, o, L₂)
cons :
  ∀ (e₁ : S k₁ = []),
    TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
      (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 (Λ'.move p k₁ k₂ q)) (List.head? [])
          (update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S k₁ (List.tail [])) k₂
            (Option.getD (List.head? []) default :: update (β := fun (k : K') ↦ List Γ') S k₁ (List.tail []) k₂)))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o
        (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) k₂
          ((a :: L₁).reverseAux (S k₂))))
cons₁ :
  ∀ (a' : Γ') (Sk : List Γ') (e₁ : S k₁ = a' :: Sk),
    TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
      (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 (Λ'.move p k₁ k₂ q)) (a' :: Sk).head?
          (update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S k₁ (a' :: Sk).tail) k₂
            ((a' :: Sk).head?.getD default :: update (β := fun (k : K') ↦ List Γ') S k₁ (a' :: Sk).tail k₂)))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o
        (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) k₂
          ((a :: L₁).reverseAux (S k₂))))
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (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 (Λ'.move p k₁ k₂ q)) (S k₁).head?
        (update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S k₁ (S k₁).tail) k₂
          ((S k₁).head?.getD default :: update (β := fun (k : K') ↦ List Γ') S k₁ (S k₁).tail k₂)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) k₂
        ((a :: L₁).reverseAux (S k₂))))

Tactic:
rcases e₁ : S k₁ with - | ⟨a', Sk⟩