-- Mathlib/Computability/TMToPartrec.lean
theorem move₂_ok {p k₁ k₂ q s L₁ o L₂} {S : K' → List Γ'} (h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂)
    (h₂ : S rev = []) (e : splitAtPred p (S k₁) = (L₁, o, L₂)) :
    Reaches₁ (TM2.step tr) ⟨some (move₂ p k₁ k₂ q), s, S⟩
      ⟨some q, none, update (update S k₁ (o.elim id List.cons L₂)) k₂ (L₁ ++ S k₂)⟩

Proof state:
case none
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ TransGen
    (fun a b =>
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    { l := some (Λ'.move (fun x => false) rev k₂ q), var := none,
      stk := update (update S k₁ L₂) rev (L₁.reverseAux (S rev)) }
    { l := some q, var := none, stk := update (update S k₁ L₂) k₂ (L₁ ++ S k₂) }

Tactic:
convert move_ok h₁.2.1.symm (splitAtPred_false _) using 2

Result:
case h.e'_2.h.e'_7
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ update (update S k₁ L₂) k₂ (L₁ ++ S k₂) =
    update (update (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))) rev []) k₂
      ((update (update S k₁ L₂) rev (L₁.reverseAux (S rev)) rev).reverseAux
        (update (update S k₁ L₂) rev (L₁.reverseAux (S rev)) k₂))

Proof state:
case h.e'_2.h.e'_7
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
val✝ : Γ'
e : splitAtPred p (S k₁) = (L₁, some val✝, L₂)
⊢ update (update S k₁ (val✝ :: L₂)) k₂ (L₁ ++ S k₂) =
    update (update S k₁ ((some val✝).iget :: L₂)) k₂
      ((update (update S rev L₁.reverse) k₁ ((some val✝).iget :: L₂) rev).reverse ++
        update (update S rev L₁.reverse) k₁ ((some val✝).iget :: L₂) k₂)

Tactic:
simp only [Function.update_of_ne h₁.1.symm, Function.update_of_ne h₁.2.2.symm,
  Function.update_of_ne h₁.2.1, Function.update_self, List.reverse_reverse]

Result:
no goals

Proof state:
case h.e'_2.h.e'_7
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
val✝ : Γ'
e : splitAtPred p (S k₁) = (L₁, some val✝, L₂)
⊢ update (update S k₁ (val✝ :: L₂)) k₂ (L₁ ++ S k₂) =
    update (update (update S rev []) k₁ ((some val✝).iget :: L₂)) k₂
      ((update (update S rev L₁.reverse) k₁ ((some val✝).iget :: L₂) rev).reverse ++
        update (update S rev L₁.reverse) k₁ ((some val✝).iget :: L₂) k₂)

Tactic:
rw [show update S rev [] = S by rw [← h₂, Function.update_eq_self]]

Result:
case h.e'_2.h.e'_7
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
val✝ : Γ'
e : splitAtPred p (S k₁) = (L₁, some val✝, L₂)
⊢ update (update S k₁ (val✝ :: L₂)) k₂ (L₁ ++ S k₂) =
    update (update S k₁ ((some val✝).iget :: L₂)) k₂
      ((update (update S rev L₁.reverse) k₁ ((some val✝).iget :: L₂) rev).reverse ++
        update (update S rev L₁.reverse) k₁ ((some val✝).iget :: L₂) k₂)

Proof state:
case some
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
val✝ : Γ'
e : splitAtPred p (S k₁) = (L₁, some val✝, L₂)
⊢ TransGen
    (fun a b =>
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    { l := some (Λ'.move (fun x => false) rev k₂ q), var := some val✝,
      stk :=
        update (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))) k₁
          ((some val✝).iget :: update (update S k₁ L₂) rev (L₁.reverseAux (S rev)) k₁) }
    { l := some q, var := none, stk := update (update S k₁ (val✝ :: L₂)) k₂ (L₁ ++ S k₂) }

Tactic:
convert move_ok h₁.2.1.symm (splitAtPred_false _) using 2

Result:
case h.e'_2.h.e'_7
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
val✝ : Γ'
e : splitAtPred p (S k₁) = (L₁, some val✝, L₂)
⊢ update (update S k₁ (val✝ :: L₂)) k₂ (L₁ ++ S k₂) =
    update
      (update
        (update (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))) k₁
          ((some val✝).iget :: update (update S k₁ L₂) rev (L₁.reverseAux (S rev)) k₁))
        rev [])
      k₂
      ((update (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))) k₁
            ((some val✝).iget :: update (update S k₁ L₂) rev (L₁.reverseAux (S rev)) k₁) rev).reverseAux
        (update (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))) k₁
          ((some val✝).iget :: update (update S k₁ L₂) rev (L₁.reverseAux (S rev)) k₁) k₂))

Proof state:
case h.e'_2.h.e'_7
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ update (update S k₁ L₂) k₂ (L₁ ++ S k₂) =
    update (update S k₁ L₂) k₂
      ((update (update S rev (L₁.reverseAux (S rev))) k₁ L₂ rev).reverseAux
        (update (update S rev (L₁.reverseAux (S rev))) k₁ L₂ k₂))

Tactic:
simp only [Function.update_of_ne h₁.2.2.symm, Function.update_of_ne h₁.2.1,
  Function.update_of_ne h₁.1.symm, List.reverseAux_eq, h₂, Function.update_self,
  List.append_nil, List.reverse_reverse]

Result:
no goals

Proof state:
case h.e'_2.h.e'_7
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ update (update S k₁ L₂) k₂ (L₁ ++ S k₂) =
    update (update (update S rev []) k₁ L₂) k₂
      ((update (update S rev (L₁.reverseAux (S rev))) k₁ L₂ rev).reverseAux
        (update (update S rev (L₁.reverseAux (S rev))) k₁ L₂ k₂))

Tactic:
rw [show update S rev [] = S by rw [← h₂, Function.update_eq_self]]

Result:
case h.e'_2.h.e'_7
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ update (update S k₁ L₂) k₂ (L₁ ++ S k₂) =
    update (update S k₁ L₂) k₂
      ((update (update S rev (L₁.reverseAux (S rev))) k₁ L₂ rev).reverseAux
        (update (update S rev (L₁.reverseAux (S rev))) k₁ L₂ k₂))

Proof state:
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₂)
⊢ TransGen (fun a b => b ∈ TM2.step tr a)
    (TM2.stepAux (tr (Λ'.push k₁ id (Λ'.move (fun x => false) rev k₂ q))) o
      (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))))
    { l := some q, var := none, stk := update (update S k₁ (o.elim id List.cons L₂)) k₂ (L₁ ++ S k₂) }

Tactic:
simp only [TM2.step, Option.mem_def, TM2.stepAux, id_eq, ne_eq, Option.elim]

Result:
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₂)
⊢ TransGen
    (fun a b =>
      (match a with
        | { l := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (tr l) v S)) =
        some b)
    (TM2.stepAux (tr (Λ'.push k₁ id (Λ'.move (fun x => false) rev k₂ q))) o
      (update (update S k₁ L₂) rev (L₁.reverseAux (S rev))))
    { l := some q, var := none,
      stk :=
        update
          (update S k₁
            ((match (motive := Option Γ' → (List Γ' → List Γ') → (Γ' → List Γ' → List Γ') → List Γ' → List Γ') o, id,
                List.cons with
              | some x, x_1, f => f x
              | none, y, x => y)
              L₂))
          k₂ (L₁ ++ S k₂) }