awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
h : TM2.SupportsStmt.{u_1, u_2, u_3, u_4} (Γ := Γ) (σ := σ) S (TM2.Stmt.halt (Γ := Γ))
refine_5 :
  (∀ (x : Λ' K Γ Λ σ),
      Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) x →
        x ∈ trSupp (Γ := Γ) M S) →
    TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) ∧
      ∀ (l' : Λ' K Γ Λ σ),
        Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) l' →
          TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ (∀ (x : Λ' K Γ Λ σ),
      Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) x →
        x ∈ trSupp (Γ := Γ) M S) →
    TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) ∧
      ∀ (l' : Λ' K Γ Λ σ),
        Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) l' →
          TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
_
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
h : TM2.SupportsStmt.{u_1, u_2, u_3, u_4} (Γ := Γ) (σ := σ) S (TM2.Stmt.halt (Γ := Γ))
h_1 :
  ∀ (x : Λ' K Γ Λ σ),
    Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) x → x ∈ trSupp (Γ := Γ) M S
refine_5 :
  TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) ∧
    ∀ (l' : Λ' K Γ Λ σ), False → TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) ∧
    ∀ (l' : Λ' K Γ Λ σ),
      Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) l' →
        TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
simp only [trStmts₁, Finset.notMem_empty]

Premises used: Finset.notMem_empty, Turing.TM2to1.trStmts₁
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
h : TM2.SupportsStmt.{u_1, u_2, u_3, u_4} (Γ := Γ) (σ := σ) S (TM2.Stmt.halt (Γ := Γ))
h_1 :
  ∀ (x : Λ' K Γ Λ σ),
    Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) x → x ∈ trSupp (Γ := Γ) M S
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) ∧
    ∀ (l' : Λ' K Γ Λ σ), False → TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
⟨trivial, fun _ ↦ False.elim⟩

