awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 :
  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₂))))
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
      (pop' k₁
        (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ s.elim true p)
          (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q)
          (push' k₂ (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ Λ'.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₂
        ((a :: L₁).reverseAux (S k₂))))

Tactic:
simp only [pop', Option.elim, TM2.stepAux, push']

Premises used: Turing.TM2.stepAux, Turing.PartrecToTM2.push', Turing.PartrecToTM2.pop', Option.elim
-- 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₂)
e₁ : S k₁ = []
⊢ ([], none, []) = (a :: L₁, o, L₂)

Tactic:
rw [e₁, splitAtPred] at e

Premises used: Turing.PartrecToTM2.splitAtPred
-- 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₂)
e₁ : S k₁ = []
e₂ : ([], none, []) = (a :: L₁, o, L₂)
⊢ S k₁ = []

Tactic:
rw [e₁, splitAtPred] at e

Premises used: Turing.PartrecToTM2.splitAtPred
-- 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₂)
a' : Γ'
Sk : List Γ'
e₁ : S k₁ = a' :: Sk
⊢ (bif p a' then ([], some a', Sk)
    else
      match (motive := List Γ' × Option Γ' × List Γ' → List Γ' × Option Γ' × List Γ') splitAtPred p Sk with
      | (l₁, o, l₂) => (a' :: l₁, o, l₂)) =
    (a :: L₁, o, L₂)

Tactic:
rw [e₁, splitAtPred] at e

Premises used: Turing.PartrecToTM2.splitAtPred
-- 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₂)
a' : Γ'
Sk : List Γ'
e₁ : S k₁ = a' :: Sk
e₂ :
  (bif p a' then ([], some a', Sk)
    else
      match (motive := List Γ' × Option Γ' × List Γ' → List Γ' × Option Γ' × List Γ') splitAtPred p Sk with
      | (l₁, o, l₂) => (a' :: l₁, o, l₂)) =
    (a :: L₁, o, L₂)
⊢ S k₁ = a' :: Sk

Tactic:
rw [e₁, splitAtPred] at e

Premises used: Turing.PartrecToTM2.splitAtPred
-- 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 : ([], none, []) = (a :: L₁, o, L₂)
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₂))))

Tactic:
cases e
-- 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 Γ'
a' : Γ'
Sk : List Γ'
e :
  (bif p a' then ([], some a', Sk)
    else
      match (motive := List Γ' × Option Γ' × List Γ' → List Γ' × Option Γ' × List Γ') splitAtPred p Sk with
      | (l₁, o, l₂) => (a' :: l₁, o, l₂)) =
    (a :: L₁, o, L₂)
e₁ : S k₁ = a' :: Sk
e₂ : p a' = false
⊢ (a' :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2) = (a :: L₁, o, L₂)

Tactic:
simp only [e₂, cond] at e

Premises used: cond
-- 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 Γ'
a' : Γ'
Sk : List Γ'
e :
  (bif p a' then ([], some a', Sk)
    else
      match (motive := List Γ' × Option Γ' × List Γ' → List Γ' × Option Γ' × List Γ') splitAtPred p Sk with
      | (l₁, o, l₂) => (a' :: l₁, o, l₂)) =
    (a :: L₁, o, L₂)
e₁ : S k₁ = a' :: Sk
e₂ : p a' = true
⊢ ([], some a', Sk) = (a :: L₁, o, L₂)

Tactic:
simp only [e₂, cond] at e

Premises used: cond
-- 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 Γ'
a' : Γ'
Sk : List Γ'
e₁ : S k₁ = a' :: Sk
e₂ : p a' = true
e : ([], some a', Sk) = (a :: L₁, o, L₂)
⊢ 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₂))))

Tactic:
cases e
-- 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 Γ'
a' : Γ'
Sk : List Γ'
e₁ : S k₁ = a' :: Sk
e₂ : p a' = false
e : (a' :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2) = (a :: L₁, o, L₂)
cons :
  ∀ (fst : List Γ') (fst_1 : Option Γ') (snd : List Γ') (e₃ : splitAtPred p Sk = (fst, fst_1, snd)),
    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) (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₂))))

Tactic:
rcases e₃ : splitAtPred p Sk with ⟨_, _, _⟩

