awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
⊢ ∀ (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))
have pos : ∀ {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))
Tactic: induction a generalizing s with intro l₁
  | one =>
    refine ⟨Γ'.bit0 :: l₁, [Γ'.bit1], some Γ'.cons, rfl, TransGen.head rfl (TransGen.single ?_)⟩
    simp [trPosNum]
  | bit1 m IH =>
    obtain ⟨l₁', l₂', s', e, h⟩ := IH (Γ'.bit0 :: l₁)
    refine ⟨l₁', l₂', s', e, TransGen.head ?_ h⟩
    simp [trPosNum]
    rfl
  | bit0 m _ =>
    refine ⟨l₁, _, some Γ'.bit0, rfl, TransGen.single ?_⟩
    simp only [TM2.step]; rw [tr]
    simp only [TM2.stepAux, pop', elim_main, elim_update_main,
      elim_rev, elim_update_rev, Function.update_self, Option.mem_def, Option.some.injEq]
    rfl
Cleared hypotheses: s, a
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
n : ℕ
c d : List Γ'
a : PosNum
pos pos₁ :
  ∀ {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))
⊢ ∀ (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))
have pos₂ : ∀ (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))
Tactic: induction a generalizing s with intro l₁
  | one =>
    refine ⟨Γ'.bit0 :: l₁, [Γ'.bit1], some Γ'.cons, rfl, TransGen.head rfl (TransGen.single ?_)⟩
    simp [trPosNum]
  | bit1 m IH =>
    obtain ⟨l₁', l₂', s', e, h⟩ := IH (Γ'.bit0 :: l₁)
    refine ⟨l₁', l₂', s', e, TransGen.head ?_ h⟩
    simp [trPosNum]
    rfl
  | bit0 m _ =>
    refine ⟨l₁, _, some Γ'.bit0, rfl, TransGen.single ?_⟩
    simp only [TM2.step]; rw [tr]
    simp only [TM2.stepAux, pop', elim_main, elim_update_main,
      elim_rev, elim_update_rev, Function.update_self, Option.mem_def, Option.some.injEq]
    rfl
Cleared hypotheses: s, a
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
s : Option Γ'
v : List ℕ
c d : List Γ'
⊢ ∃ (s' : Option Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList v) [] c d))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList v.tail) [] c d))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n :: v.tail)) [] c d))
        v.headI)
have nil : ∃ (s' : Option Γ'),
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList []) [] c d))
    (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList (List.tail [])) [] c d))
      (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n :: List.tail [])) [] c d))
      (List.headI []))
Tactic: rcases v with (_ | ⟨_ | n, v⟩)
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
s : Option Γ'
v : List ℕ
c d : List Γ'
nil :
  ∃ (s' : Option Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList []) [] c d))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList (List.tail [])) [] c d))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n :: List.tail [])) [] c d))
        (List.headI []))
⊢ ∃ (s' : Option Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList v) [] c d))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList v.tail) [] c d))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n :: v.tail)) [] c d))
        v.headI)
have cons : ∀ (v : List ℕ),
  ∃ (s' : Option Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList (0 :: v)) [] c d))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList (0 :: v).tail) [] c d))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n :: (0 :: v).tail)) [] c d))
        (0 :: v).headI)
Tactic: rcases v with (_ | ⟨_ | n, v⟩)
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
s : Option Γ'
v : List ℕ
c d : List Γ'
nil :
  ∃ (s' : Option Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList []) [] c d))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList (List.tail [])) [] c d))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n :: List.tail [])) [] c d))
        (List.headI []))
cons :
  ∀ (v : List ℕ),
    ∃ (s' : Option Γ'),
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList (0 :: v)) [] c d))
        (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList (0 :: v).tail) [] c d))
          (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
            TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n :: (0 :: v).tail)) [] c d))
          (0 :: v).headI)
⊢ ∃ (s' : Option Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList v) [] c d))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList v.tail) [] c d))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n :: v.tail)) [] c d))
        v.headI)
