awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
l₁' l₂' : List Γ'
s' : Option Γ'
e : 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))
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 :: trList v) l₁' c d))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (trPosNum a ++ Γ'.cons :: trList v) [] c d))
Tactic: refine h.trans ?_
-- 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))
l₁' l₂' : List Γ'
s' : Option Γ'
e : 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))
⊢ 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 :: trList v) l₁' c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₂) none (elim (trPosNum a ++ Γ'.cons :: trList v) [] c d))
have h₁ : elim (trPosNum a ++ Γ'.cons :: trList v) [] c d =
  update (β := fun (k : K') ↦ List Γ')
    (update (β := fun (a : K') ↦ List Γ') (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d) rev []) main
    ((elim (l₂' ++ Γ'.cons :: trList v) l₁' c d rev).reverseAux (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d main))
Tactic: convert! unrev_ok using 2
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
a : PosNum
⊢ 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 cons : ∀ (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))
Tactic: suffices ∀ l₁, ∃ l₁' l₂' s',
    List.reverseAux l₁ (trPosNum a) = List.reverseAux l₁' l₂' ∧
      Reaches₁ (TM2.step tr)
        ⟨some (q₁.pred q₂), s, K'.elim (trPosNum a.succ ++ Γ'.cons :: trList v) l₁ c d⟩
        ⟨some (unrev q₂), s', K'.elim (l₂' ++ Γ'.cons :: trList v) 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₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
s : Option Γ'
l₁ : List Γ'
⊢ ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum PosNum.one) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
          (elim (trPosNum PosNum.one.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))
have cons : TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) (some Γ'.cons)
    (elim ([] ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d) ∈
  TM2.step (Γ := fun (x : K') ↦ Γ') tr
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr (q₁.pred q₂)) s
      (elim (trPosNum PosNum.one.succ ++ Γ'.cons :: trList v) l₁ c d))
Tactic: refine ⟨Γ'.bit1::l₁, [], some Γ'.cons, rfl, TransGen.head rfl (TransGen.single ?_)⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
m : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
            (elim (trPosNum m.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))
s : Option Γ'
l₁ : List Γ'
⊢ ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum m.bit1) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
          (elim (trPosNum m.bit1.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))
have cons : ∀ (l₁' l₂' : List Γ') (s' : Option Γ') (e : (Γ'.bit1 :: l₁).reverseAux (trPosNum m) = l₁'.reverseAux l₂')
  (h :
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) (some Γ'.bit0)
        (elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))),
  ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum m.bit1) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
          (elim (trPosNum m.bit1.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))
Tactic: obtain ⟨l₁', l₂', s', e, h⟩ := IH (some Γ'.bit0) (Γ'.bit1 :: l₁)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
m : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
            (elim (trPosNum m.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))
s : Option Γ'
l₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit1 :: l₁).reverseAux (trPosNum m) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) (some Γ'.bit0)
      (elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))
⊢ ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum m.bit1) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
          (elim (trPosNum m.bit1.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))
have cons : TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) (some Γ'.bit0)
    (elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d) ∈
  TM2.step (Γ := fun (x : K') ↦ Γ') tr
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
      (elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v) l₁ c d))
Tactic: refine ⟨l₁', l₂', s', e, TransGen.head ?_ h⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
m : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
            (elim (trPosNum m.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))
s : Option Γ'
l₁ l₁' l₂' : List Γ'
s' : Option Γ'
e : (Γ'.bit1 :: l₁).reverseAux (trPosNum m) = l₁'.reverseAux l₂'
h :
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) (some Γ'.bit0)
      (elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) s' (elim (l₂' ++ Γ'.cons :: trList v) l₁' c d))
⊢ TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) (some Γ'.bit0)
      (elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d) ∈
    TM2.step (Γ := fun (x : K') ↦ Γ') tr
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
        (elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v) l₁ c d))
