-- 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 h.e'_2.h.e'_7
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
h₁ : k₁ ≠ k₂
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst✝¹ : List Γ'
fst✝ : Option Γ'
snd✝ : List Γ'
e₃ : splitAtPred p Sk = (fst✝¹, fst✝, snd✝)
e₁ : S k₁ = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k₁) = ((fst✝¹, fst✝, snd✝).1, (fst✝¹, fst✝, snd✝).2.1, (fst✝¹, fst✝, snd✝).2.2) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
        { l := some q, var := (fst✝¹, fst✝, snd✝).2.1,
          stk := update (update S k₁ (fst✝¹, fst✝, snd✝).2.2) k₂ ((fst✝¹, fst✝, snd✝).1.reverseAux (S k₂)) }
⊢ update (update S k₁ snd✝) k₂ (fst✝¹.reverse ++ a :: S k₂) =
    update (update (update (update S k₁ Sk) k₂ (a :: S k₂)) k₁ snd✝) k₂ (fst✝¹.reverse ++ a :: S k₂)

Tactic:
simp [Function.update_comm h₁.symm]

Result:
no goals

Proof state:
case cons.cons.false.mk.mk.refl
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
h₁ : k₁ ≠ k₂
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst✝¹ : List Γ'
fst✝ : Option Γ'
snd✝ : List Γ'
e₃ : splitAtPred p Sk = (fst✝¹, fst✝, snd✝)
e₁ : S k₁ = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k₁) = ((fst✝¹, fst✝, snd✝).1, (fst✝¹, fst✝, snd✝).2.1, (fst✝¹, fst✝, snd✝).2.2) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
        { l := some q, var := (fst✝¹, fst✝, snd✝).2.1,
          stk := update (update S k₁ (fst✝¹, fst✝, snd✝).2.2) k₂ ((fst✝¹, fst✝, snd✝).1.reverseAux (S k₂)) }
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    (bif
        match (a :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a :: Sk).head?, stk := update S k₁ (a :: Sk).tail }
    else
      { l := some (Λ'.move p k₁ k₂ q), var := (a :: Sk).head?,
        stk := update (update S k₁ (a :: Sk).tail) k₂ ((a :: Sk).head?.iget :: update S k₁ (a :: Sk).tail k₂) })
    { l := some q, var := (fst✝¹, fst✝, snd✝).2.1,
      stk := update (update S k₁ (fst✝¹, fst✝, snd✝).2.2) k₂ ((a :: (fst✝¹, fst✝, snd✝).1).reverseAux (S k₂)) }

Tactic:
simp only [List.head?_cons, e₂, List.tail_cons, ne_eq, cond_false]

Result:
case cons.cons.false.mk.mk.refl
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
h₁ : k₁ ≠ k₂
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst✝¹ : List Γ'
fst✝ : Option Γ'
snd✝ : List Γ'
e₃ : splitAtPred p Sk = (fst✝¹, fst✝, snd✝)
e₁ : S k₁ = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k₁) = ((fst✝¹, fst✝, snd✝).1, (fst✝¹, fst✝, snd✝).2.1, (fst✝¹, fst✝, snd✝).2.2) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
        { l := some q, var := (fst✝¹, fst✝, snd✝).2.1,
          stk := update (update S k₁ (fst✝¹, fst✝, snd✝).2.2) k₂ ((fst✝¹, fst✝, snd✝).1.reverseAux (S k₂)) }
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    { l := some (Λ'.move p k₁ k₂ q), var := some a,
      stk := update (update S k₁ Sk) k₂ ((some a).iget :: update S k₁ Sk k₂) }
    { l := some q, var := fst✝, stk := update (update S k₁ snd✝) k₂ ((a :: fst✝¹).reverseAux (S k₂)) }

Proof state:
case cons.cons.true
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 Γ'
a' : Γ'
Sk : List Γ'
e₁ : S k₁ = a' :: Sk
e₂ : p a' = true
e : ([], some a', Sk) = (a :: L₁, o, L₂)
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    (bif
        match (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      { l := some q, var := (a' :: Sk).head?, stk := update S k₁ (a' :: Sk).tail }
    else
      { l := some (Λ'.move p k₁ k₂ q), var := (a' :: Sk).head?,
        stk := update (update S k₁ (a' :: Sk).tail) k₂ ((a' :: Sk).head?.iget :: update S k₁ (a' :: Sk).tail k₂) })
    { l := some q, var := o, stk := update (update S k₁ L₂) k₂ ((a :: L₁).reverseAux (S k₂)) }

Tactic:
cases e

Result:
no goals

Proof state:
case cons.cons.false.mk.mk.refl
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
h₁ : k₁ ≠ k₂
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst✝¹ : List Γ'
fst✝ : Option Γ'
snd✝ : List Γ'
e₃ : splitAtPred p Sk = (fst✝¹, fst✝, snd✝)
e₁ : S k₁ = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k₁) = ((fst✝¹, fst✝, snd✝).1, (fst✝¹, fst✝, snd✝).2.1, (fst✝¹, fst✝, snd✝).2.2) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
        { l := some q, var := (fst✝¹, fst✝, snd✝).2.1,
          stk := update (update S k₁ (fst✝¹, fst✝, snd✝).2.2) k₂ ((fst✝¹, fst✝, snd✝).1.reverseAux (S k₂)) }
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    { l := some (Λ'.move p k₁ k₂ q), var := some a,
      stk := update (update S k₁ Sk) k₂ ((some a).iget :: update S k₁ Sk k₂) }
    { l := some q, var := fst✝, stk := update (update S k₁ snd✝) k₂ ((a :: fst✝¹).reverseAux (S k₂)) }

Tactic:
convert @IH _ (update (update S k₁ Sk) k₂ (a :: S k₂)) _ using 2 <;>
  simp [Function.update_of_ne, h₁, h₁.symm, e₃, List.reverseAux]

Result:
case h.e'_2.h.e'_7
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
h₁ : k₁ ≠ k₂
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst✝¹ : List Γ'
fst✝ : Option Γ'
snd✝ : List Γ'
e₃ : splitAtPred p Sk = (fst✝¹, fst✝, snd✝)
e₁ : S k₁ = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'},
    splitAtPred p (S k₁) = ((fst✝¹, fst✝, snd✝).1, (fst✝¹, fst✝, snd✝).2.1, (fst✝¹, fst✝, snd✝).2.2) →
      Reaches₁ (TM2.step tr) { l := some (Λ'.move p k₁ k₂ q), var := s, stk := S }
        { l := some q, var := (fst✝¹, fst✝, snd✝).2.1,
          stk := update (update S k₁ (fst✝¹, fst✝, snd✝).2.2) k₂ ((fst✝¹, fst✝, snd✝).1.reverseAux (S k₂)) }
⊢ update (update S k₁ snd✝) k₂ (fst✝¹.reverse ++ a :: S k₂) =
    update (update (update (update S k₁ Sk) k₂ (a :: S k₂)) k₁ snd✝) k₂ (fst✝¹.reverse ++ a :: S k₂)