awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
h₁ : k₁ ≠ k₂
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 (Λ'.move p k₁ k₂ q)) s S)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (fst, fst_1, snd).2.1
        (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (fst, fst_1, snd).2.2) k₂
          ((fst, fst_1, snd).1.reverseAux (S k₂))))
h :
  update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S k₁ Sk) k₂
      ((some a).getD default :: update (β := fun (k : K') ↦ List Γ') S k₁ Sk k₂) =
    update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ Sk) k₂ (a :: S k₂)
⊢ 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 (Λ'.move p k₁ k₂ q)) (some a)
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S k₁ Sk) k₂
        ((some a).getD default :: update (β := fun (k : K') ↦ List Γ') S k₁ Sk k₂)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) fst_1
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ snd) k₂
        ((a :: fst).reverseAux (S k₂))))
have h₂ : update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ snd) k₂ ((a :: fst).reverseAux (S k₂)) =
  update (β := fun (k : K') ↦ List Γ')
    (update (β := fun (a : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ Sk) k₂ (a :: S k₂)) k₁
      (fst, fst_1, snd).2.2)
    k₂
    ((fst, fst_1, snd).1.reverseAux
      (update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ Sk) k₂ (a :: S k₂) k₂))
Tactic: convert! @IH _ (update (update S k₁ Sk) k₂ (a :: S k₂)) _ using 2
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
h₁ : k₁ ≠ k₂
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 (Λ'.move p k₁ k₂ q)) s S)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (fst, fst_1, snd).2.1
        (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (fst, fst_1, snd).2.2) k₂
          ((fst, fst_1, snd).1.reverseAux (S k₂))))
h :
  update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S k₁ Sk) k₂
      ((some a).getD default :: update (β := fun (k : K') ↦ List Γ') S k₁ Sk k₂) =
    update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ Sk) k₂ (a :: S k₂)
h₂ :
  update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ snd) k₂
      ((a :: fst).reverseAux (S k₂)) =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ Sk) k₂ (a :: S k₂)) k₁
        (fst, fst_1, snd).2.2)
      k₂
      ((fst, fst_1, snd).1.reverseAux
        (update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ Sk) k₂ (a :: S k₂) k₂))
⊢ 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 (Λ'.move p k₁ k₂ q)) (some a)
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S k₁ Sk) k₂
        ((some a).getD default :: update (β := fun (k : K') ↦ List Γ') S k₁ Sk k₂)))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) fst_1
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ snd) k₂
        ((a :: fst).reverseAux (S k₂))))
have cons : splitAtPred p (update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ Sk) k₂ (a :: S k₂) k₁) =
  ((fst, fst_1, snd).1, (fst, fst_1, snd).2.1, (fst, fst_1, snd).2.2)
Tactic: convert! @IH _ (update (update S k₁ Sk) k₂ (a :: S k₂)) _ using 2
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
h₁ : k₁ ≠ k₂
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 (Λ'.move p k₁ k₂ q)) s S)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (fst, fst_1, snd).2.1
        (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (fst, fst_1, snd).2.2) k₂
          ((fst, fst_1, snd).1.reverseAux (S k₂))))
⊢ update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ snd) k₂
      ((a :: fst).reverseAux (S k₂)) =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ Sk) k₂ (a :: S k₂)) k₁
        (fst, fst_1, snd).2.2)
      k₂
      ((fst, fst_1, snd).1.reverseAux
        (update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ Sk) k₂ (a :: S k₂) k₂))
have h : update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ snd) k₂ (fst.reverse ++ a :: S k₂) =
  update (β := fun (k : K') ↦ List Γ')
    (update (β := fun (a : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ Sk) k₂ (a :: S k₂)) k₁ snd)
    k₂ (fst.reverse ++ a :: S k₂)
Tactic: simp [Function.update_of_ne, h₁, h₁.symm, e₃, List.reverseAux]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ : List Γ'
o : Option Γ'
L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ k₂
e : splitAtPred p (S k₁) = (L₁, o, L₂)
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.move p k₁ k₂ q)) s S)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) k₂ (L₁.reverseAux (S k₂))))
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 (Λ'.move p k₁ k₂ q)) s S)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) k₂
        (List.reverseAux [] (S k₂))))
