awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
⊢ f.f default = default

Tactic:
PointedMap.map_pt' _

Premises used: Turing.PointedMap.map_pt'
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l : List Γ
nil : (List.map f.f []).headI = f.f (List.headI [])
cons : ∀ (head : Γ) (tail : List Γ), (List.map f.f (head :: tail)).headI = f.f (head :: tail).headI
⊢ (List.map f.f l).headI = f.f l.headI

Tactic:
cases l
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
⊢ (List.map f.f []).headI = f.f (List.headI [])

Tactic:
(PointedMap.map_pt f).symm

Premises used: List.headI, Eq.symm, Turing.PointedMap.map_pt
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
⊢ (List.map f.f []).headI = f.f (List.headI [])

Tactic:
exact (PointedMap.map_pt f).symm

Premises used: Eq.symm, Turing.PointedMap.map_pt
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
head : Γ
tail : List Γ
⊢ (List.map f.f (head :: tail)).headI = f.f (head :: tail).headI

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l : List Γ
nil : (List.map f.f []).headI = f.f (List.headI [])
cons : ∀ (head : Γ) (tail : List Γ), (List.map f.f (head :: tail)).headI = f.f (head :: tail).headI
nil₁ : (List.map f.f []).headI = f.f (List.headI [])
cons₁ : ∀ (head : Γ) (tail : List Γ), (List.map f.f (head :: tail)).headI = f.f (head :: tail).headI
⊢ (List.map f.f l).headI = f.f l.headI

Tactic:
cases l <;> [exact (PointedMap.map_pt f).symm; rfl]