Premises used: trivial, False.elim, And.intro
-- Module: Mathlib.Computability.TuringMachine.StackTuringMachine
Goal:
K : Type u_1
Γ : K → Type u_2
Λ : Type u_3
σ : Type u_4
inst : DecidableEq K
M : Λ → TM2.Stmt Γ Λ σ
inst_1 : Inhabited Λ
S : Finset Λ
ss : TM2.Supports (Γ := Γ) M S
h : TM2.SupportsStmt.{u_1, u_2, u_3, u_4} (Γ := Γ) (σ := σ) S (TM2.Stmt.halt (Γ := Γ))
h_1 :
  ∀ (x : Λ' K Γ Λ σ),
    Membership.mem (γ := Finset (Λ' K Γ Λ σ)) (trStmts₁ (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) x → x ∈ trSupp (Γ := Γ) M S
⊢ TM1.SupportsStmt (trSupp (Γ := Γ) M S) (trNormal (Γ := Γ) (TM2.Stmt.halt (Γ := Γ))) ∧
    ∀ (l' : Λ' K Γ Λ σ), False → TM1.SupportsStmt (trSupp (Γ := Γ) M S) (tr (Γ := Γ) M l')

Tactic:
exact ⟨trivial, fun _ ↦ False.elim⟩
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : List Γ
⊢ l = l ++ List.replicate 0 default

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ : List Γ
i j : ℕ
⊢ l₁ ++ List.replicate i default ++ List.replicate j default = l₁ ++ List.replicate (i + j) default

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ : List Γ
i j : ℕ
⊢ BlankExtends l₁ (l₁ ++ List.replicate i default ++ List.replicate j default)

Tactic:
exact ⟨i + j, by simp⟩
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : List Γ
i j : ℕ
h : (l ++ List.replicate i default).length ≤ (l ++ List.replicate j default).length
h₁ : l ++ List.replicate j default = l ++ List.replicate i default ++ List.replicate (j - i) default
⊢ BlankExtends (l ++ List.replicate i default) (l ++ List.replicate j default)

Tactic:
use j - i
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : List Γ
i j : ℕ
h : (l ++ List.replicate i default).length ≤ (l ++ List.replicate j default).length
⊢ i ≤ j

Tactic:
simp only [List.length_append, Nat.add_le_add_iff_left, List.length_replicate] at h

Premises used: List.length_append, List.length_replicate, Nat.add_le_add_iff_left
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : List Γ
i j : ℕ
h : i ≤ j
⊢ l ++ List.replicate j default = l ++ List.replicate i default ++ List.replicate (j - i) default

Tactic:
simp only [← List.replicate_add, Nat.add_sub_cancel' h, List.append_assoc]

Premises used: List.append_assoc, Nat.add_sub_cancel', List.replicate_add
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
h₁ : l₂ = l₁ ++ List.replicate (i - j) default
⊢ BlankExtends l₁ l₂

Tactic:
use i - j
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ l₂ = l₁ ++ List.replicate (i - j) default

Tactic:
List.append_cancel_right (e.symm.trans ?_)

Premises used: List.append_cancel_right, Eq.symm, Eq.trans
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
h₁ : l₁ ++ List.replicate i default = l₁ ++ List.replicate (i - j) default ++ List.replicate j default
⊢ l₂ = l₁ ++ List.replicate (i - j) default

Tactic:
refine List.append_cancel_right (e.symm.trans ?_)

Premises used: List.append_cancel_right, Eq.symm, Eq.trans
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
h₁ : j ≤ i
⊢ l₁ ++ List.replicate i default = l₁ ++ List.replicate (i - j) default ++ List.replicate j default

Tactic:
rw [List.append_assoc, ← List.replicate_add, Nat.sub_add_cancel]

Premises used: List.append_assoc, Nat.sub_add_cancel, List.replicate_add
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
e : l₁ ++ List.replicate i default = l₂ ++ List.replicate j default
h : l₁.length ≤ l₂.length
⊢ (l₁ ++ List.replicate i default).length = (l₂ ++ List.replicate j default).length

Tactic:
apply_fun List.length at e

Premises used: List.length
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
h : l₁.length ≤ l₂.length
e : (l₁ ++ List.replicate i default).length = (l₂ ++ List.replicate j default).length
⊢ l₁.length + i = l₂.length + j

Tactic:
simp only [List.length_append, List.length_replicate] at e

Premises used: List.length_append, List.length_replicate
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
i j : ℕ
h : l₁.length ≤ l₂.length
e : l₁.length + i = l₂.length + j
h₁ : l₁.length + j ≤ l₁.length + i
rwa : ℕ
h₂ : l₁.length + j ≤ l₂.length + j
h₃ h₄ h₅ h₆ : l₁.length ≤ l₂.length
⊢ j ≤ i

Tactic:
rwa [← Nat.add_le_add_iff_left, e, Nat.add_le_add_iff_right]

Premises used: Nat.add_le_add_iff_right, Nat.add_le_add_iff_left
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : List Γ
⊢ BlankRel l l

Tactic:
Or.inl (BlankExtends.refl _)

Premises used: Turing.BlankRel, Turing.BlankExtends.refl, Or.inl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
⊢ BlankRel l₁ l₂ → BlankRel l₂ l₁

Tactic:
Or.symm

Premises used: Turing.BlankRel, Or.symm
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ l₃ : List Γ
⊢ BlankRel l₁ l₂ → BlankRel l₂ l₃ → BlankRel l₁ l₃

Tactic:
grind [eq_def, BlankExtends.below_of_le, BlankExtends.above_of_le, BlankExtends.trans]

Premises used: Turing.BlankExtends.below_of_le, Turing.BlankRel.eq_def, Turing.BlankExtends.above_of_le, Turing.BlankExtends.trans
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
refine_1 : ∀ (hl : l₁.length ≤ l₂.length) (h' : BlankExtends l₂ l₁), BlankExtends l₁ l₂
refine_2 : ∀ (hl : ¬l₁.length ≤ l₂.length) (h' : BlankExtends l₁ l₂), BlankExtends l₂ l₁
⊢ { l : List Γ // BlankExtends l₁ l ∧ BlankExtends l₂ l }

Tactic:
refine
    if hl : l₁.length ≤ l₂.length then ⟨l₂, Or.elim h id fun h' ↦ ?_, BlankExtends.refl _⟩
    else ⟨l₁, BlankExtends.refl _, Or.elim h (fun h' ↦ ?_) id⟩

Premises used: List.length
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
hl : l₁.length ≤ l₂.length
h' : BlankExtends l₂ l₁
⊢ BlankExtends l₁ l₂

Tactic:
(BlankExtends.refl _).above_of_le h' hl

Premises used: Turing.BlankExtends.refl, Turing.BlankExtends.above_of_le
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
hl : l₁.length ≤ l₂.length
h' : BlankExtends l₂ l₁
⊢ BlankExtends l₁ l₂

Tactic:
exact (BlankExtends.refl _).above_of_le h' hl

Premises used: Turing.BlankExtends.refl, Turing.BlankExtends.above_of_le
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
hl : ¬l₁.length ≤ l₂.length
h' : BlankExtends l₁ l₂
⊢ BlankExtends l₂ l₁

Tactic:
(BlankExtends.refl _).above_of_le h' (le_of_not_ge hl)

Premises used: le_of_not_ge, Turing.BlankExtends.refl, Turing.BlankExtends.above_of_le
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
hl : ¬l₁.length ≤ l₂.length
h' : BlankExtends l₁ l₂
⊢ BlankExtends l₂ l₁

Tactic:
exact (BlankExtends.refl _).above_of_le h' (le_of_not_ge hl)

Premises used: le_of_not_ge, Turing.BlankExtends.refl, Turing.BlankExtends.above_of_le
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
h : BlankRel l₁ l₂
refine_1 : ∀ (hl : l₁.length ≤ l₂.length) (h' : BlankExtends l₂ l₁), BlankExtends l₁ l₂
refine_2 : ∀ (hl : ¬l₁.length ≤ l₂.length) (h' : BlankExtends l₁ l₂), BlankExtends l₂ l₁
⊢ { l : List Γ // BlankExtends l l₁ ∧ BlankExtends l l₂ }

Tactic:
refine
    if hl : l₁.length ≤ l₂.length then ⟨l₁, BlankExtends.refl _, Or.elim h id fun h' ↦ ?_⟩
    else ⟨l₂, Or.elim h (fun h' ↦ ?_) id, BlankExtends.refl _⟩

Premises used: List.length
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
⊢ Equivalence.{u_1 + 1} (α := List Γ) BlankRel

Tactic:
⟨BlankRel.refl, @BlankRel.symm _ _, @BlankRel.trans _ _⟩

Premises used: Turing.BlankRel.symm, Turing.BlankRel.trans, Equivalence.mk, Turing.BlankRel.refl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
α : Sort u_2
l : ListBlank Γ
f : List Γ → α
H : ∀ (a b : List Γ), BlankExtends a b → f a = f b
a b : List Γ
h : BlankExtends a b
⊢ f a = f b

Tactic:
H _ _ h
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
α : Sort u_2
l : ListBlank Γ
f : List Γ → α
H : ∀ (a b : List Γ), BlankExtends a b → f a = f b
a b : List Γ
h : BlankExtends a b
⊢ f a = f b

Tactic:
exact H _ _ h
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
α : Sort u_2
l : ListBlank Γ
f : List Γ → α
H : ∀ (a b : List Γ), BlankExtends a b → f a = f b
a b : List Γ
h : BlankExtends b a
⊢ f a = f b

Tactic:
(H _ _ h).symm

Premises used: Eq.symm
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
α : Sort u_2
l : ListBlank Γ
f : List Γ → α
H : ∀ (a b : List Γ), BlankExtends a b → f a = f b
a b : List Γ
h : BlankExtends b a
⊢ f a = f b

Tactic:
exact (H _ _ h).symm

Premises used: Eq.symm
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
p : ListBlank Γ → Prop
q : ListBlank Γ
h : ∀ (a : List Γ), p (mk a)
⊢ p q

Tactic:
Quotient.inductionOn' q h

Premises used: Quotient.inductionOn'
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
apply : ∀ (a b : List Γ), BlankExtends a b → a.headI = b.headI
⊢ Γ

Tactic:
apply l.liftOn List.headI

Premises used: List.headI, Turing.ListBlank.liftOn
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
a : List Γ
i : ℕ
nil : List.headI [] = (HAppend.hAppend (α := List Γ) [] (List.replicate i default)).headI
cons : ∀ (head : Γ) (tail : List Γ), (head :: tail).headI = (head :: tail ++ List.replicate i default).headI
⊢ a.headI = (a ++ List.replicate i default).headI

Tactic:
cases a
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
i : ℕ
nil : List.headI [] = (HAppend.hAppend (α := List Γ) [] (List.replicate 0 default)).headI
nil₁ : ∀ (n : ℕ), List.headI [] = (HAppend.hAppend (α := List Γ) [] (List.replicate (n + 1) default)).headI
⊢ List.headI [] = (HAppend.hAppend (α := List Γ) [] (List.replicate i default)).headI

Tactic:
cases i
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
⊢ List.headI [] = (HAppend.hAppend (α := List Γ) [] (List.replicate 0 default)).headI

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
n : ℕ
⊢ List.headI [] = (HAppend.hAppend (α := List Γ) [] (List.replicate (n + 1) default)).headI

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
i : ℕ
head_1 : Γ
tail : List Γ
⊢ (head_1 :: tail).headI = (head_1 :: tail ++ List.replicate i default).headI

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : List Γ
⊢ head (mk l) = l.headI

Tactic:
rfl

Premises used: Quotient.liftOn', Turing.ListBlank.head, rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
apply : ∀ (a b : List Γ), BlankExtends a b → Eq (α := ListBlank Γ) (mk a.tail) (mk b.tail)
⊢ ListBlank Γ

Tactic:
apply l.liftOn (fun l ↦ ListBlank.mk l.tail)

Premises used: Turing.ListBlank.mk, List.tail, Turing.ListBlank.liftOn
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
a : List Γ
i : ℕ
⊢ Eq (α := ListBlank Γ) (mk a.tail) (mk (a ++ List.replicate i default).tail)

Tactic:
Quotient.sound' (Or.inl ?_)

Premises used: Quotient.sound', Turing.ListBlank.mk, Turing.ListBlank, Or.inl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
a : List Γ
i : ℕ
refine : BlankExtends a.tail (a ++ List.replicate i default).tail
⊢ Eq (α := ListBlank Γ) (mk a.tail) (mk (a ++ List.replicate i default).tail)

Tactic:
refine Quotient.sound' (Or.inl ?_)

Premises used: Quotient.sound'
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
a : List Γ
i : ℕ
nil : BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate i default)).tail
cons : ∀ (head : Γ) (tail : List Γ), BlankExtends (head :: tail).tail (head :: tail ++ List.replicate i default).tail
⊢ BlankExtends a.tail (a ++ List.replicate i default).tail

Tactic:
cases a
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
i : ℕ
nil : BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate 0 default)).tail
nil₁ : ∀ (i : ℕ), BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate (i + 1) default)).tail
⊢ BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate i default)).tail

Tactic:
rcases i with - | i
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
⊢ BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate 0 default)).tail

Tactic:
⟨0, rfl⟩

Premises used: Turing.BlankExtends, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
⊢ BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate 0 default)).tail

Tactic:
exact ⟨0, rfl⟩
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
i : ℕ
⊢ BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate (i + 1) default)).tail