have cons₁ : ∀ (v : List ℕ) (n : ℕ),
  ∃ (s' : Option Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList ((n + 1) :: v)) [] c d))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList ((n + 1) :: v).tail) [] c d))
        (fun (n_1 : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n_1 :: ((n + 1) :: v).tail)) [] c d))
        ((n + 1) :: v).headI)
Tactic: rcases v with (_ | ⟨_ | n, v⟩)
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
⊢ ∃ (s' : Option Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList []) [] c d))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList (List.tail [])) [] c d))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n :: List.tail [])) [] c d))
        (List.headI []))
have nil : Membership.mem (α := TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
  (TM2.step (Γ := fun (x : K') ↦ Γ') tr
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList []) [] c d)))
  (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) none (elim (trList (List.tail [])) [] c d))
      (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (trList (n :: List.tail [])) [] c d))
      (List.headI []) :
    TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
Tactic: refine ⟨none, TransGen.single ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
⊢ ∃ (s' : Option Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList (0 :: v)) [] c d))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList (0 :: v).tail) [] c d))
        (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n :: (0 :: v).tail)) [] c d))
        (0 :: v).headI)
have cons : Membership.mem (α := TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
  (TM2.step (Γ := fun (x : K') ↦ Γ') tr
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList (0 :: v)) [] c d)))
  (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) (some Γ'.cons) (elim (trList (0 :: v).tail) [] c d))
      (fun (n : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) (some Γ'.cons) (elim (trList (n :: (0 :: v).tail)) [] c d))
      (0 :: v).headI :
    TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
Tactic: refine ⟨some Γ'.cons, TransGen.single ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ ∃ (s' : Option Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList ((n + 1) :: v)) [] c d))
      (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) s' (elim (trList ((n + 1) :: v).tail) [] c d))
        (fun (n_1 : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
          TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) s' (elim (trList (n_1 :: ((n + 1) :: v).tail)) [] c d))
        ((n + 1) :: v).headI)
have cons : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList ((n + 1) :: v)) [] c d))
  (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) none (elim (trList ((n + 1) :: v).tail) [] c d))
    (fun (n_1 : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (trList (n_1 :: ((n + 1) :: v).tail)) [] c d))
    ((n + 1) :: v).headI)