Premises used: Eq.symm, Turing.PointedMap.map_pt
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
apply : ∀ (a b : List Γ), BlankExtends a b → Eq (α := ListBlank Γ') (mk (List.map f.f a)) (mk (List.map f.f b))
⊢ ListBlank Γ'

Tactic:
apply l.liftOn (fun l ↦ ListBlank.mk (List.map f l))

Premises used: Turing.ListBlank.mk, List.map, Turing.PointedMap.f, Turing.ListBlank.liftOn
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l_1 : ListBlank Γ
l : List Γ
i : ℕ
⊢ Eq (α := ListBlank Γ') (mk (List.map f.f l)) (mk (List.map f.f (l ++ List.replicate i default)))

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

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

Tactic:
refine Quotient.sound' (Or.inl ⟨i, ?_⟩)

Premises used: Quotient.sound'
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l_1 : ListBlank Γ
l : List Γ
i : ℕ
⊢ List.map f.f (l ++ List.replicate i default) = List.map f.f l ++ List.replicate i default

Tactic:
simp only [PointedMap.map_pt, List.map_append, List.map_replicate]

Premises used: List.map_append, List.map_replicate, Turing.PointedMap.map_pt
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l : List Γ
⊢ map f (mk l) = mk (List.map f.f l)

Tactic:
rfl

Premises used: Turing.ListBlank.mk, Quotient.liftOn', Turing.ListBlank.map, rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
rw : (map f (cons l.head l.tail)).head = f.f (cons l.head l.tail).head
⊢ (map f l).head = f.f l.head

Tactic:
rw [← ListBlank.cons_head_tail l]

Premises used: Turing.ListBlank.cons_head_tail
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
h :
  ∀ (a : List Γ),
    (map f (cons (head (Quotient.mk'' a)) (tail (Quotient.mk'' a)))).head =
      f.f (head (cons (head (Quotient.mk'' a)) (tail (Quotient.mk'' a))))
⊢ (map f (cons l.head l.tail)).head = f.f (cons l.head l.tail).head

Tactic:
induction l using Quotient.inductionOn'
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
a : List Γ
⊢ (map f (cons (head (Quotient.mk'' a)) (tail (Quotient.mk'' a)))).head =
    f.f (head (cons (head (Quotient.mk'' a)) (tail (Quotient.mk'' a))))

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
rw : (map f (cons l.head l.tail)).tail = map f (cons l.head l.tail).tail
⊢ (map f l).tail = map f l.tail

Tactic:
rw [← ListBlank.cons_head_tail l]

Premises used: Turing.ListBlank.cons_head_tail
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
h :
  ∀ (a : List Γ),
    (map f (cons (head (Quotient.mk'' a)) (tail (Quotient.mk'' a)))).tail =
      map f (tail (cons (head (Quotient.mk'' a)) (tail (Quotient.mk'' a))))
⊢ (map f (cons l.head l.tail)).tail = map f (cons l.head l.tail).tail

Tactic:
induction l using Quotient.inductionOn'
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
a : List Γ
⊢ (map f (cons (head (Quotient.mk'' a)) (tail (Quotient.mk'' a)))).tail =
    map f (tail (cons (head (Quotient.mk'' a)) (tail (Quotient.mk'' a))))

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
a : Γ
⊢ map f (cons a l) = cons (f.f a) (map f l)

Tactic:
(ListBlank.cons_head_tail _).symm.trans ?_

Premises used: Eq.symm, Turing.ListBlank.cons_head_tail, Eq.trans
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
a : Γ
refine : cons (map f (cons a l)).head (map f (cons a l)).tail = cons (f.f a) (map f l)
⊢ map f (cons a l) = cons (f.f a) (map f l)

Tactic:
refine (ListBlank.cons_head_tail _).symm.trans ?_

Premises used: Eq.symm, Turing.ListBlank.cons_head_tail, Eq.trans
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
a : Γ
⊢ cons (map f (cons a l)).head (map f (cons a l)).tail = cons (f.f a) (map f l)

Tactic:
simp only [ListBlank.head_map, ListBlank.head_cons, ListBlank.tail_map, ListBlank.tail_cons]

Premises used: Turing.ListBlank.head_map, Turing.ListBlank.head_cons, Turing.ListBlank.tail_cons, Turing.ListBlank.tail_map
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
n : ℕ
⊢ (map f l).nth n = f.f (l.nth n)

Tactic:
l.induction_on fun l ↦ ?_

Premises used: Turing.ListBlank.induction_on
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
n : ℕ
refine : ∀ (l : List Γ), (map f (mk l)).nth n = f.f (nth (mk l) n)
⊢ (map f l).nth n = f.f (l.nth n)

Tactic:
refine l.induction_on fun l ↦ ?_
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l_1 : ListBlank Γ
n : ℕ
l : List Γ
simp : (List.map f.f l).getD n default = f.f (l.getD n default)
⊢ (map f (mk l)).nth n = f.f (nth (mk l) n)

Tactic:
simp only [ListBlank.map_mk, ListBlank.nth_mk, ← List.getD_default_eq_getI]

Premises used: Turing.ListBlank.map_mk, List.getD_default_eq_getI, Turing.ListBlank.nth_mk
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l_1 : ListBlank Γ
n : ℕ
l : List Γ
rw : (List.map f.f l).getD n default = (List.map f.f l).getD n (f.f default)
⊢ (List.map f.f l).getD n default = f.f (l.getD n default)

Tactic:
rw [← List.getD_map _ _ f]

Premises used: List.getD_map, Turing.PointedMap.f
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l_1 : ListBlank Γ
n : ℕ
l : List Γ
⊢ (List.map f.f l).getD n default = (List.map f.f l).getD n (f.f default)

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
ι : Type u_1
Γ : ι → Type u_2
inst : (i : ι) → Inhabited (Γ i)
i : ι
L : ListBlank ((i : ι) → Γ i)
n : ℕ
rw : PointedMap.f (proj (Γ := Γ) i) (L.nth n) = L.nth n i
⊢ (ListBlank.map (proj (Γ := Γ) i) L).nth n = L.nth n i

Tactic:
rw [ListBlank.nth_map]

Premises used: Turing.ListBlank.nth_map
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
ι : Type u_1
Γ : ι → Type u_2
inst : (i : ι) → Inhabited (Γ i)
i : ι
L : ListBlank ((i : ι) → Γ i)
n : ℕ
⊢ PointedMap.f (proj (Γ := Γ) i) (L.nth n) = L.nth n i

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
F : PointedMap Γ Γ'
f : Γ → Γ
f' : Γ' → Γ'
H : ∀ (x : Γ), F.f (f x) = f' (F.f x)
n : ℕ
L : ListBlank Γ
zero : ∀ (L : ListBlank Γ), map F (modifyNth f 0 L) = modifyNth f' 0 (map F L)
succ :
  ∀ (n : ℕ),
    (∀ (L : ListBlank Γ), map F (modifyNth f n L) = modifyNth f' n (map F L)) →
      ∀ (L : ListBlank Γ), map F (modifyNth f (n + 1) L) = modifyNth f' (n + 1) (map F L)
⊢ map F (modifyNth f n L) = modifyNth f' n (map F L)

Tactic:
induction n generalizing L
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
F : PointedMap Γ Γ'
f : Γ → Γ
f' : Γ' → Γ'
H : ∀ (x : Γ), F.f (f x) = f' (F.f x)
L : ListBlank Γ
⊢ map F (modifyNth f 0 L) = modifyNth f' 0 (map F L)

Tactic:
simp only [*, ListBlank.head_map, ListBlank.modifyNth, ListBlank.map_cons, ListBlank.tail_map]

Premises used: Turing.ListBlank.modifyNth, Turing.ListBlank.head_map, Turing.ListBlank.map_cons, Turing.ListBlank.tail_map
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
F : PointedMap Γ Γ'
f : Γ → Γ
f' : Γ' → Γ'
H : ∀ (x : Γ), F.f (f x) = f' (F.f x)
n : ℕ
h : ∀ (L : ListBlank Γ), map F (modifyNth f n L) = modifyNth f' n (map F L)
L : ListBlank Γ
⊢ map F (modifyNth f (n + 1) L) = modifyNth f' (n + 1) (map F L)

Tactic:
simp only [*, ListBlank.head_map, ListBlank.modifyNth, ListBlank.map_cons, ListBlank.tail_map]

Premises used: Turing.ListBlank.modifyNth, Turing.ListBlank.head_map, Turing.ListBlank.map_cons, Turing.ListBlank.tail_map
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
nil : Eq (α := ListBlank Γ) (append [] (mk l₂)) (mk ([] ++ l₂))
cons :
  ∀ (head : Γ) (tail : List Γ),
    Eq (α := ListBlank Γ) (append tail (mk l₂)) (mk (tail ++ l₂)) →
      Eq (α := ListBlank Γ) (append (head :: tail) (mk l₂)) (mk (head :: tail ++ l₂))
⊢ Eq (α := ListBlank Γ) (append l₁ (mk l₂)) (mk (l₁ ++ l₂))

Tactic:
induction l₁
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₂ : List Γ
⊢ Eq (α := ListBlank Γ) (append [] (mk l₂)) (mk ([] ++ l₂))

Tactic:
simp only [*, ListBlank.append, List.nil_append, List.cons_append, ListBlank.cons_mk]

Premises used: List.nil_append, Turing.ListBlank.cons_mk, Turing.ListBlank.append, List.cons_append
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₂ : List Γ
head : Γ
tail : List Γ
tail_ih : Eq (α := ListBlank Γ) (append tail (mk l₂)) (mk (tail ++ l₂))
⊢ Eq (α := ListBlank Γ) (append (head :: tail) (mk l₂)) (mk (head :: tail ++ l₂))

Tactic:
simp only [*, ListBlank.append, List.nil_append, List.cons_append, ListBlank.cons_mk]

Premises used: List.nil_append, Turing.ListBlank.cons_mk, Turing.ListBlank.append, List.cons_append
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
l₃ : ListBlank Γ
⊢ append (l₁ ++ l₂) l₃ = append l₁ (append l₂ l₃)

Tactic:
l₃.induction_on fun l ↦ ?_

Premises used: Turing.ListBlank.induction_on
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
l₃ : ListBlank Γ
refine : ∀ (l : List Γ), Eq (α := ListBlank Γ) (append (l₁ ++ l₂) (mk l)) (append l₁ (append l₂ (mk l)))
⊢ append (l₁ ++ l₂) l₃ = append l₁ (append l₂ l₃)

Tactic:
refine l₃.induction_on fun l ↦ ?_
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
l₃ : ListBlank Γ
l : List Γ
⊢ Eq (α := ListBlank Γ) (append (l₁ ++ l₂) (mk l)) (append l₁ (append l₂ (mk l)))

Tactic:
simp only [ListBlank.append_mk, List.append_assoc]

Premises used: Turing.ListBlank.append_mk, List.append_assoc
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
l : ListBlank Γ
f : Γ → List Γ'
hf : ∃ (n : ℕ), f default = List.replicate n default
apply : ∀ (a b : List Γ), BlankExtends a b → Eq (α := ListBlank Γ') (mk (List.flatMap f a)) (mk (List.flatMap f b))
⊢ ListBlank Γ'

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

Premises used: Turing.ListBlank.mk, Turing.ListBlank.liftOn, List.flatMap
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
l_1 : ListBlank Γ
f : Γ → List Γ'
hf : ∃ (n : ℕ), f default = List.replicate n default
l : List Γ
i : ℕ
obtain :
  ∀ (n : ℕ) (e : f default = List.replicate n default),
    Eq (α := ListBlank Γ') (mk (List.flatMap f l)) (mk (List.flatMap f (l ++ List.replicate i default)))
⊢ Eq (α := ListBlank Γ') (mk (List.flatMap f l)) (mk (List.flatMap f (l ++ List.replicate i default)))

Tactic:
obtain ⟨n, e⟩ := hf
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
l_1 : ListBlank Γ
f : Γ → List Γ'
l : List Γ
i n : ℕ
e : f default = List.replicate n default
⊢ Eq (α := ListBlank Γ') (mk (List.flatMap f l)) (mk (List.flatMap f (l ++ List.replicate i default)))

Tactic:
Quotient.sound' (Or.inl ⟨i * n, ?_⟩)

Premises used: Quotient.sound', Turing.ListBlank.mk, HMul.hMul, Exists.intro, Turing.ListBlank, Or.inl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
l_1 : ListBlank Γ
f : Γ → List Γ'
l : List Γ
i n : ℕ
e : f default = List.replicate n default
refine : List.flatMap f (l ++ List.replicate i default) = List.flatMap f l ++ List.replicate (i * n) default
⊢ Eq (α := ListBlank Γ') (mk (List.flatMap f l)) (mk (List.flatMap f (l ++ List.replicate i default)))

Tactic:
refine Quotient.sound' (Or.inl ⟨i * n, ?_⟩)

Premises used: Quotient.sound'
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
l_1 : ListBlank Γ
f : Γ → List Γ'
l : List Γ
i n : ℕ
e : f default = List.replicate n default
rw : List.flatMap f l ++ List.flatMap f (List.replicate i default) = List.flatMap f l ++ List.replicate (n * i) default
⊢ List.flatMap f (l ++ List.replicate i default) = List.flatMap f l ++ List.replicate (i * n) default

Tactic:
rw [List.flatMap_append, mul_comm]

Premises used: mul_comm, List.flatMap_append
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
l_1 : ListBlank Γ
f : Γ → List Γ'
l : List Γ
i n : ℕ
e : f default = List.replicate n default
e_a : List.flatMap f (List.replicate i default) = List.replicate (n * i) default
⊢ List.flatMap f l ++ List.flatMap f (List.replicate i default) = List.flatMap f l ++ List.replicate (n * i) default

Tactic:
congr
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
l_1 : ListBlank Γ
f : Γ → List Γ'
l : List Γ
n : ℕ
e : f default = List.replicate n default
⊢ List.flatMap f (List.replicate 0 default) = List.replicate (n * 0) default

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
l_1 : ListBlank Γ
f : Γ → List Γ'
l : List Γ
n : ℕ
e : f default = List.replicate n default
i : ℕ
IH : List.flatMap f (List.replicate i default) = List.replicate (n * i) default
⊢ List.flatMap f (List.replicate (i + 1) default) = List.replicate (n * (i + 1)) default

Tactic:
simp only [IH, e, List.replicate_add, Nat.mul_succ, add_comm, List.replicate_succ,
      List.flatMap_cons]

Premises used: Nat.mul_succ, add_comm, List.flatMap_cons, List.replicate_succ, List.replicate_add
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
l_1 : ListBlank Γ
f : Γ → List Γ'
l : List Γ
i n : ℕ
e : f default = List.replicate n default
e_a : List.flatMap f (List.replicate 0 default) = List.replicate (n * 0) default
e_a₁ :
  ∀ (i : ℕ) (IH : List.flatMap f (List.replicate i default) = List.replicate (n * i) default),
    List.flatMap f (List.replicate (i + 1) default) = List.replicate (n * (i + 1)) default
⊢ List.flatMap f (List.replicate i default) = List.replicate (n * i) default

Tactic:
induction i with
  | zero => rfl
  | succ i IH =>
    simp only [IH, e, List.replicate_add, Nat.mul_succ, add_comm, List.replicate_succ,
      List.flatMap_cons]

Premises used: Nat.mul_succ, add_comm, List.flatMap_cons, List.replicate_succ, List.replicate_add
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
l : List Γ
f : Γ → List Γ'
hf : ∃ (n : ℕ), f default = List.replicate n default
⊢ flatMap (mk l) f hf = mk (List.flatMap f l)

Tactic:
rfl

Premises used: Turing.ListBlank.mk, Quotient.liftOn', Turing.ListBlank.flatMap, rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
a : Γ
l : ListBlank Γ
f : Γ → List Γ'
hf : ∃ (n : ℕ), f default = List.replicate n default
⊢ (cons a l).flatMap f hf = append (f a) (l.flatMap f hf)

Tactic:
l.induction_on fun l ↦ ?_

Premises used: Turing.ListBlank.induction_on
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
a : Γ
l : ListBlank Γ
f : Γ → List Γ'
hf : ∃ (n : ℕ), f default = List.replicate n default
refine : ∀ (l : List Γ), flatMap (cons a (mk l)) f hf = append (f a) (flatMap (mk l) f hf)
⊢ (cons a l).flatMap f hf = append (f a) (l.flatMap f hf)

Tactic:
refine l.induction_on fun l ↦ ?_
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
a : Γ
l_1 : ListBlank Γ
f : Γ → List Γ'
hf : ∃ (n : ℕ), f default = List.replicate n default
l : List Γ
⊢ flatMap (cons a (mk l)) f hf = append (f a) (flatMap (mk l) f hf)

Tactic:
simp only [ListBlank.append_mk, ListBlank.flatMap_mk, ListBlank.cons_mk, List.flatMap_cons]

Premises used: Turing.ListBlank.append_mk, Turing.ListBlank.flatMap_mk, List.flatMap_cons, Turing.ListBlank.cons_mk
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
head : Γ
left right : ListBlank Γ
⊢ Tape Γ

Tactic:
constructor
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
⊢ Γ

Tactic:
apply default

Premises used: Inhabited.default
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
⊢ ListBlank Γ

Tactic:
apply default

Premises used: Inhabited.default
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
⊢ move Dir.right (move Dir.left T) = T

Tactic:
simp [Tape.move]

Premises used: Turing.Tape.move
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
⊢ move Dir.left (move Dir.right T) = T

Tactic:
simp [Tape.move]

Premises used: Turing.Tape.move
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
L R : ListBlank Γ
⊢ (mk' L R).left = L

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
L R : ListBlank Γ
⊢ (mk' L R).head = R.head

Tactic:
rfl

Premises used: Quotient.liftOn', Turing.ListBlank.head, rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
L R : ListBlank Γ
⊢ (mk' L R).right = R.tail

Tactic:
rfl

Premises used: Quotient.liftOn', Turing.ListBlank.tail, rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
L R : ListBlank Γ
⊢ (mk' L R).right₀ = R

Tactic:
ListBlank.cons_head_tail _

Premises used: Quotient.liftOn', Turing.Tape.right₀, Turing.ListBlank.tail, Turing.ListBlank.head, Turing.ListBlank.cons_head_tail
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
⊢ mk' T.left T.right₀ = T

Tactic:
simp only [Tape.right₀, Tape.mk', ListBlank.head_cons, ListBlank.tail_cons]

Premises used: Turing.Tape.mk', Turing.ListBlank.head_cons, Turing.Tape.right₀, Turing.ListBlank.tail_cons
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
⊢ ∃ (L : ListBlank Γ), ∃ (R : ListBlank Γ), T = mk' L R

Tactic:
⟨_, _, (Tape.mk'_left_right₀ _).symm⟩

Premises used: Turing.Tape.mk'_left_right₀, Exists.intro, Eq.symm
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
L R : ListBlank Γ
⊢ move Dir.left (mk' L R) = mk' L.tail (ListBlank.cons L.head R)

Tactic:
simp only [Tape.move, Tape.mk', ListBlank.head_cons, ListBlank.cons_head_tail,
    ListBlank.tail_cons]

Premises used: Turing.Tape.mk', Turing.ListBlank.head_cons, Turing.ListBlank.tail_cons, Turing.Tape.move, Turing.ListBlank.cons_head_tail
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
L R : ListBlank Γ
⊢ move Dir.right (mk' L R) = mk' (ListBlank.cons R.head L) R.tail

Tactic:
simp only [Tape.move, Tape.mk']

Premises used: Turing.Tape.mk', Turing.Tape.move
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
⊢ T.nth 0 = T.head

Tactic:
rfl

Premises used: Turing.Tape.nth, rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
n : ℕ
zero : T.right₀.nth 0 = T.nth (↑0 : ℤ)
succ : ∀ (n : ℕ), T.right₀.nth (n + 1) = T.nth (↑(n + 1) : ℤ)
⊢ T.right₀.nth n = T.nth (↑n : ℤ)

Tactic:
cases n
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
⊢ T.right₀.nth 0 = T.nth (↑0 : ℤ)

Tactic:
simp only [Tape.nth, Tape.right₀, ListBlank.nth_zero,
    ListBlank.nth_succ, ListBlank.head_cons, ListBlank.tail_cons]

Premises used: Turing.ListBlank.nth_zero, Turing.Tape.nth, Turing.ListBlank.nth_succ, Turing.ListBlank.head_cons, Turing.Tape.right₀, Turing.ListBlank.tail_cons
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
n : ℕ
⊢ T.right₀.nth (n + 1) = T.nth (↑(n + 1) : ℤ)

Tactic:
simp only [Tape.nth, Tape.right₀, ListBlank.nth_zero,
    ListBlank.nth_succ, ListBlank.head_cons, ListBlank.tail_cons]

Premises used: Turing.ListBlank.nth_zero, Turing.Tape.nth, Turing.ListBlank.nth_succ, Turing.ListBlank.head_cons, Turing.Tape.right₀, Turing.ListBlank.tail_cons