awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
L R : ListBlank Γ
n : ℕ
rw : (mk' L R).right₀.nth n = R.nth n
rw₁ rw₂ : R.nth n = R.nth n
⊢ (mk' L R).nth (↑n : ℤ) = R.nth n

Tactic:
rw [← Tape.right₀_nth, Tape.mk'_right₀]

Premises used: Turing.Tape.mk'_right₀, Turing.Tape.right₀_nth
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
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) : ℤ)
⊢ (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)

Tactic:
rw [add_sub_cancel_right]

Premises used: add_sub_cancel_right
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
change : (ListBlank.cons a R).nth (n + 1) = R.nth 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) : ℤ)

Tactic:
change (R.cons a).nth (n + 1) = R.nth n

Premises used: HAdd.hAdd, Turing.ListBlank.cons, Turing.ListBlank.nth, OfNat.ofNat
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
a : Γ
L R : ListBlank Γ
n : ℕ
rw : (ListBlank.cons a R).tail.nth n = R.nth n
rw₁ rw₂ : R.nth n = R.nth n
⊢ (ListBlank.cons a R).nth (n + 1) = R.nth n

Tactic:
rw [ListBlank.nth_succ, ListBlank.tail_cons]

Premises used: Turing.ListBlank.nth_succ, Turing.ListBlank.tail_cons
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
i : ℤ
rhs : T.nth (i + 1)
| (move Dir.right T).nth i = T.nth (i + 1)

Tactic:
rhs
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
i : ℤ
rw : (move Dir.left (move Dir.right T)).nth (i + 1)
| T.nth (i + 1)

Tactic:
rw [← T.move_right_left]

Premises used: Turing.Tape.move_right_left
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
i : ℤ
rw : (move Dir.left (move Dir.right T)).nth (i + 1)
| (move Dir.right T).nth i = T.nth (i + 1)

Tactic:
rhs; rw [← T.move_right_left]

Premises used: Turing.Tape.move_right_left
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
i : ℤ
conv : (move Dir.right T).nth i = (move Dir.left (move Dir.right T)).nth (i + 1)
⊢ (move Dir.right T).nth i = T.nth (i + 1)

Tactic:
conv => rhs; rw [← T.move_right_left]

Premises used: Turing.Tape.move_right_left
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
i : ℤ
rw : (move Dir.right T).nth i = (move Dir.right T).nth (i + 1 - 1)
rw₁ rw₂ : (move Dir.right T).nth i = (move Dir.right T).nth i
⊢ (move Dir.right T).nth i = (move Dir.left (move Dir.right T)).nth (i + 1)

Tactic:
rw [Tape.move_left_nth, add_sub_cancel_right]

Premises used: Turing.Tape.move_left_nth, add_sub_cancel_right
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
i : ℕ
zero : ∀ (T : Tape Γ), ((move Dir.right)^[0] T).head = T.nth (↑0 : ℤ)
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) : ℤ)
⊢ ((move Dir.right)^[i] T).head = T.nth (↑i : ℤ)

Tactic:
induction i generalizing T
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
T : Tape Γ
⊢ ((move Dir.right)^[0] T).head = T.nth (↑0 : ℤ)

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
n : ℕ
h : ∀ (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:
simp only [*, Tape.move_right_nth, Int.natCast_succ, iterate_succ, Function.comp_apply]

Premises used: Function.iterate_succ, Turing.Tape.move_right_nth, Int.natCast_succ, Function.comp_apply
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
head : Γ
left right : ListBlank Γ
⊢ write { head := head, left := left, right := right : Tape Γ }.head
      { head := head, left := left, right := right : Tape Γ } =
    { head := head, left := left, right := right }

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
a b : Γ
L R : ListBlank Γ
⊢ write b { head := a, left := L, right := R : Tape Γ } = { head := b, left := L, right := R }

Tactic:
rfl

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

Tactic:
simp [mk']

Premises used: Turing.Tape.mk'
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
head : Γ
left right : ListBlank Γ
⊢ (map f { head := head, left := left, right := right : Tape Γ }).head =
    f.f { head := head, left := left, right := right : Tape Γ }.head

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
b head : Γ
left right : ListBlank Γ
⊢ map f (write b { head := head, left := left, right := right : Tape Γ }) =
    write (f.f b) (map f { head := head, left := left, right := right })

Tactic:
rfl
-- Module: Mathlib.Computability.TuringMachine.Tape
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))
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))
⊢ write (f (R.nth n)) ((move Dir.right)^[n] (mk' L R)) = (move Dir.right)^[n] (mk' L (ListBlank.modifyNth f n R))

Tactic:
induction n generalizing L R
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
f : Γ → Γ
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:
simp [*]
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
inst : Inhabited Γ
f : Γ → Γ
n : ℕ
h :
  ∀ (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:
simp [*]
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
T : Tape Γ
d : Dir
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 })
⊢ map f (move d T) = move d (map f T)

