awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
a b c d d' : List Γ'
x : K'
h : update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' main = elim a b c d' main
h₁ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' rev = elim a b c d' rev
h₂ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' aux = elim a b c d' aux
⊢ update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' x = elim a b c d' x
have h₃ : update (β := fun (a : K') ↦ List Γ') (elim a b c d) stack d' stack = elim a b c d' stack
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (hypothesis)
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
⊢ (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₁, o, l₂)
have 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₂)
Tactic: have IH := splitAtPred_eq p L
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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₂)
⊢ (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₁, o, l₂)
have none : ∀ (h₂ : Option.elim' (a :: L = l₁ ∧ l₂ = []) (fun (a_1 : α) ↦ p a_1 = true ∧ a :: L = l₁ ++ a_1 :: l₂) 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₂)) =
    (l₁, none, l₂)
Tactic: rcases o with - | o
Cleared hypotheses: o, h₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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 ([], 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₂)
⊢ (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₁, o, l₂)
have some : ∀ (o : α)
  (h₂ : Option.elim' (a :: L = l₁ ∧ l₂ = []) (fun (a_1 : α) ↦ p a_1 = true ∧ a :: L = l₁ ++ a_1 :: l₂) (some o)),
  (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₁, some o, l₂)
Tactic: rcases o with - | o
Cleared hypotheses: o, h₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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₂) 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₂)) =
    (l₁, none, l₂)
have 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₂) 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 l₁ with - | ⟨a', l₁⟩
Cleared hypotheses: l₁, h₁, h₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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₂)
⊢ (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₂)
have 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₂)
Tactic: rcases l₁ with - | ⟨a', l₁⟩
Cleared hypotheses: l₁, h₁, h₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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₂) 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₁, none, l₂)
have 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, none, [])
Tactic: rcases h₂ with ⟨⟨⟩, rfl⟩
Cleared hypotheses: l₂, a', l₁, h₁, h₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
⊢ (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, [])
have rw : ∀ x ∈ L, p x = false
Tactic: rw [h₁ a (List.Mem.head _), cond, IH L none [] _ ⟨rfl, rfl⟩]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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₂) (some o)
⊢ (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₁, some o, l₂)
have 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₂) (some o)),
  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₂))
    ([], some o, l₂)
Tactic: rcases l₁ with - | ⟨a', l₁⟩
Cleared hypotheses: l₁, h₁, h₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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₂)
⊢ (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₂)
have 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₂)
Tactic: rcases l₁ with - | ⟨a', l₁⟩
Cleared hypotheses: l₁, h₁, h₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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₂) (some o)
⊢ 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₂))
    ([], some o, l₂)
have some : ∀ (h₂ : p a = true),
  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₂))
    ([], some a, L)
Tactic: rcases h₂ with ⟨h₂, ⟨⟩⟩
Cleared hypotheses: l₂, o, h₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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₂) (some o)
⊢ (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₁, some o, l₂)
have 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 ([], 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: rcases h₂ with ⟨h₂, ⟨⟩⟩
Cleared hypotheses: L, IH, a', h₁, h₂
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
⊢ 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₂))
    ([], some a, L)
have some : Eq (α := List α × Option α × List α)
  (bif true then ([], some a, L)
  else
    match (motive := List α × Option α × List α → List α × Option α × List α) splitAtPred p L with
    | (l₁, o, l₂) => (a :: l₁, o, l₂))
  ([], some a, L)
Tactic: rw [h₂, cond]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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)
⊢ 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)
have some₁ : Eq (α := List α × Option α × List α) ([], Option.some a, L) ([], Option.some a, L)
Tactic: rw [h₂, cond]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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)
⊢ (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₂)
have rw : ∀ x ∈ l₁, p x = false
Tactic: rw [h₁ a (List.Mem.head _), cond, IH l₁ (some o) l₂ _ ⟨h₂, _⟩]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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
⊢ (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₂)
have rw₁ : l₁.append (o :: l₂) = l₁ ++ o :: l₂
Tactic: rw [h₁ a (List.Mem.head _), cond, IH l₁ (some o) l₂ _ ⟨h₂, _⟩]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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 (k : K') ↦ List Γ') (update (β := fun (a : K') ↦ List Γ') S k₁ L₂) k₂
        (List.reverseAux [] (S k₂))))
have 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₂))
Tactic: rw [(_ : [].reverseAux _ = _), Function.update_eq_self]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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₂))
⊢ 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₂))))
have rw : List.reverseAux [] (S k₂) = update (β := fun (a : K') ↦ List Γ') S k₁ L₂ k₂
Tactic: rw [(_ : [].reverseAux _ = _), Function.update_eq_self]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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₂)
⊢ List.reverseAux [] (S k₂) = update (β := fun (a : K') ↦ List Γ') S k₁ L₂ k₂
have rw : List.reverseAux [] (S k₂) = S k₂
Tactic: rw [Function.update_of_ne h₁.symm, List.reverseAux_nil]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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₂
⊢ List.reverseAux [] (S k₂) = update (β := fun (a : K') ↦ List Γ') S k₁ L₂ k₂
have rw₁ : S k₂ = S k₂
Tactic: rw [Function.update_of_ne h₁.symm, List.reverseAux_nil]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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₂))
have 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₂))
Tactic: refine TransGen.head' rfl ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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)
    (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₂))
have 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₂))
Tactic: simp only [tr_move, pop', TM2.stepAux]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
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₂))))
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 (Λ'.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 ?_