awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
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₂)
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.move (fun (x : Γ') ↦ false) rev k₂ q)) (some val)
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
          (L₁.reverseAux (S rev)))
        k₁
        (val ::
          update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
            (L₁.reverseAux (S rev)) k₁)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ')
          (update (β := fun (k : K') ↦ List Γ')
            (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
              (L₁.reverseAux (S rev)))
            k₁
            (val ::
              update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
                (L₁.reverseAux (S rev)) k₁))
          rev [])
        k₂
        ((update (β := fun (k : K') ↦ List Γ')
              (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
                (L₁.reverseAux (S rev)))
              k₁
              (val ::
                update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
                  (L₁.reverseAux (S rev)) k₁)
              rev).reverseAux
          (update (β := fun (k : K') ↦ List Γ')
            (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
              (L₁.reverseAux (S rev)))
            k₁
            (val ::
              update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
                (L₁.reverseAux (S rev)) k₁)
            k₂))))

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

Premises used: Turing.PartrecToTM2.move_ok, Turing.PartrecToTM2.splitAtPred_false, Ne.symm, And.right, And.left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
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₂)
h :
  update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (val :: L₂)) k₂ (L₁ ++ S k₂) =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ')
        (update (β := fun (k : K') ↦ List Γ')
          (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
            (L₁.reverseAux (S rev)))
          k₁
          (val ::
            update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
              (L₁.reverseAux (S rev)) k₁))
        rev [])
      k₂
      ((update (β := fun (k : K') ↦ List Γ')
            (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
              (L₁.reverseAux (S rev)))
            k₁
            (val ::
              update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
                (L₁.reverseAux (S rev)) k₁)
            rev).reverseAux
        (update (β := fun (k : K') ↦ List Γ')
          (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
            (L₁.reverseAux (S rev)))
          k₁
          (val ::
            update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
              (L₁.reverseAux (S rev)) k₁)
          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 := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.move (fun (x : Γ') ↦ false) rev k₂ q)) (some val)
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
          (L₁.reverseAux (S rev)))
        k₁
        (val ::
          update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
            (L₁.reverseAux (S rev)) k₁)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (val :: L₂)) k₂ (L₁ ++ S k₂)))

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

Premises used: Turing.PartrecToTM2.move_ok, Turing.PartrecToTM2.splitAtPred_false, Ne.symm, And.right, And.left
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
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₂)
h :
  update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (val :: L₂)) k₂ (L₁ ++ S k₂) =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S rev []) k₁ (val :: L₂)) k₂
      ((update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S rev L₁.reverse) k₁ (val :: L₂)
            rev).reverse ++
        update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S rev L₁.reverse) k₁ (val :: L₂) k₂)
⊢ update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (val :: L₂)) k₂ (L₁ ++ S k₂) =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ')
        (update (β := fun (k : K') ↦ List Γ')
          (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
            (L₁.reverseAux (S rev)))
          k₁
          (val ::
            update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
              (L₁.reverseAux (S rev)) k₁))
        rev [])
      k₂
      ((update (β := fun (k : K') ↦ List Γ')
            (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
              (L₁.reverseAux (S rev)))
            k₁
            (val ::
              update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
                (L₁.reverseAux (S rev)) k₁)
            rev).reverseAux
        (update (β := fun (k : K') ↦ List Γ')
          (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
            (L₁.reverseAux (S rev)))
          k₁
          (val ::
            update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
              (L₁.reverseAux (S rev)) k₁)
          k₂))

Tactic:
simp only [h₂, Function.update_comm h₁.1, List.reverseAux_eq, Function.update_self,
      List.append_nil, Function.update_idem]

Premises used: List.reverseAux_eq, List.append_nil, Function.update_comm, And.left, Function.update_idem, Function.update_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
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₂)
rw : update (β := fun (a : K') ↦ List Γ') S rev (S rev) = S
rw₁ rw₂ : S = S
⊢ update (β := fun (a : K') ↦ List Γ') S rev [] = S

Tactic:
rw [← h₂, Function.update_eq_self]

Premises used: Function.update_eq_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
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₂)
h :
  update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (val :: L₂)) k₂ (L₁ ++ S k₂) =
    update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (val :: L₂)) k₂
      ((update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S rev L₁.reverse) k₁ (val :: L₂)
            rev).reverse ++
        update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S rev L₁.reverse) k₁ (val :: L₂) k₂)
⊢ update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (val :: L₂)) k₂ (L₁ ++ S k₂) =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S rev []) k₁ (val :: L₂)) k₂
      ((update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S rev L₁.reverse) k₁ (val :: L₂)
            rev).reverse ++
        update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S rev L₁.reverse) k₁ (val :: L₂) k₂)

