awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'} (e : splitAtPred p (S k) = (L₁, o, L₂)),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e :
  (bif p a' then ([], some a', Sk)
    else
      match (motive := List Γ' × Option Γ' × List Γ' → List Γ' × Option Γ' × List Γ') splitAtPred p Sk with
      | (l₁, o, l₂) => (a' :: l₁, o, l₂)) =
    (a :: L₁, o, L₂)
e₁ : S k = a' :: Sk
e₂ : p a' = false
⊢ 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)
    (bif
        match (motive := Option Γ' → Bool → (Γ' → Bool) → Bool) (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (a' :: Sk).head?
        (update (β := fun (k : K') ↦ List Γ') S k (a' :: Sk).tail)
    else
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) (a' :: Sk).head?
        (update (β := fun (k : K') ↦ List Γ') S k (a' :: Sk).tail))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
have e₃ : (a' :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2) = (a :: L₁, o, L₂)
Tactic: simp only [e₂, cond] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'} (e : splitAtPred p (S k) = (L₁, o, L₂)),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e :
  (bif p a' then ([], some a', Sk)
    else
      match (motive := List Γ' × Option Γ' × List Γ' → List Γ' × Option Γ' × List Γ') splitAtPred p Sk with
      | (l₁, o, l₂) => (a' :: l₁, o, l₂)) =
    (a :: L₁, o, L₂)
e₁ : S k = a' :: Sk
e₂ : p a' = true
⊢ 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)
    (bif
        match (motive := Option Γ' → Bool → (Γ' → Bool) → Bool) (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (a' :: Sk).head?
        (update (β := fun (k : K') ↦ List Γ') S k (a' :: Sk).tail)
    else
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) (a' :: Sk).head?
        (update (β := fun (k : K') ↦ List Γ') S k (a' :: Sk).tail))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
have e₃ : ([], some a', Sk) = (a :: L₁, o, L₂)
Tactic: simp only [e₂, cond] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'} (e : splitAtPred p (S k) = (L₁, o, L₂)),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e₁ : S k = a' :: Sk
e₂ : p a' = false
e : (a' :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2) = (a :: L₁, o, L₂)
⊢ 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)
    (bif
        match (motive := Option Γ' → Bool → (Γ' → Bool) → Bool) (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (a' :: Sk).head?
        (update (β := fun (k : K') ↦ List Γ') S k (a' :: Sk).tail)
    else
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) (a' :: Sk).head?
        (update (β := fun (k : K') ↦ List Γ') S k (a' :: Sk).tail))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
have cons : ∀ (fst : List Γ') (fst_1 : Option Γ') (snd : List Γ') (e₃ : splitAtPred p Sk = (fst, fst_1, snd)),
  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)
    (bif
        match (motive := Option Γ' → Bool → (Γ' → Bool) → Bool) (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (a' :: Sk).head?
        (update (β := fun (k : K') ↦ List Γ') S k (a' :: Sk).tail)
    else
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) (a' :: Sk).head?
        (update (β := fun (k : K') ↦ List Γ') S k (a' :: Sk).tail))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
Tactic: rcases e₃ : splitAtPred p Sk with ⟨_, _, _⟩
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
a : Γ'
L₁ : List Γ'
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'} (e : splitAtPred p (S k) = (L₁, o, L₂)),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
s : Option Γ'
S : K' → List Γ'
a' : Γ'
Sk : List Γ'
e₁ : S k = a' :: Sk
e₂ : p a' = false
e : (a' :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2) = (a :: L₁, o, L₂)
fst : List Γ'
fst_1 : Option Γ'
snd : List Γ'
e₃ : splitAtPred p Sk = (fst, fst_1, snd)
⊢ 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)
    (bif
        match (motive := Option Γ' → Bool → (Γ' → Bool) → Bool) (a' :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (a' :: Sk).head?
        (update (β := fun (k : K') ↦ List Γ') S k (a' :: Sk).tail)
    else
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) (a' :: Sk).head?
        (update (β := fun (k : K') ↦ List Γ') S k (a' :: Sk).tail))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
have e₄ : (a' :: (fst, fst_1, snd).1, (fst, fst_1, snd).2.1, (fst, fst_1, snd).2.2) = (a :: L₁, o, L₂)
Tactic: rw [e₃] at e
Cleared hypotheses: e, e₃
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k : K'
q : Λ'
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst : List Γ'
fst_1 : Option Γ'
snd : List Γ'
e₃ : splitAtPred p Sk = (fst, fst_1, snd)
e₁ : S k = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'}
    (e : splitAtPred p (S k) = ((fst, fst_1, snd).1, (fst, fst_1, snd).2.1, (fst, fst_1, snd).2.2)),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (fst, fst_1, snd).2.1
        (update (β := fun (k : K') ↦ List Γ') S k (fst, fst_1, snd).2.2))
⊢ 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)
    (bif
        match (motive := Option Γ' → Bool → (Γ' → Bool) → Bool) (a :: Sk).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (a :: Sk).head?
        (update (β := fun (k : K') ↦ List Γ') S k (a :: Sk).tail)
    else
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) (a :: Sk).head?
        (update (β := fun (k : K') ↦ List Γ') S k (a :: Sk).tail))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (fst, fst_1, snd).2.1
      (update (β := fun (k : K') ↦ List Γ') S k (fst, fst_1, snd).2.2))
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 (Λ'.clear p k q)) (some a) (update (β := fun (k : K') ↦ List Γ') S k Sk))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) fst_1 (update (β := fun (k : K') ↦ List Γ') S k snd))
Tactic: simp only [List.head?_cons, e₂, List.tail_cons, cond_false]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k : K'
q : Λ'
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst : List Γ'
fst_1 : Option Γ'
snd : List Γ'
e₃ : splitAtPred p Sk = (fst, fst_1, snd)
e₁ : S k = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'}
    (e : splitAtPred p (S k) = ((fst, fst_1, snd).1, (fst, fst_1, snd).2.1, (fst, fst_1, snd).2.2)),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (fst, fst_1, snd).2.1
        (update (β := fun (k : K') ↦ List Γ') S k (fst, fst_1, snd).2.2))
⊢ 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 (Λ'.clear p k q)) (some a) (update (β := fun (k : K') ↦ List Γ') S k Sk))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) fst_1 (update (β := fun (k : K') ↦ List Γ') S k snd))
have h : update (β := fun (k : K') ↦ List Γ') S k snd =
  update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k Sk) k (fst, fst_1, snd).2.2
Tactic: convert! @IH _ (update S k Sk) _ using 2
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k : K'
q : Λ'
a : Γ'
s : Option Γ'
S : K' → List Γ'
Sk fst : List Γ'
fst_1 : Option Γ'
snd : List Γ'
e₃ : splitAtPred p Sk = (fst, fst_1, snd)
e₁ : S k = a :: Sk
e₂ : p a = false
IH :
  ∀ {s : Option Γ'} {S : K' → List Γ'}
    (e : splitAtPred p (S k) = ((fst, fst_1, snd).1, (fst, fst_1, snd).2.1, (fst, fst_1, snd).2.2)),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (fst, fst_1, snd).2.1
        (update (β := fun (k : K') ↦ List Γ') S k (fst, fst_1, snd).2.2))
h :
  update (β := fun (k : K') ↦ List Γ') S k snd =
    update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k Sk) k (fst, fst_1, snd).2.2
⊢ 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 (Λ'.clear p k q)) (some a) (update (β := fun (k : K') ↦ List Γ') S k Sk))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) fst_1 (update (β := fun (k : K') ↦ List Γ') S k snd))
have cons : splitAtPred p (update (β := fun (a : K') ↦ List Γ') S k Sk k) =
  ((fst, fst_1, snd).1, (fst, fst_1, snd).2.1, (fst, fst_1, snd).2.2)
Tactic: convert! @IH _ (update S k Sk) _ using 2
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k : K'
q : Λ'
s : Option Γ'
L₁ : List Γ'
o : Option Γ'
L₂ : List Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = (L₁, o, L₂)
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
have nil : ∀ {s : Option Γ'} {S : K' → List Γ'} (e : splitAtPred p (S k) = ([], o, L₂)),
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
Tactic: induction L₁ generalizing S s with
  | nil =>
    refine TransGen.head' rfl ?_
    rw [tr]; simp only [pop', TM2.step, Option.mem_def, TM2.stepAux, Option.elim]
    revert e; rcases S k with - | ⟨a, Sk⟩ <;> intro e
    · cases e
      rfl
    simp only [splitAtPred, List.head?, List.tail_cons] at e ⊢
    revert e; cases p a <;> intro e <;>
      simp only [cond_false, cond_true, Prod.mk.injEq, true_and, false_and, reduceCtorEq] at e ⊢
    rcases e with ⟨e₁, e₂⟩
    rw [e₁, e₂]
  | cons a L₁ IH =>
    refine TransGen.head rfl ?_
    rw [tr]; simp only [pop', TM2.step, Option.mem_def, TM2.stepAux, Option.elim]
    rcases e₁ : S k with - | ⟨a', Sk⟩ <;> rw [e₁, splitAtPred] at e
    · cases e
    cases e₂ : p a' <;> simp only [e₂, cond] at e
    swap
    · cases e
    rcases e₃ : splitAtPred p Sk with ⟨_, _, _⟩
    rw [e₃] at e
    cases e
    simp only [List.head?_cons, e₂, List.tail_cons, cond_false]
    convert! @IH _ (update S k Sk) _ using 2 <;> simp [e₃]
Cleared hypotheses: s, L₁, S, e
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k : K'
q : Λ'
s : Option Γ'
L₁ : List Γ'
o : Option Γ'
L₂ : List Γ'
S : K' → List Γ'
e : splitAtPred p (S k) = (L₁, o, L₂)
nil :
  ∀ {s : Option Γ'} {S : K' → List Γ'} (e : splitAtPred p (S k) = ([], o, L₂)),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
have cons : ∀ (a : Γ') (L₁ : List Γ')
  (IH :
    ∀ {s : Option Γ'} {S : K' → List Γ'} (e : splitAtPred p (S k) = (L₁, o, L₂)),
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂)))
  {s : Option Γ'} {S : K' → List Γ'} (e : splitAtPred p (S k) = (a :: L₁, o, L₂)),
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) s S)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
Tactic: induction L₁ generalizing S s with
  | nil =>
    refine TransGen.head' rfl ?_
    rw [tr]; simp only [pop', TM2.step, Option.mem_def, TM2.stepAux, Option.elim]
    revert e; rcases S k with - | ⟨a, Sk⟩ <;> intro e
    · cases e
      rfl
    simp only [splitAtPred, List.head?, List.tail_cons] at e ⊢
    revert e; cases p a <;> intro e <;>
      simp only [cond_false, cond_true, Prod.mk.injEq, true_and, false_and, reduceCtorEq] at e ⊢
    rcases e with ⟨e₁, e₂⟩
    rw [e₁, e₂]
  | cons a L₁ IH =>
    refine TransGen.head rfl ?_
    rw [tr]; simp only [pop', TM2.step, Option.mem_def, TM2.stepAux, Option.elim]
    rcases e₁ : S k with - | ⟨a', Sk⟩ <;> rw [e₁, splitAtPred] at e
    · cases e
    cases e₂ : p a' <;> simp only [e₂, cond] at e
    swap
    · cases e
    rcases e₃ : splitAtPred p Sk with ⟨_, _, _⟩
    rw [e₃] at e
    cases e
    simp only [List.head?_cons, e₂, List.tail_cons, cond_false]
    convert! @IH _ (update S k Sk) _ using 2 <;> simp [e₃]
Cleared hypotheses: s, L₁, S, e
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
c : List Γ'
s : Option Γ'
a d : List Γ'
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (List.reverseAux [] a) [] c (List.reverseAux [] d)))
have nil : TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (List.reverseAux [] a) [] c (List.reverseAux [] d)) ∈
  TM2.step (Γ := fun (x : K') ↦ Γ') tr (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a [] c d))
Tactic: refine TransGen.single ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
c : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a b c d))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (b.reverseAux a) [] c (b.reverseAux d)))
s : Option Γ'
a d : List Γ'
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a (x :: b) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim ((x :: b).reverseAux a) [] c ((x :: b).reverseAux 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.copy) s (elim a (x :: b) c d))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim ((x :: b).reverseAux a) [] c ((x :: b).reverseAux d)))
Tactic: refine TransGen.head rfl ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
c : List Γ'
x : Γ'
b : List Γ'
IH :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a b c d))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (b.reverseAux a) [] c (b.reverseAux d)))
s : Option Γ'
a d : List Γ'
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
      (pop' rev
        (branch (Γ := fun (x : K') ↦ Γ') Option.isSome
          (push' main (push' stack (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q.copy)))
          (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q)))
      s (elim a (x :: b) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim ((x :: b).reverseAux a) [] c ((x :: b).reverseAux d)))
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 q.copy) (some x)
    (elim ((some x).getD default :: a) b c ((some x).getD default :: d)))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (b.reverseAux (x :: a)) [] c (b.reverseAux (x :: d))))
Tactic: simp only [TM2.step, Option.mem_def, TM2.stepAux, elim_rev, List.head?_cons, Option.isSome_some,
      List.tail_cons, elim_update_rev, elim_main, elim_update_main,
      elim_stack, elim_update_stack, cond_true, List.reverseAux_cons, pop', push']
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
a b c d : List Γ'
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a b c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (b.reverseAux a) [] c (b.reverseAux d)))
have nil : ∀ (s : Option Γ') (a d : List Γ'),
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a [] c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (List.reverseAux [] a) [] c (List.reverseAux [] d)))
Tactic: induction b generalizing a d s with
  | nil =>
    refine TransGen.single ?_
    simp
  | cons x b IH =>
    refine TransGen.head rfl ?_
    rw [tr]
    simp only [TM2.step, Option.mem_def, TM2.stepAux, elim_rev, List.head?_cons, Option.isSome_some,
      List.tail_cons, elim_update_rev, elim_main, elim_update_main,
      elim_stack, elim_update_stack, cond_true, List.reverseAux_cons, pop', push']
    exact IH _ _ _
Cleared hypotheses: s, a, b, d
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
q : Λ'
s : Option Γ'
a b c d : List Γ'
nil :
  ∀ (s : Option Γ') (a d : List Γ'),
    Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a [] c d))
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (List.reverseAux [] a) [] c (List.reverseAux [] d)))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a b c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (b.reverseAux a) [] c (b.reverseAux d)))
have cons : ∀ (x : Γ') (b : List Γ')
  (IH :
    ∀ (s : Option Γ') (a d : List Γ'),
      Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a b c d))
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim (b.reverseAux a) [] c (b.reverseAux d))))
  (s : Option Γ') (a d : List Γ'),
  Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q.copy) s (elim a (x :: b) c d))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none (elim ((x :: b).reverseAux a) [] c ((x :: b).reverseAux d)))
Tactic: induction b generalizing a d s with
  | nil =>
    refine TransGen.single ?_
    simp
  | cons x b IH =>
    refine TransGen.head rfl ?_
    rw [tr]
    simp only [TM2.step, Option.mem_def, TM2.stepAux, elim_rev, List.head?_cons, Option.isSome_some,
      List.tail_cons, elim_update_rev, elim_main, elim_update_main,
      elim_stack, elim_update_stack, cond_true, List.reverseAux_cons, pop', push']
    exact IH _ _ _
Cleared hypotheses: s, a, b, d