Tactic: refine ⟨none, ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trList ((n + 1) :: v)) [] c d))
    (Nat.rec (motive := fun (x : ℕ) ↦ TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ'))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) none (elim (trList ((n + 1) :: v).tail) [] c d))
      (fun (n_1 : ℕ) (x : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (trList (n_1 :: ((n + 1) :: v).tail)) [] c d))
      ((n + 1) :: v).headI)
have cons : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
    (elim (trPosNum (Num.succ' (↑n : Num)) ++ Γ'.cons :: trList v) [] c d))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none
    (elim
      (HAppend.hAppend (α := List Γ')
        (match (motive := Num → List Γ') (↑n : Num) with
          | Num.zero => []
          | Num.pos n => trPosNum n :
          List Γ')
        (Γ'.cons :: trList v))
      [] c d))
Tactic: simp only [trList, trNat.eq_1, trNum, Nat.cast_succ, Num.add_one, Num.succ,
    List.tail_cons, List.headI_cons]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
      (elim (trPosNum (Num.succ' (↑n : Num)) ++ Γ'.cons :: trList v) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none
      (elim
        (HAppend.hAppend (α := List Γ')
          (match (motive := Num → List Γ') (↑n : Num) with
            | Num.zero => []
            | Num.pos n => trPosNum n :
            List Γ')
          (Γ'.cons :: trList v))
        [] c d))
have cons : Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
    (elim (trPosNum Num.zero.succ' ++ Γ'.cons :: trList v) [] c d))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none
    (elim
      (HAppend.hAppend (α := List Γ')
        (match (motive := Num → List Γ') Num.zero with
          | Num.zero => []
          | Num.pos n => trPosNum n :
          List Γ')
        (Γ'.cons :: trList v))
      [] c d))
Tactic: rcases (n : Num) with - | a
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
cons :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
      (elim (trPosNum Num.zero.succ' ++ Γ'.cons :: trList v) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none
      (elim
        (HAppend.hAppend (α := List Γ')
          (match (motive := Num → List Γ') Num.zero with
            | Num.zero => []
            | Num.pos n => trPosNum n :
            List Γ')
          (Γ'.cons :: trList v))
        [] c d))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
      (elim (trPosNum (Num.succ' (↑n : Num)) ++ Γ'.cons :: trList v) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none
      (elim
        (HAppend.hAppend (α := List Γ')
          (match (motive := Num → List Γ') (↑n : Num) with
            | Num.zero => []
            | Num.pos n => trPosNum n :
            List Γ')
          (Γ'.cons :: trList v))
        [] c d))
have cons₁ : ∀ (a : PosNum),
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
      (elim (trPosNum (Num.pos a).succ' ++ Γ'.cons :: trList v) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none
      (elim
        (HAppend.hAppend (α := List Γ')
          (match (motive := Num → List Γ') Num.pos a with
            | Num.zero => []
            | Num.pos n => trPosNum n :
            List Γ')
          (Γ'.cons :: trList v))
        [] c d))
Tactic: rcases (n : Num) with - | a
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (Γ'.cons :: trList v) [] c d))
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 (q₁.pred q₂)) s (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (Γ'.cons :: trList v) [] c d))
Tactic: refine TransGen.head rfl ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
      (pop' main
        (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ decide (s = some Γ'.bit0))
          (push (Γ := fun (x : K') ↦ Γ') rev (fun (x : Option Γ') ↦ Γ'.bit1)
            (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q₁.pred q₂))
          (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ natEnd (s.getD default))
            (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q₁)
            (peek' main
              (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ natEnd (s.getD default))
                (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂)
                (push (Γ := fun (x : K') ↦ Γ') rev (fun (x : Option Γ') ↦ Γ'.bit0)
                  (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂)))))))
      s (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (Γ'.cons :: trList v) [] c d))
have cons : TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
  (bif decide ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head? = some Γ'.bit0) then
    TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
          (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
        rev
        (Γ'.bit1 ::
          update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
            (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail rev))
  else
    bif natEnd ((elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?.getD default) then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
        (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
          (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail)
    else
      TM2.stepAux (Γ := fun (x : K') ↦ Γ')
        (peek' main
          (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ natEnd (s.getD default))
            (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂)
            (push (Γ := fun (x : K') ↦ Γ') rev (fun (x : Option Γ') ↦ Γ'.bit0)
              (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ unrev q₂))))
        (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).head?
        (update (β := fun (k : K') ↦ List Γ') (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d) main
          (elim (Γ'.bit1 :: Γ'.cons :: trList v) [] c d main).tail))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (Γ'.cons :: trList v) [] c d))
Tactic: simp only [pop', TM2.stepAux]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
a : PosNum
this :
  ∀ (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum a) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
            (elim (trPosNum a.succ ++ Γ'.cons :: trList v) l₁ c d))
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trPosNum a.succ ++ Γ'.cons :: trList v) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (trPosNum a ++ Γ'.cons :: trList v) [] c d))
have obtain : ∀ (l₁' l₂' : List Γ') (s' : Option Γ') (e : List.reverseAux [] (trPosNum a) = l₁'.reverseAux l₂')
  (h :
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trPosNum a.succ ++ Γ'.cons :: trList v) [] c d))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))),
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s (elim (trPosNum a.succ ++ Γ'.cons :: trList v) [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (trPosNum a ++ Γ'.cons :: trList v) [] c d))
Tactic: obtain ⟨l₁', l₂', s', e, h⟩ := this []