Tactic:
cases T
-- Module: Mathlib.Computability.TuringMachine.Tape
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 })
mk₁ :
  map f (move Dir.right { head := head, left := left, right := right : Tape Γ }) =
    move Dir.right (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 })

Tactic:
cases d
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
head : Γ
left right : ListBlank Γ
⊢ map f (move Dir.left { head := head, left := left, right := right : Tape Γ }) =
    move Dir.left (map f { head := head, left := left, right := right })

Tactic:
simp only [Tape.move, Tape.map, ListBlank.head_map,
    ListBlank.map_cons, ListBlank.tail_map]

Premises used: Turing.ListBlank.head_map, Turing.Tape.map, Turing.ListBlank.map_cons, Turing.ListBlank.tail_map, Turing.Tape.move
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
head : Γ
left right : ListBlank Γ
⊢ map f (move Dir.right { head := head, left := left, right := right : Tape Γ }) =
    move Dir.right (map f { head := head, left := left, right := right })

Tactic:
simp only [Tape.move, Tape.map, ListBlank.head_map,
    ListBlank.map_cons, ListBlank.tail_map]

Premises used: Turing.ListBlank.head_map, Turing.Tape.map, Turing.ListBlank.map_cons, Turing.ListBlank.tail_map, Turing.Tape.move
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
L R : ListBlank Γ
⊢ map f (mk' L R) = mk' (ListBlank.map f L) (ListBlank.map f R)

Tactic:
simp only [Tape.mk', Tape.map, ListBlank.head_map,
    ListBlank.tail_map]

Premises used: Turing.ListBlank.head_map, Turing.Tape.mk', Turing.Tape.map, Turing.ListBlank.tail_map
-- Module: Mathlib.Computability.TuringMachine.Tape
Goal:
Γ : Type u_1
Γ' : Type u_2
inst : Inhabited Γ
inst_1 : Inhabited Γ'
f : PointedMap Γ Γ'
L R : List Γ
⊢ map f (mk₂ L R) = mk₂ (List.map f.f L) (List.map f.f R)

Tactic:
simp only [Tape.mk₂, Tape.map_mk', ListBlank.map_mk]

Premises used: Turing.Tape.mk₂, Turing.ListBlank.map_mk, Turing.Tape.map_mk'
-- 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:
Tape.map_mk₂ _ _ _

Premises used: List.map, Turing.Tape.map_mk₂, Turing.Tape.mk₁
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
⊢ default = Γ'.consₗ

Tactic:
rfl

Premises used: Turing.PartrecToTM2.instInhabitedΓ'.default, rfl
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
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)
push :
  (k : K') →
    (s : Option Γ' → Option Γ') → (q : Λ') → ((b : Λ') → Decidable (q = b)) → (b : Λ') → Decidable (Λ'.push k s q = b)
read : (f : Option Γ' → Λ') → ((a : Option Γ') → (b : Λ') → Decidable (f a = b)) → (b : Λ') → Decidable (Λ'.read f = b)
succ : (q : Λ') → ((b : Λ') → Decidable (q = b)) → (b : Λ') → Decidable (q.succ = b)
pred :
  (q₁ q₂ : Λ') →
    ((b : Λ') → Decidable (q₁ = b)) → ((b : Λ') → Decidable (q₂ = b)) → (b : Λ') → Decidable (q₁.pred q₂ = b)
ret : (k : Cont') → (b : Λ') → Decidable (Λ'.ret k = b)
⊢ Decidable (a = b)

Tactic:
induction a generalizing b
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
b : Λ'
move : (p_1 : Γ' → Bool) → (k₁_1 k₂_1 : K') → (q_1 : Λ') → Decidable (Λ'.move p k₁ k₂ q = Λ'.move p_1 k₁_1 k₂_1 q_1)
move₁ : (p_1 : Γ' → Bool) → (k : K') → (q_1 : Λ') → Decidable (Λ'.move p k₁ k₂ q = clear p_1 k q_1)
move₂ : (q_1 : Λ') → Decidable (Λ'.move p k₁ k₂ q = q_1.copy)
move₃ : (k : K') → (s : Option Γ' → Option Γ') → (q_1 : Λ') → Decidable (Λ'.move p k₁ k₂ q = push k s q_1)
move₄ : (f : Option Γ' → Λ') → Decidable (Λ'.move p k₁ k₂ q = read f)
move₅ : (q_1 : Λ') → Decidable (Λ'.move p k₁ k₂ q = q_1.succ)
move₆ : (q₁ q₂ : Λ') → Decidable (Λ'.move p k₁ k₂ q = q₁.pred q₂)
move₇ : (k : Cont') → Decidable (Λ'.move p k₁ k₂ q = ret k)
⊢ Decidable (Λ'.move p k₁ k₂ q = b)

Tactic:
cases b
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
b : Λ'
clear : (p_1 : Γ' → Bool) → (k₁ k₂ : K') → (q_1 : Λ') → Decidable (Λ'.clear p k q = move p_1 k₁ k₂ q_1)
clear₁ : (p_1 : Γ' → Bool) → (k_1 : K') → (q_1 : Λ') → Decidable (Λ'.clear p k q = Λ'.clear p_1 k_1 q_1)
clear₂ : (q_1 : Λ') → Decidable (Λ'.clear p k q = q_1.copy)
clear₃ : (k_1 : K') → (s : Option Γ' → Option Γ') → (q_1 : Λ') → Decidable (Λ'.clear p k q = push k_1 s q_1)
clear₄ : (f : Option Γ' → Λ') → Decidable (Λ'.clear p k q = read f)
clear₅ : (q_1 : Λ') → Decidable (Λ'.clear p k q = q_1.succ)
clear₆ : (q₁ q₂ : Λ') → Decidable (Λ'.clear p k q = q₁.pred q₂)
clear₇ : (k_1 : Cont') → Decidable (Λ'.clear p k q = ret k_1)
⊢ Decidable (Λ'.clear p k q = b)

Tactic:
cases b
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
b : Λ'
copy : (p : Γ' → Bool) → (k₁ k₂ : K') → (q_1 : Λ') → Decidable (q.copy = move p k₁ k₂ q_1)
copy₁ : (p : Γ' → Bool) → (k : K') → (q_1 : Λ') → Decidable (q.copy = clear p k q_1)
copy₂ : (q_1 : Λ') → Decidable (q.copy = q_1.copy)
copy₃ : (k : K') → (s : Option Γ' → Option Γ') → (q_1 : Λ') → Decidable (q.copy = push k s q_1)
copy₄ : (f : Option Γ' → Λ') → Decidable (q.copy = read f)
copy₅ : (q_1 : Λ') → Decidable (q.copy = q_1.succ)
copy₆ : (q₁ q₂ : Λ') → Decidable (q.copy = q₁.pred q₂)
copy₇ : (k : Cont') → Decidable (q.copy = ret k)
⊢ Decidable (q.copy = b)

Tactic:
cases b
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
b : Λ'
push : (p : Γ' → Bool) → (k₁ k₂ : K') → (q_1 : Λ') → Decidable (Λ'.push k s q = move p k₁ k₂ q_1)
push₁ : (p : Γ' → Bool) → (k_1 : K') → (q_1 : Λ') → Decidable (Λ'.push k s q = clear p k_1 q_1)
push₂ : (q_1 : Λ') → Decidable (Λ'.push k s q = q_1.copy)
push₃ : (k_1 : K') → (s_1 : Option Γ' → Option Γ') → (q_1 : Λ') → Decidable (Λ'.push k s q = Λ'.push k_1 s_1 q_1)
push₄ : (f : Option Γ' → Λ') → Decidable (Λ'.push k s q = read f)
push₅ : (q_1 : Λ') → Decidable (Λ'.push k s q = q_1.succ)
push₆ : (q₁ q₂ : Λ') → Decidable (Λ'.push k s q = q₁.pred q₂)
push₇ : (k_1 : Cont') → Decidable (Λ'.push k s q = ret k_1)
⊢ Decidable (Λ'.push k s q = b)

Tactic:
cases b
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Option Γ' → Λ'
f_ih : (a : Option Γ') → (b : Λ') → Decidable (f a = b)
b : Λ'
read : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (Λ'.read f = move p k₁ k₂ q)
read₁ : (p : Γ' → Bool) → (k : K') → (q : Λ') → Decidable (Λ'.read f = clear p k q)
read₂ : (q : Λ') → Decidable (Λ'.read f = q.copy)
read₃ : (k : K') → (s : Option Γ' → Option Γ') → (q : Λ') → Decidable (Λ'.read f = push k s q)
read₄ : (f_1 : Option Γ' → Λ') → Decidable (Λ'.read f = Λ'.read f_1)
read₅ : (q : Λ') → Decidable (Λ'.read f = q.succ)
read₆ : (q₁ q₂ : Λ') → Decidable (Λ'.read f = q₁.pred q₂)
read₇ : (k : Cont') → Decidable (Λ'.read f = ret k)
⊢ Decidable (Λ'.read f = b)

Tactic:
cases b
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
b : Λ'
succ : (p : Γ' → Bool) → (k₁ k₂ : K') → (q_1 : Λ') → Decidable (q.succ = move p k₁ k₂ q_1)
succ₁ : (p : Γ' → Bool) → (k : K') → (q_1 : Λ') → Decidable (q.succ = clear p k q_1)
succ₂ : (q_1 : Λ') → Decidable (q.succ = q_1.copy)
succ₃ : (k : K') → (s : Option Γ' → Option Γ') → (q_1 : Λ') → Decidable (q.succ = push k s q_1)
succ₄ : (f : Option Γ' → Λ') → Decidable (q.succ = read f)
succ₅ : (q_1 : Λ') → Decidable (q.succ = q_1.succ)
succ₆ : (q₁ q₂ : Λ') → Decidable (q.succ = q₁.pred q₂)
succ₇ : (k : Cont') → Decidable (q.succ = ret k)
⊢ Decidable (q.succ = b)

Tactic:
cases b
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
q₁_ih : (b : Λ') → Decidable (q₁ = b)
q₂_ih : (b : Λ') → Decidable (q₂ = b)
b : Λ'
pred : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (q₁.pred q₂ = move p k₁ k₂ q)
pred₁ : (p : Γ' → Bool) → (k : K') → (q : Λ') → Decidable (q₁.pred q₂ = clear p k q)
pred₂ : (q : Λ') → Decidable (q₁.pred q₂ = q.copy)
pred₃ : (k : K') → (s : Option Γ' → Option Γ') → (q : Λ') → Decidable (q₁.pred q₂ = push k s q)
pred₄ : (f : Option Γ' → Λ') → Decidable (q₁.pred q₂ = read f)
pred₅ : (q : Λ') → Decidable (q₁.pred q₂ = q.succ)
pred₆ : (q₁_1 q₂_1 : Λ') → Decidable (q₁.pred q₂ = q₁_1.pred q₂_1)
pred₇ : (k : Cont') → Decidable (q₁.pred q₂ = ret k)
⊢ Decidable (q₁.pred q₂ = b)

Tactic:
cases b
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : Cont'
b : Λ'
ret : (p : Γ' → Bool) → (k₁ k₂ : K') → (q : Λ') → Decidable (Λ'.ret k = move p k₁ k₂ q)
ret₁ : (p : Γ' → Bool) → (k_1 : K') → (q : Λ') → Decidable (Λ'.ret k = clear p k_1 q)
ret₂ : (q : Λ') → Decidable (Λ'.ret k = q.copy)
ret₃ : (k_1 : K') → (s : Option Γ' → Option Γ') → (q : Λ') → Decidable (Λ'.ret k = push k_1 s q)
ret₄ : (f : Option Γ' → Λ') → Decidable (Λ'.ret k = read f)
ret₅ : (q : Λ') → Decidable (Λ'.ret k = q.succ)
ret₆ : (q₁ q₂ : Λ') → Decidable (Λ'.ret k = q₁.pred q₂)
ret₇ : (k_1 : Cont') → Decidable (Λ'.ret k = Λ'.ret k_1)
⊢ Decidable (Λ'.ret k = b)

Tactic:
cases b
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
p' : Γ' → Bool
k₁' k₂' : K'
q' : Λ'
⊢ move p k₁ k₂ q = move p' k₁' k₂' q' ↔ p = p' ∧ k₁ = k₁' ∧ k₂ = k₂' ∧ q = q'

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
p' : Γ' → Bool
k₁' k₂' : K'
q' : Λ'
⊢ Decidable (move p k₁ k₂ q = move p' k₁' k₂' q')

Tactic:
exact decidable_of_iff' (p = p' ∧ k₁ = k₁' ∧ k₂ = k₂' ∧ q = q') (by simp)

Premises used: And, decidable_of_iff', Eq
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
p_1 : Γ' → Bool
k₁_1 k₂_1 : K'
q_1 : Λ'
⊢ Decidable (move p k₁ k₂ q = move p_1 k₁_1 k₂_1 q_1)

Tactic:
case move.move p k₁ k₂ q _ p' k₁' k₂' q' =>
    exact decidable_of_iff' (p = p' ∧ k₁ = k₁' ∧ k₂ = k₂' ∧ q = q') (by simp)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
p' : Γ' → Bool
k' : K'
q' : Λ'
⊢ clear p k q = clear p' k' q' ↔ p = p' ∧ k = k' ∧ q = q'

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
p' : Γ' → Bool
k' : K'
q' : Λ'
⊢ Decidable (clear p k q = clear p' k' q')

Tactic:
exact decidable_of_iff' (p = p' ∧ k = k' ∧ q = q') (by simp)

Premises used: And, decidable_of_iff', Eq
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
p_1 : Γ' → Bool
k_1 : K'
q_1 : Λ'
⊢ Decidable (clear p k q = clear p_1 k_1 q_1)

Tactic:
case clear.clear p k q _ p' k' q' => exact decidable_of_iff' (p = p' ∧ k = k' ∧ q = q') (by simp)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
q' : Λ'
⊢ q.copy = q'.copy ↔ q = q'

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
q' : Λ'
⊢ Decidable (q.copy = q'.copy)

Tactic:
exact decidable_of_iff' (q = q') (by simp)

Premises used: decidable_of_iff', Eq
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
q_1 : Λ'
⊢ Decidable (q.copy = q_1.copy)

Tactic:
case copy.copy q _ q' => exact decidable_of_iff' (q = q') (by simp)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
k' : K'
s' : Option Γ' → Option Γ'
q' : Λ'
⊢ push k s q = push k' s' q' ↔ k = k' ∧ s = s' ∧ q = q'

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
k' : K'
s' : Option Γ' → Option Γ'
q' : Λ'
⊢ Decidable (push k s q = push k' s' q')

Tactic:
exact decidable_of_iff' (k = k' ∧ s = s' ∧ q = q') (by simp)

Premises used: And, decidable_of_iff', Eq
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k : K'
s : Option Γ' → Option Γ'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
k_1 : K'
s_1 : Option Γ' → Option Γ'
q_1 : Λ'
⊢ Decidable (push k s q = push k_1 s_1 q_1)

Tactic:
case push.push k s q _ k' s' q' => exact decidable_of_iff' (k = k' ∧ s = s' ∧ q = q') (by simp)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Option Γ' → Λ'
f_ih : (a : Option Γ') → (b : Λ') → Decidable (f a = b)
f' : Option Γ' → Λ'
⊢ read f = read f' ↔ ∀ (a : Option Γ'), f a = f' a

Tactic:
simp [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Option Γ' → Λ'
f_ih : (a : Option Γ') → (b : Λ') → Decidable (f a = b)
f' : Option Γ' → Λ'
⊢ Decidable (read f = read f')

Tactic:
exact decidable_of_iff' (∀ a, f a = f' a) (by simp [funext_iff])

Premises used: decidable_of_iff'
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
f : Option Γ' → Λ'
f_ih : (a : Option Γ') → (b : Λ') → Decidable (f a = b)
f_1 : Option Γ' → Λ'
⊢ Decidable (read f = read f_1)

Tactic:
case read.read f _ f' => exact decidable_of_iff' (∀ a, f a = f' a) (by simp [funext_iff])
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
q' : Λ'
⊢ q.succ = q'.succ ↔ q = q'

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
q' : Λ'
⊢ Decidable (q.succ = q'.succ)

Tactic:
exact decidable_of_iff' (q = q') (by simp)

Premises used: decidable_of_iff', Eq
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
q_1 : Λ'
⊢ Decidable (q.succ = q_1.succ)

Tactic:
case succ.succ q _ q' => exact decidable_of_iff' (q = q') (by simp)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
q₁_ih : (b : Λ') → Decidable (q₁ = b)
q₂_ih : (b : Λ') → Decidable (q₂ = b)
q₁' q₂' : Λ'
⊢ q₁.pred q₂ = q₁'.pred q₂' ↔ q₁ = q₁' ∧ q₂ = q₂'

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
q₁_ih : (b : Λ') → Decidable (q₁ = b)
q₂_ih : (b : Λ') → Decidable (q₂ = b)
q₁' q₂' : Λ'
⊢ Decidable (q₁.pred q₂ = q₁'.pred q₂')

Tactic:
exact decidable_of_iff' (q₁ = q₁' ∧ q₂ = q₂') (by simp)

Premises used: And, decidable_of_iff', Eq
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
q₁ q₂ : Λ'
q₁_ih : (b : Λ') → Decidable (q₁ = b)
q₂_ih : (b : Λ') → Decidable (q₂ = b)
q₁_1 q₂_1 : Λ'
⊢ Decidable (q₁.pred q₂ = q₁_1.pred q₂_1)

Tactic:
case pred.pred q₁ q₂ _ _ q₁' q₂' => exact decidable_of_iff' (q₁ = q₁' ∧ q₂ = q₂') (by simp)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k k' : Cont'
⊢ ret k = ret k' ↔ k = k'

Tactic:
simp
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k k' : Cont'
⊢ Decidable (ret k = ret k')

Tactic:
exact decidable_of_iff' (k = k') (by simp)

Premises used: decidable_of_iff', Eq
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
k k_1 : Cont'
⊢ Decidable (ret k = ret k_1)

Tactic:
case ret.ret k k' => exact decidable_of_iff' (k = k') (by simp)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
p_1 : Γ' → Bool
k : K'
q_1 : Λ'
⊢ Decidable (move p k₁ k₂ q = clear p_1 k q_1)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)
-- Module: Mathlib.Computability.TuringMachine.ToPartrec
Goal:
p : Γ' → Bool
k₁ k₂ : K'
q : Λ'
q_ih : (b : Λ') → Decidable (q = b)
q_1 : Λ'
⊢ Decidable (move p k₁ k₂ q = q_1.copy)

Tactic:
exact .isFalse (by rintro ⟨⟨⟩⟩)