awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
α : Type u_1
p : α → Bool
a : α
L l₁ : List α
o : Option α
l₂ : List α
h₁ : ∀ x ∈ l₁, p x = false
h₂ : Option.elim' (a :: L = l₁ ∧ l₂ = []) (fun (a_1 : α) ↦ p a_1 = true ∧ a :: L = l₁ ++ a_1 :: l₂) o
⊢ ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun (a : α) ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)

Tactic:
have IH := splitAtPred_eq p L
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
α : Type u_1
p : α → Bool
a : α
L l₁ : List α
o : Option α
l₂ : List α
h₁ : ∀ x ∈ l₁, p x = false
h₂ : Option.elim' (a :: L = l₁ ∧ l₂ = []) (fun (a_1 : α) ↦ p a_1 = true ∧ a :: L = l₁ ++ a_1 :: l₂) o
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun (a : α) ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
none :
  ∀ (h₂ : Option.elim' (a :: L = l₁ ∧ l₂ = []) (fun (a_1 : α) ↦ p a_1 = true ∧ a :: L = l₁ ++ a_1 :: l₂) Option.none),
    (bif p a then ([], Option.some a, L)
      else
        match (motive := List α × Option α × List α → List α × Option α × List α) splitAtPred p L with
        | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
      (l₁, Option.none, l₂)
some :
  ∀ (o : α)
    (h₂ :
      Option.elim' (a :: L = l₁ ∧ l₂ = []) (fun (a_1 : α) ↦ p a_1 = true ∧ a :: L = l₁ ++ a_1 :: l₂) (Option.some o)),
    (bif p a then ([], Option.some a, L)
      else
        match (motive := List α × Option α × List α → List α × Option α × List α) splitAtPred p L with
        | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
      (l₁, Option.some o, l₂)
⊢ (bif p a then ([], Option.some a, L)
    else
      match (motive := List α × Option α × List α → List α × Option α × List α) splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    (l₁, o, l₂)

Tactic:
rcases o with - | o
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
α : Type u_1
p : α → Bool
a : α
L l₁ l₂ : List α
h₁ : ∀ x ∈ l₁, p x = false
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun (a : α) ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
h₂ : Option.elim' (a :: L = l₁ ∧ l₂ = []) (fun (a_1 : α) ↦ p a_1 = true ∧ a :: L = l₁ ++ a_1 :: l₂) Option.none
none :
  ∀ (h₁ : ∀ (x : α), Membership.mem (γ := List α) [] x → p x = false)
    (h₂ : Option.elim' (a :: L = [] ∧ l₂ = []) (fun (a_1 : α) ↦ p a_1 = true ∧ a :: L = [] ++ a_1 :: l₂) Option.none),
    Eq (α := List α × Option α × List α)
      (bif p a then ([], some a, L)
      else
        match (motive := List α × Option α × List α → List α × Option α × List α) splitAtPred p L with
        | (l₁, o, l₂) => (a :: l₁, o, l₂))
      ([], Option.none, l₂)
none₁ :
  ∀ (a' : α) (l₁ : List α) (h₁ : ∀ x ∈ a' :: l₁, p x = false)
    (h₂ :
      Option.elim' (a :: L = a' :: l₁ ∧ l₂ = []) (fun (a_1 : α) ↦ p a_1 = true ∧ a :: L = a' :: l₁ ++ a_1 :: l₂)
        Option.none),
    (bif p a then ([], some a, L)
      else
        match (motive := List α × Option α × List α → List α × Option α × List α) splitAtPred p L with
        | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
      (a' :: l₁, Option.none, l₂)
⊢ (bif p a then ([], some a, L)
    else
      match (motive := List α × Option α × List α → List α × Option α × List α) splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    (l₁, Option.none, l₂)

Tactic:
rcases l₁ with - | ⟨a', l₁⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
α : Type u_1
p : α → Bool
a : α
L l₂ : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun (a : α) ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
h₁ : ∀ (x : α), Membership.mem (γ := List α) [] x → p x = false
h₂ : Option.elim' (a :: L = [] ∧ l₂ = []) (fun (a_1 : α) ↦ p a_1 = true ∧ a :: L = [] ++ a_1 :: l₂) none
⊢ Eq (α := List α × Option α × List α)
    (bif p a then ([], some a, L)
    else
      match (motive := List α × Option α × List α → List α × Option α × List α) splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂))
    ([], none, l₂)

Tactic:
rcases h₂ with ⟨⟨⟩, rfl⟩

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
α : Type u_1
p : α → Bool
a : α
L l₂ : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun (a : α) ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
a' : α
l₁ : List α
h₁ : ∀ x ∈ a' :: l₁, p x = false
h₂ :
  Option.elim' (a :: L = a' :: l₁ ∧ l₂ = []) (fun (a_1 : α) ↦ p a_1 = true ∧ a :: L = a' :: l₁ ++ a_1 :: l₂) Option.none
none :
  ∀ (h₁ : ∀ x ∈ a :: L, p x = false),
    (bif p a then ([], some a, L)
      else
        match (motive := List α × Option α × List α → List α × Option α × List α) splitAtPred p L with
        | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
      (a :: L, Option.none, [])
⊢ (bif p a then ([], some a, L)
    else
      match (motive := List α × Option α × List α → List α × Option α × List α) splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    (a' :: l₁, Option.none, l₂)

Tactic:
rcases h₂ with ⟨⟨⟩, rfl⟩

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
α : Type u_1
p : α → Bool
a : α
L : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun (a : α) ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
h₁ : ∀ x ∈ a :: L, p x = false
rw : ∀ x ∈ L, p x = false
⊢ (bif p a then ([], some a, L)
    else
      match (motive := List α × Option α × List α → List α × Option α × List α) splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    (a :: L, none, [])

Tactic:
rw [h₁ a (List.Mem.head _), cond, IH L none [] _ ⟨rfl, rfl⟩]

Premises used: cond, Option.none, And.intro, List.Mem.head, rfl, List.nil
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
α : Type u_1
p : α → Bool
a : α
L : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun (a : α) ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
h₁ : ∀ x ∈ a :: L, p x = false
⊢ ∀ x ∈ L, p x = false

Tactic:
fun x h => h₁ x (List.Mem.tail _ h)

Premises used: List.Mem.tail
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
α : Type u_1
p : α → Bool
a : α
L : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun (a : α) ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
h₁ : ∀ x ∈ a :: L, p x = false
⊢ ∀ x ∈ L, p x = false

Tactic:
exact fun x h => h₁ x (List.Mem.tail _ h)

Premises used: List.Mem.tail
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
α : Type u_1
p : α → Bool
a : α
L l₁ l₂ : List α
h₁ : ∀ x ∈ l₁, p x = false
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun (a : α) ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
o : α
h₂ : Option.elim' (a :: L = l₁ ∧ l₂ = []) (fun (a_1 : α) ↦ p a_1 = true ∧ a :: L = l₁ ++ a_1 :: l₂) (Option.some o)
some :
  ∀ (h₁ : ∀ (x : α), Membership.mem (γ := List α) [] x → p x = false)
    (h₂ :
      Option.elim' (a :: L = [] ∧ l₂ = []) (fun (a_1 : α) ↦ p a_1 = true ∧ a :: L = [] ++ a_1 :: l₂) (Option.some o)),
    Eq (α := List α × Option α × List α)
      (bif p a then ([], Option.some a, L)
      else
        match (motive := List α × Option α × List α → List α × Option α × List α) splitAtPred p L with
        | (l₁, o, l₂) => (a :: l₁, o, l₂))
      ([], Option.some o, l₂)
some₁ :
  ∀ (a' : α) (l₁ : List α) (h₁ : ∀ x ∈ a' :: l₁, p x = false)
    (h₂ :
      Option.elim' (a :: L = a' :: l₁ ∧ l₂ = []) (fun (a_1 : α) ↦ p a_1 = true ∧ a :: L = a' :: l₁ ++ a_1 :: l₂)
        (Option.some o)),
    (bif p a then ([], Option.some a, L)
      else
        match (motive := List α × Option α × List α → List α × Option α × List α) splitAtPred p L with
        | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
      (a' :: l₁, Option.some o, l₂)
⊢ (bif p a then ([], Option.some a, L)
    else
      match (motive := List α × Option α × List α → List α × Option α × List α) splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    (l₁, Option.some o, l₂)

Tactic:
rcases l₁ with - | ⟨a', l₁⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
α : Type u_1
p : α → Bool
a : α
L l₂ : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun (a : α) ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
o : α
h₁ : ∀ (x : α), Membership.mem (γ := List α) [] x → p x = false
h₂ : Option.elim' (a :: L = [] ∧ l₂ = []) (fun (a_1 : α) ↦ p a_1 = true ∧ a :: L = [] ++ a_1 :: l₂) (Option.some o)
some :
  ∀ (h₂ : p a = true),
    Eq (α := List α × Option α × List α)
      (bif p a then ([], Option.some a, L)
      else
        match (motive := List α × Option α × List α → List α × Option α × List α) splitAtPred p L with
        | (l₁, o, l₂) => (a :: l₁, o, l₂))
      ([], Option.some a, L)
⊢ Eq (α := List α × Option α × List α)
    (bif p a then ([], Option.some a, L)
    else
      match (motive := List α × Option α × List α → List α × Option α × List α) splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂))
    ([], Option.some o, l₂)

Tactic:
rcases h₂ with ⟨h₂, ⟨⟩⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
α : Type u_1
p : α → Bool
a : α
L l₂ : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun (a : α) ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
o a' : α
l₁ : List α
h₁ : ∀ x ∈ a' :: l₁, p x = false
h₂ :
  Option.elim' (a :: L = a' :: l₁ ∧ l₂ = []) (fun (a_1 : α) ↦ p a_1 = true ∧ a :: L = a' :: l₁ ++ a_1 :: l₂)
    (Option.some o)
some :
  ∀ (h₂ : p o = true) (h₁ : ∀ x ∈ a :: l₁, p x = false)
    (IH :
      ∀ (l₁_1 : List α) (o_1 : Option α) (l₂_1 : List α),
        (∀ x ∈ l₁_1, p x = false) →
          Option.elim' (l₁.append (o :: l₂) = l₁_1 ∧ l₂_1 = [])
              (fun (a : α) ↦ p a = true ∧ l₁.append (o :: l₂) = l₁_1 ++ a :: l₂_1) o_1 →
            splitAtPred p (l₁.append (o :: l₂)) = (l₁_1, o_1, l₂_1)),
    (bif p a then ([], Option.some a, l₁.append (o :: l₂))
      else
        match (motive := List α × Option α × List α → List α × Option α × List α)
          splitAtPred p (l₁.append (o :: l₂)) with
        | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
      (a :: l₁, Option.some o, l₂)
⊢ (bif p a then ([], Option.some a, L)
    else
      match (motive := List α × Option α × List α → List α × Option α × List α) splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    (a' :: l₁, Option.some o, l₂)

Tactic:
rcases h₂ with ⟨h₂, ⟨⟩⟩
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
α : Type u_1
p : α → Bool
a : α
L : List α
IH :
  ∀ (l₁ : List α) (o : Option α) (l₂ : List α),
    (∀ x ∈ l₁, p x = false) →
      Option.elim' (L = l₁ ∧ l₂ = []) (fun (a : α) ↦ p a = true ∧ L = l₁ ++ a :: l₂) o → splitAtPred p L = (l₁, o, l₂)
h₁ : ∀ (x : α), Membership.mem (γ := List α) [] x → p x = false
h₂ : p a = true
some :
  Eq (α := List α × Option α × List α)
    (bif true then ([], Option.some a, L)
    else
      match (motive := List α × Option α × List α → List α × Option α × List α) splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂))
    ([], Option.some a, L)
some₁ some₂ : Eq (α := List α × Option α × List α) ([], Option.some a, L) ([], Option.some a, L)
⊢ Eq (α := List α × Option α × List α)
    (bif p a then ([], Option.some a, L)
    else
      match (motive := List α × Option α × List α → List α × Option α × List α) splitAtPred p L with
      | (l₁, o, l₂) => (a :: l₁, o, l₂))
    ([], Option.some a, L)

Tactic:
rw [h₂, cond]

Premises used: cond
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
α : Type u_1
p : α → Bool
a : α
l₂ : List α
o : α
l₁ : List α
h₂ : p o = true
h₁ : ∀ x ∈ a :: l₁, p x = false
IH :
  ∀ (l₁_1 : List α) (o_1 : Option α) (l₂_1 : List α),
    (∀ x ∈ l₁_1, p x = false) →
      Option.elim' (l₁.append (o :: l₂) = l₁_1 ∧ l₂_1 = [])
          (fun (a : α) ↦ p a = true ∧ l₁.append (o :: l₂) = l₁_1 ++ a :: l₂_1) o_1 →
        splitAtPred p (l₁.append (o :: l₂)) = (l₁_1, o_1, l₂_1)
rw : ∀ x ∈ l₁, p x = false
rw₁ : l₁.append (o :: l₂) = l₁ ++ o :: l₂
⊢ (bif p a then ([], some a, l₁.append (o :: l₂))
    else
      match (motive := List α × Option α × List α → List α × Option α × List α) splitAtPred p (l₁.append (o :: l₂)) with
      | (l₁, o, l₂) => (a :: l₁, o, l₂)) =
    (a :: l₁, some o, l₂)

Tactic:
rw [h₁ a (List.Mem.head _), cond, IH l₁ (some o) l₂ _ ⟨h₂, _⟩]

Premises used: cond, Option.some, And.intro, List.Mem.head
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
α : Type u_1
p : α → Bool
a : α
l₂ : List α
o : α
l₁ : List α
h₂ : p o = true
h₁ : ∀ x ∈ a :: l₁, p x = false
IH :
  ∀ (l₁_1 : List α) (o_1 : Option α) (l₂_1 : List α),
    (∀ x ∈ l₁_1, p x = false) →
      Option.elim' (l₁.append (o :: l₂) = l₁_1 ∧ l₂_1 = [])
          (fun (a : α) ↦ p a = true ∧ l₁.append (o :: l₂) = l₁_1 ++ a :: l₂_1) o_1 →
        splitAtPred p (l₁.append (o :: l₂)) = (l₁_1, o_1, l₂_1)
⊢ l₁.append (o :: l₂) = l₁ ++ o :: l₂

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
α : Type u_1
p : α → Bool
a : α
l₂ : List α
o : α
l₁ : List α
h₂ : p o = true
h₁ : ∀ x ∈ a :: l₁, p x = false
IH :
  ∀ (l₁_1 : List α) (o_1 : Option α) (l₂_1 : List α),
    (∀ x ∈ l₁_1, p x = false) →
      Option.elim' (l₁.append (o :: l₂) = l₁_1 ∧ l₂_1 = [])
          (fun (a : α) ↦ p a = true ∧ l₁.append (o :: l₂) = l₁_1 ++ a :: l₂_1) o_1 →
        splitAtPred p (l₁.append (o :: l₂)) = (l₁_1, o_1, l₂_1)
⊢ l₁.append (o :: l₂) = l₁ ++ o :: l₂

Tactic:
try rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
α : Type u_1
p : α → Bool
a : α
l₂ : List α
o : α
l₁ : List α
h₂ : p o = true
h₁ : ∀ x ∈ a :: l₁, p x = false
IH :
  ∀ (l₁_1 : List α) (o_1 : Option α) (l₂_1 : List α),
    (∀ x ∈ l₁_1, p x = false) →
      Option.elim' (l₁.append (o :: l₂) = l₁_1 ∧ l₂_1 = [])
          (fun (a : α) ↦ p a = true ∧ l₁.append (o :: l₂) = l₁_1 ++ a :: l₂_1) o_1 →
        splitAtPred p (l₁.append (o :: l₂)) = (l₁_1, o_1, l₂_1)
⊢ ∀ x ∈ l₁, p x = false

Tactic:
fun x h => h₁ x (List.Mem.tail _ h)

Premises used: List.Mem.tail
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
α : Type u_1
p : α → Bool
a : α
l₂ : List α
o : α
l₁ : List α
h₂ : p o = true
h₁ : ∀ x ∈ a :: l₁, p x = false
IH :
  ∀ (l₁_1 : List α) (o_1 : Option α) (l₂_1 : List α),
    (∀ x ∈ l₁_1, p x = false) →
      Option.elim' (l₁.append (o :: l₂) = l₁_1 ∧ l₂_1 = [])
          (fun (a : α) ↦ p a = true ∧ l₁.append (o :: l₂) = l₁_1 ++ a :: l₂_1) o_1 →
        splitAtPred p (l₁.append (o :: l₂)) = (l₁_1, o_1, l₂_1)
⊢ ∀ x ∈ l₁, p x = false

Tactic:
exact fun x h => h₁ x (List.Mem.tail _ h)

Premises used: List.Mem.tail
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
α : Type u_1
L : List α
⊢ splitAtPred (fun (x : α) ↦ false) L = (L, none, [])

Tactic:
splitAtPred_eq _ _ _ _ _ (fun _ _ => rfl) ⟨rfl, rfl⟩

Premises used: Turing.PartrecToTM2.splitAtPred_eq, And.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k₁) = ([], o, L₂)
nil :
  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 (a : K') ↦ List Γ') S k₁ L₂))
rw : List.reverseAux [] (S k₂) = update (β := fun (a : K') ↦ List Γ') S k₁ L₂ 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₂
        (List.reverseAux [] (S k₂))))

Tactic:
rw [(_ : [].reverseAux _ = _), Function.update_eq_self]

Premises used: Function.update_eq_self
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k₁) = ([], o, L₂)
rw : List.reverseAux [] (S k₂) = S k₂
rw₁ rw₂ : S k₂ = S k₂
⊢ List.reverseAux [] (S k₂) = update (β := fun (a : K') ↦ List Γ') S k₁ L₂ k₂

Tactic:
rw [Function.update_of_ne h₁.symm, List.reverseAux_nil]

Premises used: List.reverseAux_nil, Ne.symm, Function.update_of_ne
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
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 (a : K') ↦ List Γ') S k₁ L₂))

Tactic:
TransGen.head' rfl ?_

Premises used: Relation.TransGen.head', StateTransition.Reaches₁, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k₁) = ([], o, L₂)
nil :
  ReflTransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr (Λ'.move p k₁ k₂ q)) s S)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (a : K') ↦ List Γ') S k₁ 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 (a : K') ↦ List Γ') S k₁ L₂))

Tactic:
refine TransGen.head' rfl ?_

Premises used: Relation.TransGen.head', rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k₁) = ([], o, L₂)
nil :
  ReflTransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (bif (S k₁).head?.elim true p then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (S k₁).head? (update (β := fun (k : K') ↦ List Γ') S k₁ (S k₁).tail)
    else
      TM2.stepAux (Γ := fun (x : K') ↦ Γ')
        (push' k₂ (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ Λ'.move p k₁ 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 (a : K') ↦ List Γ') S k₁ L₂))
⊢ ReflTransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (TM2.stepAux (Γ := fun (x : K') ↦ Γ') (tr (Λ'.move p k₁ k₂ q)) s S)
    (TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) o (update (β := fun (a : K') ↦ List Γ') S k₁ L₂))

Tactic:
simp only [tr_move, pop', TM2.stepAux]

Premises used: Turing.TM2.stepAux, Turing.PartrecToTM2.pop', Turing.PartrecToTM2.tr_move
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
s : Option Γ'
S : K' → List Γ'
e : splitAtPred p (S k₁) = ([], o, L₂)
⊢ ReflTransGen (fun (a b : TM2.Cfg (fun (x : K') ↦ Γ') Λ' (Option Γ')) ↦ b ∈ TM2.step (Γ := fun (x : K') ↦ Γ') tr a)
    (bif (S k₁).head?.elim true p then
      TM2.Cfg.mk (Γ := fun (x : K') ↦ Γ') (some q) (S k₁).head? (update (β := fun (k : K') ↦ List Γ') S k₁ (S k₁).tail)
    else
      TM2.stepAux (Γ := fun (x : K') ↦ Γ')
        (push' k₂ (goto (Γ := fun (x : K') ↦ Γ') fun (x : Option Γ') ↦ Λ'.move p k₁ 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 (a : K') ↦ List Γ') S k₁ L₂))

Tactic:
grind [splitAtPred.eq_def]

Premises used: Turing.PartrecToTM2.splitAtPred.eq_def
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
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:
TransGen.head rfl ?_

Premises used: Relation.TransGen.head, StateTransition.Reaches₁, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
o : Option Γ'
L₂ : List Γ'
h₁ : k₁ ≠ k₂
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₂)
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 (Λ'.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₂))))
⊢ 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:
refine TransGen.head rfl ?_

Premises used: Relation.TransGen.head, rfl