awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trList (a :: l)
⊢ x ≠ Γ'.consₗ
have h₁ : x ∈ trNat a ∨ x = Γ'.cons ∨ x ∈ trList l
Tactic: simp only [trList, List.mem_append, List.mem_cons] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trNat a ∨ x = Γ'.cons ∨ x ∈ trList l
⊢ x ≠ Γ'.consₗ
have inl : ∀ (h : x ∈ trNat a), x ≠ Γ'.consₗ
Tactic: obtain h | rfl | h := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trNat a ∨ x = Γ'.cons ∨ x ∈ trList l
inl : ∀ (h : x ∈ trNat a), x ≠ Γ'.consₗ
⊢ x ≠ Γ'.consₗ
have inr : Γ'.cons ≠ Γ'.consₗ
Tactic: obtain h | rfl | h := h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
a : ℕ
l : List ℕ
x : Γ'
h : x ∈ trNat a ∨ x = Γ'.cons ∨ x ∈ trList l
inl : ∀ (h : x ∈ trNat a), x ≠ Γ'.consₗ
inr : Γ'.cons ≠ Γ'.consₗ
⊢ x ≠ Γ'.consₗ
have inr₁ : ∀ (h : x ∈ trList l), x ≠ Γ'.consₗ
Tactic: obtain h | rfl | h := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (head main q)) s (elim (trList L) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList [L.headI]) [] c d))
have refine_1 : Option.elim' (elim (trList L) [] c d main = trNat L.headI ∧ trList L.tail = [])
  (fun (a : Γ') ↦ natEnd a = true ∧ elim (trList L) [] c d main = trNat L.headI ++ a :: trList L.tail) o
Tactic: refine
    (move_ok (by decide)
          (splitAtPred_eq _ _ (trNat L.headI) o (trList L.tail) (trNat_natEnd _) ?_)).trans
      (TransGen.head rfl (TransGen.head rfl ?_))
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
refine_1 :
  Option.elim' (elim (trList L) [] c d main = trNat L.headI ∧ trList L.tail = [])
    (fun (a : Γ') ↦ natEnd a = true ∧ elim (trList L) [] c d main = trNat L.headI ++ a :: trList L.tail) o
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (head main q)) s (elim (trList L) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList [L.headI]) [] c d))
have refine_2 : TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
  (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
    (tr
      ((fun (x : Option Γ') ↦
          Λ'.read fun (s : Option Γ') ↦
            (if s = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) main) (unrev q))
        o))
    o
    (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ') (elim (trList L) [] c d) main (trList L.tail)) rev
        ((trNat L.headI).reverseAux (elim (trList L) [] c d rev)))
      rev
      ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.cons) s) default : Γ')) o ::
        update (β := fun (k : K') ↦ List Γ')
          (update (β := fun (a : K') ↦ List Γ') (elim (trList L) [] c d) main (trList L.tail)) rev
          ((trNat L.headI).reverseAux (elim (trList L) [] c d rev)) rev)))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList [L.headI]) [] c d))
