awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
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') ↦ Γ')
      (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₃))
have 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.stepAux (Γ := fun (x : K') ↦ Γ')
    (tr
      (Λ'.read fun (s : Option Γ') ↦
        (if s = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) stack) (unrev q)))
    (some Γ'.cons)
    (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃)))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat a ++ Γ'.cons :: trList L₁) [] [] L₃))
Tactic: simp only [TM2.step, Option.mem_def, trList, List.append_assoc,
      List.cons_append, elim_update_stack, elim_rev, elim_update_rev, Function.update_self,
      List.headI_cons]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
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.stepAux (Γ := fun (x : K') ↦ Γ')
      (tr
        (Λ'.read fun (s : Option Γ') ↦
          (if s = some Γ'.consₗ then id else Λ'.clear (fun (x : Γ') ↦ decide (x = Γ'.consₗ)) stack) (unrev q)))
      (some Γ'.cons)
      (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat a ++ Γ'.cons :: trList L₁) [] [] L₃))
have 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 (unrev q)) (some Γ'.consₗ)
    (update (β := fun (k : K') ↦ List Γ')
      (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃)) stack
      L₃))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat a ++ Γ'.cons :: trList L₁) [] [] L₃))
Tactic: refine
      TransGen.trans
        (clear_ok
          (splitAtPred_eq _ _ (trList L₂) (some Γ'.consₗ) L₃
            (fun x h => Bool.decide_false (trList_ne_consₗ _ _ h)) ⟨rfl, by simp⟩))
        ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
L₁ : List ℕ
L₃ : List Γ'
a : ℕ
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ₗ)
      (update (β := fun (k : K') ↦ List Γ')
        (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
        stack L₃))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNat a ++ Γ'.cons :: trList L₁) [] [] L₃))
have h : elim (trNat a ++ Γ'.cons :: trList L₁) [] [] L₃ =
  update (β := fun (k : K') ↦ List Γ')
    (update (β := fun (a : K') ↦ List Γ')
      (update (β := fun (k : K') ↦ List Γ')
        (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
        stack L₃)
      rev [])
    main
    ((update (β := fun (k : K') ↦ List Γ')
          (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
          stack L₃ rev).reverseAux
      (update (β := fun (k : K') ↦ List Γ')
        (elim (trList L₁) ((some Γ'.cons).getD default :: (trNat a).reverseAux []) [] (trList L₂ ++ Γ'.consₗ :: L₃))
        stack L₃ main))
Tactic: convert! unrev_ok using 2
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trList [n]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trList [n.succ]) [] c d))
have simp : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trNum (↑n : Num) ++ [Γ'.cons]) [] c d))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum (Num.succ (↑n : Num)) ++ [Γ'.cons]) [] c d))
Tactic: simp only [trList, trNat.eq_1, Nat.cast_succ, Num.add_one]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trNum (↑n : Num) ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum (Num.succ (↑n : Num)) ++ [Γ'.cons]) [] c d))
have zero : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d))
Tactic: rcases (n : Num) with - | a
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
zero :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trNum (↑n : Num) ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum (Num.succ (↑n : Num)) ++ [Γ'.cons]) [] c d))
have pos : ∀ (a : PosNum),
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trNum (Num.pos a) ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum (Num.pos a).succ ++ [Γ'.cons]) [] c d))
Tactic: rcases (n : Num) with - | a
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d))
have zero : TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
  (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr q.succ) s (elim (trNum Num.zero ++ [Γ'.cons]) [] c d))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trNum Num.zero.succ ++ [Γ'.cons]) [] c d))
Tactic: refine TransGen.head rfl ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum a.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trPosNum a.succ ++ [Γ'.cons]) [] c d))
have obtain : ∀ (l₁' l₂' : List Γ') (s' : Option Γ') (e : List.reverseAux [] (trPosNum a.succ) = l₁'.reverseAux l₂')
  (h :
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) [] c d))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))),
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trPosNum a.succ ++ [Γ'.cons]) [] c d))
Tactic: obtain ⟨l₁', l₂', s', e, h⟩ := this []
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum a.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
l₁' l₂' : List Γ'
s' : Option Γ'
e : trPosNum a.succ = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trPosNum a.succ ++ [Γ'.cons]) [] c d))
have refine : 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)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trPosNum a.succ ++ [Γ'.cons]) [] c d))
Tactic: refine h.trans ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum a.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
l₁' l₂' : List Γ'
s' : Option Γ'
e : trPosNum a.succ = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
⊢ 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)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trPosNum a.succ ++ [Γ'.cons]) [] c d))
have h₁ : elim (trPosNum a.succ ++ [Γ'.cons]) [] c d =
  update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') (elim (l₂' ++ [Γ'.cons]) l₁' c d) rev [])
    main ((elim (l₂' ++ [Γ'.cons]) l₁' c d rev).reverseAux (elim (l₂' ++ [Γ'.cons]) l₁' c d main))
Tactic: convert! unrev_ok using 2
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (trPosNum a.succ ++ [Γ'.cons]) [] c d))
have pos : ∀ (l₁ : List Γ'),
  ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum a.succ) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum a ++ [Γ'.cons]) l₁ c d))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
Tactic: suffices ∀ l₁, ∃ l₁' l₂' s',
      List.reverseAux l₁ (trPosNum a.succ) = List.reverseAux l₁' l₂' ∧
        Reaches₁ (TM2.step tr) ⟨some q.succ, s, K'.elim (trPosNum a ++ [Γ'.cons]) l₁ c d⟩
          ⟨some (unrev q), s', K'.elim (l₂' ++ [Γ'.cons]) l₁' c d⟩ by
    obtain ⟨l₁', l₂', s', e, h⟩ := this []
    simp only [List.reverseAux] at e
    refine h.trans ?_
    convert! unrev_ok using 2
    simp [e, List.reverseAux_eq]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
n : ℕ
c d : List Γ'
s : Option Γ'
l₁ : List Γ'
⊢ ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum PosNum.one.succ) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum PosNum.one ++ [Γ'.cons]) l₁ c d))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
have pos : TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (some Γ'.cons)
    (elim ([Γ'.bit1] ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d) ∈
  TM2.step (Γ := fun (x : K') ↦ Γ') tr
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr q.succ) s (elim (trPosNum PosNum.one ++ [Γ'.cons]) l₁ c d))
Tactic: refine ⟨Γ'.bit0 :: l₁, [Γ'.bit1], some Γ'.cons, rfl, TransGen.head rfl (TransGen.single ?_)⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
IH :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
s : Option Γ'
l₁ : List Γ'
⊢ ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum m.bit1.succ) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m.bit1 ++ [Γ'.cons]) l₁ c d))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
have pos : ∀ (l₁' l₂' : List Γ') (s' : Option Γ') (e : (Γ'.bit0 :: l₁).reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂')
  (h :
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) (some Γ'.bit1)
        (elim (trPosNum m ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))),
  ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum m.bit1.succ) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m.bit1 ++ [Γ'.cons]) l₁ c d))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
Tactic: obtain ⟨l₁', l₂', s', e, h⟩ := IH (Γ'.bit0 :: l₁)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
IH :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
s : Option Γ'
l₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit0 :: l₁).reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) (some Γ'.bit1)
      (elim (trPosNum m ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
⊢ ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum m.bit1.succ) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m.bit1 ++ [Γ'.cons]) l₁ c d))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
have pos : TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) (some Γ'.bit1) (elim (trPosNum m ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d) ∈
  TM2.step (Γ := fun (x : K') ↦ Γ') tr
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m.bit1 ++ [Γ'.cons]) l₁ c d))
Tactic: refine ⟨l₁', l₂', s', e, TransGen.head ?_ h⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
IH :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
s : Option Γ'
l₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit0 :: l₁).reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) (some Γ'.bit1)
      (elim (trPosNum m ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
⊢ TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) (some Γ'.bit1)
      (elim (trPosNum m ++ [Γ'.cons]) (Γ'.bit0 :: l₁) c d) ∈
    TM2.step (Γ := fun (x : K') ↦ Γ') tr
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m.bit1 ++ [Γ'.cons]) l₁ c d))
have pos : some Γ'.bit1 = some Γ'.bit1
Tactic: simp [trPosNum]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
a_ih :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
s : Option Γ'
l₁ : List Γ'
⊢ ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum m.bit0.succ) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m.bit0 ++ [Γ'.cons]) l₁ c d))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
have pos : TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (some Γ'.bit0) (elim (trPosNum m.bit0.succ ++ [Γ'.cons]) l₁ c d) ∈
  TM2.step (Γ := fun (x : K') ↦ Γ') tr
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m.bit0 ++ [Γ'.cons]) l₁ c d))
Tactic: refine ⟨l₁, _, some Γ'.bit0, rfl, TransGen.single ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
n : ℕ
c d : List Γ'
m : PosNum
a_ih :
  ∀ {s : Option Γ'} (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m.succ) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) s (elim (trPosNum m ++ [Γ'.cons]) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) s' (elim (l₂' ++ [Γ'.cons]) l₁' c d))
s : Option Γ'
l₁ : List Γ'
⊢ TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (some Γ'.bit0)
      (elim (trPosNum m.bit0.succ ++ [Γ'.cons]) l₁ c d) ∈
    some
      (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
        (pop' main
          (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ decide (s = some Γ'.bit1))
            (push (Γ := fun (x : K') ↦ Γ') rev (fun (x : Option Γ') ↦ Γ'.bit0)
              (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q.succ))
            (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ decide (s = some Γ'.cons))
              (push (Γ := fun (x : K') ↦ Γ') main (fun (x : Option Γ') ↦ Γ'.cons)
                (push (Γ := fun (x : K') ↦ Γ') main (fun (x : Option Γ') ↦ Γ'.bit1)
                  (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q)))
              (push (Γ := fun (x : K') ↦ Γ') main (fun (x : Option Γ') ↦ Γ'.bit1)
                (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q)))))
        s (elim (trPosNum m.bit0 ++ [Γ'.cons]) l₁ c d))
have pos : (bif decide ((trPosNum m.bit0 ++ [Γ'.cons]).head? = some Γ'.bit1) then
    TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.succ) (trPosNum m.bit0 ++ [Γ'.cons]).head?
      (elim (trPosNum m.bit0 ++ [Γ'.cons]).tail (Γ'.bit0 :: l₁) c d)
  else
    bif decide ((trPosNum m.bit0 ++ [Γ'.cons]).head? = some Γ'.cons) then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (trPosNum m.bit0 ++ [Γ'.cons]).head?
        (elim (Γ'.bit1 :: Γ'.cons :: (trPosNum m.bit0 ++ [Γ'.cons]).tail) l₁ c d)
    else
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (trPosNum m.bit0 ++ [Γ'.cons]).head?
        (elim (Γ'.bit1 :: (trPosNum m.bit0 ++ [Γ'.cons]).tail) l₁ c d)) =
  TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q)) (some Γ'.bit0) (elim (trPosNum m.bit0.succ ++ [Γ'.cons]) l₁ c d)
Tactic: simp only [TM2.stepAux, pop', elim_main, elim_update_main,
      elim_rev, elim_update_rev, Function.update_self, Option.mem_def, Option.some.injEq]