-- 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))
pos₂ 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))
⊢ ∀ (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),
  (∀ {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))
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