Tactic: induction L₁ generalizing S s with
  | nil =>
    rw [(_ : [].reverseAux _ = _), Function.update_eq_self]
    swap
    · rw [Function.update_of_ne h₁.symm, List.reverseAux_nil]
    refine TransGen.head' rfl ?_
    simp only [tr_move, pop', TM2.stepAux]
    grind [splitAtPred.eq_def]
  | cons a L₁ IH =>
    refine TransGen.head rfl ?_
    rw [tr]; simp only [pop', Option.elim, TM2.stepAux, push']
    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 (update S k₁ Sk) k₂ (a :: S k₂)) _ using 2 <;>
      simp [Function.update_of_ne, h₁, h₁.symm, e₃, List.reverseAux]
    simp [Function.update_comm h₁.symm]
Cleared hypotheses: s, L₁, S, e
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ : List Γ'
o : Option Γ'
L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ k₂
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 (Λ'.move p k₁ k₂ q)) s S)
      (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o
        (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) k₂
          (List.reverseAux [] (S k₂))))
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.move p k₁ k₂ q)) s S)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) k₂ (L₁.reverseAux (S k₂))))
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 (Λ'.move p k₁ k₂ q)) s S)
        (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o
          (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) k₂
            (L₁.reverseAux (S k₂)))))
  {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 (Λ'.move p k₁ k₂ q)) s S)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) k₂
        ((a :: L₁).reverseAux (S k₂))))
Tactic: induction L₁ generalizing S s with
  | nil =>
    rw [(_ : [].reverseAux _ = _), Function.update_eq_self]
    swap
    · rw [Function.update_of_ne h₁.symm, List.reverseAux_nil]
    refine TransGen.head' rfl ?_
    simp only [tr_move, pop', TM2.stepAux]
    grind [splitAtPred.eq_def]
  | cons a L₁ IH =>
    refine TransGen.head rfl ?_
    rw [tr]; simp only [pop', Option.elim, TM2.stepAux, push']
    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 (update S k₁ Sk) k₂ (a :: S k₂)) _ using 2 <;>
      simp [Function.update_of_ne, h₁, h₁.symm, e₃, List.reverseAux]
    simp [Function.update_comm h₁.symm]
Cleared hypotheses: s, L₁, S, e
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ : List Γ'
o : Option Γ'
L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, o, L₂)
⊢ Reaches₁ (TM2.step (Γ := fun (x : K') ↦ Γ') tr) (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (move₂ p k₁ k₂ q)) s S)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (o.elim id List.cons L₂)) k₂
        (L₁ ++ S k₂)))
have refine : TransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
  (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr (Λ'.push k₁ id (Λ'.move (fun (x : Γ') ↦ false) rev k₂ q))) o
    (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev (L₁.reverseAux (S rev))))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none
    (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (o.elim id List.cons L₂)) k₂
      (L₁ ++ S k₂)))
Tactic: refine (move_ok h₁.1 e).trans (TransGen.head rfl ?_)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ : List Γ'
o : Option Γ'
L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (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') ↦ Γ') (tr (Λ'.push k₁ id (Λ'.move (fun (x : Γ') ↦ false) rev k₂ q))) o
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev (L₁.reverseAux (S rev))))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (o.elim id List.cons L₂)) k₂
        (L₁ ++ S k₂)))
have simp : 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.stepAux (Γ := fun (x : K') ↦ Γ') (tr (Λ'.push k₁ id (Λ'.move (fun (x : Γ') ↦ false) rev k₂ q))) o
    (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev (L₁.reverseAux (S rev))))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none
    (update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ') S k₁
        ((match (motive :=
            Option Γ' → ((a : List Γ') → List Γ') → (Γ' → (a : List Γ') → List Γ') → (a : List Γ') → List Γ') o, id,
            List.cons with
          | some x, x_1, f => f x
          | none, y, x => y)
          L₂))
      k₂ (L₁ ++ S k₂)))
Tactic: simp only [TM2.step, Option.mem_def, Option.elim]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ : List Γ'
o : Option Γ'
L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (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)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr (Λ'.push k₁ id (Λ'.move (fun (x : Γ') ↦ false) rev k₂ q))) o
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev (L₁.reverseAux (S rev))))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ') S k₁
          ((match (motive :=
              Option Γ' → ((a : List Γ') → List Γ') → (Γ' → (a : List Γ') → List Γ') → (a : List Γ') → List Γ') o, id,
              List.cons with
            | some x, x_1, f => f x
            | none, y, x => y)
            L₂))
        k₂ (L₁ ++ S k₂)))
