-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
s : Option Γ'
c d : List Γ'
v : List ℕ
n : ℕ
a : PosNum
cons cons₁ :
  ∀ (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))
cons₂ cons₃ :
  ∀ (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))
cons₄ cons₅ :
  ∀ (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))
⊢ ∀ (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:
induction a generalizing s with intro l₁
  | one =>
    refine ⟨Γ'.bit1::l₁, [], some Γ'.cons, rfl, TransGen.head rfl (TransGen.single ?_)⟩
    simp [trPosNum, show PosNum.one.succ = PosNum.one.bit0 from rfl]
  | bit1 m IH =>
    obtain ⟨l₁', l₂', s', e, h⟩ := IH (some Γ'.bit0) (Γ'.bit1 :: l₁)
    refine ⟨l₁', l₂', s', e, TransGen.head ?_ h⟩
    simp
    rfl
  | bit0 m IH =>
    obtain ⟨a, l, e, h⟩ : ∃ a l, (trPosNum m = a::l) ∧ natEnd a = false := by
      cases m <;> refine ⟨_, _, rfl, rfl⟩
    refine ⟨Γ'.bit0 :: l₁, _, some a, rfl, TransGen.single ?_⟩
    simp [trPosNum, PosNum.succ, e, h, show some Γ'.bit1 ≠ some Γ'.bit0 by decide,
      Option.getD, -natEnd]
    rfl

Premises used: Option.getD, Turing.PartrecToTM2.trPosNum, Turing.PartrecToTM2.natEnd, PosNum.succ, Bool.false, rfl