Tactic: refine
    (move_ok (by decide)
          (splitAtPred_eq _ _ (trNat L.headI) o (trList L.tail) (trNat_natEnd _) ?_)).trans
      (TransGen.head rfl (TransGen.head rfl ?_))
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ Option.elim' (elim (trList L) [] c d main = trNat L.headI ∧ trList L.tail = [])
    (fun (a : Γ') ↦ natEnd a = true ∧ elim (trList L) [] c d main = trNat L.headI ++ a :: trList L.tail) o
have refine_1 : let o : Option Γ' :=
  List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') [] none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons;
Option.elim' (elim (trList []) [] c d main = trNat (List.headI []) ∧ trList (List.tail []) = [])
  (fun (a : Γ') ↦ natEnd a = true ∧ elim (trList []) [] c d main = trNat (List.headI []) ++ a :: trList (List.tail []))
  o
Tactic: cases L
Cleared hypotheses: L, o
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
refine_1 :
  let o : Option Γ' :=
    List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') [] none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons;
  Option.elim' (elim (trList []) [] c d main = trNat (List.headI []) ∧ trList (List.tail []) = [])
    (fun (a : Γ') ↦
      natEnd a = true ∧ elim (trList []) [] c d main = trNat (List.headI []) ++ a :: trList (List.tail []))
    o
⊢ Option.elim' (elim (trList L) [] c d main = trNat L.headI ∧ trList L.tail = [])
    (fun (a : Γ') ↦ natEnd a = true ∧ elim (trList L) [] c d main = trNat L.headI ++ a :: trList L.tail) o
have refine_1₁ : ∀ (head : ℕ) (tail : List ℕ),
  let o : Option Γ' :=
    List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') (head :: tail) none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons;
  Option.elim' (elim (trList (head :: tail)) [] c d main = trNat (head :: tail).headI ∧ trList (head :: tail).tail = [])
    (fun (a : Γ') ↦
      natEnd a = true ∧
        elim (trList (head :: tail)) [] c d main = trNat (head :: tail).headI ++ a :: trList (head :: tail).tail)
    o
Tactic: cases L
Cleared hypotheses: L, o
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
      (goto (Γ := fun (x : K') ↦ Γ') fun (s : Option Γ') ↦
        (if s = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) main) (unrev q))
      o
      (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
        (update (β := fun (k : K') ↦ List Γ')
          (update (β := fun (a : K') ↦ List Γ') (elim (trList L) [] c d) main (trList L.tail)) rev
          ((trNat L.headI).reverseAux (elim (trList L) [] c d rev)))
        rev
        ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.cons) s) default : Γ')) o ::
          update (β := fun (k : K') ↦ List Γ')
            (update (β := fun (a : K') ↦ List Γ') (elim (trList L) [] c d) main (trList L.tail)) rev
            ((trNat L.headI).reverseAux (elim (trList L) [] c d rev)) rev)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList [L.headI]) [] c d))
have refine_2 : 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 ((if o = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) main) (unrev q))) o
    (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat L.headI ++ [Γ'.cons]) [] c d))
Tactic: simp only [TM2.step, Option.mem_def, TM2.stepAux, elim_update_main, elim_rev, elim_update_rev,
    Function.update_self, trList]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ o ≠ some Γ'.consₗ
have nil : let o : Option Γ' :=
  List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') [] none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons;
o ≠ some Γ'.consₗ
Tactic: cases L
Cleared hypotheses: L, o
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
nil :
  let o : Option Γ' :=
    List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') [] none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons;
  o ≠ some Γ'.consₗ
⊢ o ≠ some Γ'.consₗ
have cons : ∀ (head : ℕ) (tail : List ℕ),
  let o : Option Γ' :=
    List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') (head :: tail) none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons;
  o ≠ some Γ'.consₗ
Tactic: cases L
Cleared hypotheses: L, o
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ 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 ((if o = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) main) (unrev q))) o
      (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat L.headI ++ [Γ'.cons]) [] c d))
have refine_2 : 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 (Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) main (unrev q))) o
    (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat L.headI ++ [Γ'.cons]) [] c d))
Tactic: rw [if_neg (show o ≠ some Γ'.consₗ by cases L <;> simp [o])]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
⊢ 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 (Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) main (unrev q))) o
      (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat L.headI ++ [Γ'.cons]) [] c d))
have refine_2 : ∀ x ∈ elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d main,
  decide (x = Γ'.consₗ) = false
Tactic: refine (clear_ok (splitAtPred_eq _ _ _ none [] ?_ ⟨rfl, rfl⟩)).trans ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.cons
refine_2 :
  ∀ x ∈ elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d main,
    decide (x = Γ'.consₗ) = false
⊢ 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 (Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) main (unrev q))) o
      (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat L.headI ++ [Γ'.cons]) [] c d))
have refine_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 (unrev q)) none
    (update (β := fun (k : K') ↦ List Γ')
      (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main []))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat L.headI ++ [Γ'.cons]) [] c d))
Tactic: refine (clear_ok (splitAtPred_eq _ _ _ none [] ?_ ⟨rfl, rfl⟩)).trans ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
L : List ℕ
c d : List Γ'
o : Option Γ' := List.casesOn (motive := fun (x : List ℕ) ↦ Option Γ') L none fun (x : ℕ) (x_1 : List ℕ) ↦ some Γ'.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 (unrev q)) none
      (update (β := fun (k : K') ↦ List Γ')
        (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main []))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat L.headI ++ [Γ'.cons]) [] c d))
have h : elim (trNat L.headI ++ [Γ'.cons]) [] c d =
  update (β := fun (k : K') ↦ List Γ')
    (update (β := fun (a : K') ↦ List Γ')
      (update (β := fun (k : K') ↦ List Γ')
        (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main [])
      rev [])
    main
    ((update (β := fun (k : K') ↦ List Γ')
          (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main []
          rev).reverseAux
      (update (β := fun (k : K') ↦ List Γ')
        (elim (trList L.tail) ((some Γ'.cons).getD default :: (trNat L.headI).reverseAux []) c d) main [] main))
Tactic: convert! unrev_ok using 2
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
L₁ L₂ : List ℕ
L₃ : List Γ'
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (head stack q)) s (elim (trList L₁) [] [] (trList L₂ ++ Γ'.consₗ :: L₃)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList (L₂.headI :: L₁)) [] [] L₃))
have nil : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (head stack q)) s (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList (List.headI [] :: L₁)) [] [] L₃))
Tactic: rcases L₂ with - | ⟨a, L₂⟩
Cleared hypotheses: L₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
L₁ L₂ : List ℕ
L₃ : List Γ'
nil :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (head stack q)) s (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList (List.headI [] :: L₁)) [] [] L₃))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (head stack q)) s (elim (trList L₁) [] [] (trList L₂ ++ Γ'.consₗ :: L₃)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList (L₂.headI :: L₁)) [] [] L₃))
have cons : ∀ (a : ℕ) (L₂ : List ℕ),
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (head stack q)) s
      (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList ((a :: L₂).headI :: L₁)) [] [] L₃))
Tactic: rcases L₂ with - | ⟨a, L₂⟩
Cleared hypotheses: L₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (head stack q)) s (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList (List.headI [] :: L₁)) [] [] L₃))
have nil : TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
  (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
    (tr
      ((fun (x : Option Γ') ↦
          Λ'.read fun (s : Option Γ') ↦
            (if s = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) stack) (unrev q))
        (some Γ'.consₗ)))
    (some Γ'.consₗ)
    (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ') (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)) stack L₃) rev
        (List.reverseAux [] (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃) rev)))
      rev
      ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.cons) s) default : Γ')) (some Γ'.consₗ) ::
        update (β := fun (k : K') ↦ List Γ')
          (update (β := fun (a : K') ↦ List Γ') (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)) stack L₃) rev
          (List.reverseAux [] (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃) rev)) rev)))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList (List.headI [] :: L₁)) [] [] L₃))
Tactic: refine
      TransGen.trans
        (move_ok (by decide)
          (splitAtPred_eq _ _ [] (some Γ'.consₗ) L₃ (by rintro _ ⟨⟩) ⟨rfl, rfl⟩))
        (TransGen.head rfl (TransGen.head rfl ?_))
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
      (goto (Γ := fun (x : K') ↦ Γ') fun (s : Option Γ') ↦
        (if s = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) stack) (unrev q))
      (some Γ'.consₗ)
      (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
        (update (β := fun (k : K') ↦ List Γ')
          (update (β := fun (a : K') ↦ List Γ') (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)) stack L₃) rev
          (List.reverseAux [] (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃) rev)))
        rev
        ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.cons) s) default : Γ')) (some Γ'.consₗ) ::
          update (β := fun (k : K') ↦ List Γ')
            (update (β := fun (a : K') ↦ List Γ') (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃)) stack L₃) rev
            (List.reverseAux [] (elim (trList L₁) [] [] (trList [] ++ Γ'.consₗ :: L₃) rev)) rev)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList (List.headI [] :: L₁)) [] [] L₃))
have nil : 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 (unrev q)) (some Γ'.consₗ)
    (elim (trList L₁) [(some Γ'.cons).getD default] [] L₃))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (Γ'.cons :: trList L₁) [] [] L₃))
Tactic: simp only [TM2.step, Option.mem_def, TM2.stepAux, ite_true, id_eq, trList, List.nil_append,
      elim_update_stack, elim_rev, List.reverseAux_nil, elim_update_rev, Function.update_self,
      List.headI_nil, trNat_default]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
⊢ 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 (unrev q)) (some Γ'.consₗ)
      (elim (trList L₁) [(some Γ'.cons).getD default] [] L₃))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (Γ'.cons :: trList L₁) [] [] L₃))
have h : elim (Γ'.cons :: trList L₁) [] [] L₃ =
  update (β := fun (k : K') ↦ List Γ')
    (update (β := fun (a : K') ↦ List Γ') (elim (trList L₁) [(some Γ'.cons).getD default] [] L₃) rev []) main
    ((elim (trList L₁) [(some Γ'.cons).getD default] [] L₃ rev).reverseAux
      (elim (trList L₁) [(some Γ'.cons).getD default] [] L₃ main))
Tactic: convert! unrev_ok using 2
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
L₂ : List ℕ
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (head stack q)) s
      (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList ((a :: L₂).headI :: L₁)) [] [] L₃))
have cons : TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
  (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
    (tr
      ((fun (x : Option Γ') ↦
          Λ'.read fun (s : Option Γ') ↦
            (if s = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) stack) (unrev q))
        (some Γ'.cons)))
    (some Γ'.cons)
    (update (β := fun (k : K') ↦ List ((fun (x : K') ↦ Γ') k))
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ') (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃)) stack
          (trList L₂ ++ Γ'.consₗ :: L₃))
        rev ((trNat a).reverseAux (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃) rev)))
      rev
      ((fun (s : Option Γ') ↦ (Option.getD ((fun (x : Option Γ') ↦ some Γ'.cons) s) default : Γ')) (some Γ'.cons) ::
        update (β := fun (k : K') ↦ List Γ')
          (update (β := fun (a : K') ↦ List Γ') (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃)) stack
            (trList L₂ ++ Γ'.consₗ :: L₃))
          rev ((trNat a).reverseAux (elim (trList L₁) [] [] (trList (a :: L₂) ++ Γ'.consₗ :: L₃) rev)) rev)))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList ((a :: L₂).headI :: L₁)) [] [] L₃))
Tactic: refine
      TransGen.trans
        (move_ok (by decide)
          (splitAtPred_eq _ _ (trNat a) (some Γ'.cons) (trList L₂ ++ Γ'.consₗ :: L₃)
            (trNat_natEnd _) ⟨rfl, by simp⟩))
        (TransGen.head rfl (TransGen.head rfl ?_))