mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Computability.NFA

Goal state before:
pp: α : Type u
σ : Type v
M : NFA α σ
S : Set σ
p : Prop
x : List α
⊢ x ∈ M.acceptsFrom {s | s ∈ S ∧ p} ↔ x ∈ M.acceptsFrom S ∧ p

Tactic:
by
  induction x generalizing S with
  | nil => simp only [nil_mem_acceptsFrom, mem_ofPred_eq]; tauto
  | cons a x ih =>
    have h : M.stepSet {s ∈ S | p} a = {s ∈ M.stepSet S a | p} := by
      ext s; simp only [stepSet, mem_ofPred_eq, mem_iUnion, exists_prop]; tauto
    simp [h, ih]

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case append_singleton
α : Type u
σ : Type v
M : εNFA α σ
x : List α
a : α
ih : M.evalFrom ∅ x = ∅
⊢ M.evalFrom ∅ (x ++ [a]) = ∅

Tactic:
evalFrom_append_singleton,

Goal state after:
case append_singleton
α : Type u
σ : Type v
M : εNFA α σ
x : List α
a : α
ih : M.evalFrom ∅ x = ∅
⊢ M.stepSet (M.evalFrom ∅ x) a = ∅
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case append_singleton
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l✝ : List α
a✝ : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l✝ ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l✝
s : σ
⊢ s ∈ M.evalFrom S (l✝ ++ [a✝]) ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} (l✝ ++ [a✝])

Tactic:
evalFrom_append_singleton,

Goal state after:
case append_singleton
α : Type u
σ : Type v
M : εNFA α σ
S : Set σ
l✝ : List α
a✝ : α
ih : ∀ {s : σ}, s ∈ M.evalFrom S l✝ ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} l✝
s : σ
⊢ s ∈ M.stepSet (M.evalFrom S l✝) a✝ ↔ ∃ t ∈ S, s ∈ M.stepSet (M.evalFrom {t} l✝) a✝
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: b : Bool
n : ℕ
ih : ofNat' (n + 1) = ofNat' n + 1
⊢ ofNat' (Nat.bit b n + 1) = ofNat' (Nat.bit b n) + 1

Tactic:
by
    cases b
    · erw [ofNat'_bit true n, ofNat'_bit]
      simp only [← bit1_of_bit1, ← bit0_of_bit0, cond]
    · rw [show n.bit true + 1 = (n + 1).bit false by simp [Nat.bit, mul_add],
        ofNat'_bit, ofNat'_bit, ih]
      simp only [cond, add_one, bit1_succ]

Goal state after:
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: a b c : Num
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
transfer_rw; apply le_trans

Goal state after:
Module: Mathlib.Computability.EpsilonNFA

Goal state before:
pp: case append_singleton
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
⊢ s₂ ∈ M.evalFrom {s₁} (x ++ [a]) ↔ ∃ x', x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'

Tactic:
evalFrom_append_singleton,

Goal state after:
case append_singleton
α : Type u
σ : Type v
M : εNFA α σ
s₁ : σ
x : List α
a : α
ih : ∀ {s₂ : σ}, s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x'
s₂ : σ
⊢ s₂ ∈ M.stepSet (M.evalFrom {s₁} x) a ↔ ∃ x', x'.reduceOption = x ++ [a] ∧ M.IsPath s₁ s₂ x'
Module: Mathlib.Data.Num.Lemmas

Goal state before:
pp: p : PosNum
⊢ castNum <$> (pos p).ppred = (↑(pos p)).ppred