Tactic:
⟨i, rfl⟩

Premises used: Turing.BlankExtends, Exists.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
i : ℕ
⊢ BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate (i + 1) default)).tail

Tactic:
exact ⟨i, rfl⟩
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
i : ℕ
nil : BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate 0 default)).tail
nil₁ : ∀ (i : ℕ), BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate (i + 1) default)).tail
nil₂ : BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate 0 default)).tail
nil₃ : ∀ (i : ℕ), BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate (i + 1) default)).tail
⊢ BlankExtends (List.tail []) (HAppend.hAppend (α := List Γ) [] (List.replicate i default)).tail

Tactic:
rcases i with - | i <;> [exact ⟨0, rfl⟩; exact ⟨i, rfl⟩]
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
i : ℕ
head : Γ
tail : List Γ
⊢ BlankExtends (head :: tail).tail (head :: tail ++ List.replicate i default).tail

Tactic:
⟨i, rfl⟩

Premises used: Turing.BlankExtends, Exists.intro, rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
i : ℕ
head : Γ
tail_1 : List Γ
⊢ BlankExtends (head :: tail_1).tail (head :: tail_1 ++ List.replicate i default).tail

Tactic:
exact ⟨i, rfl⟩
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : List Γ
⊢ Eq (α := ListBlank Γ) (tail (mk l)) (mk l.tail)

