-- Mathlib/Computability/TMToPartrec.lean
theorem move_ok {p k₁ k₂ q s L₁ o L₂} {S : K' → List Γ'} (h₁ : k₁ ≠ k₂)
    (e : splitAtPred p (S k₁) = (L₁, o, L₂)) :
    Reaches₁ (TM2.step tr) ⟨some (Λ'.move p k₁ k₂ q), s, S⟩
      ⟨some q, o, update (update S k₁ L₂) k₂ (L₁.reverseAux (S k₂))⟩

Proof state:
case nil
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
s : Option Γ'
S : K' → List Γ'
⊢ splitAtPred p (S k₁) = ([], o, L₂) →
    ReflTransGen (fun a b => b ∈ TM2.step tr a)
      (bif (S k₁).head?.elim true p then { l := some q, var := (S k₁).head?, stk := update S k₁ (S k₁).tail }
      else TM2.stepAux (push' k₂ (goto fun x => Λ'.move p k₁ k₂ q)) (S k₁).head? (update S k₁ (S k₁).tail))
      { l := some q, var := o, stk := update S k₁ L₂ }

Tactic:
rcases S k₁ with - | ⟨a, Sk⟩ <;> intro e

Result:
case nil.nil
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p [] = ([], o, L₂)
⊢ ReflTransGen (fun a b => b ∈ TM2.step tr a)
    (bif [].head?.elim true p then { l := some q, var := [].head?, stk := update S k₁ [].tail }
    else TM2.stepAux (push' k₂ (goto fun x => Λ'.move p k₁ k₂ q)) [].head? (update S k₁ [].tail))
    { l := some q, var := o, stk := update S k₁ L₂ }

case nil.cons
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
e : splitAtPred p (a :: Sk) = ([], o, L₂)
⊢ ReflTransGen (fun a b => b ∈ TM2.step tr a)
    (bif (a :: Sk).head?.elim true p then { l := some q, var := (a :: Sk).head?, stk := update S k₁ (a :: Sk).tail }
    else TM2.stepAux (push' k₂ (goto fun x => Λ'.move p k₁ k₂ q)) (a :: Sk).head? (update S k₁ (a :: Sk).tail))
    { l := some q, var := o, stk := update S k₁ L₂ }

Proof state:
case cons
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k₁) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
        { l := some q, var := o, stk := update (update S k₁ L₂) k₂ (L₁.reverseAux (S k₂)) }
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k₁) = (a :: L₁, o, L₂)
⊢ Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
    { l := some q, var := o, stk := update (update S k₁ L₂) k₂ ((a :: L₁).reverseAux (S k₂)) }

Tactic:
refine TransGen.head rfl ?_

Result:
case cons
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k₁) = (L₁, o, L₂) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
        { l := some q, var := o, stk := update (update S k₁ L₂) k₂ (L₁.reverseAux (S k₂)) }
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k₁) = (a :: L₁, o, L₂)
⊢ TransGen (fun a b => b ∈ TM2.step tr a) (TM2.stepAux (tr (Λ'.move p k₁ k₂ q)) s S)
    { l := some q, var := o, stk := update (update S k₁ L₂) k₂ ((a :: L₁).reverseAux (S k₂)) }

Proof state:
case nil.nil.refl
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
h₁ : k₁ ≠ k₂
s : Option Γ'
S : K' → List Γ'
⊢ ReflTransGen (fun a b => b ∈ TM2.step tr a)
    (bif [].head?.elim true p then { l := some q, var := [].head?, stk := update S k₁ [].tail }
    else TM2.stepAux (push' k₂ (goto fun x => Λ'.move p k₁ k₂ q)) [].head? (update S k₁ [].tail))
    { l := some q, var := none, stk := update S k₁ [] }

Tactic:
rfl

Result:
no goals