diff --git a/Cslib/Computability/Automata/Acceptors/Acceptor.lean b/Cslib/Computability/Automata/Acceptors/Acceptor.lean
index f3f98dc77..fba01cf8d 100644
--- a/Cslib/Computability/Automata/Acceptors/Acceptor.lean
+++ b/Cslib/Computability/Automata/Acceptors/Acceptor.lean
@@ -23,12 +23,12 @@ namespace Acceptor
 variable {Symbol : Type v}
 
 /-- The language of an `Acceptor` is the set of strings it `Accepts`. -/
-@[scoped grind .]
+@[automata .]
 def language [Acceptor A Symbol] (a : A) : Language Symbol :=
   { xs | Accepts a xs }
 
 /-- A string is in the language of an acceptor iff the acceptor accepts it. -/
-@[simp, scoped grind =]
+@[simp, automata =]
 theorem mem_language [Acceptor A Symbol] (a : A) (xs : List Symbol) :
   xs ∈ language a ↔ Accepts a xs := Iff.rfl
 
diff --git a/Cslib/Computability/Automata/Acceptors/OmegaAcceptor.lean b/Cslib/Computability/Automata/Acceptors/OmegaAcceptor.lean
index 251b3b95d..05bc59b94 100644
--- a/Cslib/Computability/Automata/Acceptors/OmegaAcceptor.lean
+++ b/Cslib/Computability/Automata/Acceptors/OmegaAcceptor.lean
@@ -22,12 +22,12 @@ namespace ωAcceptor
 variable {Symbol : Type v}
 
 /-- The language of an `ωAcceptor` is the set of sequences it `Accepts`. -/
-@[scoped grind .]
+@[automata .]
 def language [ωAcceptor A Symbol] (a : A) : ωLanguage Symbol :=
   { xs | Accepts a xs }
 
 /-- A string is in the language of an acceptor iff the acceptor accepts it. -/
-@[simp, scoped grind =]
+@[simp, automata =]
 theorem mem_language [ωAcceptor A Symbol] (a : A) (xs : ωSequence Symbol) :
   xs ∈ language a ↔ Accepts a xs := Iff.rfl
 
diff --git a/Cslib/Computability/Automata/DA/Basic.lean b/Cslib/Computability/Automata/DA/Basic.lean
index 6914f8fc3..6dec38683 100644
--- a/Cslib/Computability/Automata/DA/Basic.lean
+++ b/Cslib/Computability/Automata/DA/Basic.lean
@@ -29,7 +29,7 @@ finiteness assumptions), deterministic Buchi automata, and deterministic Muller
 -/
 
 open List Filter Cslib.ωSequence
-open scoped Cslib.FLTS
+open Cslib.FLTS
 
 namespace Cslib.Automata
 
@@ -43,31 +43,31 @@ namespace DA
 variable {State Symbol : Type*}
 
 /-- Helper function for defining `run` below. -/