Tactic:
rfl

Premises used: Turing.ListBlank.mk, Quotient.liftOn', Turing.ListBlank.tail, rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
a : Γ
l : ListBlank Γ
apply : ∀ (a_1 b : List Γ), BlankExtends a_1 b → Eq (α := ListBlank Γ) (mk (a :: a_1)) (mk (a :: b))
⊢ ListBlank Γ

Tactic:
apply l.liftOn (fun l ↦ ListBlank.mk (List.cons a l))

Premises used: Turing.ListBlank.mk, List.cons, Turing.ListBlank.liftOn
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
a : Γ
l : ListBlank Γ
a_1 : List Γ
i : ℕ
⊢ Eq (α := ListBlank Γ) (mk (a :: a_1)) (mk (a :: (a_1 ++ List.replicate i default)))

Tactic:
Quotient.sound' (Or.inl ⟨i, rfl⟩)

Premises used: Quotient.sound', Turing.ListBlank.mk, Exists.intro, Turing.ListBlank, Or.inl, rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
a : Γ
l : ListBlank Γ
a_1 : List Γ
i : ℕ
⊢ Eq (α := ListBlank Γ) (mk (a :: a_1)) (mk (a :: (a_1 ++ List.replicate i default)))

Tactic:
exact Quotient.sound' (Or.inl ⟨i, rfl⟩)