Premises used: Turing.PartrecToTM2.splitAtPred
-- 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 Γ'
a' : Γ'
Sk : List Γ'
e₁ : S k₁ = a' :: Sk
e₂ : p a' = false
e : (a' :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2) = (a :: L₁, o, L₂)
fst : List Γ'
fst_1 : Option Γ'
snd : List Γ'
e₃ : splitAtPred p Sk = (fst, fst_1, snd)
⊢ (a' :: (fst, fst_1, snd).1, (fst, fst_1, snd).2.1, (fst, fst_1, snd).2.2) = (a :: L₁, o, L₂)

Tactic:
rw [e₃] at e
-- 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 Γ'
a' : Γ'
Sk : List Γ'
e₁ : S k₁ = a' :: Sk
e₂ : p a' = false
e : (a' :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2) = (a :: L₁, o, L₂)
fst : List Γ'
fst_1 : Option Γ'
snd : List Γ'
e₃ : splitAtPred p Sk = (fst, fst_1, snd)
e₄ : (a' :: (fst, fst_1, snd).1, (fst, fst_1, snd).2.1, (fst, fst_1, snd).2.2) = (a :: L₁, o, L₂)
⊢ splitAtPred p Sk = (fst, fst_1, snd)

Tactic:
rw [e₃] at e
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
h₁ : k₁ ≠ k₂
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst : List Γ'
fst_1 : Option Γ'
snd : List Γ'
e₃ : splitAtPred p Sk = (fst, fst_1, snd)
e₁ : S k₁ = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'}
    (e : splitAtPred p (S k₁) = ((fst, fst_1, snd).1, (fst, fst_1, snd).2.1, (fst, fst_1, snd).2.2)),
    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) (fst, fst_1, snd).2.1
        (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (fst, fst_1, snd).2.2) k₂
          ((fst, fst_1, snd).1.reverseAux (S k₂))))
cons :
  TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.move p k₁ k₂ q)) (some a)
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S k₁ Sk) k₂
        ((some a).getD default :: update (β := fun (k : K') ↦ List Γ') S k₁ Sk k₂)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) fst_1
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ snd) k₂
        ((a :: fst).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) (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) (fst, fst_1, snd).2.1
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (fst, fst_1, snd).2.2) k₂
        ((a :: (fst, fst_1, snd).1).reverseAux (S k₂))))

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

Premises used: List.tail_cons, List.head?_cons, cond_false
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
h₁ : k₁ ≠ k₂
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst : List Γ'
fst_1 : Option Γ'
snd : List Γ'
e₃ : splitAtPred p Sk = (fst, fst_1, snd)
e₁ : S k₁ = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'}
    (e : splitAtPred p (S k₁) = ((fst, fst_1, snd).1, (fst, fst_1, snd).2.1, (fst, fst_1, snd).2.2)),
    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) (fst, fst_1, snd).2.1
        (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (fst, fst_1, snd).2.2) k₂
          ((fst, fst_1, snd).1.reverseAux (S k₂))))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.move p k₁ k₂ q)) (some a)
      (update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ Sk) k₂ (a :: S k₂)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (fst, fst_1, snd).2.1
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ')
          (update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ Sk) k₂ (a :: S k₂)) k₁
          (fst, fst_1, snd).2.2)
        k₂
        ((fst, fst_1, snd).1.reverseAux
          (update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ Sk) k₂ (a :: S k₂) k₂))))

Tactic:
@IH _ (update (update S k₁ Sk) k₂ (a :: S k₂)) _
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
h₁ : k₁ ≠ k₂
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst : List Γ'
fst_1 : Option Γ'
snd : List Γ'
e₃ : splitAtPred p Sk = (fst, fst_1, snd)
e₁ : S k₁ = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'}
    (e : splitAtPred p (S k₁) = ((fst, fst_1, snd).1, (fst, fst_1, snd).2.1, (fst, fst_1, snd).2.2)),
    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) (fst, fst_1, snd).2.1
        (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (fst, fst_1, snd).2.2) k₂
          ((fst, fst_1, snd).1.reverseAux (S k₂))))
h :
  update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S k₁ Sk) k₂
      ((some a).getD default :: update (β := fun (k : K') ↦ List Γ') S k₁ Sk k₂) =
    update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ Sk) k₂ (a :: S k₂)
h₂ :
  update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ snd) k₂
      ((a :: fst).reverseAux (S k₂)) =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ Sk) k₂ (a :: S k₂)) k₁
        (fst, fst_1, snd).2.2)
      k₂
      ((fst, fst_1, snd).1.reverseAux
        (update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ Sk) k₂ (a :: S k₂) k₂))
cons :
  splitAtPred p
      (update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ Sk) k₂ (a :: S k₂) k₁) =
    ((fst, fst_1, snd).1, (fst, fst_1, snd).2.1, (fst, fst_1, snd).2.2)
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.move p k₁ k₂ q)) (some a)
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S k₁ Sk) k₂
        ((some a).getD default :: update (β := fun (k : K') ↦ List Γ') S k₁ Sk k₂)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) fst_1
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ snd) k₂
        ((a :: fst).reverseAux (S k₂))))

Tactic:
convert! @IH _ (update (update S k₁ Sk) k₂ (a :: S k₂)) _ using 2
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
h₁ : k₁ ≠ k₂
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst : List Γ'
fst_1 : Option Γ'
snd : List Γ'
e₃ : splitAtPred p Sk = (fst, fst_1, snd)
e₁ : S k₁ = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'}
    (e : splitAtPred p (S k₁) = ((fst, fst_1, snd).1, (fst, fst_1, snd).2.1, (fst, fst_1, snd).2.2)),
    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) (fst, fst_1, snd).2.1
        (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (fst, fst_1, snd).2.2) k₂
          ((fst, fst_1, snd).1.reverseAux (S k₂))))
⊢ update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S k₁ Sk) k₂
      ((some a).getD default :: update (β := fun (k : K') ↦ List Γ') S k₁ Sk k₂) =
    update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ Sk) k₂ (a :: S k₂)

Tactic:
simp [Function.update_of_ne, h₁, h₁.symm, e₃, List.reverseAux]

Premises used: List.reverseAux, Ne.symm, Function.update_of_ne