awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
⊢ ∀
    (e :
      (bif p a then ([], some a, Sk) else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
        ([], o, L₂)),
    ReflTransGen
      (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 p a then TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (some a) (update (β := fun (k : K') ↦ List Γ') S k Sk)
      else
        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) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
have nil : ∀
  (e :
    (bif false then ([], some a, Sk) else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
      ([], o, L₂)),
  ReflTransGen
    (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 false then TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (some a) (update (β := fun (k : K') ↦ List Γ') S k Sk)
    else
      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) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
Tactic: cases p a
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
nil :
  ∀
    (e :
      (bif false then ([], some a, Sk)
        else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
        ([], o, L₂)),
    ReflTransGen
      (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 false then
        TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (some a) (update (β := fun (k : K') ↦ List Γ') S k Sk)
      else
        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) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
⊢ ∀
    (e :
      (bif p a then ([], some a, Sk) else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
        ([], o, L₂)),
    ReflTransGen
      (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 p a then TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (some a) (update (β := fun (k : K') ↦ List Γ') S k Sk)
      else
        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) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
have nil₁ : ∀
  (e :
    (bif true then ([], some a, Sk) else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
      ([], o, L₂)),
  ReflTransGen
    (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 true then TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (some a) (update (β := fun (k : K') ↦ List Γ') S k Sk)
    else
      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) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
Tactic: cases p a
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
e :
  (bif true then ([], some a, Sk) else (a :: (splitAtPred p Sk).1, (splitAtPred p Sk).2.1, (splitAtPred p Sk).2.2)) =
    ([], o, L₂)
⊢ ReflTransGen
    (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 true then TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (some a) (update (β := fun (k : K') ↦ List Γ') S k Sk)
    else
      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) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
have e₁ : some a = o ∧ Sk = L₂
Tactic: simp only [cond_false, cond_true, Prod.mk.injEq, true_and, false_and, reduceCtorEq] 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 Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
e : some a = o ∧ Sk = L₂
⊢ ReflTransGen
    (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) (some a) (update (β := fun (k : K') ↦ List Γ') S k Sk))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
have e₁ : some a = o
Tactic: rcases e with ⟨e₁, e₂⟩
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
Goal:
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
e : some a = o ∧ Sk = L₂
e₁ : some a = o
⊢ ReflTransGen
    (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) (some a) (update (β := fun (k : K') ↦ List Γ') S k Sk))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
have e₂ : Sk = L₂
Tactic: rcases e with ⟨e₁, e₂⟩
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
e₁ : some a = o
e₂ : Sk = L₂
⊢ ReflTransGen
    (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) (some a) (update (β := fun (k : K') ↦ List Γ') S k Sk))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
have nil : ReflTransGen
  (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) o (update (β := fun (k : K') ↦ List Γ') S k Sk))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
Tactic: rw [e₁, e₂]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
s : Option Γ'
S : K' → List Γ'
a : Γ'
Sk : List Γ'
e₁ : some a = o
e₂ : Sk = L₂
nil :
  ReflTransGen
    (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) o (update (β := fun (k : K') ↦ List Γ') S k Sk))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
⊢ ReflTransGen
    (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) (some a) (update (β := fun (k : K') ↦ List Γ') S k Sk))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
have nil₁ : ReflTransGen
  (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) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
Tactic: rw [e₁, 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 Γ'
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₂))
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 (Λ'.clear p k q)) s S)
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
Tactic: refine TransGen.head rfl ?_
-- 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 Γ'
e : splitAtPred p (S k) = (a :: L₁, o, L₂)
⊢ TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
      (pop' k
        (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ s.elim true p)
          (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ q)
          (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ Λ'.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 : 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) (S k).head?, true, p with
      | some x, x_1, f => f x
      | none, y, x => y then
    TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (S k).head? (update (β := fun (k : K') ↦ List Γ') S k (S k).tail)
  else
    TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) (S k).head?
      (update (β := fun (k : K') ↦ List Γ') S k (S k).tail))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
Tactic: simp only [pop', TM2.step, Option.mem_def, TM2.stepAux, Option.elim]
-- 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 Γ'
e : splitAtPred p (S k) = (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) (S k).head?, true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (S k).head? (update (β := fun (k : K') ↦ List Γ') S k (S k).tail)
    else
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) (S k).head?
        (update (β := fun (k : K') ↦ List Γ') S k (S k).tail))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
have cons : ∀ (e₁ : S k = []),
  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) List.head? [], true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (List.head? [])
        (update (β := fun (k : K') ↦ List Γ') S k (List.tail []))
    else
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) (List.head? [])
        (update (β := fun (k : K') ↦ List Γ') S k (List.tail [])))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
Tactic: rcases e₁ : S k with - | ⟨a', Sk⟩
-- 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 Γ'
e : splitAtPred p (S k) = (a :: L₁, o, L₂)
e₁ : S k = []
⊢ 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) List.head? [], true, p with
        | some x, x_1, f => f x
        | none, y, x => y then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (List.head? [])
        (update (β := fun (k : K') ↦ List Γ') S k (List.tail []))
    else
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.clear p k q)) (List.head? [])
        (update (β := fun (k : K') ↦ List Γ') S k (List.tail [])))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (k : K') ↦ List Γ') S k L₂))
have e₂ : ([], none, []) = (a :: L₁, o, L₂)
Tactic: rw [e₁, splitAtPred] at e
Cleared hypotheses: e, 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 Γ'
e : splitAtPred p (S k) = (a :: L₁, o, L₂)
a' : Γ'
Sk : List Γ'
e₁ : S k = a' :: Sk
⊢ 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₂ : (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₂)
Tactic: rw [e₁, splitAtPred] at e
Cleared hypotheses: e, 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 :
  (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
⊢ 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 : ∀ (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₂))
Tactic: cases e₂ : p a'