have none : ∀ (e : splitAtPred p (S k₁) = (L₁, none, 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)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr (Λ'.push k₁ id (Λ'.move (fun (x : Γ') ↦ false) rev k₂ q))) none
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev (L₁.reverseAux (S rev))))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none
      (update (β := fun (k : K') ↦ List Γ')
        (update (β := fun (a : K') ↦ List Γ') S k₁
          ((match (motive :=
              Option Γ' → ((a : List Γ') → List Γ') → (Γ' → (a : List Γ') → List Γ') → (a : List Γ') → List Γ') none,
              id, List.cons with
            | some x, x_1, f => f x
            | none, y, x => y)
            L₂))
        k₂ (L₁ ++ S k₂)))
Tactic: cases o
Cleared hypotheses: o, e
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, 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)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ')
      (branch (Γ := fun (x : K') ↦ Γ') (fun (s : Option Γ') ↦ (id s).isSome)
        (push (Γ := fun (x : K') ↦ Γ') k₁ (fun (s : Option Γ') ↦ (id s).getD default)
          (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ Λ'.move (fun (x : Γ') ↦ false) rev k₂ q))
        (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ Λ'.move (fun (x : Γ') ↦ false) rev k₂ q))
      none
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev (L₁.reverseAux (S rev))))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ (id L₂)) k₂ (L₁ ++ S k₂)))
have none : 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 (Λ'.move (fun (x : Γ') ↦ false) rev k₂ q)) none
    (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev (L₁.reverseAux (S rev))))
  (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none
    (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) k₂ (L₁ ++ S k₂)))
Tactic: simp only [id, TM2.stepAux, Option.isSome, cond_true, cond_false]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, 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)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some (Λ'.move (fun (x : Γ') ↦ false) rev k₂ q)) none
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev (L₁.reverseAux (S rev))))
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) none
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) k₂ (L₁ ++ S k₂)))
have h : update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) k₂ (L₁ ++ S k₂) =
  update (β := fun (k : K') ↦ List Γ')
    (update (β := fun (a : K') ↦ List Γ')
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev (L₁.reverseAux (S rev)))
      rev [])
    k₂
    ((update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev (L₁.reverseAux (S rev))
          rev).reverseAux
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev (L₁.reverseAux (S rev))
        k₂))
Tactic: convert! move_ok h₁.2.1.symm (splitAtPred_false _) using 2
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) k₂ (L₁ ++ S k₂) =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ')
        (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev
          (L₁.reverseAux (S rev)))
        rev [])
      k₂
      ((update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev (L₁.reverseAux (S rev))
            rev).reverseAux
        (update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) rev (L₁.reverseAux (S rev))
          k₂))
have h : update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) k₂ (L₁ ++ S k₂) =
  update (β := fun (k : K') ↦ List Γ')
    (update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S rev []) k₁ L₂) k₂
    ((update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S rev (L₁.reverseAux (S rev))) k₁ L₂
          rev).reverseAux
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S rev (L₁.reverseAux (S rev))) k₁ L₂
        k₂))
Tactic: simp only [Function.update_comm h₁.1, Function.update_idem]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ update (β := fun (a : K') ↦ List Γ') S rev [] = S
have rw : update (β := fun (a : K') ↦ List Γ') S rev (S rev) = S
Tactic: rw [← h₂, Function.update_eq_self]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
rw : update (β := fun (a : K') ↦ List Γ') S rev (S rev) = S
⊢ update (β := fun (a : K') ↦ List Γ') S rev [] = S
have rw₁ : S = S
Tactic: rw [← h₂, Function.update_eq_self]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
s : Option Γ'
L₁ L₂ : List Γ'
S : K' → List Γ'
h₁ : k₁ ≠ rev ∧ k₂ ≠ rev ∧ k₁ ≠ k₂
h₂ : S rev = []
e : splitAtPred p (S k₁) = (L₁, none, L₂)
⊢ update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) k₂ (L₁ ++ S k₂) =
    update (β := fun (k : K') ↦ List Γ')
      (update (β := fun (a : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S rev []) k₁ L₂) k₂
      ((update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S rev (L₁.reverseAux (S rev))) k₁ L₂
            rev).reverseAux
        (update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S rev (L₁.reverseAux (S rev))) k₁ L₂
          k₂))
have h : update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) k₂ (L₁ ++ S k₂) =
  update (β := fun (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) k₂
    ((update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S rev (L₁.reverseAux (S rev))) k₁ L₂
          rev).reverseAux
      (update (β := fun (k : K') ↦ List Γ') (update (β := fun (k : K') ↦ List Γ') S rev (L₁.reverseAux (S rev))) k₁ L₂
        k₂))
Tactic: rw [show update S rev [] = S by rw [← h₂, Function.update_eq_self]]