awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
f : Γ → Γ
n i : ℕ
L : ListBlank Γ
zero : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f 0 L).nth i = if i = 0 then f (L.nth i) else L.nth i
⊢ (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i
have succ : ∀ (n : ℕ) (IH : ∀ (i : ℕ) (L : ListBlank Γ), (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i) (i : ℕ)
  (L : ListBlank Γ), (modifyNth f (n + 1) L).nth i = if i = n + 1 then f (L.nth i) else L.nth i
Tactic: induction n generalizing i L with
  | zero =>
    cases i <;> simp only [ListBlank.nth_zero, if_true, ListBlank.head_cons, ListBlank.modifyNth,
      ListBlank.nth_succ, if_false, ListBlank.tail_cons, reduceCtorEq]
  | succ n IH =>
    cases i
    · rw [if_neg (Nat.succ_ne_zero _).symm]
      simp only [ListBlank.nth_zero, ListBlank.head_cons, ListBlank.modifyNth]
    · simp only [IH, ListBlank.modifyNth, ListBlank.nth_succ, ListBlank.tail_cons, Nat.succ.injEq]
Cleared hypotheses: n, i, L
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l : List Γ
⊢ (List.map f.f l).headI = f.f l.headI
have nil : (List.map f.f []).headI = f.f (List.headI [])
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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 [])
⊢ (List.map f.f l).headI = f.f l.headI
have cons : ∀ (head : Γ) (tail : List Γ), (List.map f.f (head :: tail)).headI = f.f (head :: tail).headI
Tactic: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l : List Γ
⊢ (List.map f.f l).headI = f.f l.headI
have nil : (List.map f.f []).headI = f.f (List.headI [])
Tactic: cases l <;> [exact (PointedMap.map_pt f).symm; rfl]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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 [])
⊢ (List.map f.f l).headI = f.f l.headI
have cons : ∀ (head : Γ) (tail : List Γ), (List.map f.f (head :: tail)).headI = f.f (head :: tail).headI
Tactic: cases l <;> [exact (PointedMap.map_pt f).symm; rfl]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ ListBlank Γ'
have apply : ∀ (a b : List Γ), BlankExtends a b → Eq (α := ListBlank Γ') (mk (List.map f.f a)) (mk (List.map f.f b))
Tactic: apply l.liftOn (fun l ↦ ListBlank.mk (List.map f l))
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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)))
have refine : List.map f.f (l ++ List.replicate i default) = List.map f.f l ++ List.replicate i default
Tactic: refine Quotient.sound' (Or.inl ⟨i, ?_⟩)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ (map f l).head = f.f l.head
have rw : (map f (cons l.head l.tail)).head = f.f (cons l.head l.tail).head
Tactic: rw [← ListBlank.cons_head_tail l]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ (map f (cons l.head l.tail)).head = f.f (cons l.head l.tail).head
have 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))))
Tactic: induction l using Quotient.inductionOn'
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ (map f l).tail = map f l.tail
have rw : (map f (cons l.head l.tail)).tail = map f (cons l.head l.tail).tail
Tactic: rw [← ListBlank.cons_head_tail l]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l : ListBlank Γ
⊢ (map f (cons l.head l.tail)).tail = map f (cons l.head l.tail).tail
have 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))))
Tactic: induction l using Quotient.inductionOn'
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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)
have refine : cons (map f (cons a l)).head (map f (cons a l)).tail = cons (f.f a) (map f l)
Tactic: refine (ListBlank.cons_head_tail _).symm.trans ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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)
have refine : ∀ (l : List Γ), (map f (mk l)).nth n = f.f (nth (mk l) n)
Tactic: refine l.induction_on fun l ↦ ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
l_1 : ListBlank Γ
n : ℕ
l : List Γ
⊢ (map f (mk l)).nth n = f.f (nth (mk l) n)
have simp : (List.map f.f l).getD n default = f.f (l.getD n default)
Tactic: simp only [ListBlank.map_mk, ListBlank.nth_mk, ← List.getD_default_eq_getI]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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 = f.f (l.getD n default)
have rw : (List.map f.f l).getD n default = (List.map f.f l).getD n (f.f default)
Tactic: rw [← List.getD_map _ _ f]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
ι : Type u_1
Γ : ι → Type u_2
inst : (i : ι) → Inhabited (Γ i)
i : ι
L : ListBlank ((i : ι) → Γ i)
n : ℕ
⊢ (ListBlank.map (proj (Γ := Γ) i) L).nth n = L.nth n i
have rw : PointedMap.f (proj (Γ := Γ) i) (L.nth n) = L.nth n i
Tactic: rw [ListBlank.nth_map]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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 Γ
⊢ map F (modifyNth f n L) = modifyNth f' n (map F L)
have zero : ∀ (L : ListBlank Γ), map F (modifyNth f 0 L) = modifyNth f' 0 (map F L)
Tactic: induction n generalizing L
Cleared hypotheses: n, L
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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)
⊢ map F (modifyNth f n L) = modifyNth f' n (map F L)
have 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)
Tactic: induction n generalizing L
Cleared hypotheses: n, L
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
⊢ Eq (α := ListBlank Γ) (append l₁ (mk l₂)) (mk (l₁ ++ l₂))
have nil : Eq (α := ListBlank Γ) (append [] (mk l₂)) (mk ([] ++ l₂))
Tactic: induction l₁
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
nil : Eq (α := ListBlank Γ) (append [] (mk l₂)) (mk ([] ++ l₂))
⊢ Eq (α := ListBlank Γ) (append l₁ (mk l₂)) (mk (l₁ ++ l₂))
have cons : ∀ (head : Γ) (tail : List Γ),
  Eq (α := ListBlank Γ) (append tail (mk l₂)) (mk (tail ++ l₂)) →
    Eq (α := ListBlank Γ) (append (head :: tail) (mk l₂)) (mk (head :: tail ++ l₂))