Tactic:
rw [show update S rev [] = S by rw [← h₂, Function.update_eq_self]]
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
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 (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (val :: L₂)) k₂ (L₁ ++ S k₂) =
    update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (val :: L₂)) k₂
      ((update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S rev L₁.reverse) k₁ (val :: L₂)
            rev).reverse ++
        update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S rev L₁.reverse) k₁ (val :: 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]

Premises used: Ne.symm, List.reverse_reverse, And.right, And.left, Function.update_self, Function.update_of_ne
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = ([], o, L₂)
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))

Tactic:
TransGen.head' rfl ?_

Premises used: Relation.TransGen.head', StateTransition.Reaches₁, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = ([], o, L₂)
nil :
  ReflTransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr (Λ'.clear p k q)) s S)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))

Tactic:
refine TransGen.head' rfl ?_

Premises used: Relation.TransGen.head', rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = ([], o, L₂)
nil :
  ReflTransGen
    (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 := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (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 (Λ'.clear p k q)) (S k).head?
        (update (β := fun (k : K') ↦ List Γ') S k (S k).tail))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
⊢ ReflTransGen (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)
          (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ Λ'.clear p k q)))
      s S)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))

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

Premises used: Turing.TM2.stepAux, Turing.TM2.step, Turing.PartrecToTM2.pop', Option.elim, Option.mem_def
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = ([], o, L₂)
nil :
  ∀ (e : splitAtPred p (S k) = ([], o, L₂)),
    ReflTransGen
      (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 := none, var := var, stk := stk } => none
          | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
          some b)
      (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 (Λ'.clear p k q)) (S k).head?
          (update (β := fun (k : K') ↦ List Γ') S k (S k).tail))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
⊢ ReflTransGen
    (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 := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (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 (Λ'.clear p k q)) (S k).head?
        (update (β := fun (k : K') ↦ List Γ') S k (S k).tail))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))

Tactic:
revert e
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p [] = ([], o, L₂)
nil :
  ReflTransGen
    (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 := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (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 (Λ'.clear p k q)) (List.head? [])
        (update (β := fun (k : K') ↦ List Γ') S k (List.tail [])))
    (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 (Λ'.clear p k q)) (List.head? [])
        (update (β := fun (k : K') ↦ List Γ') S k (List.tail [])))
⊢ ReflTransGen
    (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 := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (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 (Λ'.clear p k q)) (List.head? [])
        (update (β := fun (k : K') ↦ List Γ') S k (List.tail [])))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))

Tactic:
cases e
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
s : Option Γ'
S : K' → List Γ'
⊢ ReflTransGen
    (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 := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (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 (Λ'.clear p k q)) (List.head? [])
        (update (β := fun (k : K') ↦ List Γ') S k (List.tail [])))
    (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 (Λ'.clear p k q)) (List.head? [])
        (update (β := fun (k : K') ↦ List Γ') S k (List.tail [])))

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
e : splitAtPred p (a :: Sk) = ([], o, L₂)
nil :
  ReflTransGen
    (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 := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (bif p a then TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (some a) (update (β := fun (k : K') ↦ List Γ') S k Sk)
    else
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) (some a)
        (update (β := fun (k : K') ↦ List Γ') S k Sk))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
⊢ ReflTransGen
    (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 := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (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 (Λ'.clear p k q)) (a :: Sk).head?
        (update (β := fun (k : K') ↦ List Γ') S k (a :: Sk).tail))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))

Tactic:
simp only [splitAtPred, List.head?, List.tail_cons] at e ⊢

Premises used: List.head?, List.tail_cons, Turing.PartrecToTM2.splitAtPred
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
e :
  (bif p a then ([], some a, Sk) else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
    ([], o, L₂)
nil :
  ∀
    (e :
      (bif p a then ([], some a, Sk) else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
        ([], o, L₂)),
    ReflTransGen
      (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 := none, var := var, stk := stk } => none
          | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
          some b)
      (bif p a then TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (some a) (update (β := fun (k : K') ↦ List Γ') S k Sk)
      else
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) (some a)
          (update (β := fun (k : K') ↦ List Γ') S k Sk))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
⊢ ReflTransGen
    (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 := none, var := var, stk := stk } => none
        | { l := some l, var := v, stk := S } => some (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr l) v S)) =
        some b)
    (bif p a then TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (some a) (update (β := fun (k : K') ↦ List Γ') S k Sk)
    else
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) (some a)
        (update (β := fun (k : K') ↦ List Γ') S k Sk))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))

Tactic:
revert e