Premises used: Quotient.sound'
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
a : Γ
l : List Γ
⊢ Eq (α := ListBlank Γ) (cons a (mk l)) (mk (a :: l))

Tactic:
rfl

Premises used: Turing.ListBlank.mk, Quotient.liftOn', Turing.ListBlank.cons, rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
a : Γ
⊢ ∀ (l : ListBlank Γ), (cons a l).head = a

Tactic:
Quotient.ind' fun _ ↦ rfl

Premises used: Turing.ListBlank, Quotient.ind'
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
a : Γ
⊢ ∀ (l : ListBlank Γ), (cons a l).tail = l

Tactic:
Quotient.ind' fun _ ↦ rfl

Premises used: Turing.ListBlank, Quotient.ind'
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
h : ∀ (a : List Γ), Eq (α := ListBlank Γ) (cons (head (Quotient.mk'' a)) (tail (Quotient.mk'' a))) (Quotient.mk'' a)
⊢ ∀ (l : ListBlank Γ), cons l.head l.tail = l

Tactic:
apply Quotient.ind'
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
⊢ ∀ (a : List Γ), Eq (α := ListBlank Γ) (cons (head (Quotient.mk'' a)) (tail (Quotient.mk'' a))) (Quotient.mk'' a)

Tactic:
fun l ↦ Quotient.sound' (Or.inr ?_)

Premises used: Quotient.sound', Turing.ListBlank.mk, Quotient.liftOn', Turing.ListBlank.cons, Turing.ListBlank, Or.inr
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
h : ∀ (l : List Γ), BlankExtends l (head (Quotient.mk'' l) :: l.tail)
⊢ ∀ (a : List Γ), Eq (α := ListBlank Γ) (cons (head (Quotient.mk'' a)) (tail (Quotient.mk'' a))) (Quotient.mk'' a)

Tactic:
refine fun l ↦ Quotient.sound' (Or.inr ?_)

Premises used: Quotient.sound'
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : List Γ
h : BlankExtends.{u_1} (Γ := Γ) [] (head (Quotient.mk'' []) :: List.tail [])
h₁ : ∀ (head : Γ) (tail : List Γ), BlankExtends (head :: tail) (head :: tail)
⊢ BlankExtends l (head (Quotient.mk'' l) :: l.tail)

Tactic:
cases l
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
⊢ BlankExtends.{u_1} (Γ := Γ) [] (head (Quotient.mk'' []) :: List.tail [])

Tactic:
⟨1, rfl⟩

Premises used: Turing.BlankExtends, Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
⊢ BlankExtends.{u_1} (Γ := Γ) [] (head (Quotient.mk'' []) :: List.tail [])

Tactic:
exact ⟨1, rfl⟩
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
head : Γ
tail : List Γ
⊢ BlankExtends (head :: tail) (head :: tail)

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
⊢ ∃ (a : Γ), ∃ (l' : ListBlank Γ), l = cons a l'

Tactic:
⟨_, _, (ListBlank.cons_head_tail _).symm⟩

Premises used: Exists.intro, Eq.symm, Turing.ListBlank.cons_head_tail
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l : ListBlank Γ
n : ℕ
apply : ∀ (a b : List Γ), BlankExtends a b → a.getI n = b.getI n
⊢ Γ

Tactic:
apply l.liftOn (fun l ↦ List.getI l n)

Premises used: Turing.ListBlank.liftOn, List.getI
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l_1 : ListBlank Γ
n : ℕ
l : List Γ
i : ℕ
inl : ∀ (h : n < l.length), l.getI n = (l ++ List.replicate i default).getI n
inr : ∀ (h : l.length ≤ n), l.getI n = (l ++ List.replicate i default).getI n
⊢ l.getI n = (l ++ List.replicate i default).getI n

Tactic:
rcases lt_or_ge n _ with h | h

Premises used: lt_or_ge
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l_1 : ListBlank Γ
n : ℕ
l : List Γ
i : ℕ
h : n < l.length
inl inl₁ : l.getI n = l.getI n
⊢ l.getI n = (l ++ List.replicate i default).getI n

Tactic:
rw [List.getI_append _ _ _ h]

Premises used: List.getI_append