Tactic: induction l₁
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
l₁ l₂ : List Γ
l₃ : ListBlank Γ
⊢ append (l₁ ++ l₂) l₃ = append l₁ (append l₂ l₃)
have refine : ∀ (l : List Γ), Eq (α := ListBlank Γ) (append (l₁ ++ l₂) (mk l)) (append l₁ (append l₂ (mk l)))
Tactic: refine l₃.induction_on fun l ↦ ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
l : ListBlank Γ
f : Γ → List Γ'
hf : ∃ (n : ℕ), f default = List.replicate n default
⊢ ListBlank Γ'
have apply : ∀ (a b : List Γ), BlankExtends a b → Eq (α := ListBlank Γ') (mk (List.flatMap f a)) (mk (List.flatMap f b))
Tactic: apply l.liftOn (fun l ↦ ListBlank.mk (l.flatMap f))
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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 : ℕ
⊢ Eq (α := ListBlank Γ') (mk (List.flatMap f l)) (mk (List.flatMap f (l ++ List.replicate i default)))
have 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)))
Tactic: obtain ⟨n, e⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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)))
have refine : List.flatMap f (l ++ List.replicate i default) = List.flatMap f l ++ List.replicate (i * n) default
Tactic: refine Quotient.sound' (Or.inl ⟨i * n, ?_⟩)
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ List.flatMap f (l ++ List.replicate i default) = List.flatMap f l ++ List.replicate (i * n) default
have rw : List.flatMap f l ++ List.flatMap f (List.replicate i default) = List.flatMap f l ++ List.replicate (n * i) default
Tactic: rw [List.flatMap_append, mul_comm]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ List.flatMap f l ++ List.flatMap f (List.replicate i default) = List.flatMap f l ++ List.replicate (n * i) default
have e_a : List.flatMap f (List.replicate i default) = List.replicate (n * i) default
Tactic: congr
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ List.flatMap f (List.replicate i default) = List.replicate (n * i) default
have e_a : List.flatMap f (List.replicate 0 default) = List.replicate (n * 0) 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]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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
⊢ List.flatMap f (List.replicate i default) = List.replicate (n * i) default
have 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
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]
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
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)
have refine : ∀ (l : List Γ), flatMap (cons a (mk l)) f hf = append (f a) (flatMap (mk l) f hf)
Tactic: refine l.induction_on fun l ↦ ?_
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
⊢ Tape Γ
have head : Γ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
head : Γ
⊢ Tape Γ
have left : ListBlank Γ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
n : ℕ
⊢ T.right₀.nth n = T.nth (↑n : ℤ)
have zero : T.right₀.nth 0 = T.nth (↑0 : ℤ)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
n : ℕ
zero : T.right₀.nth 0 = T.nth (↑0 : ℤ)
⊢ T.right₀.nth n = T.nth (↑n : ℤ)
have succ : ∀ (n : ℕ), T.right₀.nth (n + 1) = T.nth (↑(n + 1) : ℤ)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
L R : ListBlank Γ
n : ℕ
⊢ (mk' L R).nth (↑n : ℤ) = R.nth n
have rw : (mk' L R).right₀.nth n = R.nth n
Tactic: rw [← Tape.right₀_nth, Tape.mk'_right₀]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
L R : ListBlank Γ
n : ℕ
rw : (mk' L R).right₀.nth n = R.nth n
⊢ (mk' L R).nth (↑n : ℤ) = R.nth n
have rw₁ : R.nth n = R.nth n
Tactic: rw [← Tape.right₀_nth, Tape.mk'_right₀]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
⊢ (move Dir.left { head := a, left := L, right := R : Tape Γ }).nth (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) =
    { head := a, left := L, right := R : Tape Γ }.nth (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1 - 1)
have rw : (move Dir.left { head := a, left := L, right := R : Tape Γ }).nth (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) =
  { head := a, left := L, right := R : Tape Γ }.nth (↑(n + 1) : ℤ)
Tactic: rw [add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
⊢ (move Dir.left { head := a, left := L, right := R : Tape Γ }).nth (HAdd.hAdd (α := ℤ) (↑(n + 1) : ℤ) 1) =
    { head := a, left := L, right := R : Tape Γ }.nth (↑(n + 1) : ℤ)
have change : (ListBlank.cons a R).nth (n + 1) = R.nth n
Tactic: change (R.cons a).nth (n + 1) = R.nth n
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
⊢ (ListBlank.cons a R).nth (n + 1) = R.nth n
have rw : (ListBlank.cons a R).tail.nth n = R.nth n
Tactic: rw [ListBlank.nth_succ, ListBlank.tail_cons]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
rw : (ListBlank.cons a R).tail.nth n = R.nth n
⊢ (ListBlank.cons a R).nth (n + 1) = R.nth n
have rw₁ : R.nth n = R.nth n
Tactic: rw [ListBlank.nth_succ, ListBlank.tail_cons]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
i : ℤ
| (move Dir.right T).nth i = T.nth (i + 1)
have rhs : T.nth (i + 1)
Tactic: rhs
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
i : ℤ
| T.nth (i + 1)
have rw : (move Dir.left (move Dir.right T)).nth (i + 1)
Tactic: rw [← T.move_right_left]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
i : ℤ
| (move Dir.right T).nth i = T.nth (i + 1)
have rw : (move Dir.left (move Dir.right T)).nth (i + 1)
Tactic: rhs; rw [← T.move_right_left]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
i : ℤ
⊢ (move Dir.right T).nth i = T.nth (i + 1)
have conv : (move Dir.right T).nth i = (move Dir.left (move Dir.right T)).nth (i + 1)
Tactic: conv => rhs; rw [← T.move_right_left]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
i : ℤ
⊢ (move Dir.right T).nth i = (move Dir.left (move Dir.right T)).nth (i + 1)
have rw : (move Dir.right T).nth i = (move Dir.right T).nth (i + 1 - 1)
Tactic: rw [Tape.move_left_nth, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
i : ℤ
rw : (move Dir.right T).nth i = (move Dir.right T).nth (i + 1 - 1)
⊢ (move Dir.right T).nth i = (move Dir.left (move Dir.right T)).nth (i + 1)
have rw₁ : (move Dir.right T).nth i = (move Dir.right T).nth i
Tactic: rw [Tape.move_left_nth, add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
i : ℕ
⊢ ((move Dir.right)^[i] T).head = T.nth (↑i : ℤ)
have zero : ∀ (T : Tape Γ), ((move Dir.right)^[0] T).head = T.nth (↑0 : ℤ)
Tactic: induction i generalizing T
Cleared hypotheses: T, i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
i : ℕ
zero : ∀ (T : Tape Γ), ((move Dir.right)^[0] T).head = T.nth (↑0 : ℤ)
⊢ ((move Dir.right)^[i] T).head = T.nth (↑i : ℤ)
have succ : ∀ (n : ℕ),
  (∀ (T : Tape Γ), ((move Dir.right)^[n] T).head = T.nth (↑n : ℤ)) →
    ∀ (T : Tape Γ), ((move Dir.right)^[n + 1] T).head = T.nth (↑(n + 1) : ℤ)
Tactic: induction i generalizing T
Cleared hypotheses: T, i
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
f : Γ → Γ
L R : ListBlank Γ
n : ℕ
⊢ write (f (R.nth n)) ((move Dir.right)^[n] (mk' L R)) = (move Dir.right)^[n] (mk' L (ListBlank.modifyNth f n R))
have zero : ∀ (L R : ListBlank Γ),
  write (f (R.nth 0)) ((move Dir.right)^[0] (mk' L R)) = (move Dir.right)^[0] (mk' L (ListBlank.modifyNth f 0 R))
Tactic: induction n generalizing L R
Cleared hypotheses: L, R, n
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
inst : Inhabited Γ
f : Γ → Γ
L R : ListBlank Γ
n : ℕ
zero :
  ∀ (L R : ListBlank Γ),
    write (f (R.nth 0)) ((move Dir.right)^[0] (mk' L R)) = (move Dir.right)^[0] (mk' L (ListBlank.modifyNth f 0 R))
⊢ write (f (R.nth n)) ((move Dir.right)^[n] (mk' L R)) = (move Dir.right)^[n] (mk' L (ListBlank.modifyNth f n R))
have succ : ∀ (n : ℕ),
  (∀ (L R : ListBlank Γ),
      write (f (R.nth n)) ((move Dir.right)^[n] (mk' L R)) = (move Dir.right)^[n] (mk' L (ListBlank.modifyNth f n R))) →
    ∀ (L R : ListBlank Γ),
      write (f (R.nth (n + 1))) ((move Dir.right)^[n + 1] (mk' L R)) =
        (move Dir.right)^[n + 1] (mk' L (ListBlank.modifyNth f (n + 1) R))
Tactic: induction n generalizing L R
Cleared hypotheses: L, R, n
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
T : Tape Γ
d : Dir
⊢ map f (move d T) = move d (map f T)
have mk : ∀ (head : Γ) (left right : ListBlank Γ),
  map f (move d { head := head, left := left, right := right : Tape Γ }) =
    move d (map f { head := head, left := left, right := right })
Tactic: cases T
Cleared hypotheses: T
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
d : Dir
head : Γ
left right : ListBlank Γ
⊢ map f (move d { head := head, left := left, right := right : Tape Γ }) =
    move d (map f { head := head, left := left, right := right })
have mk : map f (move Dir.left { head := head, left := left, right := right : Tape Γ }) =
  move Dir.left (map f { head := head, left := left, right := right })
Tactic: cases d
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.Tape (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
d : Dir
head : Γ
left right : ListBlank Γ
mk :
  map f (move Dir.left { head := head, left := left, right := right : Tape Γ }) =
    move Dir.left (map f { head := head, left := left, right := right })
⊢ map f (move d { head := head, left := left, right := right : Tape Γ }) =
    move d (map f { head := head, left := left, right := right })
have mk₁ : map f (move Dir.right { head := head, left := left, right := right : Tape Γ }) =
  move Dir.right (map f { head := head, left := left, right := right })
Tactic: cases d
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
a b : Λ'
⊢ Decidable (a = b)
have move : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → ((b : Λ') → Decidable (q = b)) → (b : Λ') → Decidable (move p k₁ k₂ q = b)
Tactic: induction a generalizing b
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
a b : Λ'
move :
  (p : Γ' → Bool) →
    (k₁ k₂ : K') → (q : Λ') → ((b : Λ') → Decidable (q = b)) → (b : Λ') → Decidable (Λ'.move p k₁ k₂ q = b)
⊢ Decidable (a = b)
have clear : (p : Γ' → Bool) → (k : K') → (q : Λ') → ((b : Λ') → Decidable (q = b)) → (b : Λ') → Decidable (clear p k q = b)
Tactic: induction a generalizing b
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
a b : Λ'
move :
  (p : Γ' → Bool) →
    (k₁ k₂ : K') → (q : Λ') → ((b : Λ') → Decidable (q = b)) → (b : Λ') → Decidable (Λ'.move p k₁ k₂ q = b)
clear :
  (p : Γ' → Bool) → (k : K') → (q : Λ') → ((b : Λ') → Decidable (q = b)) → (b : Λ') → Decidable (Λ'.clear p k q = b)
⊢ Decidable (a = b)
have copy : (q : Λ') → ((b : Λ') → Decidable (q = b)) → (b : Λ') → Decidable (q.copy = b)
Tactic: induction a generalizing b
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Computability.TuringMachine.ToPartrec (goal)
Goal:
a b : Λ'
move :
  (p : Γ' → Bool) →
    (k₁ k₂ : K') → (q : Λ') → ((b : Λ') → Decidable (q = b)) → (b : Λ') → Decidable (Λ'.move p k₁ k₂ q = b)
clear :
  (p : Γ' → Bool) → (k : K') → (q : Λ') → ((b : Λ') → Decidable (q = b)) → (b : Λ') → Decidable (Λ'.clear p k q = b)
copy : (q : Λ') → ((b : Λ') → Decidable (q = b)) → (b : Λ') → Decidable (q.copy = b)
⊢ Decidable (a = b)
have push : (k : K') →
  (s : Option Γ' → Option Γ') → (q : Λ') → ((b : Λ') → Decidable (q = b)) → (b : Λ') → Decidable (push k s q = b)
Tactic: induction a generalizing b
Cleared hypotheses: a, b