-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ : List Γ'
o : Option Γ'
L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, o, L₂)
none :
  ∀ (e : splitAtPred p (S k₁) = (L₁, Option.none, L₂)),
    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 := Option.none, var := var, stk := stk } => Option.none
          | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
          some b)
      (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr (Λ'.push k₁ id (Λ'.move (fun (x : Γ') ↦ false) rev k₂ q))) Option.none
        (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
          (L₁.reverseAux (S rev))))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) Option.none
        (update (β := fun (k : K') ↦ List Γ')
          (update (β := fun (a : K') ↦ List Γ') S k₁
            ((match (motive :=
                Option Γ' → ((a : List Γ') → List Γ') → (Γ' → (a : List Γ') → List Γ') → (a : List Γ') → List Γ')
                Option.none, id, List.cons with
              | some x, x_1, f => f x
              | Option.none, y, x => y)
              L₂))
          k₂ (L₁ ++ S k₂)))
⊢ 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 := Option.none, var := var, stk := stk } => Option.none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr (Λ'.push k₁ id (Λ'.move (fun (x : Γ') ↦ false) rev k₂ q))) o
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev (L₁.reverseAux (S rev))))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) Option.none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ') S k₁
          ((match (motive :=
              Option Γ' → ((a : List Γ') → List Γ') → (Γ' → (a : List Γ') → List Γ') → (a : List Γ') → List Γ') o, id,
              List.cons with
            | some x, x_1, f => f x
            | Option.none, y, x => y)
            L₂))
        k₂ (L₁ ++ S k₂)))
have some : ∀ (val : Γ') (e : splitAtPred p (S k₁) = (L₁, some val, L₂)),
  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 := Option.none, var := var, stk := stk } => Option.none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr (Λ'.push k₁ id (Λ'.move (fun (x : Γ') ↦ false) rev k₂ q))) (some val)
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev (L₁.reverseAux (S rev))))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) Option.none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ') S k₁
          ((match (motive :=
              Option Γ' → ((a : List Γ') → List Γ') → (Γ' → (a : List Γ') → List Γ') → (a : List Γ') → List Γ')
              some val, id, List.cons with
            | some x, x_1, f => f x
            | Option.none, y, x => y)
            L₂))
        k₂ (L₁ ++ S k₂)))
Tactic: cases o
Cleared hypotheses: o, e