-@[scoped grind =]
+@[automata =]
 def run' (da : DA State Symbol) (xs : ωSequence Symbol) : ℕ → State
   | 0 => da.start
   | n + 1 => da.tr (run' da xs n) (xs n)
 
 /-- Infinite run. -/
-@[scoped grind =]
+@[automata =]
 def run (da : DA State Symbol) (xs : ωSequence Symbol) : ωSequence State := da.run' xs
 
-@[simp, scoped grind =]
+@[simp, automata =]
 theorem run_zero {da : DA State Symbol} {xs : ωSequence Symbol} :
     da.run xs 0 = da.start :=
   rfl
 
-@[simp, scoped grind =]
+@[simp, automata =]
 theorem run_succ {da : DA State Symbol} {xs : ωSequence Symbol} {n : ℕ} :
     da.run xs (n + 1) = da.tr (da.run xs n) (xs n) := by
   rfl
 
-@[simp, scoped grind =]
+@[simp, automata =]
 theorem mtr_extract_eq_run {da : DA State Symbol} {xs : ωSequence Symbol} {n : ℕ} :
     da.mtr da.start (xs.extract 0 n) = da.run xs n := by
   induction n
   case zero => rfl
-  case succ n h_ind => grind
+  case succ n h_ind => grind [automata]
 
 /-- A deterministic automaton that accepts finite strings (lists of symbols). -/
 structure FinAcc (State Symbol : Type*) extends DA State Symbol where
diff --git a/Cslib/Computability/Automata/DA/Buchi.lean b/Cslib/Computability/Automata/DA/Buchi.lean
index 346cfd267..2e4067579 100644
--- a/Cslib/Computability/Automata/DA/Buchi.lean
+++ b/Cslib/Computability/Automata/DA/Buchi.lean
@@ -17,7 +17,7 @@ open Filter
 
 namespace Cslib.Automata.DA
 
-open scoped FinAcc Buchi
+open FinAcc Buchi
 
 variable {State Symbol : Type*}
 
@@ -25,7 +25,7 @@ open Acceptor ωAcceptor in
 /-- The ω-language accepted by a deterministic Buchi automaton is the ω-limit
 of the language accepted by the same automaton.
 -/
-@[scoped grind =]
+@[automata =]
 theorem buchi_eq_finAcc_omegaLim {da : DA State Symbol} {acc : Set State} :
     language (Buchi.mk da acc) = (language (FinAcc.mk da acc))↗ω := by
   ext xs
diff --git a/Cslib/Computability/Automata/DA/Congr.lean b/Cslib/Computability/Automata/DA/Congr.lean
index 6301073dc..374dc0bdd 100644
--- a/Cslib/Computability/Automata/DA/Congr.lean
+++ b/Cslib/Computability/Automata/DA/Congr.lean
@@ -15,7 +15,7 @@ public import Cslib.Computability.Languages.Congruences.RightCongruence
 
 namespace Cslib
 
-open scoped FLTS RightCongruence
+open FLTS RightCongruence
 
 variable {Symbol : Type*}
 
@@ -58,7 +58,7 @@ the equivalence class corresponding to `s`. -/
 @[simp]
 theorem congr_language_eq {a : Quotient c.eq} : language (FinAcc.mk c.toDA {a}) = eqvCls a := by
   ext
-  grind
+  grind [automata]
 
 end FinAcc
 
diff --git a/Cslib/Computability/Automata/DA/Prod.lean b/Cslib/Computability/Automata/DA/Prod.lean
index cf16fbd97..77314cf0d 100644
--- a/Cslib/Computability/Automata/DA/Prod.lean
+++ b/Cslib/Computability/Automata/DA/Prod.lean
@@ -16,21 +16,21 @@ public import Cslib.Foundations.Semantics.FLTS.Prod
 namespace Cslib.Automata
 
 open List
-open scoped FLTS
+open FLTS
 
 variable {State1 State2 Symbol : Type*}
 
 namespace DA
 
 /-- The product of two deterministic automata. -/
-@[scoped grind =]
+@[automata =]
 def prod (da1 : DA State1 Symbol) (da2 : DA State2 Symbol) : DA (State1 × State2) Symbol where
   toFLTS := da1.toFLTS.prod da2.toFLTS
   start := (da1.start, da2.start)
 
 /-- A state is reachable by the product automaton iff its components are reachable by
 the respective automaton components. -/
-@[simp, scoped grind =]
+@[simp, automata =]
 theorem prod_mtr_eq (da1 : DA State1 Symbol) (da2 : DA State2 Symbol)
     (s : State1 × State2) (xs : List Symbol) :
     (da1.prod da2).mtr s xs = (da1.mtr s.fst xs, da2.mtr s.snd xs) :=
diff --git a/Cslib/Computability/Automata/DA/ToNA.lean b/Cslib/Computability/Automata/DA/ToNA.lean
index dabbdc147..100c8ae2d 100644
--- a/Cslib/Computability/Automata/DA/ToNA.lean
+++ b/Cslib/Computability/Automata/DA/ToNA.lean
@@ -23,63 +23,61 @@ variable {State Symbol : Type*}
 section NA
 
 /-- `DA` is a special case of `NA`. -/
-@[scoped grind =]
+@[automata =]
 def toNA (a : DA State Symbol) : NA State Symbol :=
   { a.toLTS with start := {a.start} }
 
 instance : Coe (DA State Symbol) (NA State Symbol) where
   coe := toNA
 
-open scoped FLTS NA NA.Run LTS in
-@[simp, scoped grind =]
+open FLTS NA NA.Run LTS in
+@[simp, automata =]
 theorem toNA_run {a : DA State Symbol} {xs : ωSequence Symbol} {ss : ωSequence State} :
     a.toNA.Run xs ss ↔ a.run xs = ss := by
   constructor
   · rintro _
     ext n
-    induction n <;> grind [NA.Run]
-  · grind [NA.Run]
+    induction n <;> grind [automata, NA.Run]
+  · grind [automata, NA.Run]
 
 namespace FinAcc
 
 /-- `DA.FinAcc` is a special case of `NA.FinAcc`. -/
-@[scoped grind =]
+@[automata =]
 def toNAFinAcc (a : DA.FinAcc State Symbol) : NA.FinAcc State Symbol :=
   { a.toNA with accept := a.accept }
 
-open Acceptor in
-open scoped FLTS NA.FinAcc in
+open Acceptor FLTS NA.FinAcc in
 /-- The `NA.FinAcc` constructed from a `DA.FinAcc` has the same language. -/
-@[simp, scoped grind _=_]
+@[simp, automata _=_]
 theorem toNAFinAcc_language_eq {a : DA.FinAcc State Symbol} :
     language a.toNAFinAcc = language a := by
   ext xs
   constructor
-  · grind
+  · grind [automata]
   · intro _
     use a.start
-    grind
+    grind [automata]
 
 end FinAcc
 
 namespace Buchi
 
 /-- `DA.Buchi` is a special case of `NA.Buchi`. -/
-@[scoped grind =]
+@[automata =]
 def toNABuchi (a : DA.Buchi State Symbol) : NA.Buchi State Symbol :=
   { a.toNA with accept := a.accept }
 
-open ωAcceptor in
-open scoped NA.Buchi in
+open ωAcceptor NA.Buchi in
 /-- The `NA.Buchi` constructed from a `DA.Buchi` has the same ω-language. -/
-@[simp, scoped grind _=_]
+@[simp, automata _=_]
 theorem toNABuchi_language_eq {a : DA.Buchi State Symbol} :
     language a.toNABuchi = language a := by
   ext xs; constructor
-  · grind
+  · grind [automata]
   · intro _
     use (a.run xs)
-    grind
+    grind [automata]
 
 end Buchi
 
diff --git a/Cslib/Computability/Automata/EpsilonNA/Basic.lean b/Cslib/Computability/Automata/EpsilonNA/Basic.lean
index ae2174f45..e3d14ed28 100644
--- a/Cslib/Computability/Automata/EpsilonNA/Basic.lean
+++ b/Cslib/Computability/Automata/EpsilonNA/Basic.lean
@@ -43,7 +43,7 @@ namespace FinAcc
 
 /-- An `εNA.FinAcc` accepts a string if there is a saturated multistep accepting derivative with
 that trace from the start state. -/
-@[scoped grind =]
+@[automata =]
 instance : Acceptor (FinAcc State Symbol) Symbol where
   Accepts (a : FinAcc State Symbol) (xs : List Symbol) :=
     ∃ s ∈ a.εClosure a.start, ∃ s' ∈ a.accept,
diff --git a/Cslib/Computability/Automata/EpsilonNA/ToNA.lean b/Cslib/Computability/Automata/EpsilonNA/ToNA.lean
index 4882cf657..a79234c3b 100644
--- a/Cslib/Computability/Automata/EpsilonNA/ToNA.lean
+++ b/Cslib/Computability/Automata/EpsilonNA/ToNA.lean
@@ -26,7 +26,7 @@ private lemma LTS.noε_saturate_tr
   lts.saturate.Tr s μ s' ↔ lts.saturate.noε.Tr s μ' s' := by
   grind
 
-@[scoped grind =]
+@[automata =]
 lemma LTS.noε_saturate_mTr {lts : LTS State (Option Label)} :
   lts.saturate.MTr s (μs.map some) = lts.saturate.noε.MTr s μs := by
   ext s'
@@ -37,22 +37,21 @@ namespace Automata.εNA.FinAcc
 variable {State Symbol : Type*}
 
 /-- Any `εNA.FinAcc` can be converted into an `NA.FinAcc` that does not use ε-transitions. -/
-@[scoped grind]
+@[automata]
 def toNAFinAcc (a : εNA.FinAcc State Symbol) : NA.FinAcc State Symbol where
   start := a.εClosure a.start
   accept := a.accept
   Tr := a.saturate.noε.Tr
 
-open Acceptor in
-open scoped NA.FinAcc in
+open Acceptor NA.FinAcc in
 /-- Correctness of `toNAFinAcc`. -/
-@[scoped grind _=_]
+@[automata _=_]
 theorem toNAFinAcc_language_eq {ena : εNA.FinAcc State Symbol} :
     language ena.toNAFinAcc = language ena := by
   ext xs
   have : ∀ s s', ena.saturate.MTr s (xs.map some) s' = ena.saturate.noε.MTr s xs s' := by
     simp [LTS.noε_saturate_mTr]
-  grind
+  grind [automata]
 
 end Automata.εNA.FinAcc
 
diff --git a/Cslib/Computability/Automata/NA/Basic.lean b/Cslib/Computability/Automata/NA/Basic.lean
index 88ee3901f..27525e710 100644
--- a/Cslib/Computability/Automata/NA/Basic.lean
+++ b/Cslib/Computability/Automata/NA/Basic.lean
@@ -60,7 +60,7 @@ namespace FinAcc
 accept state.
 
 This is the standard string recognition performed by NFAs in the literature. -/
-@[simp, scoped grind =]
+@[simp, automata =]
 instance : Acceptor (FinAcc State Symbol) Symbol where
   Accepts (a : FinAcc State Symbol) (xs : List Symbol) :=
     ∃ s ∈ a.start, ∃ s' ∈ a.accept, a.MTr s xs s'
@@ -75,7 +75,7 @@ structure Buchi (State Symbol : Type*) extends NA State Symbol where
 namespace Buchi
 
 /-- An infinite run is accepting iff accepting states occur infinitely many times. -/
-@[simp, scoped grind =]
+@[simp, automata =]
 instance : ωAcceptor (Buchi State Symbol) Symbol where
   Accepts (a : Buchi State Symbol) (xs : ωSequence Symbol) :=
     ∃ ss, a.Run xs ss ∧ ∃ᶠ k in atTop, ss k ∈ a.accept
@@ -91,7 +91,7 @@ namespace Muller
 
 /-- An infinite run is accepting iff the set of states that occur infinitely many times
 is one of the sets in `accept`. -/
-@[simp, scoped grind =]
+@[simp, automata =]
 instance : ωAcceptor (Muller State Symbol) Symbol where
   Accepts (a : Muller State Symbol) (xs : ωSequence Symbol) :=
     ∃ ss, a.Run xs ss ∧ ss.infOcc ∈ a.accept
diff --git a/Cslib/Computability/Automata/NA/BuchiEquiv.lean b/Cslib/Computability/Automata/NA/BuchiEquiv.lean
index 3c065975d..0847b8806 100644
--- a/Cslib/Computability/Automata/NA/BuchiEquiv.lean
+++ b/Cslib/Computability/Automata/NA/BuchiEquiv.lean
@@ -13,7 +13,7 @@ public import Cslib.Computability.Automata.NA.Basic
 /-! # Equivalence of nondeterministic Buchi automata (NBAs). -/
 
 open Set Function Filter Cslib.ωSequence
-open scoped Cslib.LTS
+open Cslib.LTS
 
 universe u v w
 
@@ -24,7 +24,7 @@ open ωAcceptor
 variable {Symbol : Type u} {State : Type v} {State' : Type w}
 
 /-- Lifts an equivalence on states to an equivalence on NBAs. -/
-@[scoped grind =]
+@[automata =]
 def reindex (f : State ≃ State') : Buchi State Symbol ≃ Buchi State' Symbol where
   toFun nba := {
     Tr s x t := nba.Tr (f.symm s) x (f.symm t)
@@ -54,15 +54,15 @@ theorem reindex_run_iff' {f : State ≃ State'} {nba : Buchi State Symbol}
     (nba.reindex f).Run xs (ss.map f) ↔ nba.Run xs ss := by
   simp [reindex_run_iff]
 
-@[simp, scoped grind =]
+@[simp, automata =]
 theorem reindex_language_eq {f : State ≃ State'} {nba : Buchi State Symbol} :
     language (nba.reindex f) = language nba := by
   ext xs
   constructor
   · rintro ⟨ss', h_run', h_acc'⟩
-    grind [reindex_run_iff]
+    grind [automata, reindex_run_iff]
   · rintro ⟨ss, h_run, h_acc⟩
     use ss.map f
-    constructor <;> grind [reindex_run_iff']
+    constructor <;> grind [automata, reindex_run_iff']
 
 end Cslib.Automata.NA.Buchi
diff --git a/Cslib/Computability/Automata/NA/BuchiInter.lean b/Cslib/Computability/Automata/NA/BuchiInter.lean
index 9a8d51c75..c179b9bc4 100644
--- a/Cslib/Computability/Automata/NA/BuchiInter.lean
+++ b/Cslib/Computability/Automata/NA/BuchiInter.lean
@@ -27,35 +27,35 @@ simply because toggling can be easily modeled by the boolean operation `not`.
 namespace Cslib.Automata.NA.Buchi
 
 open Set Prod Filter ωSequence ωAcceptor
-open scoped LTS
+open LTS
 
 variable {Symbol : Type*} {State : Bool → Type*}
 
 /-- The initial history state. -/
-@[scoped grind =, nolint unusedArguments]
+@[automata =, nolint unusedArguments]
 def histStart (_ : Π i, State i) : Bool := false
 
 /-- The two accepting conditions of the intersection automaton. -/
-@[scoped grind =]
+@[automata =]
 def interAcc (j : Bool) (acc : (i : Bool) → Set (State i)) : Set ((Π i, State i) × Bool) :=
   { (s, h) | s j ∈ acc j ∧ h = j }
 
 open scoped Classical in
 /-- The transition function of the history state. -/
-@[scoped grind =, nolint unusedArguments]
+@[automata =, nolint unusedArguments]
 noncomputable def histTrans (acc : (i : Bool) → Set (State i))
     (s : (Π i, State i) × Bool) (_ : Symbol) (_ : Π i, State i) : Bool :=
   if s ∈ interAcc false acc then true else
   if s ∈ interAcc true acc then false else s.snd
 
 /-- The intersection automaton. -/
-@[scoped grind =]
+@[automata =]
 noncomputable def interNA (na : (i : Bool) → NA (State i) Symbol)
     (acc : (i : Bool) → Set (State i)) : NA ((Π i, State i) × Bool) Symbol :=
   (iProd na).addHist histStart (histTrans acc)
 
 /-- The overall accepting conditon of the intersection automaton. -/
-@[scoped grind =]
+@[automata =]
 def interAccept (acc : (i : Bool) → Set (State i)) : Set ((Π i, State i) × Bool) :=
   interAcc false acc ∪ interAcc true acc
 
@@ -70,11 +70,11 @@ lemma inter_freq_acc_freq_acc {xs : ωSequence Symbol} {ss : ωSequence ((Π i,
   apply frequently_leadsTo_frequently h_inf
   apply leadsTo_trans (q := {s | s.snd = !i})
   · apply step_leadsTo
-    grind
+    grind [automata]
   · apply until_frequently_not_leadsTo
-    · grind
+    · grind [automata]
     · apply Frequently.mono h_inf
-      grind
+      grind [automata]
 
 /-- If the intersection automaton sees the accepting condtions of both component automata
 infinitely many times, then its own accepting condition also happens infinitely many times. -/
@@ -86,18 +86,18 @@ lemma inter_freq_comp_acc_freq_acc {xs : ωSequence Symbol} {ss : ωSequence ((
   have (k : ℕ) := (h_run.trans k).right
   have h_univ : ∃ᶠ k in atTop, ss k ∈ univ := by simp [atTop_neBot]
   have (b : Bool) : interAcc b acc = {⟨_, b'⟩ | b' = b} ∩ {⟨p,_⟩ | p b ∈ acc b} := by
-    ext; grind
+    ext; grind [automata]
   have : {⟨_, b⟩ : (Π i, State i) × Bool | b = false}ᶜ = {⟨_, b⟩ | b = true} := by
     ext; grind
   apply frequently_leadsTo_frequently h_univ
   apply leadsTo_cases_or (q := {⟨_, b⟩ | b = false}) <;>
-  grind [until_frequently_leadsTo_and, univ_inter]
+  grind [automata, until_frequently_leadsTo_and, univ_inter]
 
 -- TODO: fix proof to work with backward.isDefEq.respectTransparency
 set_option backward.isDefEq.respectTransparency false in
 /-- The language accepted by the intersection automaton is the intersection of
 the languages accepted by the two component automata. -/
-@[simp, scoped grind =]
+@[simp, automata =]
 theorem inter_language_eq :
     language (Buchi.mk (interNA na acc) (interAccept acc)) =
     ⋂ i, language (Buchi.mk (na i) (acc i)) := by
@@ -112,18 +112,18 @@ theorem inter_language_eq :
       cases i
       · rcases h_inf with h_inf_f | h_inf_t
         · apply Frequently.mono h_inf_f
-          grind
+          grind [automata]
         · apply Frequently.mono <| inter_freq_acc_freq_acc h_run h_inf_t
-          grind
+          grind [automata]
       · rcases h_inf with h_inf_f | h_inf_t
         · apply Frequently.mono <| inter_freq_acc_freq_acc h_run h_inf_f
-          grind
+          grind [automata]
         · apply Frequently.mono h_inf_t
-          grind
+          grind [automata]
   · intro h
     choose ss_i h_ss_i using h
     let ss_p : ωSequence (Π i, State i) := fun k i ↦ ss_i i k
-    have h_ss_p : (iProd na).Run xs ss_p := by grind [Run]
+    have h_ss_p : (iProd na).Run xs ss_p := by grind [automata, Run]
     have (k : ℕ) (i : Bool) : ss_p k i = ss_i i k := rfl
     obtain ⟨ss, h_run, _⟩ := hist_run_exists h_ss_p
     use ss, h_run
diff --git a/Cslib/Computability/Automata/NA/Concat.lean b/Cslib/Computability/Automata/NA/Concat.lean
index 4fb1d75e7..9c355a6a3 100644
--- a/Cslib/Computability/Automata/NA/Concat.lean
+++ b/Cslib/Computability/Automata/NA/Concat.lean
@@ -19,7 +19,7 @@ open Sum ωSequence Acceptor
 
 variable {Symbol State1 State2 : Type*}
 
-open scoped Classical in
+open Classical in
 /-- `concat na1 na2` starts by running `na1` and then nondeterministically switches to `na2`
 by identifying an accepting state of `na1` with an initial state of `na2`. If `na1` accepts the
 empty word, it may also start running `na2` from the beginning. Once it starts running `na2`,
@@ -163,7 +163,7 @@ theorem finConcat_language_eq [Inhabited Symbol] :
     refine ⟨xl.take n, ?_, xl.drop n, ?_, ?_⟩
     · grind [totalize_language_eq, take_append_of_le_length]
     · have : ss xl.length = (ss.drop n) (xl.length - n) := by grind
-      grind [drop_append_of_le_length, take_append_of_le_length, totalize_run_mtr]
+      grind [automata, drop_append_of_le_length, take_append_of_le_length, totalize_run_mtr]
     · exact xl.take_append_drop n
   · rintro ⟨xl1, h_xl1, xl2, h_xl2, rfl⟩
     rw [← totalize_language_eq] at h_xl1
@@ -171,7 +171,7 @@ theorem finConcat_language_eq [Inhabited Symbol] :
     obtain ⟨_, _, h_run2, _, _⟩ := totalize_mtr_run h_s2 h_mtr2
     obtain ⟨ss, ⟨_, h_ωtr⟩, _⟩ := concat_run_exists h_xl1 h_run2
     grind [
-      finConcat, List.length_append, take_append_of_le_length,
+      automata, finConcat, List.length_append, take_append_of_le_length,
       extract_eq_drop_take, =_ append_append_ωSequence, get_drop xl2.length xl1.length ss,
       LTS.ωTr_mTr h_ωtr (zero_le (xl1.length + xl2.length))
     ]
diff --git a/Cslib/Computability/Automata/NA/Hist.lean b/Cslib/Computability/Automata/NA/Hist.lean
index 004a1af2a..6ad18fdf3 100644
--- a/Cslib/Computability/Automata/NA/Hist.lean
+++ b/Cslib/Computability/Automata/NA/Hist.lean
@@ -19,14 +19,14 @@ state. But the evolution of the original state is not constrained by the history
 namespace Cslib.Automata.NA
 
 open Prod ωSequence
-open scoped LTS
+open LTS
 
 variable {Symbol State Hist : Type*}
 
 /-- The construction of adding a history state.  Note that `start'` can depend on the initial
 value of the original state and `tr'` can depend on the new value of the original state.
 So there is no loss of generality in their being functions, rather than relations. -/
-@[scoped grind =]
+@[automata =]
 def addHist (na : NA State Symbol) (start' : State → Hist)
     (tr' : State × Hist → Symbol → State → Hist) : NA (State × Hist) Symbol where
   Tr s x t := na.Tr s.fst x t.fst ∧ tr' s x t.fst = t.snd
@@ -40,10 +40,10 @@ theorem hist_run_proj {xs : ωSequence Symbol} {ss : ωSequence (State × Hist)}
     (h_run : (na.addHist start' tr').Run xs ss) : na.Run xs (ss.map fst) := by
   obtain ⟨h_start, h_trans⟩ := h_run
   simp only [addHist] at h_trans
-  grind [Run]
+  grind [automata, Run]
 
 /-- Given a run of the original automaton, `makeHist` builds a run of the history state. -/
-@[scoped grind =]
+@[automata =]
 def makeHist (start' : State → Hist) (tr' : State × Hist → Symbol → State → Hist)
   (xs : ωSequence Symbol) (ss : ωSequence State) : ℕ → Hist
   | 0 => start' (ss 0)
@@ -56,7 +56,7 @@ theorem hist_run_exists {xs : ωSequence Symbol} {ss : ωSequence State}
   use ⟨fun n ↦ (ss n, makeHist start' tr' xs ss n)⟩
   constructor
   · simp only [addHist]
-    grind [Run]
+    grind [automata, Run]
   · grind
 
 end Cslib.Automata.NA
diff --git a/Cslib/Computability/Automata/NA/Loop.lean b/Cslib/Computability/Automata/NA/Loop.lean
index 61dcd854a..5d62a023a 100644
--- a/Cslib/Computability/Automata/NA/Loop.lean
+++ b/Cslib/Computability/Automata/NA/Loop.lean
@@ -162,7 +162,7 @@ end Buchi
 
 namespace FinAcc
 
-open scoped Computability
+open Computability
 
 /-- `finLoop na` is the loop construction applied to the "totalized" version of `na`. -/
 def finLoop (na : FinAcc State Symbol) : NA (Unit ⊕ (State ⊕ Unit)) Symbol :=
diff --git a/Cslib/Computability/Automata/NA/Pair.lean b/Cslib/Computability/Automata/NA/Pair.lean
index 6b1540426..e2e1b89d6 100644
--- a/Cslib/Computability/Automata/NA/Pair.lean
+++ b/Cslib/Computability/Automata/NA/Pair.lean
@@ -24,7 +24,7 @@ from state `s` to state `t`. -/
 def LTS.pairLang (lts : LTS State Symbol) (s t : State) : Language Symbol :=
   { xs | lts.MTr s xs t }
 
-@[simp, scoped grind =]
+@[simp, automata =]
 theorem LTS.mem_pairLang {lts : LTS State Symbol} {s t : State} {xs : List Symbol} :
     xs ∈ lts.pairLang s t ↔ lts.MTr s xs t := Iff.rfl
 
@@ -42,7 +42,7 @@ from state `s` to state `t` via a state in `via`. -/
 def LTS.pairViaLang (lts : LTS State Symbol) (via : Set State) (s t : State) : Language Symbol :=
   ⨆ r ∈ via, lts.pairLang s r * lts.pairLang r t
 
-@[simp, scoped grind =]
+@[simp, automata =]
 theorem LTS.mem_pairViaLang {lts : LTS State Symbol} {via : Set State}
     {s t : State} {xs : List Symbol} : xs ∈ lts.pairViaLang via s t ↔
       ∃ r ∈ via, ∃ xs1 xs2, lts.MTr s xs1 r ∧ lts.MTr r xs2 t ∧ xs1 ++ xs2 = xs := by
@@ -58,14 +58,14 @@ theorem LTS.pairViaLang_regular [Inhabited Symbol] [Finite State] {lts : LTS Sta
 theorem LTS.pairLang_append {lts : LTS State Symbol} {s0 s1 s2 : State} {xs1 xs2 : List Symbol}
     (h1 : xs1 ∈ lts.pairLang s0 s1) (h2 : xs2 ∈ lts.pairLang s1 s2) :
     xs1 ++ xs2 ∈ lts.pairLang s0 s2 := by
-  grind [<= LTS.MTr.comp]
+  grind [automata, <= LTS.MTr.comp]
 
 theorem LTS.pairLang_split {lts : LTS State Symbol} {s0 s2 : State} {xs1 xs2 : List Symbol}
     (h : xs1 ++ xs2 ∈ lts.pairLang s0 s2) :
     ∃ s1, xs1 ∈ lts.pairLang s0 s1 ∧ xs2 ∈ lts.pairLang s1 s2 := by
   obtain ⟨r, _, _⟩ := LTS.MTr.split <| LTS.mem_pairLang.mp h
   use r
-  grind
+  grind [automata]
 
 theorem LTS.pairViaLang_append_pairLang {lts : LTS State Symbol}
     {s0 s1 s2 : State} {xs1 xs2 : List Symbol} {via : Set State}
@@ -74,13 +74,13 @@ theorem LTS.pairViaLang_append_pairLang {lts : LTS State Symbol}
   obtain ⟨r, _, _, _, _, _, rfl⟩ := LTS.mem_pairViaLang.mp h1
   apply LTS.mem_pairViaLang.mpr
   use r
-  grind [<= LTS.MTr.comp]
+  grind [automata, <= LTS.MTr.comp]
 
 theorem LTS.pairLang_append_pairViaLang {lts : LTS State Symbol}
     {s0 s1 s2 : State} {xs1 xs2 : List Symbol} {via : Set State}
     (h1 : xs1 ∈ lts.pairLang s0 s1) (h2 : xs2 ∈ lts.pairViaLang via s1 s2) :
     xs1 ++ xs2 ∈ lts.pairViaLang via s0 s2 := by
-  grind [<= LTS.MTr.comp]
+  grind [automata, <= LTS.MTr.comp]
 
 theorem LTS.pairViaLang_split {lts : LTS State Symbol} {s0 s2 : State} {xs1 xs2 : List Symbol}
     {via : Set State} (h : xs1 ++ xs2 ∈ lts.pairViaLang via s0 s2) :
@@ -90,10 +90,10 @@ theorem LTS.pairViaLang_split {lts : LTS State Symbol} {s0 s2 : State} {xs1 xs2
   obtain ⟨zs1, rfl, rfl⟩ | ⟨zs2, rfl, rfl⟩ := List.append_eq_append_iff.mp h_eq
   · obtain ⟨s1, _, _⟩ := LTS.MTr.split h_ys2
     use s1
-    grind
+    grind [automata]
   · obtain ⟨s1, _, _⟩ := LTS.MTr.split h_ys1
     use s1
-    grind
+    grind [automata]
 
 namespace Automata.NA.Buchi
 
diff --git a/Cslib/Computability/Automata/NA/Prod.lean b/Cslib/Computability/Automata/NA/Prod.lean
index 9fb08c8b3..f48b15c95 100644
--- a/Cslib/Computability/Automata/NA/Prod.lean
+++ b/Cslib/Computability/Automata/NA/Prod.lean
@@ -15,19 +15,19 @@ public import Cslib.Computability.Automata.NA.Basic
 namespace Cslib.Automata.NA
 
 open Set List Cslib.ωSequence
-open scoped LTS
+open LTS
 
 variable {Symbol I : Type*} {State : I → Type*}
 
 /-- The product of an indexed family of nondeterministic automata. -/
-@[scoped grind =]
+@[automata =]
 def iProd (na : (i : I) → NA (State i) Symbol) : NA (Π i, State i) Symbol where
   Tr s x t := ∀ i, (na i).Tr (s i) x (t i)
   start := ⋂ i, (· i) ⁻¹' (na i).start
 
 /-- Every run of the product automaton projects onto runs of its component automata,
 and vice versa. -/
-@[simp, scoped grind =]
+@[simp, automata =]
 theorem iProd_run_iff {na : (i : I) → NA (State i) Symbol}
     {xs : ωSequence Symbol} {ss : ωSequence (Π i, State i)} :
     (iProd na).Run xs ss ↔ ∀ i, (na i).Run xs (ss.map (· i)) := by
diff --git a/Cslib/Computability/Automata/NA/Sum.lean b/Cslib/Computability/Automata/NA/Sum.lean
index 9fa33116d..699c2900f 100644
--- a/Cslib/Computability/Automata/NA/Sum.lean
+++ b/Cslib/Computability/Automata/NA/Sum.lean
@@ -13,20 +13,20 @@ public import Cslib.Computability.Automata.NA.Basic
 /-! # Sum of nondeterministic automata. -/
 
 open Set Function Filter Cslib.ωSequence
-open scoped Cslib.LTS
+open Cslib.LTS
 
 namespace Cslib.Automata.NA
 
 variable {Symbol I : Type*} {State : I → Type*}
 
 /-- The sum of an indexed family of nondeterministic automata. -/
-@[scoped grind =]
+@[automata =]
 def iSum (na : (i : I) → NA (State i) Symbol) : NA (Σ i, State i) Symbol where
   start := ⋃ i, Sigma.mk i '' (na i).start
   Tr s x t := ∃ i s_i t_i, (na i).Tr s_i x t_i ∧ ⟨i, s_i⟩ = s ∧ ⟨i, t_i⟩ = t
 
 /-- An infinite run of the sum automaton is an infinite run of one of its component automata. -/
-@[simp, scoped grind =]
+@[simp, automata =]
 theorem iSum_run_iff {na : (i : I) → NA (State i) Symbol}
     {xs : ωSequence Symbol} {ss : ωSequence (Σ i, State i)} :
     (iSum na).Run xs ss ↔ ∃ i ss_i, (na i).Run xs ss_i ∧ ss_i.map (Sigma.mk i) = ss := by
@@ -52,7 +52,7 @@ theorem iSum_run_iff {na : (i : I) → NA (State i) Symbol}
     · simp only [iSum, get_map, mem_iUnion]
       grind [NA.Run]
     · simp only [LTS.ωTr]
-      grind [NA.Run]
+      grind [automata, NA.Run]
 
 namespace Buchi
 
@@ -71,11 +71,11 @@ theorem iSum_language_eq {na : (i : I) → NA (State i) Symbol} {acc : (i : I) 
   constructor
   · rintro ⟨ss, h_run, h_acc⟩
     simp only [mem_iUnion] at h_acc
-    grind
+    grind [automata]
   · rintro ⟨i, ss_i, _⟩
     use ss_i.map (Sigma.mk i)
     simp only [mem_iUnion]
-    grind
+    grind [automata]
 
 end Buchi
 
diff --git a/Cslib/Computability/Automata/NA/ToDA.lean b/Cslib/Computability/Automata/NA/ToDA.lean
index 041f6ab34..62a3baace 100644
--- a/Cslib/Computability/Automata/NA/ToDA.lean
+++ b/Cslib/Computability/Automata/NA/ToDA.lean
@@ -24,25 +24,25 @@ variable {State Symbol : Type*}
 section SubsetConstruction
 
 /-- Converts an `NA` into a `DA` using the subset construction. -/
-@[scoped grind =]
+@[automata =]
 def toDA (a : NA State Symbol) : DA (Set State) Symbol :=
   { a.toFLTS with start := a.start }
 
 namespace FinAcc
 
 /-- Converts an `NA.FinAcc` into a `DA.FinAcc` using the subset construction. -/
-@[scoped grind =]
+@[automata =]
 def toDAFinAcc (a : NA.FinAcc State Symbol) : DA.FinAcc (Set State) Symbol :=
   { a.toDA with accept := { S | ∃ s ∈ S, s ∈ a.accept } }
 
 open Acceptor in
-open scoped DA.FinAcc LTS in
+open DA.FinAcc LTS in
 /-- The `DA` constructed from an `NA` has the same language. -/
-@[scoped grind _=_]
+@[automata _=_]
 theorem toDAFinAcc_language_eq {na : NA.FinAcc State Symbol} :
   language na.toDAFinAcc = language na := by
   ext xs
-  grind
+  grind [automata]
 
 end FinAcc
 
diff --git a/Cslib/Computability/Languages/OmegaRegularLanguage.lean b/Cslib/Computability/Languages/OmegaRegularLanguage.lean
index 94f25f205..446c6b3f7 100644
--- a/Cslib/Computability/Languages/OmegaRegularLanguage.lean
+++ b/Cslib/Computability/Languages/OmegaRegularLanguage.lean
@@ -120,7 +120,7 @@ theorem IsRegular.sup {p1 p2 : ωLanguage Symbol}
   ext xs
   simp only [NA.Buchi.iSum_language_eq, mem_sup, mem_language]
   rw [mem_iUnion, Fin.exists_fin_two]
-  grind
+  grind [automata]
 
 -- TODO: fix proof to work with backward.isDefEq.respectTransparency
 set_option backward.isDefEq.respectTransparency false in
@@ -142,7 +142,7 @@ theorem IsRegular.inf {p1 p2 : ωLanguage Symbol}
   ext xs
   simp only [inter_language_eq, mem_inf, mem_language]
   rw [mem_iInter, Bool.forall_bool]
-  grind
+  grind [automata]
 
 /-- The union of any finite number of ω-regular languages is ω-regular. -/
 @[simp]
diff --git a/Cslib/Computability/Languages/RegularLanguage.lean b/Cslib/Computability/Languages/RegularLanguage.lean
index af7e9f51b..726f270da 100644
--- a/Cslib/Computability/Languages/RegularLanguage.lean
+++ b/Cslib/Computability/Languages/RegularLanguage.lean
@@ -51,17 +51,17 @@ theorem IsRegular.iff_nfa {l : Language Symbol} :
   rw [IsRegular.iff_dfa]; constructor
   · rintro ⟨State, h_fin, ⟨da, acc⟩, rfl⟩
     use State, h_fin, ⟨da.toNA, acc⟩
-    grind
+    grind [automata]
   · rintro ⟨State, _, na, rfl⟩
     use Set State, inferInstance, na.toDAFinAcc
-    grind
+    grind [automata]
 
 /-- The complementation of a regular language is regular. -/
 theorem IsRegular.compl {l : Language Symbol} (h : l.IsRegular) : (lᶜ).IsRegular := by
   rw [IsRegular.iff_dfa] at h ⊢
   obtain ⟨State, _, ⟨da, acc⟩, rfl⟩ := h
   use State, inferInstance, ⟨da, accᶜ⟩
-  grind
+  grind [automata]
 
 /-- The empty language is regular. -/
 @[simp]
@@ -69,7 +69,7 @@ theorem IsRegular.zero : (0 : Language Symbol).IsRegular := by
   rw [IsRegular.iff_dfa]
   let flts := FLTS.mk (fun () (_ : Symbol) ↦ ())
   use Unit, inferInstance, ⟨DA.mk flts (), ∅⟩
-  grind
+  grind [automata]
 
 /-- The language containing only the empty word is regular. -/
 @[simp]
@@ -80,8 +80,11 @@ theorem IsRegular.one : (1 : Language Symbol).IsRegular := by
   ext; constructor
   · intro h; by_contra h'
     have := dropLast_append_getLast h'
-    grind
-  · grind [Language.mem_one]
+    grind [automata]
+  · grind only [
+      Language.mem_one, = mem_language, = language.eq_1, = DA.FinAcc.instAcceptor.eq_1,
+      = mem_singleton_iff, = FLTS.mtr_nil_eq
+    ]
 
 /-- The language of all finite words is regular. -/
 @[simp]
@@ -97,7 +100,7 @@ theorem IsRegular.inf {l1 l2 : Language Symbol}
   obtain ⟨State1, h_fin1, ⟨da1, acc1⟩, rfl⟩ := h1
   obtain ⟨State2, h_fin1, ⟨da2, acc2⟩, rfl⟩ := h2
   use State1 × State2, inferInstance, ⟨da1.prod da2, fst ⁻¹' acc1 ∩ snd ⁻¹' acc2⟩
-  ext; grind [Language.mem_inf]
+  ext; grind [automata, Language.mem_inf]
 
 /-- The union of two regular languages is regular. -/
 @[simp]
@@ -107,7 +110,7 @@ theorem IsRegular.add {l1 l2 : Language Symbol}
   obtain ⟨State1, h_fin1, ⟨da1, acc1⟩, rfl⟩ := h1
   obtain ⟨State2, h_fin1, ⟨da2, acc2⟩, rfl⟩ := h2
   use State1 × State2, inferInstance, ⟨da1.prod da2, fst ⁻¹' acc1 ∪ snd ⁻¹' acc2⟩
-  ext; grind [Language.mem_add]
+  ext; grind [automata, Language.mem_add]
 
 /-- The intersection of any finite number of regular languages is regular. -/
 @[simp]
diff --git a/Cslib/Init.lean b/Cslib/Init.lean
index 623933d76..8c6e47236 100644
--- a/Cslib/Init.lean
+++ b/Cslib/Init.lean
@@ -10,6 +10,8 @@ public import Cslib.Foundations.Lint.Basic
 public import Mathlib.Init
 public import Mathlib.Tactic.Common
 
+register_grind_attr automata
+
 /-!
 # CSLib Initialization
 
diff --git a/CslibTests/GrindLint.lean b/CslibTests/GrindLint.lean
index 67673a40b..ab11da43b 100644
--- a/CslibTests/GrindLint.lean
+++ b/CslibTests/GrindLint.lean
@@ -40,13 +40,8 @@ open_scoped_all Cslib
 #grind_lint skip Cslib.ωSequence.drop_const
 #grind_lint skip Cslib.ωSequence.get_cons_append_zero
 #grind_lint skip Cslib.ωSequence.map_id
-#grind_lint skip Cslib.Automata.DA.buchi_eq_finAcc_omegaLim
 #grind_lint skip Cslib.LTS.MTr.stepL
 #grind_lint skip Cslib.LTS.STr.trans_τ
-#grind_lint skip Cslib.Automata.DA.FinAcc.toNAFinAcc_language_eq
-#grind_lint skip Cslib.Automata.NA.Buchi.reindex_language_eq
-#grind_lint skip Cslib.Automata.NA.FinAcc.toDAFinAcc_language_eq
-#grind_lint skip Cslib.Automata.εNA.FinAcc.toNAFinAcc_language_eq
 #grind_lint skip Cslib.CLL.Proof.parr_inversion.eq_1
 #grind_lint skip Cslib.CLL.Proof.with_inversion₁.eq_1
 #grind_lint skip Cslib.CLL.Proof.with_inversion₂.eq_1
diff --git a/lake-manifest.json b/lake-manifest.json
index 4a6781507..070efa877 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9b1001cbdbfe51cbc92398637317609eb7bbf139",
+   "rev": "a237616fe5742014bd87366490691a7c1de9d1a7",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",