have cons : (bif decide ((trPosNum m.bit1.succ).head?.getD Γ'.cons = Γ'.bit0) then
    TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) (some ((trPosNum m.bit1.succ).head?.getD Γ'.cons))
      (elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v).tail (Γ'.bit1 :: l₁) c d)
  else
    bif
        match (motive := Γ' → Bool) (trPosNum m.bit1.succ).head?.getD Γ'.cons with
        | Γ'.consₗ => true
        | Γ'.cons => true
        | x => false then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) (some ((trPosNum m.bit1.succ).head?.getD Γ'.cons))
        (elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v).tail l₁ c d)
    else
      bif
          match (motive := Γ' → Bool)
            (getElem? (valid := fun (as : List Γ') (i : ℕ) ↦ i < as.length)
                  (trPosNum m.bit1.succ ++ Γ'.cons :: trList v) 1).getD
              Γ'.consₗ with
          | Γ'.consₗ => true
          | Γ'.cons => true
          | x => false then
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂))
          (getElem? (valid := fun (as : List Γ') (i : ℕ) ↦ i < as.length) (trPosNum m.bit1.succ ++ Γ'.cons :: trList v)
            1)
          (elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v).tail l₁ c d)
      else
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂))
          (getElem? (valid := fun (as : List Γ') (i : ℕ) ↦ i < as.length) (trPosNum m.bit1.succ ++ Γ'.cons :: trList v)
            1)
          (elim (trPosNum m.bit1.succ ++ Γ'.cons :: trList v).tail (Γ'.bit0 :: l₁) c d)) =
  TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) (some Γ'.bit0)
    (elim (trPosNum m.succ ++ Γ'.cons :: trList v) (Γ'.bit1 :: l₁) c d)
Tactic: simp
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
m : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
            (elim (trPosNum m.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))
s : Option Γ'
l₁ : List Γ'
⊢ ∃ (a : Γ') (l : List Γ'), trPosNum m = a :: l ∧ natEnd a = false
have one : ∀
  (IH :
    ∀ (s : Option Γ') (l₁ : List Γ'),
      ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
        l₁.reverseAux (trPosNum PosNum.one) = l₁'.reverseAux l₂' ∧
          Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
            (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
              (elim (trPosNum PosNum.one.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))),
  ∃ (a : Γ') (l : List Γ'), trPosNum PosNum.one = a :: l ∧ natEnd a = false
Tactic: cases m
Cleared hypotheses: m, IH
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
m : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
            (elim (trPosNum m.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))
s : Option Γ'
l₁ : List Γ'
one :
  ∀
    (IH :
      ∀ (s : Option Γ') (l₁ : List Γ'),
        ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
          l₁.reverseAux (trPosNum PosNum.one) = l₁'.reverseAux l₂' ∧
            Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
              (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
                (elim (trPosNum PosNum.one.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))),
    ∃ (a : Γ') (l : List Γ'), trPosNum PosNum.one = a :: l ∧ natEnd a = false
⊢ ∃ (a : Γ') (l : List Γ'), trPosNum m = a :: l ∧ natEnd a = false
have bit1 : ∀ (a : PosNum)
  (IH :
    ∀ (s : Option Γ') (l₁ : List Γ'),
      ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
        l₁.reverseAux (trPosNum a.bit1) = l₁'.reverseAux l₂' ∧
          Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
            (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
              (elim (trPosNum a.bit1.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))),
  ∃ (a_1 : Γ') (l : List Γ'), trPosNum a.bit1 = a_1 :: l ∧ natEnd a_1 = false
Tactic: cases m
Cleared hypotheses: m, IH
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
m : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
            (elim (trPosNum m.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))
s : Option Γ'
l₁ : List Γ'
one :
  ∀
    (IH :
      ∀ (s : Option Γ') (l₁ : List Γ'),
        ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
          l₁.reverseAux (trPosNum PosNum.one) = l₁'.reverseAux l₂' ∧
            Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
              (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
                (elim (trPosNum PosNum.one.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))),
    ∃ (a : Γ') (l : List Γ'), trPosNum PosNum.one = a :: l ∧ natEnd a = false
bit1 :
  ∀ (a : PosNum)
    (IH :
      ∀ (s : Option Γ') (l₁ : List Γ'),
        ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
          l₁.reverseAux (trPosNum a.bit1) = l₁'.reverseAux l₂' ∧
            Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
              (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
                (elim (trPosNum a.bit1.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))),
    ∃ (a_1 : Γ') (l : List Γ'), trPosNum a.bit1 = a_1 :: l ∧ natEnd a_1 = false
⊢ ∃ (a : Γ') (l : List Γ'), trPosNum m = a :: l ∧ natEnd a = false
have bit0 : ∀ (a : PosNum)
  (IH :
    ∀ (s : Option Γ') (l₁ : List Γ'),
      ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
        l₁.reverseAux (trPosNum a.bit0) = l₁'.reverseAux l₂' ∧
          Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
            (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
              (elim (trPosNum a.bit0.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))),
  ∃ (a_1 : Γ') (l : List Γ'), trPosNum a.bit0 = a_1 :: l ∧ natEnd a_1 = false
Tactic: cases m
Cleared hypotheses: m, IH
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
m : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
            (elim (trPosNum m.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))
s : Option Γ'
l₁ : List Γ'
⊢ ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum m.bit0) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
          (elim (trPosNum m.bit0.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))
have cons : ∀ (a : Γ') (l : List Γ') (e : trPosNum m = a :: l) (h : natEnd a = false),
  ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum m.bit0) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
          (elim (trPosNum m.bit0.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))
Tactic: obtain ⟨a, l, e, h⟩ : ∃ a l, (trPosNum m = a::l) ∧ natEnd a = false := by
      cases m <;> refine ⟨_, _, rfl, rfl⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
m : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
            (elim (trPosNum m.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))
s : Option Γ'
l₁ : List Γ'
a : Γ'
l : List Γ'
e : trPosNum m = a :: l
h : natEnd a = false
⊢ ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
    l₁.reverseAux (trPosNum m.bit0) = l₁'.reverseAux l₂' ∧
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
          (elim (trPosNum m.bit0.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))
have cons : TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) (some a)
    (elim (trPosNum m ++ Γ'.cons :: trList v) (Γ'.bit0 :: l₁) c d) ∈
  TM2.step (Γ := fun (x : K') ↦ Γ') tr
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
      (elim (trPosNum m.bit0.succ ++ Γ'.cons :: trList v) l₁ c d))
Tactic: refine ⟨Γ'.bit0 :: l₁, _, some a, rfl, TransGen.single ?_⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q₁ q₂ : Λ'
c d : List Γ'
v : List ℕ
n : ℕ
m : PosNum
IH :
  ∀ (s : Option Γ') (l₁ : List Γ'),
    ∃ (l₁' : List Γ') (l₂' : List Γ') (s' : Option Γ'),
      l₁.reverseAux (trPosNum m) = l₁'.reverseAux l₂' ∧
        Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
          (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
            (elim (trPosNum m.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))
s : Option Γ'
l₁ : List Γ'
a : Γ'
l : List Γ'
e : trPosNum m = a :: l
h : natEnd a = false
⊢ TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) (some a)
      (elim (trPosNum m ++ Γ'.cons :: trList v) (Γ'.bit0 :: l₁) c d) ∈
    TM2.step (Γ := fun (x : K') ↦ Γ') tr
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (q₁.pred q₂)) s
        (elim (trPosNum m.bit0.succ ++ Γ'.cons :: trList v) l₁ c d))
have cons : (bif natEnd Γ'.bit1 then
    TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q₁) (some Γ'.bit1) (elim (a :: (l ++ Γ'.cons :: trList v)) l₁ c d)
  else
    TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) (some a)
      (elim (a :: (l ++ Γ'.cons :: trList v)) (Γ'.bit0 :: l₁) c d)) =
  TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (unrev q₂)) (some a)
    (elim (a :: (l ++ Γ'.cons :: trList v)) (Γ'.bit0 :: l₁) c d)
Tactic: simp [trPosNum, PosNum.succ, e, h, show some Γ'.bit1 ≠ some Γ'.bit0 by decide,
      Option.getD, -natEnd]