Tactic:
by
    rw [ppred, Option.map_eq_map, Option.map_some, Nat.ppred_eq_some.2]
    rw [PosNum.pred'_to_nat, Nat.succ_pred_eq_of_pos (PosNum.to_nat_pos _)]
    rfl

Goal state after:
Module: Mathlib.Computability.TuringMachine.Tape

Goal state before:
pp: case inr
Γ : Type ?u.5
inst✝ : Inhabited Γ
l✝ : ListBlank Γ
n : ℕ
l : List Γ
i : ℕ
h : l.length ≤ n
⊢ l.getI n = (l ++ List.replicate i default).getI n

Tactic:
List.getI_eq_default _ h

Goal state after:
case inr
Γ : Type ?u.5
inst✝ : Inhabited Γ
l✝ : ListBlank Γ
n : ℕ
l : List Γ
i : ℕ
h : l.length ≤ n
⊢ default = (l ++ List.replicate i default).getI n
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case right.some.some.branch
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ),
    some q₁ ∈ TM1.stmts M S →
      some (trAux M a q₁ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₁ → some val✝ ∈ TM1.stmts M S
IH₂ :
  ∀ (v : σ),
    some q₂ ∈ TM1.stmts M S →
      some (trAux M a q₂ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₂ → some val✝ ∈ TM1.stmts M S
v : σ
h₂ : some (TM1.Stmt.branch p q₁ q₂) ∈ TM1.stmts M S
h₁ : some (trAux M a (TM1.Stmt.branch p q₁ q₂) v) = some ((some val✝, v'), s)
hs : TM1.SupportsStmt S (TM1.Stmt.branch p q₁ q₂)
⊢ some val✝ ∈ TM1.stmts M S

Tactic:
cases h : p a v

Goal state after:
case right.some.some.branch.false
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ),
    some q₁ ∈ TM1.stmts M S →
      some (trAux M a q₁ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₁ → some val✝ ∈ TM1.stmts M S
IH₂ :
  ∀ (v : σ),
    some q₂ ∈ TM1.stmts M S →
      some (trAux M a q₂ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₂ → some val✝ ∈ TM1.stmts M S
v : σ
h₂ : some (TM1.Stmt.branch p q₁ q₂) ∈ TM1.stmts M S
h₁ : some (trAux M a (TM1.Stmt.branch p q₁ q₂) v) = some ((some val✝, v'), s)
hs : TM1.SupportsStmt S (TM1.Stmt.branch p q₁ q₂)
h : p a v = false
⊢ some val✝ ∈ TM1.stmts M S

case right.some.some.branch.true
Γ : Type u_1
Λ : Type u_2
inst✝² : Inhabited Λ
σ : Type u_3
inst✝¹ : Inhabited σ
M : Λ → TM1.Stmt Γ Λ σ
inst✝ : Fintype σ
S : Finset Λ
ss : TM1.Supports M S
a : Γ
s : TM0.Stmt Γ
v' : σ
val✝ : TM1.Stmt Γ Λ σ
p : Γ → σ → Bool
q₁ q₂ : TM1.Stmt Γ Λ σ
IH₁ :
  ∀ (v : σ),
    some q₁ ∈ TM1.stmts M S →
      some (trAux M a q₁ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₁ → some val✝ ∈ TM1.stmts M S
IH₂ :
  ∀ (v : σ),
    some q₂ ∈ TM1.stmts M S →
      some (trAux M a q₂ v) = some ((some val✝, v'), s) → TM1.SupportsStmt S q₂ → some val✝ ∈ TM1.stmts M S
v : σ
h₂ : some (TM1.Stmt.branch p q₁ q₂) ∈ TM1.stmts M S
h₁ : some (trAux M a (TM1.Stmt.branch p q₁ q₂) v) = some ((some val✝, v'), s)
hs : TM1.SupportsStmt S (TM1.Stmt.branch p q₁ q₂)
h : p a v = true
⊢ some val✝ ∈ TM1.stmts M S
Module: Mathlib.Computability.TuringMachine.PostTuringMachine

Goal state before:
pp: case nil
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
l₁ l₂' : List Bool
e : l₂'.length = [].length
⊢ stepAux (write [] q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append l₂' R')) =
    stepAux q v (Tape.mk' (ListBlank.append ([].reverseAux l₁) L') R')

Tactic:
cases List.length_eq_zero_iff.1 e

Goal state after:
case nil.refl
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
n : ℕ
enc : Γ → List.Vector Bool n
inst✝ : Inhabited Γ
enc0 : enc default = List.Vector.replicate n false
q : Stmt Bool (Λ' Γ Λ σ) σ
v : σ
L' R' : ListBlank Bool
l₁ : List Bool
e : [].length = [].length
⊢ stepAux (write [] q) v (Tape.mk' (ListBlank.append l₁ L') (ListBlank.append [] R')) =
    stepAux q v (Tape.mk' (ListBlank.append ([].reverseAux l₁) L') R')
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case prim.comp
n : ℕ
f : List.Vector ℕ n →. ℕ
n✝¹ : ℕ
f✝¹ : List.Vector ℕ n✝¹ → ℕ
m✝ n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
g : Fin n✝ → List.Vector ℕ m✝ → ℕ
hf : Nat.Primrec' f✝
hg : ∀ (i : Fin n✝), Nat.Primrec' (g i)
IHf : ∃ c, ∀ (v : List.Vector ℕ n✝), c.eval ↑v = pure <$> ↑f✝ v
IHg : ∀ (i : Fin n✝), ∃ c, ∀ (v : List.Vector ℕ m✝), c.eval ↑v = pure <$> ↑(g i) v
⊢ ∃ c, ∀ (v : List.Vector ℕ m✝), c.eval ↑v = pure <$> (↑fun a ↦ f✝ (List.Vector.ofFn fun i ↦ g i a)) v

Tactic:
simpa [Part.bind_eq_bind] using exists_code.comp IHf IHg

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case prim.prec.zero
n✝¹ : ℕ
f✝¹ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f✝ : List.Vector ℕ n✝ → ℕ
n : ℕ
f : List.Vector ℕ n → ℕ
g : List.Vector ℕ (n + 2) → ℕ
a✝¹ : Nat.Primrec' f
a✝ : Nat.Primrec' g
cf cg : Code
v : List.Vector ℕ (n + 1)
hf : cf.eval (↑v).tail = pure (pure (f v.tail))
hg : ∀ (a b : ℕ), cg.eval (a :: b :: (↑v).tail) = pure (pure (g (a ::ᵥ b ::ᵥ v.tail)))
⊢ (cf.prec cg).eval (0 :: (↑v).tail) =
    pure (pure (Nat.rec (f (0 ::ᵥ v.tail).tail) (fun y IH ↦ g (y ::ᵥ IH ::ᵥ (0 ::ᵥ v.tail).tail)) (0 ::ᵥ v.tail).head))

Tactic:
simp [prec, hf, Bind.bind]

Goal state after:
Module: Mathlib.Computability.TuringMachine.Config

Goal state before:
pp: case pos
n✝¹ : ℕ
f✝ : List.Vector ℕ n✝¹ →. ℕ
n✝ : ℕ
f : List.Vector ℕ (n✝ + 1) → ℕ
a✝ : Nat.Partrec' ↑f
cf : Code
v : List.Vector ℕ n✝
hf : ∀ (a : ℕ), cf.eval (a :: ↑v) = Part.some [f (a ::ᵥ v)]
v' v₀ : List ℕ
n : ℕ
h2 :
  v' ∈
    PFun.fix
      (fun v ↦
        (cf.eval v).bind fun y ↦
          Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
      (n :: ↑v)
IH :
  ∀ (a'' : List ℕ),
    (Sum.inr a'' ∈
        (cf.eval (n :: ↑v)).bind fun y ↦
          Part.some
            (if y.headI = 0 then Sum.inl ((n :: ↑v).headI.succ :: (n :: ↑v).tail)
            else Sum.inr ((n :: ↑v).headI.succ :: (n :: ↑v).tail))) →
      ∀ (n : ℕ),
        a'' = n :: ↑v →
          (∀ m < n, ¬f (m ::ᵥ v) = 0) →
            ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]
hm : ∀ m < n, ¬f (m ::ᵥ v) = 0
h : [f (n ::ᵥ v)].headI = 0
this :
  Sum.inl v' ∈ Part.some (Sum.inl ((n :: ↑v).headI.succ :: (n :: ↑v).tail)) ∨
    ∃ a',
      Sum.inr a' ∈ Part.some (Sum.inl ((n :: ↑v).headI.succ :: (n :: ↑v).tail)) ∧
        v' ∈
          PFun.fix
            (fun v ↦
              (cf.eval v).bind fun y ↦
                Part.some (if y.headI = 0 then Sum.inl (v.headI.succ :: v.tail) else Sum.inr (v.headI.succ :: v.tail)))
            a'
⊢ ∃ a, (f (a ::ᵥ v) = 0 ∧ ∀ {m : ℕ}, m < a → ¬f (m ::ᵥ v) = 0) ∧ [a] = [v'.headI.pred]

Tactic:
simp only [List.headI_cons, exists_false, or_false, Part.mem_some_iff,
          List.tail_cons, false_and, Sum.inl.injEq, reduceCtorEq] at this
        subst this
        exact ⟨_, ⟨h, @hm⟩, rfl⟩

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case move.clear
p✝¹ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ Decidable (move p✝¹ k₁✝ k₂✝ q✝¹ = clear p✝ k✝ q✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case move.copy
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ Decidable (move p✝ k₁✝ k₂✝ q✝¹ = q✝.copy)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case move.push
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ Decidable (move p✝ k₁✝ k₂✝ q✝¹ = push k✝ s✝ q✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case move.read
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
f✝ : Option Γ' → Λ'
⊢ Decidable (move p✝ k₁✝ k₂✝ q✝ = read f✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case move.succ
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ Decidable (move p✝ k₁✝ k₂✝ q✝¹ = q✝.succ)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case move.pred
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
q₁✝ q₂✝ : Λ'
⊢ Decidable (move p✝ k₁✝ k₂✝ q✝ = q₁✝.pred q₂✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case move.ret
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
k✝ : Cont'
⊢ Decidable (move p✝ k₁✝ k₂✝ q✝ = ret k✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case clear.move
p✝¹ : Γ' → Bool
k✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ Decidable (clear p✝¹ k✝ q✝¹ = move p✝ k₁✝ k₂✝ q✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case clear.copy
p✝ : Γ' → Bool
k✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ Decidable (clear p✝ k✝ q✝¹ = q✝.copy)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case clear.push
p✝ : Γ' → Bool
k✝¹ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ Decidable (clear p✝ k✝¹ q✝¹ = push k✝ s✝ q✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case clear.read
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
f✝ : Option Γ' → Λ'
⊢ Decidable (clear p✝ k✝ q✝ = read f✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case clear.succ
p✝ : Γ' → Bool
k✝ : K'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ Decidable (clear p✝ k✝ q✝¹ = q✝.succ)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case clear.pred
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
q₁✝ q₂✝ : Λ'
⊢ Decidable (clear p✝ k✝ q✝ = q₁✝.pred q₂✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case clear.ret
p✝ : Γ' → Bool
k✝¹ : K'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
k✝ : Cont'
⊢ Decidable (clear p✝ k✝¹ q✝ = ret k✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case copy.move
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ Decidable (q✝¹.copy = move p✝ k₁✝ k₂✝ q✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case copy.clear
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ Decidable (q✝¹.copy = clear p✝ k✝ q✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case copy.push
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ Decidable (q✝¹.copy = push k✝ s✝ q✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case copy.read
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
f✝ : Option Γ' → Λ'
⊢ Decidable (q✝.copy = read f✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case copy.succ
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ Decidable (q✝¹.copy = q✝.succ)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case copy.pred
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
q₁✝ q₂✝ : Λ'
⊢ Decidable (q✝.copy = q₁✝.pred q₂✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case copy.ret
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
k✝ : Cont'
⊢ Decidable (q✝.copy = ret k✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case push.move
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ Decidable (push k✝ s✝ q✝¹ = move p✝ k₁✝ k₂✝ q✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case push.clear
k✝¹ : K'
s✝ : Option Γ' → Option Γ'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ Decidable (push k✝¹ s✝ q✝¹ = clear p✝ k✝ q✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case push.copy
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ Decidable (push k✝ s✝ q✝¹ = q✝.copy)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case push.read
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
f✝ : Option Γ' → Λ'
⊢ Decidable (push k✝ s✝ q✝ = read f✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case push.succ
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ Decidable (push k✝ s✝ q✝¹ = q✝.succ)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case push.pred
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
q₁✝ q₂✝ : Λ'
⊢ Decidable (push k✝ s✝ q✝ = q₁✝.pred q₂✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case push.ret
k✝¹ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
k✝ : Cont'
⊢ Decidable (push k✝¹ s✝ q✝ = ret k✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case read.move
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ Decidable (read f✝ = move p✝ k₁✝ k₂✝ q✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case read.clear
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ Decidable (read f✝ = clear p✝ k✝ q✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case read.copy
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
q✝ : Λ'
⊢ Decidable (read f✝ = q✝.copy)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case read.push
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ Decidable (read f✝ = push k✝ s✝ q✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case read.succ
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
q✝ : Λ'
⊢ Decidable (read f✝ = q✝.succ)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case read.pred
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
q₁✝ q₂✝ : Λ'
⊢ Decidable (read f✝ = q₁✝.pred q₂✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case read.ret
f✝ : Option Γ' → Λ'
f_ih✝ : (a : Option Γ') → (b : Λ') → Decidable (f✝ a = b)
k✝ : Cont'
⊢ Decidable (read f✝ = ret k✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case succ.move
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ Decidable (q✝¹.succ = move p✝ k₁✝ k₂✝ q✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case succ.clear
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ Decidable (q✝¹.succ = clear p✝ k✝ q✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case succ.copy
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
q✝ : Λ'
⊢ Decidable (q✝¹.succ = q✝.copy)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case succ.push
q✝¹ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝¹ = b)
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ Decidable (q✝¹.succ = push k✝ s✝ q✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case succ.read
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
f✝ : Option Γ' → Λ'
⊢ Decidable (q✝.succ = read f✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case succ.pred
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
q₁✝ q₂✝ : Λ'
⊢ Decidable (q✝.succ = q₁✝.pred q₂✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case succ.ret
q✝ : Λ'
q_ih✝ : (b : Λ') → Decidable (q✝ = b)
k✝ : Cont'
⊢ Decidable (q✝.succ = ret k✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pred.move
q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ Decidable (q₁✝.pred q₂✝ = move p✝ k₁✝ k₂✝ q✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pred.clear
q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ Decidable (q₁✝.pred q₂✝ = clear p✝ k✝ q✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pred.copy
q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
q✝ : Λ'
⊢ Decidable (q₁✝.pred q₂✝ = q✝.copy)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pred.push
q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
k✝ : K'
s✝ : Option Γ' → Option Γ'
q✝ : Λ'
⊢ Decidable (q₁✝.pred q₂✝ = push k✝ s✝ q✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pred.read
q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
f✝ : Option Γ' → Λ'
⊢ Decidable (q₁✝.pred q₂✝ = read f✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pred.succ
q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
q✝ : Λ'
⊢ Decidable (q₁✝.pred q₂✝ = q✝.succ)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case pred.ret
q₁✝ q₂✝ : Λ'
q₁_ih✝ : (b : Λ') → Decidable (q₁✝ = b)
q₂_ih✝ : (b : Λ') → Decidable (q₂✝ = b)
k✝ : Cont'
⊢ Decidable (q₁✝.pred q₂✝ = ret k✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case ret.move
k✝ : Cont'
p✝ : Γ' → Bool
k₁✝ k₂✝ : K'
q✝ : Λ'
⊢ Decidable (ret k✝ = move p✝ k₁✝ k₂✝ q✝)

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

Goal state after:
Module: Mathlib.Computability.TuringMachine.ToPartrec

Goal state before:
pp: case ret.clear
k✝¹ : Cont'
p✝ : Γ' → Bool
k✝ : K'
q✝ : Λ'
⊢ Decidable (ret k✝¹ = clear p✝ k✝ q✝)

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

Goal state after: