diff --git a/LeanPool/PDL/AllPdlRule.lean b/LeanPool/PDL/AllPdlRule.lean
index 5ea169d54b..b074bd0699 100644
--- a/LeanPool/PDL/AllPdlRule.lean
+++ b/LeanPool/PDL/AllPdlRule.lean
@@ -135,7 +135,7 @@ lemma PdlRule.all_spec {X Y} (bas : X.basic) (r : PdlRule X Y) : ⟨Y, r⟩ ∈
       cases α_def : α <;> simp_all only [LoadFormula.boxes_nil, all, Finset.singleton_union,
         AnyFormula.split, LoadFormula.unload, List.cons_append, List.nil_append, List.mem_cons,
         Sigma.mk.injEq, Finset.union_singleton, List.not_mem_nil, or_false]
-      case atom_prog a => aesop
+      case atom_prog a => aesop (rule_sets := [-default])
       all_goals
         -- Here we need `bas` to disallow non-atomic freeL applications
         subst_eqs
@@ -180,7 +180,7 @@ lemma PdlRule.all_spec {X Y} (bas : X.basic) (r : PdlRule X Y) : ⟨Y, r⟩ ∈
       cases α_def : α <;> simp_all only [LoadFormula.boxes_nil, all, Finset.singleton_union,
         AnyFormula.split, LoadFormula.unload, List.cons_append, List.nil_append, List.mem_cons,
         Sigma.mk.injEq, Finset.union_singleton, List.not_mem_nil, or_false]
-      case atom_prog a => aesop
+      case atom_prog a => aesop (rule_sets := [-default])
       all_goals
         -- Here we need `bas` to disallow non-atomic freeL applications
         subst_eqs
diff --git a/LeanPool/PDL/Beth.lean b/LeanPool/PDL/Beth.lean
index 5b903d6723..b25aca9608 100644
--- a/LeanPool/PDL/Beth.lean
+++ b/LeanPool/PDL/Beth.lean
@@ -49,7 +49,7 @@ theorem beth (φ : Formula) (h : φ.impDef p) :
       and_imp] at h
     intro w_φp0 w_p0
     specialize h w_φp0
-    aesop
+    aesop (rule_sets := [-default])
   rcases interpolation this with ⟨ψ, ip_voc, ip_one, ip_two⟩
   clear this
   use ψ
@@ -85,7 +85,7 @@ theorem beth (φ : Formula) (h : φ.impDef p) :
         simp only [Formula.voc, Finset.union_singleton, Finset.mem_inter, Finset.mem_insert,
           true_or, Sum.inl.injEq, p0_neq_p1, false_or, true_and] at ip_voc
         rw [repl_in_F_voc_def] at ip_voc
-        aesop
+        aesop (rule_sets := [-default])
     have ip_two_p : tautology (ψ ↣ (φ ↣ ·p)) := by
       clear ip_one
       have := non_occ_taut_then_taut_imp_repl_in
@@ -99,7 +99,7 @@ theorem beth (φ : Formula) (h : φ.impDef p) :
         simp only [Formula.voc, Finset.union_singleton, Finset.mem_inter, Finset.mem_insert,
           Sum.inl.injEq, true_or, and_true] at ip_voc
         rw [repl_in_F_voc_def] at ip_voc
-        aesop
+        aesop (rule_sets := [-default])
       · assumption
     intro W M w w_φ
     simp at w_φ
diff --git a/LeanPool/PDL/Completeness/BuildTree.lean b/LeanPool/PDL/Completeness/BuildTree.lean
index a69e7fd00d..16bcbf2e56 100644
--- a/LeanPool/PDL/Completeness/BuildTree.lean
+++ b/LeanPool/PDL/Completeness/BuildTree.lean
@@ -120,7 +120,7 @@ lemma BuildTree.size_lt_loc (H : History) (X : Sequent) (nbas : ¬X.basic)
   have : ∀ lt, (next lt).size = (next lt).6.size := fun lt => by
     cases next lt; simp [BuildChoice.size]
   simp_rw [this]
-  grind
+  grind only []
 
 lemma BuildTree.size_lt_pdl (H : History) (X : Sequent) (bas : X.basic)
     (someR : PdlRule.all X ≠ [])
@@ -131,7 +131,7 @@ lemma BuildTree.size_lt_pdl (H : History) (X : Sequent) (bas : X.basic)
     simp only [List.mem_map, Sigma.exists]
     use Y, r, PdlRule.all_spec bas _
   have := List.le_sum_of_mem this
-  grind
+  grind only []
 
 @[simp]
 lemma BuildChoice.fst_eq {H X YS} {bc : BuildChoice H X YS} : bc.1 = H := by cases bc; rfl
@@ -512,7 +512,7 @@ lemma Match.btAt_newHist_length_eq_length_plus_oldHist {H X} {bt : BuildTree H X
     unfold btAt
     rw [IH]
     simp
-    grind
+    grind only []
   | pdl tail => by
     have IH := Match.btAt_newHist_length_eq_length_plus_oldHist tail
     simp only [length]
diff --git a/LeanPool/PDL/Completeness/BuildTreeExistence.lean b/LeanPool/PDL/Completeness/BuildTreeExistence.lean
index 1ece72a2cd..5b1567fbef 100644
--- a/LeanPool/PDL/Completeness/BuildTreeExistence.lean
+++ b/LeanPool/PDL/Completeness/BuildTreeExistence.lean
@@ -221,7 +221,7 @@ lemma Sequent.not_closed_of_sub {L R L' R' : Finset Formula} {O O' : Olf}
     (hL : ∀ f ∈ L', f ∈ L) (hR : ∀ f ∈ R', f ∈ R) (h : ¬ Sequent.closed ⟨L, R, O⟩) :
     ¬ Sequent.closed ⟨L', R', O'⟩ := by
   simp only [Sequent.closed, Sequent.mem_def, Sequent.L_eq, Sequent.R_eq] at h ⊢
-  grind
+  grind only []
 
 /-- Applying the rule `(L-)` to free the loaded formula: all formulas we had are kept. -/
 lemma PdlRule.exists_freeStep {Z : Sequent} (hZ : Z.O ≠ none) :
diff --git a/LeanPool/PDL/Completeness/Modelgraphs.lean b/LeanPool/PDL/Completeness/Modelgraphs.lean
index 2728eb0d92..3b18a6ab0e 100644
--- a/LeanPool/PDL/Completeness/Modelgraphs.lean
+++ b/LeanPool/PDL/Completeness/Modelgraphs.lean
@@ -108,7 +108,7 @@ theorem loadClaimHelper {Worlds : Finset (Finset Formula)}
         rw [← length_def]
         simp only [List.append_eq, List.length_append, List.length_cons, List.length_nil,
           zero_add] at hyp
-        linarith
+        omega
       simp only [pairRel, List.zip_cons_cons, List.append_eq, List.getElem_cons_succ,
         List.getElem_zip] at lchain
       convert lchain
@@ -254,8 +254,9 @@ theorem loadedTruthLemmaProg {Worlds} (MG : ModelGraph Worlds) α :
     induction n generalizing X φ -- not generalizing Y, but φ to be replaced φ with ⌈∗β⌉φ below!
     · rcases claim with ⟨YS, X_def, Y_def, _⟩
       have : YS.head = YS.last := by
+        clear * -YS
         have := List.Vector.exists_eq_cons YS
-        aesop
+        aesop (rule_sets := [-default])
       rw [this] at X_def
       subst X_def Y_def
       have := ((MG.2.1 (YS.last)).1 φ φ (∗β)).right.right.right.left boxP_in_X
@@ -265,9 +266,10 @@ theorem loadedTruthLemmaProg {Worlds} (MG : ModelGraph Worlds) α :
       rcases claim with ⟨YS, X_def, Y_def, relSteps⟩
       let Z := YS.get 1
       have X_β_Z : relate MG.1 β X Z := by
+        clear * -relSteps X_def
         specialize relSteps 0
         unfold Z
-        convert relSteps <;> aesop
+        convert relSteps <;> aesop (rule_sets := [-default])
       have := ((MG.2.1 X).1 φ φ (∗β)).right.right.right.left boxP_in_X
       rcases this with ⟨ℓ, mysat⟩
       simp only [Bset, List.all_append, List.all_map, Bool.and_eq_true, List.all_eq_true,
@@ -297,18 +299,18 @@ theorem loadedTruthLemmaProg {Worlds} (MG : ModelGraph Worlds) α :
         refine ⟨YS.tail, ?_, ?_, ?_⟩
         · rw [← List.Vector.get_zero]
           rw [List.Vector.get_tail_succ]
-          aesop
+          aesop (rule_sets := [-default])
         · rw [List.Vector.last_def]
           rw [List.Vector.get_tail_succ]
-          aesop
+          aesop (rule_sets := [-default])
         · intro i
           clear * -relSteps
           specialize relSteps i.succ
           have : ((List.Vector.tail YS).get i.castSucc) = (YS.get ((Fin.succ i).castSucc)) := by
-            aesop
+            aesop (rule_sets := [-default])
           rw [this]; clear this
           have : ((List.Vector.tail YS).get i.succ) = (YS.get ((Fin.succ i).succ)) := by
-            aesop
+            aesop (rule_sets := [-default])
           rw [this]; clear this
           exact relSteps
       case inr δ_notEmpty =>
@@ -360,9 +362,11 @@ theorem loadedTruthLemmaProg {Worlds} (MG : ModelGraph Worlds) α :
         · intro i
           clear * -relSteps
           specialize relSteps i.succ
-          have : ((List.Vector.tail YS).get i.castSucc) = (YS.get i.succ.castSucc) := by aesop
+          have : ((List.Vector.tail YS).get i.castSucc) = (YS.get i.succ.castSucc) := by
+            aesop (rule_sets := [-default])
           rw [this]; clear this
-          have : ((List.Vector.tail YS).get i.succ) = (YS.get i.succ.succ) := by aesop
+          have : ((List.Vector.tail YS).get i.succ) = (YS.get i.succ.succ) := by
+            aesop (rule_sets := [-default])
           rw [this]; clear this
           exact relSteps
   -- remaining cases: sequence, union, test
@@ -384,7 +388,7 @@ theorem loadedTruthLemmaProg {Worlds} (MG : ModelGraph Worlds) α :
       (by simp only [vDash.SemImplies, evaluatePoint, conEval]; exact X_F)
     rcases this with ⟨δ, δ_in_P, X_δ_Y⟩
     have δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ X.val := by
-      simp_all only [relate, Subtype.exists]
+      clear * -Bset_sub_X δ_in_P α_def
       subst_eqs
       apply Bset_sub_X
       right
@@ -458,13 +462,14 @@ theorem Qsteps_single : Qsteps R [α] v w ↔ Q R α v w := by
 theorem Qsteps_append : Qsteps R (δ1 ++ δ2) v w ↔ ∃ u, Qsteps R δ1 v u ∧ Qsteps R δ2 u w := by
   induction δ1 generalizing v w
   case nil =>
-    simp [Qsteps]
+    simp only [List.nil_append, Qsteps, beq_iff_eq, exists_eq_left']
   case cons α δ IH =>
-    simp only [List.cons_append, Qsteps, Relation.Comp, Subtype.exists]
-    constructor <;> rintro ⟨z, z_in, hyp⟩
-    · rw [IH] at hyp
-      aesop
-    · aesop
+    simp only [List.cons_append, Qsteps, Relation.Comp, IH]
+    constructor
+    · rintro ⟨u, hu, z, h1, h2⟩
+      exact ⟨z, ⟨u, hu, h1⟩, h2⟩
+    · rintro ⟨z, ⟨u, hu, h1⟩, h2⟩
+      exact ⟨u, hu, z, h1, h2⟩
 
 /-- Q_Fδ for a list of tests F and a list or programs δ. -/
 def Qcombo {W : Finset (Finset Formula)} (R : Nat → W → W → Prop)
diff --git a/LeanPool/PDL/Completeness/TableauGame.lean b/LeanPool/PDL/Completeness/TableauGame.lean
index 6e42f027f9..242fd3dbc3 100644
--- a/LeanPool/PDL/Completeness/TableauGame.lean
+++ b/LeanPool/PDL/Completeness/TableauGame.lean
@@ -74,7 +74,7 @@ def posOf (H : History) (X : Sequent) : ProverPos H X ⊕ BuilderPos H X :=
 lemma posOf_eq_inr_then_lpr {H X p} :
     posOf H X = Sum.inr p → ∃ lpr, p = .lpr lpr := by
   unfold posOf
-  grind
+  grind only []
 
 /-! ## Moves -/
 
@@ -206,7 +206,7 @@ private theorem theMoves_loaded_forward {H : History} {next : GamePos}
   dsimp only
   unfold theMoves at mv
   rcases χ with (⟨⟨χ⟩⟩|⟨⟨χ⟩⟩) <;> rcases χ with ⟨δ,φ|χ⟩ <;> cases δ <;> simp_all
-  all_goals grind
+  all_goals grind only []
 
 /-- Characterization of `theMoves`. -/
 lemma theMoves_iff {H X} {p : ProverPos H X ⊕ BuilderPos H X} {next : GamePos} :
@@ -363,7 +363,7 @@ lemma no_moves_of_rep {H X pos} (h : rep H X ∧ X.isFree) :
   push Not at hyp
   rcases hyp with ⟨p, p_in⟩
   unfold theMoves at p_in
-  rcases X with ⟨L,R,_|o⟩ <;> rcases pos with (_|_|_)|(_|_) <;> aesop
+  rcases X with ⟨L,R,_|o⟩ <;> rcases pos with (_|_|_)|(_|_) <;> aesop (rule_sets := [-default])
 
 /-- The finite set given by `theMoves` indeed agrees with the relation `move`.
 Other direction is `mem_theMoves_of_move`. -/
@@ -451,7 +451,7 @@ lemma move_of_mem_theMoves {pos next} :
           simp [loadMulti, LoadFormula.boxes]
       · constructor; apply Move.prPdl; apply PdlRule.modR rfl rfl
     all_goals
-      grind
+      grind only []
   · subst mv
     exact ⟨Move.prLocTab⟩
   · subst mv
@@ -494,7 +494,7 @@ lemma mem_theMoves_of_move {pos next} :
           use a, AnyFormula.normal ψ
           simp only [AnyFormula.normal.injEq, exists_eq_left', reduceCtorEq, false_and,
             exists_false, LoadFormula.unload, false_or, true_and]
-          aesop
+          aesop (rule_sets := [-default])
         all_goals
           absurd bas
           rintro ⟨bas, nclos⟩
@@ -529,7 +529,7 @@ lemma mem_theMoves_of_move {pos next} :
           use a, AnyFormula.normal ψ
           simp only [AnyFormula.normal.injEq, exists_eq_left', reduceCtorEq, false_and,
             exists_false, LoadFormula.unload, false_or, true_and]
-          aesop
+          aesop (rule_sets := [-default])
         all_goals
           absurd bas
           rintro ⟨bas, nclos⟩
@@ -560,22 +560,22 @@ lemma mem_theMoves_of_move {pos next} :
       left
       use a, ξ
       simp only [true_and]
-      cases ξ <;> grind
+      cases ξ <;> grind only []
     case some.modR =>
-    · grind -- sus that this works but did not in `modL` case?!
+    · grind only [] -- sus that this works but did not in `modL` case?!
   case prLocTab nbas nrep =>
-    grind
+    grind only []
   case buEnd Y ltX nbas Y_in nrep =>
-    grind
+    grind only []
 
 lemma move.hist {Hist next pos} (mov : move ⟨Hist, X, pos⟩ next) :
       (∃ newPos, next = ⟨Hist, X, newPos⟩) -- this is for the annoying `prLocTab` case;-)
     ∨ (∃ Y newPos, next = ⟨X :: Hist, Y, newPos⟩)  := by
   rcases mov with ⟨mov⟩
   cases mov
-  case prPdl => right; grind
-  case prLocTab => left; grind
-  case buEnd => right; grind
+  case prPdl => right; grind only []
+  case prLocTab => left; grind only []
+  case buEnd => right; grind only []
 
 lemma move.hist_suffix {Hist next pos} (mov : move ⟨Hist, X, pos⟩ next) : Hist <:+ next.1 := by
   have := move.hist mov
@@ -610,10 +610,10 @@ lemma move.trans_hist {pX pY} (movt : Relation.TransGen move pX pY) :
       simp_all
     · cases Y_def
       simp
-      aesop
+      aesop (rule_sets := [-default])
     · cases HXP_eq
       simp at *
-      aesop
+      aesop (rule_sets := [-default])
     · cases Y_def
       simp only [] at *
       rcases pX with ⟨X, H, p⟩
@@ -950,7 +950,7 @@ lemma move_then_not_flprep {H X next} {p : (ProverPos H X ⊕ BuilderPos H X)} :
     move ⟨H, X, p⟩ next → ¬ flprep H X := by
   simp only [move, Nonempty.forall]
   intro next_p hyp
-  cases next_p <;> grind
+  cases next_p <;> grind only []
 
 /-- Helper lemma for `matchesFinite`: if a property of natural numbers holds arbitrarily late,
 then we can enumerate witnesses for it with gaps of at least two. -/
@@ -1349,7 +1349,7 @@ theorem gameP_general Hist (X : Sequent) (sP : Strategy tableauGame Prover) (pos
         all_goals
           -- non-atomic program is impossible, X would not have been basic then
           exfalso
-          grind
+          grind only []
       · -- COPY PASTA only changed L to R
         rcases χ with ⟨α, (ψ : AnyFormula)⟩
         cases α
@@ -1377,7 +1377,7 @@ theorem gameP_general Hist (X : Sequent) (sP : Strategy tableauGame Prover) (pos
         all_goals
           -- non-atomic program is impossible, X would not have been basic then
           exfalso
-          grind
+          grind only []
     case nbas nrep X_nbas =>
       -- not basic, Prover must move to the uniform local tableau
       -- COPY PASTA from bas case ...
diff --git a/LeanPool/PDL/Completeness/Theorem.lean b/LeanPool/PDL/Completeness/Theorem.lean
index cb3592676b..1436ddd482 100644
--- a/LeanPool/PDL/Completeness/Theorem.lean
+++ b/LeanPool/PDL/Completeness/Theorem.lean
@@ -147,7 +147,7 @@ theorem completeness : ∀ X, consistent X → satisfiable X :=
   intro f f_in
   apply truthLemma M w f
   apply h
-  aesop
+  aesop (rule_sets := [-default])
 
 theorem consIffSat : ∀ X, X.isFree → (consistent X ↔ satisfiable X) :=
   fun X X_isFree => ⟨completeness X, correctness X X_isFree⟩
diff --git a/LeanPool/PDL/Discon.lean b/LeanPool/PDL/Discon.lean
index ba253eb074..2b50480e49 100644
--- a/LeanPool/PDL/Discon.lean
+++ b/LeanPool/PDL/Discon.lean
@@ -34,7 +34,7 @@ theorem conempty : con ∅ = (⊤ : Formula) := by rfl
 theorem consingle {f : Formula} : con [f] = f := by rfl
 
 theorem listEq_to_conEq : l1 = l2 → con l1 = con l2 := by
-  aesop
+  aesop (rule_sets := [-default])
 
 theorem conEvalHT {X f W M} {w : W} :
     evaluate M w (con (f :: X)) ↔ evaluate M w f ∧ evaluate M w (con X) :=
@@ -106,7 +106,7 @@ theorem disempty : dis ∅ = (⊥ : Formula) := rfl
 theorem dissingle {f : Formula} : dis [f] = f := rfl
 
 theorem listEq_to_disEq : l1 = l2 → dis l1 = dis l2 := by
-  aesop
+  aesop (rule_sets := [-default])
 
 theorem disEvalHT {X f W M} {w : W} :
     evaluate M w (dis (f :: X)) ↔ evaluate M w f ∨ evaluate M w (dis X) :=
@@ -356,7 +356,7 @@ theorem disconAnd {XS YS} : discon (XS ⊎ YS) ≡ discon XS ⋀ discon YS :=
     exists_exists_and_eq_and, exists_exists_and_exists_and_eq_and, List.mem_append, evaluate]
   rw [disconEval XS]
   rw [disconEval YS]
-  aesop
+  aesop (rule_sets := [-default])
 
 theorem union_elem_uplus {XS YS : Finset (Finset Formula)} {X Y : Finset Formula} :
   X ∈ XS → Y ∈ YS → ((X ∪ Y) ∈ (XS ⊎ YS)) :=
@@ -371,6 +371,6 @@ theorem mapCon_mapForall (M : KripkeModel W) w φ
     (∃ f ∈ List.map (fun Fδ => con (g Fδ φ)) X, evaluate M w f) ↔
     ∃ fs ∈ List.map (fun Fδ => g Fδ φ) X, ∀ f ∈ fs, evaluate M w f := by
   simp_all only [List.mem_map, Prod.exists, ↓existsAndEq, and_true]
-  constructor <;> grind [conEval]
+  constructor <;> grind only [conEval]
 
 end PDL
diff --git a/LeanPool/PDL/Distance.lean b/LeanPool/PDL/Distance.lean
index 07366b8ccf..a71f40741f 100644
--- a/LeanPool/PDL/Distance.lean
+++ b/LeanPool/PDL/Distance.lean
@@ -257,7 +257,7 @@ lemma distance_list_eq_distance_steps (M : KripkeModel W) (v w : W) δ :
     (distanceList M v w δ) = (distance M (Program.steps δ) v w) := by
   induction δ generalizing v w
   · simp_all [distanceList, distance]
-    aesop
+    aesop (rule_sets := [-default])
   case cons α δ IH =>
     simp_all [distanceList, distance]
 
@@ -466,8 +466,8 @@ theorem relateSeq_existsD_dist (v_αγ_w : relateSeq M (α :: γ) v w)
     rw [distance_list_cons] at αγ_not_inf
     rw [distance_list_cons]
     refine ⟨u, ?_, ?_, u_minimizes⟩
-    · rw [← dist_iff_rel]; aesop
-    · rw [← distance_list_iff_relate_Seq]; aesop
+    · rw [← dist_iff_rel]; aesop (rule_sets := [-default])
+    · rw [← distance_list_iff_relate_Seq]; aesop (rule_sets := [-default])
   rcases claim with ⟨u, v_α_u, u_w, αγ_eq_α_γ⟩
   have := rel_existsD_dist v_α_u -- applying (f)
   rcases this with ⟨⟨X,δ⟩, in_D, v_X, δ_eq_α⟩
@@ -577,8 +577,8 @@ theorem exists_same_distance_list_relateSeq_concat (w_δα_v : relateSeq M (δ +
   rcases this with ⟨x, same_dist⟩
   refine ⟨x, ?_, ?_, same_dist⟩
   · rw [← distance_list_iff_relate_Seq]
-    aesop
+    aesop (rule_sets := [-default])
   · rw [← dist_iff_rel]
-    aesop
+    aesop (rule_sets := [-default])
 
 end PDL
diff --git a/LeanPool/PDL/FischerLadner.lean b/LeanPool/PDL/FischerLadner.lean
index 6de9aca854..d206a3ada9 100644
--- a/LeanPool/PDL/FischerLadner.lean
+++ b/LeanPool/PDL/FischerLadner.lean
@@ -211,7 +211,7 @@ lemma FL_box_cup {φ α β ψ} :
   intro hyp
   have := FL_trans hyp
   simp [FL, FLb] at this
-  aesop
+  aesop (rule_sets := [-default])
 
 /- Lemma 6.2(iv) -/
 lemma FL_box_seq {φ α β ψ} :
@@ -219,7 +219,7 @@ lemma FL_box_seq {φ α β ψ} :
   intro hyp
   have := FL_trans hyp
   simp [FL, FLb] at this
-  aesop
+  aesop (rule_sets := [-default])
 
 /- Lemma 6.2(v) -/
 lemma FL_box_star {φ α ψ} :
@@ -227,7 +227,7 @@ lemma FL_box_star {φ α ψ} :
   intro hyp
   have := FL_trans hyp
   simp [FL, FLb] at this
-  aesop
+  aesop (rule_sets := [-default])
 
 /-! ## Closure of a list -/
 
@@ -281,7 +281,7 @@ lemma FLL_diff_sub {L K} : FLL (L \ K) ⊆ FLL L := FLL_sub (List.diff_subset L
 /-- Being a member of the FL closure of a list does not depend on the position. -/
 lemma FLL_ext (h : ∀ φ, φ ∈ L1 ↔ φ ∈ L2) φ : φ ∈ FLL L1  ↔ φ ∈ FLL L2 := by
   simp [FLL] at *
-  aesop
+  aesop (rule_sets := [-default])
 
 /-! ## FL Closure of a Finset of Formulas -/
 
@@ -305,7 +305,7 @@ lemma FL_refl_sub {X : Finset Formula} : X ⊆ X.FL := by
 lemma FL_sub {X Y : Finset Formula} : X ⊆ Y → FL X ⊆ FL Y := by
   unfold FL
   intro h x x_in
-  aesop
+  aesop (rule_sets := [-default])
 
 @[simp]
 lemma FL_nil : Finset.FL {} = {} := rfl
@@ -353,7 +353,7 @@ lemma FL_union_eq {X Y : Finset Formula} :
 lemma FL_diff_sub {X Y : Finset Formula} : FL (X \ Y) ⊆ FL X := by
   simp only [FL,]
   intro φ φ_in
-  aesop
+  aesop (rule_sets := [-default])
 
 end Finset
 
diff --git a/LeanPool/PDL/Flip.lean b/LeanPool/PDL/Flip.lean
index 71c6cd5cf9..44ebd57475 100644
--- a/LeanPool/PDL/Flip.lean
+++ b/LeanPool/PDL/Flip.lean
@@ -97,8 +97,8 @@ lemma basic_flip {X : Sequent} : X.flip.basic ↔ X.basic := by
     · intro φ φ_in
       apply fs_basic
       rcases φ_in with h|h|h|h
-      · grind
-      · grind
+      · grind only []
+      · grind only []
       · right
         right
         right
@@ -111,14 +111,14 @@ lemma basic_flip {X : Sequent} : X.flip.basic ↔ X.basic := by
         simp only [Olf.flip, Option.map_eq_some_iff, Sum.exists, Sum.swap_inl, reduceCtorEq,
           and_false, exists_false, Sum.swap_inr, Sum.inl.injEq, exists_eq_right, false_or]
         exact h
-    · aesop
+    · aesop (rule_sets := [-default])
   · intro ⟨fs_basic, not_closed⟩
     constructor
     · intro φ φ_in
       apply fs_basic
       rcases φ_in with h|h|h|h
-      · grind
-      · grind
+      · grind only []
+      · grind only []
       · right
         right
         right
@@ -131,7 +131,7 @@ lemma basic_flip {X : Sequent} : X.flip.basic ↔ X.basic := by
         simp only [Olf.flip, Option.map_eq_some_iff, Sum.exists, Sum.swap_inl, Sum.inr.injEq,
           exists_eq_right, Sum.swap_inr, reduceCtorEq, and_false, exists_false, or_false] at h
         exact h
-    · aesop
+    · aesop (rule_sets := [-default])
 
 /-- Reflect a local rule by exchanging its left and right components. -/
 def LocalRule.flip {Lcond Ocond Rcond ress} (lr : LocalRule (Lcond, Rcond, Ocond) ress) :
@@ -162,7 +162,7 @@ def LocalRule.flip {Lcond Ocond Rcond ress} (lr : LocalRule (Lcond, Rcond, Ocond
 
 lemma LocalRule.flip_flip {Lcond Ocond Rcond ress} (lr : LocalRule (Lcond, Rcond, Ocond) ress) :
     lr.flip.flip = Olf.flip_flip ▸ Sequent.image_flip_image_flip ▸ lr := by
-  cases lr <;> simp_all [LocalRule.flip] <;> grind
+  cases lr <;> simp_all [LocalRule.flip] <;> grind only []
 
 /-- Note: is it possible and useful to rewrite this in more term and less tactic mode? -/
 def LocalRuleApp.flip : LocalRuleApp → LocalRuleApp := by
@@ -191,10 +191,10 @@ lemma LocalRuleApp.flip_flip {lra : LocalRuleApp} :
   rcases lra with ⟨L, R, O, C, Lcond, Rcond, Ocond, ress, rule, hC, preconditionProof⟩
   simp only [flip, Olf.flip_flip, Sequent.image_flip_image_flip, mk.injEq, and_true, true_and]
   rw [LocalRule.flip_flip]
-  grind
+  grind only []
 
 lemma Sequent.flip_mem_of_mem_image_flip {B : Finset Sequent} {Y : Sequent} :
-    Y ∈ B.image Sequent.flip → Y.flip ∈ B := by aesop
+    Y ∈ B.image Sequent.flip → Y.flip ∈ B := by aesop (rule_sets := [-default])
 
 /-- Reflect every rule and branch of a local tableau. -/
 def LocalTableau.flip {X} : LocalTableau X → LocalTableau X.flip
@@ -216,16 +216,16 @@ lemma LocalTableau.flip_flip {lt : LocalTableau X} : lt.flip.flip = Sequent.flip
       intro X X' X_heq_X'
       apply Function.hfunext
       · rw [LocalRuleApp.flip_flip]
-        grind
-      · grind
-  · grind
+        grind only []
+      · grind only []
+  · grind only []
 
 lemma LocalTableau.flip_inj {X} {lt : LocalTableau X} :
     lt.flip.flip = (Sequent.flip_flip ▸ lt) := by
   cases lt
   case byLocalRule =>
     rw [LocalTableau.flip_flip]
-  · grind [LocalTableau.flip]
+  · grind only [LocalTableau.flip]
 
 lemma endNodesOf_flip {X} {lt : LocalTableau X} {Y} :
     Y ∈ endNodesOf lt.flip → Y.flip ∈ endNodesOf lt := by
@@ -235,7 +235,7 @@ lemma endNodesOf_flip {X} {lt : LocalTableau X} {Y} :
     simp only [LocalTableau.flip, endNodesOf, Finset.sup_image, Function.id_comp, Finset.mem_sup,
       Finset.mem_attach, true_and, Subtype.exists] at *
     rcases Y_in with ⟨W, W_in_B, Y_in_end⟩
-    refine ⟨W.flip, ?_, ?_⟩ <;> grind
+    refine ⟨W.flip, ?_, ?_⟩ <;> grind only []
   case sim Z Zbas =>
     simp_all [LocalTableau.flip]
 
@@ -296,7 +296,7 @@ def PdlRule.flip {X Y} (r : PdlRule X Y) : PdlRule X.flip Y.flip := by
 
 lemma PdlRule.flip_flip {X Y} (r : PdlRule X Y) :
     r.flip.flip = (Sequent.flip_flip ▸ Sequent.flip_flip ▸ r) := by
-  cases r <;> simp [PdlRule.flip] <;> grind
+  cases r <;> simp [PdlRule.flip] <;> grind only []
 
 /-- Flipping sequents is injective. -/
 @[simp]
@@ -336,14 +336,14 @@ lemma flprep_flip {Hist} :
     exists_eq_right, and_true, Sequent.isFree, Sequent.flip_isLoaded]
   refine ⟨?_,?_⟩
   · rintro (frep|⟨⟨lpr⟩⟩ )
-    · grind
+    · grind only []
     · have := lpr.flip
       right
       simp only [List.map_map, Sequent.flip_comp_flip, List.map_id_fun, id_eq, Sequent.flip_flip]
         at this
       exact ⟨this⟩
   · rintro (frep|⟨⟨lpr⟩⟩ )
-    · grind
+    · grind only []
     · have := lpr.flip
       right
       exact ⟨this⟩
@@ -391,9 +391,9 @@ lemma Tableau.flip_flip {Hist X} {tab : Tableau Hist X} :
     nth_rewrite 1 [Tableau.flip]
     rw [IH]; clear IH
     rw [PdlRule.flip_flip]
-    grind
+    grind only []
   case lrep lpr =>
-    grind [Tableau.flip, LoadedPathRepeat.flip_flip]
+    grind only [Tableau.flip, LoadedPathRepeat.flip_flip]
 
 /-- Map a tableau path to the corresponding path in the reflected tableau. -/
 def PathIn.flip {Hist X} {tab : Tableau Hist X} : PathIn tab → PathIn tab.flip
@@ -420,7 +420,7 @@ lemma PathIn_helper {HistA HistB XA XB} {tabA : Tableau HistA XA} {tabB : Tablea
 lemma PathIn_type_flip_flip {Hist} {tab : Tableau Hist X} :
     PathIn tab.flip.flip = PathIn tab := by
   rw [Tableau.flip_flip]
-  grind
+  grind only []
 
 /-- `Eq.mpr` is a heterogeneous identity. -/
 theorem flip_aux_eq_mpr_heq {a b : Sort u} (h : a = b) (x : b) : HEq (Eq.mpr h x) x := by
diff --git a/LeanPool/PDL/Interpolation/Cluster.lean b/LeanPool/PDL/Interpolation/Cluster.lean
index 87d0fd9dc7..6c5b2445c4 100644
--- a/LeanPool/PDL/Interpolation/Cluster.lean
+++ b/LeanPool/PDL/Interpolation/Cluster.lean
@@ -583,7 +583,7 @@ lemma stepOfL_ne_nil (C : LoadedCluster tab) {Δ : Sequent}
   have := stepOf_ne_nil C h
   unfold stepOfL
   simp
-  grind
+  grind only []
 
 /-! ### Uniformity
 
@@ -632,7 +632,7 @@ lemma mem_fineCLplus_of_child (C : LoadedCluster tab) {f g : FinePathIn tab}
     exact Or.inl h
   · unfold fineCLplus
     simp_all [fineExits]
-    grind
+    grind only []
 
 /-- The right component of a fine node of `C⁺` is in `Λ₂[C⁺]`. -/
 lemma mem_lambdaTwoPlus_of_mem_fineCLplus (C : LoadedCluster tab) {f : FinePathIn tab}
@@ -649,7 +649,7 @@ lemma lambdaTwo_subset_lambdaTwoPlus (C : LoadedCluster tab) :
   apply C.mem_lambdaTwoPlus_of_mem_fineCLplus
   unfold fineCLplus fineExits
   simp
-  grind
+  grind only []
 
 /-- The labels given by `stepOf` are in `Λ₂[C⁺]`. This is the invariant needed in Def 9.8:
 a node of `Q` is labelled with an element of `Λ₂[C⁺]`, and it is a leaf exactly when it is
@@ -719,7 +719,7 @@ lemma LoadedCluster.thetaOf_left (C : LoadedCluster tab) (θ : FinePathIn tab 
     simp only [evaluate, thetaOf, Finset.disEval, Finset.mem_image, exists_exists_and_eq_and,
       not_exists, not_and] at h1 ⊢
     intro hcon
-    grind
+    grind only []
   · exact hw _ (Finset.mem_union_right _ hmem)
 
 open HasSat in
diff --git a/LeanPool/PDL/Interpolation/ClusterRho.lean b/LeanPool/PDL/Interpolation/ClusterRho.lean
index 171d47099f..b8e8d74e0f 100644
--- a/LeanPool/PDL/Interpolation/ClusterRho.lean
+++ b/LeanPool/PDL/Interpolation/ClusterRho.lean
@@ -110,7 +110,7 @@ lemma evaluate_rho_iff {W} {M : KripkeModel W} {w : W} {n} (h : C.Q.atOpt x = so
   constructor
   · rintro ⟨_, t, hev⟩
     simp [conEval] at hev
-    grind
+    grind only []
   · rintro ⟨t, ht, hev⟩
     simp only [conEval, Formula.mem_pdlSort]
     use t
@@ -243,7 +243,7 @@ lemma leftEntails_thetaOf (hθ : ∀ f ∈ C.fineExits, isPartInterpolant f.labe
   by_contra hcon
   exact C.thetaOf_left θ hθ Δ t ht ⟨W, M, w, by
     intro φ hφ
-    aesop⟩
+    aesop (rule_sets := [-default])⟩
 
 /-- Case `k(x) = 1` where `x` is a leaf that is not a repeat: `ι_x = θ_{Δ_x}` and every
 node of the region is an exit node, so Lemma 9.14 (a) applies. -/
diff --git a/LeanPool/PDL/Interpolation/FinePath.lean b/LeanPool/PDL/Interpolation/FinePath.lean
index c91c20aca6..bee097e6fc 100644
--- a/LeanPool/PDL/Interpolation/FinePath.lean
+++ b/LeanPool/PDL/Interpolation/FinePath.lean
@@ -224,7 +224,7 @@ lemma LocalPathIn.mem_internalLocalPaths {X} {lt : LocalTableau X} (lp : LocalPa
     simp only [internalLocalPaths, List.mem_cons, reduceCtorEq, List.mem_flatMap, List.mem_attach,
       List.mem_map, cons.injEq, true_and, Subtype.exists, Finset.mem_seqSort, false_or]
     exact ⟨Y, Y_in, tail, IH (by simpa [LocalPathIn.isInternal, LocalPathIn.ltAt] using! h),
-      rfl, by grind⟩
+      rfl, by grind only []⟩
 
 /-! ## Fine paths: all nodes of a tableau
 
@@ -351,7 +351,7 @@ theorem FinePathIn.mem_allFinePaths {H X} {tab : Tableau H X} (f : FinePathIn ta
     simp only [allFinePaths, List.mem_append, List.mem_map, List.mem_attach, reduceCtorEq,
       and_false, exists_false, List.mem_flatMap, loc.injEq, true_and, Subtype.exists,
       Finset.mem_seqSort, false_or]
-    exact ⟨_, Y_in, tail, IH, rfl, by grind⟩
+    exact ⟨_, Y_in, tail, IH, rfl, by grind only []⟩
   case pdl tail IH =>
     simp only [allFinePaths, List.mem_cons, List.mem_map]
     exact Or.inr ⟨tail, IH, rfl⟩
@@ -648,7 +648,7 @@ lemma FinePathIn.exists_child_coarseChildrenBelow {H X} {tab : Tableau H X}
     obtain ⟨g, g_in, hg⟩ := IH q' hq'
     refine ⟨.loc Y_in g, by
       simp only [children, Finset.mem_image, loc.injEq, heq_eq_eq, true_and,
-        exists_eq_right]; grind, ?_⟩
+        exists_eq_right]; grind only [], ?_⟩
     rcases hg with ⟨h1, h2⟩ | ⟨h1, h2⟩
     · exact Or.inl ⟨by simp [FinePathIn.base, h1], by
         simp only [FinePathIn.coarseChildrenBelow, List.mem_map]; exact ⟨q', h2, rfl⟩⟩
@@ -658,7 +658,7 @@ lemma FinePathIn.exists_child_coarseChildrenBelow {H X} {tab : Tableau H X}
     obtain ⟨q', hq', rfl⟩ := hq
     obtain ⟨g, g_in, hg⟩ := IH q' hq'
     refine ⟨.pdl g, by simp only [children, Finset.mem_image, pdl.injEq,
-      exists_eq_right]; grind, ?_⟩
+      exists_eq_right]; grind only [], ?_⟩
     rcases hg with ⟨h1, h2⟩ | ⟨h1, h2⟩
     · exact Or.inl ⟨by simp [FinePathIn.base, h1], by
         simp only [FinePathIn.coarseChildrenBelow, List.mem_map]; exact ⟨q', h2, rfl⟩⟩
diff --git a/LeanPool/PDL/Interpolation/Local.lean b/LeanPool/PDL/Interpolation/Local.lean
index 699a3d2219..118f54d846 100644
--- a/LeanPool/PDL/Interpolation/Local.lean
+++ b/LeanPool/PDL/Interpolation/Local.lean
@@ -47,9 +47,9 @@ lemma LoadRule.voc {ress} (lr : LoadRule (~'χ) ress) : lfovocFin ress ⊆ χ.vo
       negUnload, Formula.voc.eq_3] at *
     · rcases x_in_V with ⟨f, f_in_fs, x_in⟩
       specialize unfvoc f_in_fs
-      aesop
+      aesop (rule_sets := [-default])
     · simp [pairUnload] at unfvoc
-      rcases x_in_V with ⟨f, f_in_fs, x_in⟩|_ <;> aesop
+      rcases x_in_V with ⟨f, f_in_fs, x_in⟩|_ <;> aesop (rule_sets := [-default])
   case dia' α φ notAtom =>
     have unfvoc := @unfoldDiamond_voc x α φ
     rw [← unfoldDiamondLoaded'_eq α φ] at unfvoc
@@ -64,9 +64,9 @@ lemma LoadRule.voc {ress} (lr : LoadRule (~'χ) ress) : lfovocFin ress ⊆ χ.vo
       negUnload, Formula.voc.eq_3] at *
     · rcases x_in_V with ⟨f, f_in_fs, x_in⟩
       specialize unfvoc f_in_fs
-      aesop
+      aesop (rule_sets := [-default])
     · simp [pairUnload] at unfvoc
-      rcases x_in_V with ⟨f, f_in_fs, x_in⟩|_ <;> aesop
+      rcases x_in_V with ⟨f, f_in_fs, x_in⟩|_ <;> aesop (rule_sets := [-default])
 
 theorem localRule_does_not_increase_vocab_L {Cond B}
     (rule : LocalRule Cond B) :
@@ -83,10 +83,10 @@ theorem localRule_does_not_increase_vocab_L {Cond B}
       Finset.sup_image, Function.id_comp, Finset.mem_sup] at *
     rcases x_in_res with ⟨ψ, ψ_in, x_in_voc_ψ⟩
     cases orule
-    case nCo => aesop
+    case nCo => aesop (rule_sets := [-default])
     case box α φ α_notAt => have := unfoldBox_voc_fin L_in ψ_in x_in_voc_ψ; simp_all
     case dia => have := unfoldDiamond_voc_fin L_in ψ_in x_in_voc_ψ; simp_all
-    all_goals aesop
+    all_goals aesop (rule_sets := [-default])
   case loadedL ress χ lrule B_def =>
     subst B_def
     simp only [Finset.mem_image, Prod.exists] at res_in_B
@@ -109,7 +109,7 @@ theorem localRule_does_not_increase_vocab_L {Cond B}
       · simpa [Olf.L, onlfvoc] using h
   -- other cases are all trivial (as in Bml)
   all_goals
-    aesop
+    aesop (rule_sets := [-default])
 
 theorem localRule_does_not_increase_vocab_R {Cond} (rule : LocalRule Cond B) :
     ∀ res ∈ B, res.right.pdlFvoc ⊆ Cond.right.pdlFvoc := by
@@ -125,10 +125,10 @@ theorem localRule_does_not_increase_vocab_R {Cond} (rule : LocalRule Cond B) :
       Finset.sup_image, Function.id_comp, Finset.mem_sup] at *
     rcases x_in_res with ⟨ψ, ψ_in, x_in_voc_ψ⟩
     cases orule
-    case nCo => aesop
+    case nCo => aesop (rule_sets := [-default])
     case box α φ α_notAt => have := unfoldBox_voc_fin L_in ψ_in x_in_voc_ψ; simp_all
     case dia => have := unfoldDiamond_voc_fin L_in ψ_in x_in_voc_ψ; simp_all
-    all_goals aesop
+    all_goals aesop (rule_sets := [-default])
   case loadedR ress χ lrule B_def =>
     subst B_def
     simp only [Finset.mem_image, Prod.exists] at res_in_B
@@ -151,7 +151,7 @@ theorem localRule_does_not_increase_vocab_R {Cond} (rule : LocalRule Cond B) :
       · simpa [Olf.R, onlfvoc] using h
   -- other cases are all trivial (as in Bml)
   all_goals
-    aesop
+    aesop (rule_sets := [-default])
 
 theorem localRuleApp_does_not_increase_jvoc (lra : LocalRuleApp) :
     ∀ Y ∈ lra.C, jvoc Y ⊆ jvoc lra.X := by
diff --git a/LeanPool/PDL/Interpolation/QFormula.lean b/LeanPool/PDL/Interpolation/QFormula.lean
index 0e4527ecd0..6de1c7142a 100644
--- a/LeanPool/PDL/Interpolation/QFormula.lean
+++ b/LeanPool/PDL/Interpolation/QFormula.lean
@@ -246,7 +246,7 @@ theorem voc_nf (σ : Var → Formula) (ι : QFormula Var) :
   | and ι1 ι2 IH1 IH2 =>
       rw [mem_voc_nf] at IH1 IH2 ⊢
       simp only [Spl, List.mem_append, subst_and, Formula.voc, Finset.mem_union]
-      grind
+      grind only []
   | boxes as ι IH =>
       rw [mem_voc_nf] at IH ⊢
       simp only [Spl, List.mem_map, subst_boxes, Formula.voc_boxes, Finset.mem_union]
diff --git a/LeanPool/PDL/Interpolation/SingletonCluster.lean b/LeanPool/PDL/Interpolation/SingletonCluster.lean
index 1efebe3540..6f628a609b 100644
--- a/LeanPool/PDL/Interpolation/SingletonCluster.lean
+++ b/LeanPool/PDL/Interpolation/SingletonCluster.lean
@@ -27,7 +27,7 @@ lemma isPartInterpolant_of_mem_iff {Z Y : Sequent} {θ : Formula}
     simp only [jvoc, Finset.mem_inter] at x_in ⊢
     have := fvoc_subset_of_mem_voc (fun f hf => ⟨f, (hl f).mpr hf, subset_rfl⟩) x_in.1
     have := fvoc_subset_of_mem_voc (fun f hf => ⟨f, (hr f).mpr hf, subset_rfl⟩) x_in.2
-    grind
+    grind only []
   · rw [Finset.ext hl]; exact hL
   · rw [Finset.ext hr]; exact hR
 
@@ -72,7 +72,6 @@ The rules treated here are (L-), i.e. `freeL` and `freeR`, and the modal rule (M
 which form a singleton cluster. -/
 
 
--- Reason: the many `simp` calls about `Finset` membership below are slow.
 open HasSat in
 /-- Interpolant for the modal rule (M) applied to a node loaded on the left.
 The lists `Xl, Xr` are the two components of the premise and `Yl, Yr` those of the
@@ -137,9 +136,10 @@ lemma exists_itp_modL {A : Nat} {L R Xl Xr Yl Yr : Finset Formula} {ψ θ : Form
         rw [Finset.mem_inter] at this ⊢
         exact ⟨hYlXl this.1, hYrXr this.2⟩
     · rintro ⟨W, M, w, hw⟩
-      have hXlw : ∀ f ∈ Xl, evaluate M w f := fun f hf => hw f (by simp_all)
+      have hXlw : ∀ f ∈ Xl, evaluate M w f := fun f hf => hw f (Finset.mem_union_right _ hf)
       obtain ⟨v, hv, hvYl⟩ := exists_succ W M w hXlw
-      have h1 : evaluate M w (~~⌈·A⌉(~θ)) := hw _ (by simp_all)
+      have h1 : evaluate M w (~~⌈·A⌉(~θ)) :=
+        hw _ (Finset.mem_union_left _ (Finset.mem_singleton_self _))
       simp only [evaluate, relate, not_not] at h1
       refine hL ⟨W, M, v, ?_⟩
       intro f hf
@@ -148,8 +148,9 @@ lemma exists_itp_modL {A : Nat} {L R Xl Xr Yl Yr : Finset Formula} {ψ θ : Form
       · exact h1 v hv
       · exact hvYl f hf
     · rintro ⟨W, M, w, hw⟩
-      have hXrw : ∀ f ∈ Xr, evaluate M w f := fun f hf => hw f (by simp; tauto)
-      have h1 : evaluate M w (~⌈·A⌉(~θ)) := hw _ (by simp)
+      have hXrw : ∀ f ∈ Xr, evaluate M w f := fun f hf => hw f (Finset.mem_union_right _ hf)
+      have h1 : evaluate M w (~⌈·A⌉(~θ)) :=
+        hw _ (Finset.mem_union_left _ (Finset.mem_singleton_self _))
       simp only [evaluate, relate, not_forall, not_not] at h1
       obtain ⟨v, hv, hvθ⟩ := h1
       refine hR ⟨W, M, v, ?_⟩
@@ -179,11 +180,10 @@ lemma exists_itp_modL {A : Nat} {L R Xl Xr Yl Yr : Finset Formula} {ψ θ : Form
       · exact hvYl f hf
     refine ⟨⊥, by simp, ?_, ?_⟩
     · rintro ⟨W, M, w, hw⟩
-      exact Xl_unsat ⟨W, M, w, fun f hf => hw f (by simp_all)⟩
+      exact Xl_unsat ⟨W, M, w, fun f hf => hw f (Finset.mem_union_right _ hf)⟩
     · rintro ⟨W, M, w, hw⟩
-      simp_all
+      exact hw ⊥ (Finset.mem_union_left _ (Finset.mem_singleton_self _))
 
--- Reason: the many `simp` calls about `Finset` membership below are slow.
 open HasSat in
 /-- Interpolant for the modal rule (M) applied to a node loaded on the right.
 The interpolant is `⌈·A⌉θ`, unless the projection of the left component is empty,
@@ -246,8 +246,9 @@ lemma exists_itp_modR {A : Nat} {L R Xl Xr Yl Yr : Finset Formula} {ψ θ : Form
         rw [Finset.mem_inter] at this ⊢
         exact ⟨hYlXl this.1, hYrXr this.2⟩
     · rintro ⟨W, M, w, hw⟩
-      have hXlw : ∀ f ∈ Xl, evaluate M w f := fun f hf => hw f (by simp_all)
-      have h1 : evaluate M w (~⌈·A⌉θ) := hw _ (by simp_all)
+      have hXlw : ∀ f ∈ Xl, evaluate M w f := fun f hf => hw f (Finset.mem_union_right _ hf)
+      have h1 : evaluate M w (~⌈·A⌉θ) :=
+        hw _ (Finset.mem_union_left _ (Finset.mem_singleton_self _))
       simp only [evaluate, relate, not_forall] at h1
       obtain ⟨v, hv, hvθ⟩ := h1
       refine hL ⟨W, M, v, ?_⟩
@@ -257,9 +258,10 @@ lemma exists_itp_modR {A : Nat} {L R Xl Xr Yl Yr : Finset Formula} {ψ θ : Form
       · simpa using hvθ
       · exact succ_Yl W M w v hXlw hv f hf
     · rintro ⟨W, M, w, hw⟩
-      have hXrw : ∀ f ∈ Xr, evaluate M w f := fun f hf => hw f (by simp_all)
+      have hXrw : ∀ f ∈ Xr, evaluate M w f := fun f hf => hw f (Finset.mem_union_right _ hf)
       obtain ⟨v, hv, hvYr⟩ := exists_succ W M w hXrw
-      have h1 : evaluate M w (⌈·A⌉θ) := hw _ (by simp_all)
+      have h1 : evaluate M w (⌈·A⌉θ) :=
+        hw _ (Finset.mem_union_left _ (Finset.mem_singleton_self _))
       simp only [evaluate, relate] at h1
       refine hR ⟨W, M, v, ?_⟩
       intro f hf
@@ -289,9 +291,9 @@ lemma exists_itp_modR {A : Nat} {L R Xl Xr Yl Yr : Finset Formula} {ψ θ : Form
       · exact hvYr f hf
     refine ⟨~⊥, by simp, ?_, ?_⟩
     · rintro ⟨W, M, w, hw⟩
-      simpa using hw (~~⊥) (by simp_all)
+      exact hw (~~⊥) (Finset.mem_union_left _ (Finset.mem_singleton_self _)) id
     · rintro ⟨W, M, w, hw⟩
-      exact Xr_unsat ⟨W, M, w, fun f hf => hw f (by simp_all)⟩
+      exact Xr_unsat ⟨W, M, w, fun f hf => hw f (Finset.mem_union_right _ hf)⟩
 
 /-- Given an interpolant for the conclusion of a `PdlRule` applied to a *loaded* sequent,
 we get an interpolant for the premise. This is the loaded analogue of
diff --git a/LeanPool/PDL/Local/AllLocalTab.lean b/LeanPool/PDL/Local/AllLocalTab.lean
index 598614c889..84e3293be9 100644
--- a/LeanPool/PDL/Local/AllLocalTab.lean
+++ b/LeanPool/PDL/Local/AllLocalTab.lean
@@ -406,7 +406,7 @@ lemma LocalRuleApp.all_X (X : Sequent) : ∀ lra ∈ LocalRuleApp.all X, lra.X =
   simp only [all, List.reduceOption_mem_iff, List.mem_map, List.mem_attach, true_and,
     Subtype.exists, List.mem_flatMap, List.mem_sublists, List.mem_cons,
     List.not_mem_nil, or_false] at lra_in
-  grind [Option.map_eq_some_iff]
+  grind only [Option.map_eq_some_iff]
 
 lemma LocalRuleApp.all_spec (lrA : LocalRuleApp) : lrA ∈ LocalRuleApp.all lrA.X := by
   rcases lrA with ⟨L, R, O, Lcond, Rcond, Ocond, ress, lr, C, hC, ⟨hL, hR, hO⟩⟩
@@ -642,8 +642,8 @@ lemma combo_mem_of_forall_in {α : Type} [DecidableEq α] {q : α → Type} {L :
     cases x_in
   case cons x xs IH =>
     simp only [combo, List.mem_flatMap, List.mem_map]
-    specialize IH (fun y y_in => f y (by aesop))
-    exact ⟨fun y y_in => g _ (by simp_all), IH _ (by grind), (by grind)⟩
+    specialize IH (fun y y_in => f y (by aesop (rule_sets := [-default])))
+    exact ⟨fun y y_in => g _ (by simp_all), IH _ (by grind only []), (by grind only [])⟩
 
 /-- Version of `combo` for `Finset`s. -/
 def comboF {q : Sequent → Type} (s : Finset Sequent)
diff --git a/LeanPool/PDL/Local/Rules.lean b/LeanPool/PDL/Local/Rules.lean
index bbaba80f81..f8e6f8d7e6 100644
--- a/LeanPool/PDL/Local/Rules.lean
+++ b/LeanPool/PDL/Local/Rules.lean
@@ -364,7 +364,7 @@ lemma oneSidedL_preserves_right {LRO : Sequent}
   rintro ⟨L',R',O'⟩
   subst YS_def
   simp at *
-  grind
+  grind only []
 
 lemma oneSidedR_preserves_left {LRO : Sequent}
     {Rcond : Finset Formula} (Rpreproof : Rcond ⊆ LRO.R)
@@ -375,7 +375,7 @@ lemma oneSidedR_preserves_left {LRO : Sequent}
   rintro ⟨L',R',O'⟩
   subst YS_def
   simp at *
-  grind
+  grind only []
 
 open HasSat
 
@@ -388,7 +388,7 @@ lemma oneSidedL_sat_down (LRO : Sequent)
   rcases LRO with ⟨L,R,O⟩
   subst YS_def
   rcases LX_sat with ⟨W, M, w, satM⟩
-  have : evaluate M w (con Lcond.sort) := by simp [conEval]; aesop
+  have : evaluate M w (con Lcond.sort) := by simp [conEval]; aesop (rule_sets := [-default])
   have := (oneSidedLocalRuleTruth orule W M w).1 this
   rw [Finset.disconEval] at this
   rcases this with ⟨L', L'_in, w_L'⟩
@@ -397,7 +397,7 @@ lemma oneSidedL_sat_down (LRO : Sequent)
   refine ⟨L', L'_in, W, M, w, fun φ φ_in => ?_⟩
   specialize @satM φ
   simp only [Finset.mem_union, Finset.mem_sdiff] at φ_in
-  rcases φ_in with φ_in_LnoCond | φ_in_L' | φ_in_O <;> aesop
+  rcases φ_in with φ_in_LnoCond | φ_in_L' | φ_in_O <;> aesop (rule_sets := [-default])
 
 lemma oneSidedR_sat_down (LRO : Sequent)
     {Rcond : Finset Formula} (Rpreproof : Rcond ⊆ LRO.R)
@@ -408,7 +408,7 @@ lemma oneSidedR_sat_down (LRO : Sequent)
   rcases LRO with ⟨L,R,O⟩
   subst YS_def
   rcases RX_sat with ⟨W, M, w, satM⟩
-  have : evaluate M w (con Rcond.sort) := by simp [conEval]; aesop
+  have : evaluate M w (con Rcond.sort) := by simp [conEval]; aesop (rule_sets := [-default])
   have := (oneSidedLocalRuleTruth orule W M w).1 this
   rw [Finset.disconEval] at this
   rcases this with ⟨L', L'_in, w_L'⟩
@@ -417,7 +417,7 @@ lemma oneSidedR_sat_down (LRO : Sequent)
   refine ⟨L', L'_in, W, M, w, fun φ φ_in => ?_⟩
   specialize @satM φ
   simp only [Finset.mem_union, Finset.mem_sdiff] at φ_in
-  rcases φ_in with φ_in_LnoCond | φ_in_L' | φ_in_O <;> aesop
+  rcases φ_in with φ_in_LnoCond | φ_in_L' | φ_in_O <;> aesop (rule_sets := [-default])
 
 -- Following four lemmas are almost the same, but then for the loaded diamond rules.
 
@@ -873,11 +873,11 @@ lemma nonbasic_of_localRuleApp (lra : LocalRuleApp) : ¬ lra.X.basic := by
   case LRnegL =>
     right
     simp [Sequent.closed]
-    aesop
+    aesop (rule_sets := [-default])
   case LRnegR =>
     right
     simp [Sequent.closed]
-    aesop
+    aesop (rule_sets := [-default])
   case loadedL ress χ lrule ress_def =>
     obtain ⟨-, -, hO⟩ := preconditionProof
     rw [Option.some_subseteq] at hO
@@ -981,7 +981,7 @@ lemma basic_iff_noLocalRuleApp {Y : Sequent} :
     Y.basic ↔ ¬ ∃ (lra : LocalRuleApp),lra.X = Y := by
   constructor
   · have := nonbasic_of_localRuleApp
-    grind
+    grind only []
   · intro no_lra
     by_contra Y_nonbas
     unfold Sequent.basic at Y_nonbas
@@ -1000,11 +1000,11 @@ lemma basic_iff_noLocalRuleApp {Y : Sequent} :
         simp only [LocalRuleApp.X, not_exists, Sequent.mem_def, Sequent.L_eq, Sequent.R_eq] at *
         cases φ_in <;> cases not_φ_in
         · refine ⟨⟨L,R,O, {φ, ~φ}, {}, none, {}, .oneSidedL (.not _) rfl, {}, rfl, ?_⟩, by simp⟩
-          simp_all; grind
+          simp_all; grind only [Finset.insert_subset_iff, Finset.singleton_subset_iff]
         · exact ⟨⟨L,R,O, {φ}, {~φ}, none, {}, LocalRule.LRnegL φ, {}, rfl, by simp_all⟩, by simp⟩
         · exact ⟨⟨L,R,O, {~φ}, {φ}, none, {}, LocalRule.LRnegR φ, {}, rfl, by simp_all⟩, by simp⟩
         · refine ⟨⟨L,R,O, {}, {φ, ~φ}, none, {}, .oneSidedR (.not _) rfl, {}, rfl, ?_⟩, by simp⟩
-          simp_all; grind
+          simp_all; grind only [Finset.insert_subset_iff, Finset.singleton_subset_iff]
     rcases Y with ⟨L,R,O⟩
     simp_all only [LocalRuleApp.X, not_exists, Sequent.toFinset, Finset.union_assoc,
       Finset.mem_union, Option.mem_toFinset, Option.mem_def, Option.map_eq_some_iff, Sum.exists,
@@ -1067,30 +1067,40 @@ lemma LocalRuleApp.preserve_bottom_down (lra : LocalRuleApp) :
     ∀ Y ∈ lra.C, ⊥ ∈ lra.X.toFinset → ⊥ ∈ Y.toFinset := by
   rcases lra with ⟨L, R, O, Lcond, Rcond, Ocond, ress, rule, C, hC, pre⟩
   subst hC
-  cases rule <;> simp_all only [applyLocalRule, Finset.sdiff_empty, Finset.mem_image,
+  dsimp only [LocalRuleApp.X]
+  cases rule
+  case' oneSidedL => clear pre
+  case' oneSidedR => clear pre
+  all_goals simp_all only [applyLocalRule, Finset.sdiff_empty, Finset.mem_image,
     exists_exists_and_eq_and, Finset.union_empty, Olf.change_old_none_none, Sequent.toFinset,
     Finset.union_assoc, Finset.mem_union, Option.mem_toFinset, Option.mem_def,
     Option.map_eq_some_iff, Sum.exists, Sum.elim_inl, negUnload, reduceCtorEq, and_false,
     exists_false, Sum.elim_inr, or_self, or_false, forall_exists_index, and_imp,
     forall_apply_eq_imp_iff₂, Finset.mem_sdiff, Finset.image_empty, Finset.notMem_empty,
     exists_const_iff, and_true, IsEmpty.forall_iff, implies_true, Prod.exists, ↓existsAndEq]
-  case oneSidedL ress orule ress_def => cases orule <;> simp_all <;> grind
-  case oneSidedR ress orule ress_def => cases orule <;> simp_all <;> grind
+  case oneSidedL ress orule ress_def =>
+    cases orule <;> simp_all <;> grind only []
+  case oneSidedR ress orule ress_def =>
+    cases orule <;> simp_all <;> grind only []
   case loadedL ress chi lrule ress_def => cases lrule <;> simp_all only [Finset.empty_subset,
     Option.some_subseteq, true_and, List.pdlToFinFinOpt, List.mem_toFinset, List.mem_map,
     Prod.mk.injEq, Prod.exists, exists_eq_right_right, forall_exists_index, and_imp] <;>
-    intros <;> subst_eqs <;> simp_all <;> grind
+    intros <;> subst_eqs <;> simp_all <;> grind only []
   case loadedR ress chi lrule ress_def => cases lrule <;> simp_all only [Finset.empty_subset,
     Option.some_subseteq, true_and, List.pdlToFinFinOpt, List.mem_toFinset, List.mem_map,
     Prod.mk.injEq, Prod.exists, exists_eq_right_right, forall_exists_index, and_imp] <;>
-    intros <;> subst_eqs <;> simp_all <;> grind
+    intros <;> subst_eqs <;> simp_all <;> grind only []
 
 lemma LocalRuleApp.preserve_atom_down (lra : LocalRuleApp) :
     ∀ Y ∈ lra.C, ∀ p : Nat,
       Formula.atom_prop p ∈ lra.X.toFinset → Formula.atom_prop p ∈ Y.toFinset := by
   rcases lra with ⟨L, R, O, Lcond, Rcond, Ocond, ress, rule, C, hC, pre⟩
   subst hC
-  cases rule <;> simp_all only [applyLocalRule, Finset.sdiff_empty, Finset.mem_image,
+  dsimp only [LocalRuleApp.X]
+  cases rule
+  case' oneSidedL => clear pre
+  case' oneSidedR => clear pre
+  all_goals simp_all only [applyLocalRule, Finset.sdiff_empty, Finset.mem_image,
     exists_exists_and_eq_and, Finset.union_empty, Olf.change_old_none_none, Sequent.toFinset,
     Finset.union_assoc, Finset.mem_union, Option.mem_toFinset, Option.mem_def,
     Option.map_eq_some_iff, Sum.exists, Sum.elim_inl, negUnload, reduceCtorEq, and_false,
@@ -1098,43 +1108,51 @@ lemma LocalRuleApp.preserve_atom_down (lra : LocalRuleApp) :
     forall_apply_eq_imp_iff₂, Finset.mem_sdiff, Finset.image_empty, Finset.notMem_empty,
     exists_const_iff, and_true, not_isEmpty_of_nonempty, IsEmpty.forall_iff, implies_true,
     Prod.exists, ↓existsAndEq]
-  case oneSidedL ress orule ress_def => cases orule <;> simp_all <;> grind
-  case oneSidedR ress orule ress_def => cases orule <;> simp_all <;> grind
+  case oneSidedL ress orule ress_def =>
+    cases orule <;> simp_all <;> grind only []
+  case oneSidedR ress orule ress_def =>
+    cases orule <;> simp_all <;> grind only []
   case loadedL ress chi lrule ress_def =>
     cases lrule <;> simp_all only [Finset.empty_subset, Option.some_subseteq, true_and,
       List.pdlToFinFinOpt, List.mem_toFinset, List.mem_map, Prod.mk.injEq, Prod.exists,
       exists_eq_right_right, forall_exists_index, and_imp] <;> intros <;> subst_eqs <;> simp_all
-        <;> grind
+        <;> grind only []
   case loadedR ress chi lrule ress_def =>
     cases lrule <;> simp_all only [Finset.empty_subset, Option.some_subseteq, true_and,
       List.pdlToFinFinOpt, List.mem_toFinset, List.mem_map, Prod.mk.injEq, Prod.exists,
       exists_eq_right_right, forall_exists_index, and_imp] <;> intros <;> subst_eqs <;> simp_all
-        <;> grind
+        <;> grind only []
 
 lemma LocalRuleApp.preserve_neg_atom_down (lra : LocalRuleApp) :
     ∀ Y ∈ lra.C, ∀ p : Nat,
       (~(Formula.atom_prop p)) ∈ lra.X.toFinset → (~(Formula.atom_prop p)) ∈ Y.toFinset := by
   rcases lra with ⟨L, R, O, Lcond, Rcond, Ocond, ress, rule, C, hC, pre⟩
   subst hC
-  cases rule <;> simp_all only [applyLocalRule, Finset.sdiff_empty, Finset.mem_image,
+  dsimp only [LocalRuleApp.X]
+  cases rule
+  case' oneSidedL => clear pre
+  case' oneSidedR => clear pre
+  all_goals simp_all only [applyLocalRule, Finset.sdiff_empty, Finset.mem_image,
     exists_exists_and_eq_and, Finset.union_empty, Olf.change_old_none_none, Sequent.toFinset,
     Finset.union_assoc, Finset.mem_union, Option.mem_toFinset, Option.mem_def,
     Option.map_eq_some_iff, Sum.exists, Sum.elim_inl, negUnload, Formula.neg.injEq, Sum.elim_inr,
     forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, Finset.mem_sdiff, Finset.image_empty,
     Finset.notMem_empty, not_isEmpty_of_nonempty, IsEmpty.forall_iff, implies_true, Prod.exists,
     ↓existsAndEq, and_true]
-  case oneSidedL ress orule ress_def => cases orule <;> grind
-  case oneSidedR ress orule ress_def => cases orule <;> grind
+  case oneSidedL ress orule ress_def =>
+    cases orule <;> grind only [Finset.mem_insert, Finset.mem_singleton, Finset.notMem_empty]
+  case oneSidedR ress orule ress_def =>
+    cases orule <;> grind only [Finset.mem_insert, Finset.mem_singleton, Finset.notMem_empty]
   case loadedL ress chi lrule ress_def =>
     cases lrule <;> simp_all only [Finset.empty_subset, Option.some_subseteq, true_and,
       List.pdlToFinFinOpt, List.mem_toFinset, List.mem_map, Prod.mk.injEq, Prod.exists,
       exists_eq_right_right, forall_exists_index, and_imp] <;> intros <;> subst_eqs <;> simp_all
-        <;> grind
+        <;> grind only []
   case loadedR ress chi lrule ress_def =>
     cases lrule <;> simp_all only [Finset.empty_subset, Option.some_subseteq, true_and,
       List.pdlToFinFinOpt, List.mem_toFinset, List.mem_map, Prod.mk.injEq, Prod.exists,
       exists_eq_right_right, forall_exists_index, and_imp] <;> intros <;> subst_eqs <;> simp_all
-        <;> grind
+        <;> grind only []
 
 lemma LocalRuleApp.preserve_local_atom_down (lra : LocalRuleApp) :
     ∀ Y ∈ lra.C, ∀ f,
@@ -1232,7 +1250,7 @@ private theorem formulaExpansion_oneSidedL
     · subst f; right; simp
     · left
       rcases hf with hf | hf | hf | hf
-      all_goals aesop
+      all_goals aesop (rule_sets := [-default])
   case con φ ψ =>
     simp_all only [applyLocalRule, Finset.sdiff_empty, Finset.image_singleton,
       Finset.union_insert, Finset.union_singleton, Finset.union_empty, Olf.change_old_none_none,
@@ -1246,7 +1264,7 @@ private theorem formulaExpansion_oneSidedL
     · subst f; right; simp
     · left
       rcases hf with hf | hf | hf | hf
-      all_goals aesop
+      all_goals aesop (rule_sets := [-default])
   case nCo φ ψ =>
     simp_all only [applyLocalRule, Finset.sdiff_empty, Finset.image_insert,
       Finset.image_singleton, Finset.union_singleton, Finset.union_empty,
@@ -1260,10 +1278,10 @@ private theorem formulaExpansion_oneSidedL
       right
       intro φ' ψ' _
       rcases hY with hY | hY <;> subst Y <;>
-        simp <;> aesop
+        simp <;> aesop (rule_sets := [-default])
     · left
       rcases hf with hf | hf | hf | hf
-      all_goals aesop
+      all_goals aesop (rule_sets := [-default])
   case box α φ notAtom =>
     simp_all only [applyLocalRule, Finset.sdiff_empty, List.pdlToFinFin, Finset.mem_image,
       List.mem_toFinset, List.mem_map, exists_exists_and_eq_and, Finset.union_empty,
@@ -1288,7 +1306,7 @@ private theorem formulaExpansion_oneSidedL
       simp [hx]
     · left
       rcases hf with hf | hf | hf | hf
-      all_goals aesop
+      all_goals aesop (rule_sets := [-default])
   case dia α φ notAtom =>
     simp_all only [applyLocalRule, Finset.sdiff_empty, List.pdlToFinFin, Finset.mem_image,
       List.mem_toFinset, List.mem_map, exists_exists_and_eq_and, Finset.union_empty,
@@ -1315,7 +1333,7 @@ private theorem formulaExpansion_oneSidedL
       simp [hx]
     · left
       rcases hf with hf | hf | hf | hf
-      all_goals aesop
+      all_goals aesop (rule_sets := [-default])
   all_goals simp_all [applyLocalRule]
 
 /-- Preservation and expansion for a local rule acting on the R component. -/
@@ -1347,7 +1365,7 @@ private theorem formulaExpansion_oneSidedR
     · subst f; right; simp
     · left
       rcases hf with hf | hf | hf | hf
-      all_goals aesop
+      all_goals aesop (rule_sets := [-default])
   case con φ ψ =>
     simp_all only [applyLocalRule, Finset.sdiff_empty, Finset.image_singleton,
       Finset.union_insert, Finset.union_singleton, Finset.union_empty, Olf.change_old_none_none,
@@ -1361,7 +1379,7 @@ private theorem formulaExpansion_oneSidedR
     · subst f; right; simp
     · left
       rcases hf with hf | hf | hf | hf
-      all_goals aesop
+      all_goals aesop (rule_sets := [-default])
   case nCo φ ψ =>
     simp_all only [applyLocalRule, Finset.sdiff_empty, Finset.image_insert,
       Finset.image_singleton, Finset.union_singleton, Finset.union_empty,
@@ -1375,10 +1393,10 @@ private theorem formulaExpansion_oneSidedR
       right
       intro φ' ψ' _
       rcases hY with hY | hY <;> subst Y <;>
-        simp <;> aesop
+        simp <;> aesop (rule_sets := [-default])
     · left
       rcases hf with hf | hf | hf | hf
-      all_goals aesop
+      all_goals aesop (rule_sets := [-default])
   case box α φ notAtom =>
     simp_all only [applyLocalRule, Finset.sdiff_empty, List.pdlToFinFin, Finset.mem_image,
       List.mem_toFinset, List.mem_map, exists_exists_and_eq_and, Finset.union_empty,
@@ -1403,7 +1421,7 @@ private theorem formulaExpansion_oneSidedR
       simp [hx]
     · left
       rcases hf with hf | hf | hf | hf
-      all_goals aesop
+      all_goals aesop (rule_sets := [-default])
   case dia α φ notAtom =>
     simp_all only [applyLocalRule, Finset.sdiff_empty, List.pdlToFinFin, Finset.mem_image,
       List.mem_toFinset, List.mem_map, exists_exists_and_eq_and, Finset.union_empty,
@@ -1430,7 +1448,7 @@ private theorem formulaExpansion_oneSidedR
       simp [hx]
     · left
       rcases hf with hf | hf | hf | hf
-      all_goals aesop
+      all_goals aesop (rule_sets := [-default])
   all_goals simp_all [applyLocalRule]
 
 /-- Preservation and expansion for a local rule acting on the L component. -/
@@ -1478,7 +1496,7 @@ private theorem formulaExpansion_loadedL
       · simp only [Finset.mem_union, List.mem_toFinset]
         tauto
       · rcases w with _ | nlf <;> simp_all [Olf.L]
-    · left; aesop
+    · left; aesop (rule_sets := [-default])
   case dia' α φ notAtom =>
     simp_all only [applyLocalRule, Finset.sdiff_empty, List.pdlToFinFinOpt, Finset.mem_image,
       List.mem_toFinset, List.mem_map, Prod.exists, Prod.mk.injEq, exists_eq_right_right,
@@ -1506,7 +1524,7 @@ private theorem formulaExpansion_loadedL
       · simp only [Finset.mem_union, List.mem_toFinset]
         tauto
       · rcases w with _ | nlf <;> simp_all [Olf.L]
-    · left; aesop
+    · left; aesop (rule_sets := [-default])
 
 /-- Preservation and expansion for a local rule acting on the R component. -/
 private theorem formulaExpansion_loadedR
@@ -1553,7 +1571,7 @@ private theorem formulaExpansion_loadedR
       · simp only [Finset.mem_union, List.mem_toFinset]
         tauto
       · rcases w with _ | nlf <;> simp_all [Olf.R]
-    · left; aesop
+    · left; aesop (rule_sets := [-default])
   case dia' α φ notAtom =>
     simp_all only [applyLocalRule, Finset.sdiff_empty, List.pdlToFinFinOpt, Finset.mem_image,
       List.mem_toFinset, List.mem_map, Prod.exists, Prod.mk.injEq, exists_eq_right_right,
@@ -1581,7 +1599,7 @@ private theorem formulaExpansion_loadedR
       · simp only [Finset.mem_union, List.mem_toFinset]
         tauto
       · rcases w with _ | nlf <;> simp_all [Olf.R]
-    · left; aesop
+    · left; aesop (rule_sets := [-default])
 
 /-- Every formula at the source of a local rule is retained by the chosen child or has
 its principal-formula expansion in that child. -/
@@ -1631,11 +1649,11 @@ lemma Sequent.basic_then_saturated {X : Sequent} : X.basic → saturated X.toFin
   intro Fs φ ψ α
   refine ⟨?_, ?_, ?_, ?box, ?dia⟩
   · simp_all [basic, Fs, toFinset]
-    grind
+    grind only []
   · simp_all [basic, Fs, toFinset]
-    grind
+    grind only []
   · simp_all [basic, Fs, toFinset]
-    grind
+    grind only []
   case box =>
     intro _in_F
     simp_all only [basic, toFinset, Finset.union_assoc, Finset.mem_union, Option.mem_toFinset,
@@ -1653,7 +1671,7 @@ lemma Sequent.basic_then_saturated {X : Sequent} : X.basic → saturated X.toFin
       exact _in_F
     all_goals
       simp [TP, testsOfProgram,Bset,P,F]
-      grind
+      grind only []
   case dia =>
     intro _in_F
     cases α
@@ -1667,7 +1685,7 @@ lemma Sequent.basic_then_saturated {X : Sequent} : X.basic → saturated X.toFin
     all_goals
       simp_all [basic, Fs, toFinset]
       simp [Dset, Yset]
-      grind
+      grind only []
 
 /-- A set of formulas is *lcoally consistent* iff it does not contain `⊥`
 and for all atoms `p ∈ X` we do not have `~p ∈ X`. Part of Def 6.2 -/
@@ -1717,7 +1735,7 @@ lemma LocalRuleApp.preserve_saturated_up (lra : LocalRuleApp) :
       f ∈ (({lra.X} ∪ rest).image Sequent.toFinset).sup id →
       f ∈ lra.X.toFinset ∨ f ∈ (rest.image Sequent.toFinset).sup id := by simp
   have child_in_rest (f : Formula) (hf : f ∈ Y.toFinset) :
-      f ∈ (rest.image Sequent.toFinset).sup id := by simp; grind
+      f ∈ (rest.image Sequent.toFinset).sup id := by simp; grind only []
   have lift_rest (f : Formula) :
       f ∈ (rest.image Sequent.toFinset).sup id →
       f ∈ (({lra.X} ∪ rest).image Sequent.toFinset).sup id := by simp_all
@@ -1874,7 +1892,7 @@ lemma LocalRuleApp.wForms_negLoad_preserved_or_unfolded (lra : LocalRuleApp) {Y
     · simp only [List.all_eq_true, decide_eq_true_eq]
       intro f f_in
       rw [Sequent.mem_wForms_normal_iff]
-      aesop
+      aesop (rule_sets := [-default])
     · cases onew with
       | none => simp
       | some nl =>
@@ -1896,7 +1914,7 @@ lemma LocalRuleApp.wForms_negLoad_preserved_or_unfolded (lra : LocalRuleApp) {Y
     · simp only [List.all_eq_true, decide_eq_true_eq]
       intro f f_in
       rw [Sequent.mem_wForms_normal_iff]
-      aesop
+      aesop (rule_sets := [-default])
     · cases onew with
       | none => simp
       | some nl =>
@@ -1925,25 +1943,31 @@ lemma LocalRuleApp.preserve_basic_down (lra : LocalRuleApp) :
     ∀ Y ∈ lra.C, ∀ f, f.basic → f ∈ lra.X.toFinset → f ∈ Y.toFinset := by
   rcases lra with ⟨L, R, O, Lcond, Rcond, Ocond, ress, rule, C, hC, pre⟩
   subst hC
-  cases rule <;> simp_all only [applyLocalRule, Finset.sdiff_empty, Finset.mem_image,
+  dsimp only [LocalRuleApp.X]
+  cases rule
+  case' oneSidedL => clear pre
+  case' oneSidedR => clear pre
+  all_goals simp_all only [applyLocalRule, Finset.sdiff_empty, Finset.mem_image,
     exists_exists_and_eq_and, Finset.union_empty, Olf.change_old_none_none, Formula.basic,
     decide_false, decide_true, Sequent.toFinset, Finset.union_assoc, Finset.mem_union,
     Option.mem_toFinset, Option.mem_def, Option.map_eq_some_iff, Sum.exists, Sum.elim_inl,
     negUnload, Sum.elim_inr, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
     Finset.mem_sdiff, Finset.image_empty, Finset.notMem_empty, implies_true, forall_const,
     not_isEmpty_of_nonempty, IsEmpty.forall_iff, Prod.exists, ↓existsAndEq, and_true]
-  case oneSidedL ress orule ress_def => cases orule <;> simp_all <;> grind [Program.isAtomic]
-  case oneSidedR ress orule ress_def => cases orule <;> simp_all <;> grind [Program.isAtomic]
+  case oneSidedL ress orule ress_def =>
+    cases orule <;> simp_all <;> grind only [Program.isAtomic]
+  case oneSidedR ress orule ress_def =>
+    cases orule <;> simp_all <;> grind only [Program.isAtomic]
   case loadedL ress chi lrule ress_def =>
     cases lrule <;> simp_all only [Finset.empty_subset, Option.some_subseteq, true_and,
       List.pdlToFinFinOpt, List.mem_toFinset, List.mem_map, Prod.mk.injEq, Prod.exists,
       exists_eq_right_right, forall_exists_index, and_imp] <;> intros <;> subst_eqs <;> simp_all
-        <;> grind [Program.isAtomic]
+        <;> grind only [Program.isAtomic]
   case loadedR ress chi lrule ress_def =>
     cases lrule <;> simp_all only [Finset.empty_subset, Option.some_subseteq, true_and,
       List.pdlToFinFinOpt, List.mem_toFinset, List.mem_map, Prod.mk.injEq, Prod.exists,
       exists_eq_right_right, forall_exists_index, and_imp] <;> intros <;> subst_eqs <;> simp_all
-        <;> grind [Program.isAtomic]
+        <;> grind only [Program.isAtomic]
 
 /-- Local rules never *load* a formula: if the sequent we apply a local rule to is free,
 then so are all children. (The rules `loadedL` and `loadedR` are not applicable to a free
diff --git a/LeanPool/PDL/Local/Soundness.lean b/LeanPool/PDL/Local/Soundness.lean
index 5a545bba67..5031c2032a 100644
--- a/LeanPool/PDL/Local/Soundness.lean
+++ b/LeanPool/PDL/Local/Soundness.lean
@@ -229,7 +229,7 @@ private theorem localLoadedDiamondList_leftNested {W : Type} {M : KripkeModel W}
     have := precons.2.2
     simp only [Option.some_subseteq] at this
     rw [← this] at negLoad_in
-    cases side <;> aesop
+    cases side <;> aesop (rule_sets := [-default])
   subst α_same -- But cannot do `subst χ_def`.
   -- This F,δ pair is also used for one result in `B`:
   have in_C : (L ∪ F.toFinset, R, some (Sum.inl (~'⌊⌊δ⌋⌋χ'))) ∈ C := by
@@ -281,7 +281,7 @@ private theorem localLoadedDiamondList_leftNested {W : Type} {M : KripkeModel W}
             -- Here δ is [] and thus α can have distance 0
             rw [distance_list_nil_self] at same_dist
             exact same_dist.symm
-          aesop
+          aesop (rule_sets := [-default])
         · intro f f_in
           simp only [List.mem_union_iff] at f_in; cases f_in
           · apply v_F; assumption
@@ -455,7 +455,7 @@ private theorem localLoadedDiamondList_leftNormal {W : Type} {M : KripkeModel W}
             Olf.change, Option.pdlOverwrite, AnyNegFormula.inSide, splitLast,
             Option.map_none] at *
         · rw [negLoad_in]; simp
-        · subst hC; exfalso; aesop
+        · subst hC; exfalso; aesop (rule_sets := [-default])
     -- We do not know `Y` yet because ltab may continue after `(L ++ F ++ [~φ], R, none)`.
     -- So let's use localTableauTruth to find a free end node, similar to αs = [] case.
     have v_Z : (M, v) ⊨ (show Sequent from (L ∪ (F.toFinset ∪ {~φ}), R, none)) := by
@@ -594,7 +594,7 @@ private theorem localLoadedDiamondList_rightNested {W : Type} {M : KripkeModel W
     have := precons.2.2
     simp only [Option.some_subseteq] at this
     rw [← this] at negLoad_in
-    cases side <;> aesop
+    cases side <;> aesop (rule_sets := [-default])
   subst α_same -- But cannot do `subst χ_def`.
   -- This F,δ pair is also used for one result in `C`:
   have in_C : (L, R ∪ F.toFinset, some (Sum.inr (~'⌊⌊δ⌋⌋χ'))) ∈ C := by
@@ -648,7 +648,7 @@ private theorem localLoadedDiamondList_rightNested {W : Type} {M : KripkeModel W
             -- Here δ is [] and thus α can have distance 0
             rw [distance_list_nil_self] at same_dist
             exact same_dist.symm
-          aesop
+          aesop (rule_sets := [-default])
         · intro f f_in
           simp only [List.mem_union_iff] at f_in; cases f_in
           · apply v_F; assumption
@@ -820,7 +820,7 @@ private theorem localLoadedDiamondList_rightNormal {W : Type} {M : KripkeModel W
             reduceCtorEq, and_false, Option.some.injEq, true_and, AnyFormula.boxes_nil,
             Olf.change, Option.pdlOverwrite, AnyNegFormula.inSide, splitLast,
             Option.map_none] at *
-        · subst hC; exfalso; aesop
+        · subst hC; exfalso; aesop (rule_sets := [-default])
         · rw [negLoad_in]; simp
     -- No IH needed because we reach a free node.
     clear IH
@@ -968,7 +968,7 @@ theorem localLoadedDiamondList (αs : List Program) {X : Sequent}
         simp_all only [and_self, and_true]
         use (L \ Lcond ∪ res, R, O)
         simp_all only [exists_prop, and_true]
-        grind
+        grind only []
       case oneSidedR YS orule YS_def => -- analogous to oneSidedL
         simp_all only [applyLocalRule, Finset.sdiff_empty, Finset.mem_image,
           exists_exists_and_eq_and, Finset.union_empty, Olf.change_old_none_none,
@@ -988,7 +988,7 @@ theorem localLoadedDiamondList (αs : List Program) {X : Sequent}
         simp_all only [and_self, and_true]
         use (L, R \ Rcond ∪ res, O)
         simp_all only [exists_prop, and_true]
-        grind
+        grind only []
       case LRnegL φ =>
         simp_all
       case LRnegR =>
diff --git a/LeanPool/PDL/Local/Tableau.lean b/LeanPool/PDL/Local/Tableau.lean
index f0f02c77ce..e1cb6ff25e 100644
--- a/LeanPool/PDL/Local/Tableau.lean
+++ b/LeanPool/PDL/Local/Tableau.lean
@@ -103,11 +103,11 @@ decreasing_by
 
 theorem lmOfFormula_lt_box_of_nonAtom (h : ¬ α.isAtomic) :
     lmOfFormula φ < lmOfFormula (⌈α⌉φ) := by
-  cases α <;> simp_all [Program.isAtomic, testsOfProgram] <;> linarith
+  cases α <;> simp_all [Program.isAtomic, testsOfProgram] <;> omega
 
 theorem lmOfFormula_lt_dia_of_nonAtom (h : ¬ α.isAtomic) :
     lmOfFormula (~φ) < lmOfFormula (~⌈α⌉φ) := by
-  cases α <;> simp_all [Program.isAtomic, testsOfProgram] <;> linarith
+  cases α <;> simp_all [Program.isAtomic, testsOfProgram] <;> omega
 
 
 /-- The multiset of unloaded formulas represented by an optional loading. -/
@@ -164,12 +164,12 @@ theorem unfoldBox.decreases_lmOf_nonAtomic {α : Program} {φ : Formula} {X : Li
       simp [lmOfFormula]
   case union α β => -- based on sequence case
     rcases ubc with one | ⟨τ, τ_in, def_ψ⟩ | ⟨a, δ, def_ψ, _⟩
-    · subst_eqs; linarith
+    · subst_eqs; omega
     · subst def_ψ
       suffices lmOfFormula (~τ)
           < (List.map (fun x => lmOfFormula (~ (x.1))) (testsOfProgram (α⋓β)).attach).sum.succ by
         simp_all
-        linarith
+        omega
       rw [@List.attach_map_val _ _ (testsOfProgram (α⋓β)) (fun x => lmOfFormula (~↑x))]
       rw [Nat.lt_succ_iff]
       exact List.single_le_sum (by simp) _ (by rw [List.mem_map]; use τ)
@@ -177,12 +177,12 @@ theorem unfoldBox.decreases_lmOf_nonAtomic {α : Program} {φ : Formula} {X : Li
       simp [lmOfFormula]
   case star β => -- based on sequence case
     rcases ubc with one | ⟨τ, τ_in, def_ψ⟩ | ⟨a, δ, def_ψ, _⟩
-    · subst_eqs; linarith
+    · subst_eqs; omega
     · subst def_ψ
       suffices lmOfFormula (~τ)
           < (List.map (fun x => lmOfFormula (~ (x.1))) (testsOfProgram (∗β)).attach).sum.succ by
         simp_all
-        linarith
+        omega
       rw [@List.attach_map_val _ _ (testsOfProgram (∗β)) (fun x => lmOfFormula (~↑x))]
       rw [Nat.lt_succ_iff]
       exact List.single_le_sum (by simp) _ (by rw [List.mem_map]; use τ)
@@ -190,12 +190,12 @@ theorem unfoldBox.decreases_lmOf_nonAtomic {α : Program} {φ : Formula} {X : Li
       simp [lmOfFormula]
   case test τ0 => -- based on sequence case
     rcases ubc with one | ⟨τ, τ_in, def_ψ⟩ | ⟨a, δ, def_ψ, _⟩
-    · subst_eqs; linarith
+    · subst_eqs; omega
     · subst def_ψ
       suffices lmOfFormula (~τ)
           < (List.map (fun x => lmOfFormula (~ (x.1))) (testsOfProgram (?'τ0)).attach).sum.succ by
         simp_all
-        linarith
+        omega
       rw [@List.attach_map_val _ _ (testsOfProgram (?'τ0)) (fun x => lmOfFormula (~↑x))]
       rw [Nat.lt_succ_iff]
       exact List.single_le_sum (by simp) _ (by rw [List.mem_map]; use τ)
@@ -293,36 +293,36 @@ theorem unfoldDiamond.decreases_lmOf_nonAtomic {α : Program} {φ : Formula} {X
     case sequence α β =>
       suffices lmOfFormula ψ < (List.map lmOfFormula (testsOfProgram (α;'β))).sum.succ by
         simp_all [testsOfProgram]
-        linarith
+        omega
       suffices ∃ τ' ∈ testsOfProgram (α;'β), lmOfFormula ψ < 1 + lmOfFormula τ' by
         rw [Nat.lt_succ_iff]
         apply List.le_sum_of_mem
         simp_all [testsOfProgram]
-        aesop
+        aesop (rule_sets := [-default])
       simp_all [testsOfProgram]
-      aesop
+      aesop (rule_sets := [-default])
     case union α β =>
       suffices lmOfFormula ψ < (List.map lmOfFormula (testsOfProgram (α⋓β))).sum.succ by
         simp_all [testsOfProgram]
-        linarith
+        omega
       suffices ∃ τ' ∈ testsOfProgram (α;'β), lmOfFormula ψ < 1 + lmOfFormula τ' by
         rw [Nat.lt_succ_iff]
         apply List.le_sum_of_mem
         simp_all [testsOfProgram]
-        aesop
+        aesop (rule_sets := [-default])
       simp_all [testsOfProgram]
-      aesop
+      aesop (rule_sets := [-default])
     case star β =>
       suffices lmOfFormula ψ < (List.map lmOfFormula (testsOfProgram (∗β))).sum.succ by
         simp_all [testsOfProgram]
-        linarith
+        omega
       suffices ∃ τ' ∈ testsOfProgram (∗β), lmOfFormula ψ < 1 + lmOfFormula τ' by
         rw [Nat.lt_succ_iff]
         apply List.le_sum_of_mem
         simp_all [testsOfProgram]
-        aesop
+        aesop (rule_sets := [-default])
       simp_all [testsOfProgram]
-      aesop
+      aesop (rule_sets := [-default])
   · simp only [lmOfFormula, gt_iff_lt]
     cases α <;> simp_all [Program.isAtomic]
 
@@ -336,12 +336,12 @@ lemma finset_sum_trichotomy {A : Type*} [DecidableEq A]
   have h_sum_split : (∑ x ∈ X.toFinset, f x) ≤ (∑ x ∈ (X.toFinset.erase a), f x) + f a := by
     by_cases ha : a ∈ X.toFinset <;> simp_all +decide only [List.mem_toFinset, not_false_eq_true,
       Finset.erase_eq_of_notMem, le_add_iff_nonneg_right, zero_le]
-    rw [← Finset.sum_erase_add _ _ (by aesop : a ∈ X.toFinset), add_comm]
+    rw [← Finset.sum_erase_add _ _ (by aesop (rule_sets := [-default]) : a ∈ X.toFinset), add_comm]
   have h_sum_le : (∑ x ∈ X.toFinset.erase a, f x) ≤ (∑ x ∈ (bs.toFinset), f x) := by
     have h_sum_le' : (∑ x ∈ X.toFinset.erase a, f x) ≤
         (∑ x ∈ (X.toFinset.erase a ∩ bs.toFinset), f x) := by
       rw [← Finset.sum_subset (Finset.inter_subset_left)]
-      intro x hx hx'; specialize h x; aesop
+      intro x hx hx'; specialize h x; aesop (rule_sets := [-default])
     exact h_sum_le'.trans (Finset.sum_le_sum_of_subset_of_nonneg
       (Finset.inter_subset_right) (fun _ _ _ => Nat.zero_le _))
   apply le_trans h_sum_split
@@ -351,7 +351,7 @@ lemma finset_sum_trichotomy {A : Type*} [DecidableEq A]
     intro l; induction l <;> simp_all +decide only [List.toFinset_nil, Finset.sum_empty,
       List.map_nil, List.sum_nil, Std.le_refl, List.toFinset_cons, List.map_cons, List.sum_cons]
     by_cases hh : ‹A› ∈ ‹List A›.toFinset <;> simp_all +decide only [List.mem_toFinset,
-      Finset.insert_eq_of_mem, not_false_eq_true, Finset.sum_insert, add_le_add_iff_left]; linarith!
+      Finset.insert_eq_of_mem, not_false_eq_true, Finset.sum_insert, add_le_add_iff_left]; omega
   exact h_toFinset_le bs
 
 /-- This is a summary lemma and not used as a whole anywhere.
@@ -402,7 +402,7 @@ lemma measureProp {α : Program} {φ φ₁ φ₂ : Formula} :
     case test τ =>
       simp_all [testsOfProgram, unfoldDiamond, Dset, Yset]
       subst X_in
-      by_cases h : τ = ~φ <;> simp_all; grind
+      by_cases h : τ = ~φ <;> simp_all; grind only []
     all_goals
       have tri : ∀ ψ ∈ X, ψ = (~φ) ∨ ψ ∈ testsOfProgram α ∨ lmOfFormula ψ = 0 := by
         have udc := unfoldDiamondContent _ _ _ X_in
@@ -414,7 +414,7 @@ lemma measureProp {α : Program} {φ φ₁ φ₂ : Formula} :
       have := finset_sum_trichotomy lmOfFormula X (~φ) (testsOfProgram α) tri
       subst α_def
       simp only [lmOfFormula, List.map_subtype, List.unattach_attach, gt_iff_lt] at *
-      linarith
+      omega
 
 /-- The end sequents of a local tableau. -/
 @[simp]
@@ -699,7 +699,7 @@ theorem endNodeIsEndNodeOfChild {X} {lrA : LocalRuleApp}
   ∃ Y h, E ∈ endNodesOf (subTabs Y h) := by
   have := endNodeToEndNodeOfChild def_X subTabs E_in
   use this
-  aesop
+  aesop (rule_sets := [-default])
 
 theorem endNodeOfChild_to_endNode
     {Y : Sequent}
@@ -717,13 +717,13 @@ theorem endNodeOfChild_to_endNode
     subst h
     simp only [endNodesOf, Finset.sup_image, Function.id_comp, Finset.mem_sup, Finset.mem_attach,
       true_and, Subtype.exists]
-    grind
+    grind only []
   case byLocalRule C' subTabs' lrA' =>
     subst h
     rw [h'] at Z_in
     simp only [endNodesOf, Finset.sup_image, Function.id_comp, Finset.mem_sup, Finset.mem_attach,
       true_and, Subtype.exists]
-    grind
+    grind only []
 
 /-- Membership in the end nodes of a local tableau given by a local rule application. -/
 lemma mem_endNodesOf_byLocalRule_iff {X} {lra : LocalRuleApp} {X_def : X = lra.X}
@@ -738,11 +738,18 @@ lemma mem_endNodesOf_byLocalRule_iff {X} {lra : LocalRuleApp} {X_def : X = lra.X
 theorem localTableauTruth {X} (lt : LocalTableau X) {W} (M : KripkeModel W) (w : W) :
     (M, w) ⊨ X  ↔ ∃ Y ∈ endNodesOf lt, (M, w) ⊨ Y := by
   induction lt
-  case byLocalRule Y lrA X_def next IH  =>
-    have := localRuleTruth lrA M w
-    aesop
+  case byLocalRule Y lrA X_def next IH =>
+    subst Y
+    rw [localRuleTruth lrA M w]
+    constructor
+    · rintro ⟨child, hchild, hsat⟩
+      obtain ⟨leaf, hleaf, hsat⟩ := (IH child hchild).mp hsat
+      exact ⟨leaf, mem_endNodesOf_byLocalRule_iff.mpr ⟨child, hchild, hleaf⟩, hsat⟩
+    · rintro ⟨leaf, hleaf, hsat⟩
+      obtain ⟨child, hchild, hleaf⟩ := mem_endNodesOf_byLocalRule_iff.mp hleaf
+      exact ⟨child, hchild, (IH child hchild).mpr ⟨leaf, hleaf, hsat⟩⟩
   case sim =>
-    simp_all
+    simp only [endNodesOf, Finset.mem_singleton, exists_eq_left]
 
 open HasSat
 
@@ -769,7 +776,7 @@ lemma endNodesOf_basic {X Z} {ltZ : LocalTableau Z} : X ∈ endNodesOf ltZ → X
   case byLocalRule B lrA next IH =>
     intro X_in
     simp [endNodesOf] at X_in
-    aesop
+    aesop (rule_sets := [-default])
   case sim X =>
     simp_all
 
@@ -779,7 +786,7 @@ theorem endNodesOf_nonbasic_non_eq {X Y} (lt : LocalTableau X) (X_nonbas : ¬ X.
     Y ∈ endNodesOf lt → Y ≠ X := by
   intro Y_in
   have := endNodesOf_basic Y_in
-  grind
+  grind only []
 
 -- upstream me / Haitian?;-)
 lemma IsDershowitzMannaLT.irrefl [Preorder α] [WellFoundedLT α] (X : Multiset α) :
diff --git a/LeanPool/PDL/Local/UnfoldBox.lean b/LeanPool/PDL/Local/UnfoldBox.lean
index 80e4a7418d..a04a8737e5 100644
--- a/LeanPool/PDL/Local/UnfoldBox.lean
+++ b/LeanPool/PDL/Local/UnfoldBox.lean
@@ -76,10 +76,10 @@ theorem signature_iff {W} {M : KripkeModel W} {w : W} :
   · intro w_ℓ τ τ_in
     cases em (ℓ ⟨τ, τ_in⟩)
     · specialize w_ℓ τ τ τ_in
-      aesop
+      aesop (rule_sets := [-default])
     · specialize w_ℓ (~τ) τ τ_in
-      aesop
-  · aesop
+      aesop (rule_sets := [-default])
+  · aesop (rule_sets := [-default])
 
 -- Now come two out of the three facts about test profiles and signatures.
 
@@ -97,7 +97,7 @@ theorem top_equiv_disj_TP : ∀ α, tautology (dis ((allTP α).map (signature α
     forall_exists_index]
     intro f τ τ_in def_f
     subst def_f
-    aesop
+    aesop (rule_sets := [-default])
 
 /-- This is currently unused. -/
 theorem signature_contradiction_of_neq_TPs {ℓ ℓ' : TP α} :
@@ -151,16 +151,16 @@ lemma F_sub_testsOfProgram_map_neg (α : Program) (ℓ : TP α) :
   case sequence α β =>
     have IHα := F_sub_testsOfProgram_map_neg α
     have IHβ := F_sub_testsOfProgram_map_neg β
-    grind
+    grind only [= List.subset_def, = List.mem_union_iff, = List.mem_append]
   case union α β =>
     have IHα := F_sub_testsOfProgram_map_neg α
     have IHβ := F_sub_testsOfProgram_map_neg β
-    grind
+    grind only [= List.subset_def, = List.mem_union_iff, = List.mem_append]
   case star α =>
     have IHα := F_sub_testsOfProgram_map_neg α
-    grind
+    grind only []
   case test =>
-    split <;> grind
+    split <;> grind only [= List.subset_def, = List.mem_cons]
 
 /-- The residual program sequences produced by box unfolding under a test profile. -/
 def P : (α : Program) →  (ℓ : TP α) → List (List Program)
@@ -401,8 +401,9 @@ theorem boxHelperTermination α (ℓ : TP α) :
         use a
         subst δ'_def
         simp at *
-        grind
-      · rcases IH.2 with ⟨a, ⟨δ1n, δ'_def⟩, ⟨_, δ'_sub⟩⟩ <;> simp_all [subprograms] <;> grind
+        grind only [= List.subset_def, =_ List.cons_append, = List.mem_append, = List.mem_cons]
+      · rcases IH.2 with ⟨a, ⟨δ1n, δ'_def⟩, ⟨_, δ'_sub⟩⟩ <;> simp_all [subprograms] <;>
+        grind only [→ List.mem_of_mem_erase, = List.subset_def, = List.mem_append]
     · by_cases [] ∈ P α ℓ
       · simp_all only [true_and, subprograms, List.cons_append, List.nil_append, List.mem_cons,
         reduceCtorEq, List.mem_append, false_or, List.erase_cons_head]
@@ -427,16 +428,18 @@ theorem boxHelperTermination α (ℓ : TP α) :
           cases IH
           subst_eqs
           simp_all [subprograms]
-          aesop
+          aesop (rule_sets := [-default])
         · rw [Program.isStar_iff] at *
           rename _ => hyp
           rcases hyp with ⟨γ, α_def⟩
           specialize IH γ
           simp_all
-          rcases IH with ⟨a, δ1n, δ'_def⟩ <;> simp_all [subprograms]; grind
+          rcases IH with ⟨a, δ1n, δ'_def⟩ <;> simp_all [subprograms];
+            grind only [= List.subset_def, = List.mem_append, = List.mem_cons,
+              ← List.not_mem_nil]
         · cases IH
           simp_all [subprograms]
-          grind
+          grind only [→ List.mem_of_mem_erase, = List.subset_def, = List.mem_append]
       · simp_all
   case union α β =>
     cases δ_in
@@ -455,7 +458,8 @@ theorem boxHelperTermination α (ℓ : TP α) :
         simp_all
         have IH := boxHelperTermination (∗γ) ℓ δ δ_in
         simp [subprograms] at *
-        grind
+        grind only [=_ List.cons_append, = List.subset_def, = List.mem_cons, = List.mem_append,
+          ← List.not_mem_nil]
       case neg hyp1 hyp2 =>
         rcases hyp1 with ⟨a, α_def⟩
         subst α_def
@@ -463,7 +467,8 @@ theorem boxHelperTermination α (ℓ : TP α) :
         simp_all [Program.isAtomic_iff, Program.isStar_iff, subprograms]
       · have IH := boxHelperTermination (α) ℓ δ δ_in
         simp_all [Program.isAtomic_iff, Program.isStar_iff]
-        grind
+        grind only [= List.mem_erase_of_ne, = List.subset_def, = List.mem_append,
+          → List.mem_of_mem_erase]
     case inr δ_in =>
       by_cases β.isAtomic <;> by_cases β.isStar <;>
         simp_all only [Program.isAtomic_iff, Program.isStar_iff, subprograms, List.cons_append,
@@ -479,7 +484,7 @@ theorem boxHelperTermination α (ℓ : TP α) :
         simp_all
         have IH := boxHelperTermination (∗γ) ℓ δ δ_in
         simp [subprograms] at *
-        grind
+        grind only [= List.subset_def, = List.mem_append, = List.mem_cons, ← List.not_mem_nil]
       case neg hyp1 hyp2 =>
         rcases hyp1 with ⟨a, β_def⟩
         subst β_def
@@ -487,7 +492,8 @@ theorem boxHelperTermination α (ℓ : TP α) :
         simp_all [Program.isAtomic_iff, Program.isStar_iff, subprograms]
       · have IH := boxHelperTermination (β) ℓ δ δ_in
         simp_all [Program.isAtomic_iff, Program.isStar_iff]
-        grind
+        grind only [= List.mem_erase_of_ne, = List.subset_def, = List.mem_append,
+          → List.mem_of_mem_erase]
   case star β =>
     rcases δ_in with _|hyp
     · left; assumption
@@ -525,7 +531,7 @@ theorem boxHelperTermination α (ℓ : TP α) :
       · rcases IH with ⟨a, δ1n, δ'_def, a_in, δ'_sub⟩
         use a
         simp_all [subprograms]
-        grind
+        grind only [= List.mem_erase_of_ne, = List.subset_def, → List.mem_of_mem_erase]
 
 /-- Proven from `boxHelperTermination`. -/
 theorem PgoesDown : γ ∈ δ → δ ∈ P α ℓ →
@@ -536,7 +542,7 @@ theorem PgoesDown : γ ∈ δ → δ ∈ P α ℓ →
   intro γ_in δ_in
   have bht := boxHelperTermination α ℓ δ δ_in; clear δ_in
   by_cases α.isAtomic
-  case pos α_atom => grind
+  case pos α_atom => grind only [= List.mem_cons, ← List.not_mem_nil]
   case neg α_not_atom =>
     by_cases α.isStar
     case pos α_star =>
@@ -546,7 +552,7 @@ theorem PgoesDown : γ ∈ δ → δ ∈ P α ℓ →
         and_self, IsEmpty.forall_iff, ne_eq, List.mem_erase_of_ne, true_and, Program.star.injEq,
         forall_eq', and_false, ↓reduceIte, lengthOfProgram]
       rcases bht with _|⟨a, δ1n, δ_def, a_in, δ1n_sub⟩
-      · exfalso; grind
+      · exfalso; grind only [← List.not_mem_nil]
       · subst δ_def
         simp_all only [subprograms, List.cons_append, List.nil_append, List.mem_cons,
           reduceCtorEq, false_or, List.erase_cons_head, List.mem_append, List.not_mem_nil,
@@ -561,7 +567,7 @@ theorem PgoesDown : γ ∈ δ → δ ∈ P α ℓ →
       rcases bht with ⟨h1,h2,bht⟩; clear h1 h2
       specialize bht ⟨α_not_atom, α_not_star⟩
       have := @length_lt_of_mem_subprograms_erase α
-      grind
+      grind only [← List.not_mem_nil, = List.subset_def]
 
 /-- Where formulas in the unfolding can come from.
 The article also says `φ ∈ fischerLadner [⌈α⌉ψ]` which we prove later in `unfoldBox_in_FL`. -/
@@ -642,7 +648,7 @@ theorem unfoldBoxContent α ψ :
           right
           use δ1n
           simp
-          grind
+          grind only [= List.subset_def, = List.mem_append]
       case star β =>
         rcases bht with _ | ⟨a, δ1n, δ_def, a_in, δ_sub⟩
         · subst_eqs; simp
@@ -651,7 +657,7 @@ theorem unfoldBoxContent α ψ :
             Formula.box.injEq, Program.atom_prog.injEq, ↓existsAndEq, true_and]
           right
           use δ1n ++ [∗β]
-          grind
+          grind only [= List.subset_def, = List.mem_append, = List.mem_cons, ← List.not_mem_nil]
 
 theorem unfoldBox_voc {x α φ} {L} (L_in : L ∈ unfoldBox α φ) {ψ} (ψ_in : ψ ∈ L)
     (x_in_voc_ψ : x ∈ ψ.voc) : x ∈ α.voc ∨ x ∈ φ.voc := by
@@ -693,7 +699,7 @@ theorem boxHelperTP α (ℓ : TP α) :
   refine ⟨?_, ?_, ?_⟩
   · intro τ τ_in
     have := F_mem_iff_neg α ℓ (~τ)
-    aesop
+    aesop (rule_sets := [-default])
   · intro W M w
     simp only [evaluate, conEval, signature, List.mem_map, List.mem_attach, true_and,
       Subtype.exists, forall_exists_index, and_iff_right_iff_imp]
@@ -703,22 +709,22 @@ theorem boxHelperTP α (ℓ : TP α) :
     clear this
     rcases φ_in with ⟨τ, τ_in, φ_def, not_ℓ_τ⟩
     specialize w_ℓ φ τ
-    aesop
+    aesop (rule_sets := [-default])
   · intro ψ W M w
     simp only [evaluate, Bset, conEval, List.mem_append, List.mem_map, forall_exists_index,
       and_imp, forall_apply_eq_imp_iff₂, and_congr_left_iff]
     intro w_sign
     constructor
     · intro lhs δ δ_in
-      aesop
+      aesop (rule_sets := [-default])
     · rintro rhs φ (φ_in_F | ⟨δ,δ_in,def_φ⟩)
       · rw [F_mem_iff_neg α ℓ φ] at φ_in_F
         rcases φ_in_F with ⟨τ, τ_in, φ_def, not_ℓ_τ⟩
         subst φ_def
         simp_all [signature, conEval]
         specialize w_sign (~τ) τ
-        aesop
-      · aesop
+        aesop (rule_sets := [-default])
+      · aesop (rule_sets := [-default])
 
 theorem guardToStar (x : Nat) β χ0 χ1 ρ ψ
     (x_notin_beta : Sum.inl x ∉ β.voc)
@@ -843,7 +849,7 @@ theorem localBoxTruth_connector γ ψ :
       constructor
       · assumption
       · simp_all [signature, conEval]
-        aesop
+        aesop (rule_sets := [-default])
     simp_all
 
 /-- A box-star expansion implies every compatible test-profile expansion. -/
@@ -951,14 +957,14 @@ private theorem boxStar_forward (β : Program) (ψ : Formula)
       rintro f (f_in_F| ⟨δ, δ_in, def_f⟩)
       · simp only [F_mem_iff_neg, exists_and_left] at f_in_F
         unfold ℓ' at f_in_F
-        aesop
+        aesop (rule_sets := [-default])
       · subst def_f
         specialize step ℓ' W M w
         simp only [List.mem_singleton, forall_eq] at step
         rw [conEval] at step
         simp only [evaluate, relate, signature, conEval, List.mem_map, List.mem_attach, true_and,
           Subtype.exists, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at step
-        apply step <;> aesop
+        apply step <;> aesop (rule_sets := [-default])
   intro ℓ W M w
   simp only [List.mem_singleton, forall_eq]
   intro hyp
@@ -1064,7 +1070,7 @@ private theorem boxStar_backward (β : Program) (ψ : Formula)
           intro f δ δ_in _ def_f
           apply w_Xβ
           right
-          aesop
+          aesop (rule_sets := [-default])
       · right -- choose χ1
         unfold χ1 T1 φ'
         simp only [ne_eq, decide_not, disEval, List.mem_map, List.mem_filter,
@@ -1075,7 +1081,7 @@ private theorem boxStar_backward (β : Program) (ψ : Formula)
         intro f δ δ_in _ def_f
         apply w_Xβ
         right
-        aesop
+        aesop (rule_sets := [-default])
     · rintro (⟨w_c, w_χ0⟩ | w_χ1)
       · unfold χ0 T0 φ' at w_χ0
         simp only [ne_eq, decide_not, disEval, List.mem_map, List.mem_filter, decide_eq_true_eq,
@@ -1085,7 +1091,7 @@ private theorem boxStar_backward (β : Program) (ψ : Formula)
         use ℓ
         simp_all only [true_and]
         rintro φ (φ_in_Fβ | ⟨δ, δ_in, def_φ⟩)
-        · aesop
+        · aesop (rule_sets := [-default])
         · subst def_φ
           cases em (δ = [])
           · simp_all
@@ -1153,7 +1159,7 @@ private theorem boxStar_backward (β : Program) (ψ : Formula)
           specialize left_to_right W M
           simp [evalBoxes] at left_to_right w_Xℓ
           simp [evalBoxes]
-          aesop
+          aesop (rule_sets := [-default])
     case inr empty_not_in_Pβ =>
       right
       -- exactly the same as inl case!
@@ -1189,7 +1195,7 @@ private theorem boxStar_backward (β : Program) (ψ : Formula)
           specialize left_to_right W M
           simp [evalBoxes] at left_to_right w_Xℓ
           simp [evalBoxes]
-          aesop
+          aesop (rule_sets := [-default])
   · -- ρ ⊨ ψ
     unfold ρ
     simp only [Bset, P, List.cons_union, List.nil_union, List.mem_map, List.mem_filter,
@@ -1215,13 +1221,17 @@ private theorem boxUnion_profile (α β : Program) (ψ : Formula) (ℓ : TP (α
   simp only [evaluate, and_congr_left_iff, relate] at *
   intro w_sign_ℓ
   specialize IHα ?_
-  · simp_all [signature, conEval, testsOfProgram]
+  · clear IHα IHβ
+    simp_all [signature, conEval, testsOfProgram]
   specialize IHβ ?_
-  · simp_all [signature, conEval, testsOfProgram]
+  · clear IHα IHβ
+    simp_all [signature, conEval, testsOfProgram]
   -- rewrite using semantics of union and the two IH:
   have : (∀ (v : W), relate M α w v ∨ relate M β w v → evaluate M v ψ)
       ↔ ((∀ (v : W), relate M α w v → evaluate M v ψ)
-       ∧ (∀ (v : W), relate M β w v → evaluate M v ψ)) := by aesop
+       ∧ (∀ (v : W), relate M β w v → evaluate M v ψ)) := by
+    clear IHα IHβ w_sign_ℓ
+    aesop (rule_sets := [-default])
   rw [this, IHα, IHβ]
   clear this IHα IHβ
   -- signature is true, so we can add it for free:
@@ -1303,14 +1313,16 @@ private theorem boxSequence_profile (α β : Program) (ψ : Formula) (ℓ : TP (
   simp only [evaluate, relate, forall_exists_index, and_imp, and_congr_left_iff] at *
   intro w_sign_ℓ
   specialize IHα ?_
-  · simp_all [signature, conEval, testsOfProgram]
+  · clear IHα IHβ
+    simp_all [signature, conEval, testsOfProgram]
   specialize IHβ ?_
-  · simp_all [signature, conEval, testsOfProgram]
+  · clear IHα IHβ
+    simp_all [signature, conEval, testsOfProgram]
   -- only rewriting with IHα here, but not yet IHβ
   have : (∀ (v x : W), relate M α w x → relate M β x v → evaluate M v ψ)
         ↔ ∀ (v : W), relate M α w v → ∀ (v_1 : W), relate M β v v_1 → evaluate M v_1 ψ := by
-    clear IHα IHβ
-    aesop
+    clear IHα IHβ w_sign_ℓ
+    aesop (rule_sets := [-default])
   rw [this, IHα]
   clear this IHα
   constructor
@@ -1336,12 +1348,13 @@ private theorem boxSequence_profile (α β : Program) (ψ : Formula) (ℓ : TP (
       rcases δ_from_Pα with ⟨δ_α, bla, def_δ⟩
       use δ_α
       subst def_δ
+      clear IHβ w_sign_ℓ
       simp_all [boxes_append]
     · subst def_φ
       cases em ([] ∈ P α ℓ)
       · simp_all only [true_and]
         apply IHβ.1 ?_ (⌈⌈δ⌉⌉ψ) <;> clear IHβ
-        · right; aesop
+        · right; aesop (rule_sets := [-default])
         · have := lhs (⌈β⌉ψ)
           simp only [evaluate] at this; apply this; clear this -- sounds like daft punk ;-)
           right
diff --git a/LeanPool/PDL/Local/UnfoldDia.lean b/LeanPool/PDL/Local/UnfoldDia.lean
index c82be42425..b4b8fd07ed 100644
--- a/LeanPool/PDL/Local/UnfoldDia.lean
+++ b/LeanPool/PDL/Local/UnfoldDia.lean
@@ -335,7 +335,7 @@ theorem unfoldDiamondContent α ψ :
     use τ
   · -- φ is made from some δ from Dset α
     have := Dset_mem_sequence α in_D
-    aesop
+    aesop (rule_sets := [-default])
 
 theorem unfoldDiamond_voc {x α φ} {L} (L_in : L ∈ unfoldDiamond α φ) {ψ} (ψ_in : ψ ∈ L)
     (x_in_voc_ψ : x ∈ ψ.voc) : x ∈ α.voc ∨ x ∈ φ.voc := by
@@ -401,7 +401,7 @@ theorem guardToStarDiamond (x : Nat)
     simp only [vDash.SemImplies, Formula.or, evaluatePoint, evaluate] at u_2
     rw [← @or_iff_not_and_not] at u_2
     specialize repl_imp_rho W M u
-    aesop
+    aesop (rule_sets := [-default])
   -- It remains to show the goal using claim.
   intro w hyp
   simp only [Formula.or, List.mem_singleton, forall_eq, evaluate, relate, not_forall,
@@ -419,7 +419,7 @@ theorem guardToStarDiamond (x : Nat)
 
 private theorem helper : ∀ (p : List Formula × List Program → Formula) X,
         (∃ f ∈ List.map p X, evaluate M w f)
-      ↔ (∃ Fδ ∈ X, evaluate M w (p Fδ)) := by aesop
+      ↔ (∃ Fδ ∈ X, evaluate M w (p Fδ)) := by aesop (rule_sets := [-default])
 
 /-- A model of the unfolded diamond-star formula reaches a counterexample to the box. -/
 private theorem localDiamondTruth_star_reverse (β : Program) (ψ : Formula)
@@ -447,7 +447,7 @@ private theorem localDiamondTruth_star_reverse (β : Program) (ψ : Formula)
       or_false, evaluate, forall_eq, relate, not_forall]
     use w
   case inr hyp =>
-    have : ∃ γ, δ = γ ++ [∗β] ∧ γ ≠ [] ∧ (Fs,γ) ∈ Dset β := by aesop
+    have : ∃ γ, δ = γ ++ [∗β] ∧ γ ≠ [] ∧ (Fs,γ) ∈ Dset β := by aesop (rule_sets := [-default])
     rcases this with ⟨γ, ⟨δ_def, _, Fγ_in⟩⟩
     subst δ_def
     simp only [Yset, List.mem_union_iff, List.mem_singleton] at w_Con
diff --git a/LeanPool/PDL/Semantics.lean b/LeanPool/PDL/Semantics.lean
index d99ae9840f..6aba72563e 100644
--- a/LeanPool/PDL/Semantics.lean
+++ b/LeanPool/PDL/Semantics.lean
@@ -136,7 +136,7 @@ theorem notsatisfnotThenTaut : ∀ φ, ¬ satisfiable (~φ) → tautology φ :=
 
 theorem subsetSat {M : KripkeModel W} {w : W} {X Y : List Formula} :
     (∀ φ ∈ X, evaluate M w φ) → Y ⊆ X → ∀ φ ∈ Y, evaluate M w φ :=
-  by aesop
+  by aesop (rule_sets := [-default])
 
 theorem semEquiv.refl : Std.Refl semEquiv := by
   constructor
@@ -234,17 +234,17 @@ theorem forms_to_lists {φ ψ : Formula} : φ⊨ψ → ([φ] : List Formula)⊨(
   apply impTaut
   · rw [←vDashSingleton_iff_vDash_formula φ] at lhs
     tauto
-  · aesop
+  · aesop (rule_sets := [-default])
 
 /-- The Local Deduction Theorem. -/
 theorem deduction (X : List Formula) (ψ φ : Formula) :
     X ++ [ψ] ⊨ φ ↔ (X ⊨ ψ ↣ φ) := by
   constructor
   · intro Xφ_then_ψ W M w w_X
-    aesop
+    aesop (rule_sets := [-default])
   · intro X_ W M w w_X
     specialize X_ W M w
-    aesop
+    aesop (rule_sets := [-default])
 
 theorem notSat_iff_semImplies (X : List Formula) (φ : Formula) :
     ¬ satisfiable (X ∪ [~φ]) ↔ X ⊨ ([φ] : List Formula) := by
@@ -253,7 +253,7 @@ theorem notSat_iff_semImplies (X : List Formula) (φ : Formula) :
     intro nSat W M w satX
     specialize nSat W M w
     rcases nSat with ⟨φ, phi_in, not_phi⟩
-    aesop
+    aesop (rule_sets := [-default])
   · intro X_φ
     by_contra hyp
     simp only [satisfiable] at hyp
@@ -363,7 +363,7 @@ theorem relateSeq_append {M : KripkeModel W} {l1 l2 : List Program} {w v : W} :
   · simp [relateSeq]
   case cons l l1 IH =>
     simp [relateSeq]
-    aesop
+    aesop (rule_sets := [-default])
 
 lemma relate_steps_iff_relateSeq (M : KripkeModel W) (δ : List Program) (w v : W) :
     relate M (Program.steps δ) w v ↔ relateSeq M δ w v := by
@@ -379,11 +379,11 @@ theorem relateSeq_iff_exists_Vector (M : KripkeModel W) (δ : List Program) (w v
     List.get_eq_getElem, IsEmpty.forall_iff, and_true]
     constructor <;> intro h
     · use ⟨[w], by simp⟩
-      aesop
+      aesop (rule_sets := [-default])
     · rcases h with ⟨⟨ws, ws_len_eq_1⟩ , w_def, v_def⟩
       rw [List.length_eq_one_iff] at ws_len_eq_1
       rcases ws_len_eq_1 with ⟨x, ws_def⟩
-      aesop
+      aesop (rule_sets := [-default])
   case cons d δ IH =>
     simp only [relateSeq_cons, List.length_cons, Nat.succ_eq_add_one, List.get_eq_getElem]
     constructor <;> intro h
@@ -404,8 +404,8 @@ theorem relateSeq_iff_exists_Vector (M : KripkeModel W) (δ : List Program) (w v
             simp [List.Vector.get]
           · rcases ws with ⟨ws, ws_len⟩
             have := List.exists_of_length_succ _ ws_len
-            aesop
-        · aesop
+            aesop (rule_sets := [-default])
+        · aesop (rule_sets := [-default])
     · rcases h with ⟨wws, w_def, v_def, claim⟩
       let u := wws[1]
       use wws[1]
@@ -427,7 +427,7 @@ theorem relateSeq_iff_exists_Vector (M : KripkeModel W) (δ : List Program) (w v
             (by simp at wws_len; assumption : t.length = δ.length + 1)
           rcases this with ⟨y, tt, t_def⟩
           subst t_def
-          aesop
+          aesop (rule_sets := [-default])
         · rw [v_def]
           -- copied from previous case
           rcases wws with ⟨wws, wws_len⟩
@@ -437,10 +437,10 @@ theorem relateSeq_iff_exists_Vector (M : KripkeModel W) (δ : List Program) (w v
             (by simp at wws_len; assumption : t.length = δ.length + 1)
           rcases this with ⟨y, tt, t_def⟩
           subst t_def
-          aesop
+          aesop (rule_sets := [-default])
         · intro i
           specialize claim i.succ
-          aesop
+          aesop (rule_sets := [-default])
 
 /-- Relating along `Program.unions L` means relating along one of the programs in `L`. -/
 lemma relate_unions {W} {M : KripkeModel W} : ∀ (L : List Program) (v u : W),
diff --git a/LeanPool/PDL/Sequent.lean b/LeanPool/PDL/Sequent.lean
index 0bd237934c..5af23f9bec 100644
--- a/LeanPool/PDL/Sequent.lean
+++ b/LeanPool/PDL/Sequent.lean
@@ -71,19 +71,19 @@ instance Option.insHasSdiff [DecidableEq α] : SDiff (Option α) := SDiff.mk
 lemma Option.insHasSdiff_none [DecidableEq α] :
     (none : Option α) \ o = none := by
   unfold Option.insHasSdiff
-  grind
+  grind only []
 
 @[simp]
 lemma Option.insHasSdiff_remove_none_cancel [DecidableEq α] :
     o \ (none : Option α) = o := by
   unfold Option.insHasSdiff
-  grind
+  grind only []
 
 @[simp]
 lemma Option.insHasSdiff_remove_sem_eq_none [DecidableEq α] :
     (some x) \ (some x : Option α) = none := by
   unfold Option.insHasSdiff
-  grind
+  grind only []
 
 /-- The unloaded left formula contributed by an optional loading. -/
 def Olf.L : Olf → Finset Formula
@@ -428,8 +428,8 @@ lemma Sequent.satisfiable_top_cons_right {X : Sequent} (h_left_nil : X.left = {}
   simp only [toFinset, Finset.empty_union, Finset.mem_union, Option.mem_toFinset, Option.mem_def,
     Option.map_eq_some_iff, Sum.exists, Sum.elim_inl, negUnload, Sum.elim_inr] at φ_in
   rcases φ_in with _|_|⟨⟨χ⟩, ⟨O_def, def_φ⟩⟩
-  · aesop
-  · aesop
+  · aesop (rule_sets := [-default])
+  · aesop (rule_sets := [-default])
   · subst O_def def_φ
     unfold right at w_
     simp only [Top.top, R_eq, O_eq, Olf.R_inr] at w_
@@ -447,7 +447,7 @@ theorem Sequent.without_normal_isFree_iff_isFree (LRO : Sequent) :
     (LRO.without (~''(.normal φ))).isFree ↔ LRO.isFree := by
   rcases LRO with ⟨L, R, O⟩
   simp [Sequent.without, isFree, isLoaded]
-  aesop
+  aesop (rule_sets := [-default])
 
 @[simp]
 theorem Sequent.isFree_then_without_isFree (LRO : Sequent) :
@@ -544,7 +544,7 @@ theorem Sequent.without_loaded_in_side_isFree (LRO : Sequent) ξ side :
   rcases LRO with ⟨L, R, _|(OL|OR)⟩ <;> cases side
   all_goals
     simp [Sequent.without, isFree, isLoaded, AnyNegFormula.inSide]
-    try aesop
+    try aesop (rule_sets := [-default])
 
 /-! ## Whatever formulas
 
diff --git a/LeanPool/PDL/Soundness.lean b/LeanPool/PDL/Soundness.lean
index 1ea12b0138..f52e5c6af5 100644
--- a/LeanPool/PDL/Soundness.lean
+++ b/LeanPool/PDL/Soundness.lean
@@ -43,7 +43,7 @@ theorem pdlRuleSat (r : PdlRule X Y) (satX : satisfiable X) : satisfiable Y := b
        Finset.mem_insert, Finset.mem_union, Finset.mem_erase, ne_eq] at φ_in
     rcases φ_in with φ_def | ⟨φ_neq, bla⟩ | bla <;>
     all_goals
-      apply w_; simp [Sequent.toFinset]; grind
+      apply w_; simp [Sequent.toFinset]; grind only []
   case loadR =>
     use W, M, w
     simp_all [vDash.SemImplies, Sequent.toFinset]
@@ -852,7 +852,7 @@ private theorem loadedDiamondPathsPDL_modL (α : Program) (X : Sequent) (tab : T
             rw [tabAt_t_def]
             simp_all [Sequent.toFinset]
             have := @Finset.mem_projection
-            grind
+            grind only []
           apply this
           simp only [relate]
           exact v_α_w
@@ -873,7 +873,7 @@ private theorem loadedDiamondPathsPDL_modL (α : Program) (X : Sequent) (tab : T
             rw [tabAt_t_def]
             simp_all [Sequent.toFinset]
             have := @Finset.mem_projection
-            grind
+            grind only []
           apply this
           simp only [relate]
           exact v_α_w
@@ -1002,7 +1002,7 @@ private theorem loadedDiamondPathsPDL_modR (α : Program) (X : Sequent) (tab : T
             rw [tabAt_t_def]
             simp_all [Sequent.toFinset]
             have := @Finset.mem_projection
-            grind
+            grind only []
           apply this
           simp only [relate]
           exact v_α_w
@@ -1023,7 +1023,7 @@ private theorem loadedDiamondPathsPDL_modR (α : Program) (X : Sequent) (tab : T
             rw [tabAt_t_def]
             simp_all [Sequent.toFinset]
             have := @Finset.mem_projection
-            grind
+            grind only []
           apply this
           exact v_α_w
     · -- (c)
@@ -1064,12 +1064,12 @@ lemma loadedDiamondPathsPDL
     exfalso
     simp only [nodeAt, AnyNegFormula.inSide] at negLoad_in
     rw [tabAt_t_def] at negLoad_in
-    aesop
+    aesop (rule_sets := [-default])
   case loadR =>
     exfalso
     simp only [nodeAt, AnyNegFormula.inSide] at negLoad_in
     rw [tabAt_t_def] at negLoad_in
-    aesop
+    aesop (rule_sets := [-default])
   case freeL L R δ β φ Z_def Y_def =>
     subst Z_def Y_def
     -- Leaving cluster, interesting that IH is not needed here.
@@ -1106,9 +1106,9 @@ lemma loadedDiamondPathsPDL
     · apply not_cEquiv_of_free_loaded
       -- use lemma that load and free are never in same cluster
       · simp only [Sequent.isFree, Sequent.isLoaded, nodeAt]
-        grind
+        grind only []
       · simp only [Sequent.isLoaded, nodeAt]
-        grind
+        grind only []
   case freeR L R δ β φ Z_def Y_def =>
     subst Z_def Y_def
     -- Leaving cluster, interesting that IH is not needed here.
@@ -1145,9 +1145,9 @@ lemma loadedDiamondPathsPDL
     · apply not_cEquiv_of_free_loaded
       -- use lemma that load and free are never in same cluster
       · simp only [Sequent.isFree, Sequent.isLoaded, nodeAt]
-        grind
+        grind only []
       · simp only [Sequent.isLoaded, nodeAt]
-        grind
+        grind only []
   case modL L R a ξ' Z_def Y_def =>
     exact loadedDiamondPathsPDL_modL α X tab t v_t ξ negLoad_in v_α_w w_nξ
       bas nflprep next Y_def Z_def tabAt_t_def
@@ -1575,7 +1575,7 @@ theorem tableauThenNotSat {Root} (tab : Tableau .nil Root) (Root_isFree : Root.i
       case nil =>
         simp only [loadMulti, List.foldr_nil] at lf_def
         have in_t : (~''(⌊α⌋φ)).inSide _theSide (nodeAt t) := by
-          simp_all [nodeAt]; aesop
+          simp_all [nodeAt]; aesop (rule_sets := [-default])
         -- Let C be the cluster to which `t` belongs.
         -- We claim that any ◃-path of satisfiable nodes starting at t must remain in C.
         have claim : ∀ s, t ◃⁺ s → satisfiable (nodeAt s) → s ≡ᶜ t := by
@@ -1615,7 +1615,7 @@ theorem tableauThenNotSat {Root} (tab : Tableau .nil Root) (Root_isFree : Root.i
           · have : (nodeAt t).isLoaded := by
               unfold Sequent.isLoaded
               simp [AnyNegFormula.inSide] at in_t
-              aesop
+              aesop (rule_sets := [-default])
             apply ePropB.e_help _ _ this rest_s_free t_to_s
       case cons β δ =>
         rintro ⟨W,M,v,v_⟩
@@ -1661,7 +1661,7 @@ theorem tableauThenNotSat {Root} (tab : Tableau .nil Root) (Root_isFree : Root.i
           · have : (nodeAt t).isLoaded := by
               unfold Sequent.isLoaded
               simp [AnyNegFormula.inSide] at in_t
-              aesop
+              aesop (rule_sets := [-default])
             apply ePropB.e_help _ _ this rest_s_free t_to_s
 
 theorem correctness : ∀ LR : Sequent, LR.isFree → satisfiable LR → consistent LR := by
diff --git a/LeanPool/PDL/Star.lean b/LeanPool/PDL/Star.lean
index 5b0ad07c97..e650b692e2 100644
--- a/LeanPool/PDL/Star.lean
+++ b/LeanPool/PDL/Star.lean
@@ -62,17 +62,17 @@ theorem ReflTransGen.to_finitelyManySteps {r : α → α → Prop} (h : Relation
   induction h using Relation.ReflTransGen.head_induction_on
   case refl =>
     use 0, List.Vector.cons z List.Vector.nil
-    aesop
+    aesop (rule_sets := [-default])
   case head a b a_r_b b_rS_z IH_b_z =>
     rcases IH_b_z with ⟨m, zs, b_is_head_zs, z_is_last_zs, zs_steps⟩
     use m + 1
     use a ::ᵥ zs
     simp only [List.Vector.head_cons, List.Vector.get_cons_succ, true_and]
     constructor
-    · aesop
+    · aesop (rule_sets := [-default])
     · intro i
       induction i using Fin.induction
-      all_goals aesop
+      all_goals aesop (rule_sets := [-default])
 
 /-- `a = x₀ ∧ r x₀ x₁ ∧ ... ∧ xₙ = b` implies `ReflTransGen r a b`.
 Similar to `List.relationReflTransGen_of_exists_chain` in mathlib. -/
@@ -116,7 +116,7 @@ theorem ReflTransGen.from_finitelyManySteps (r : α → α → Prop) {n : ℕ} :
       · intro i
         specialize steprel i.succ
         induction i
-        all_goals aesop
+        all_goals aesop (rule_sets := [-default])
 
 /-- `ReflTransGen r a b` is equivalent to `∃ x₀ ... xₙ, a = x₀ ∧ r x₀ x₁ ∧ ... ∧ r xₙ = b` -/
 theorem ReflTransGen.iff_finitelyManySteps (r : α → α → Prop) (x z : α) :
diff --git a/LeanPool/PDL/StayingInFL.lean b/LeanPool/PDL/StayingInFL.lean
index 6f87a8c1d3..6d28436a99 100644
--- a/LeanPool/PDL/StayingInFL.lean
+++ b/LeanPool/PDL/StayingInFL.lean
@@ -423,10 +423,10 @@ lemma unfoldBox_in_FL (α : Program) (ψ : Formula) (X : List Formula) :
     rcases this with ⟨τ, τ_in, def_φ⟩
     subst def_φ
     have := @neg_testsOfProgram_in_FLb τ α τ_in ψ
-    grind
+    grind only []
   · subst def_φ
     have := P_in_FL _ _ _ ψ in_P
-    grind [FL]
+    grind only [FL]
 
 /-- Helper for `LocalRule.stays_in_FL` -/
 theorem OneSidedLocalRule.stays_in_FL {precond ress}
diff --git a/LeanPool/PDL/Substitution.lean b/LeanPool/PDL/Substitution.lean
index 826bbbf648..86a3346364 100644
--- a/LeanPool/PDL/Substitution.lean
+++ b/LeanPool/PDL/Substitution.lean
@@ -162,18 +162,18 @@ lemma repl_in_F_voc_def p φ ψ :
   cases ψ <;> simp only [replInF, Formula.voc, Finset.empty_sdiff, Finset.notMem_empty,
     ↓reduceIte, Finset.union_idempotent, beq_iff_eq, Finset.mem_singleton, Sum.inl.injEq,
     Finset.mem_union]
-  case atom_prop q => by_cases q = p <;> aesop
+  case atom_prop q => by_cases q = p <;> aesop (rule_sets := [-default])
   case neg => apply repl_in_F_voc_def
   case and ψ1 ψ2 =>
     ext x
     have := repl_in_F_voc_def p φ ψ1
     have := repl_in_F_voc_def p φ ψ2
-    aesop
+    aesop (rule_sets := [-default])
   case box α ψ =>
     ext x
     have := repl_in_F_voc_def p φ ψ
     have := repl_in_P_voc_def p φ α
-    aesop
+    aesop (rule_sets := [-default])
 
 lemma repl_in_P_voc_def p φ α :
     (replInP p φ α).voc = (α.voc \ {Sum.inl p}) ∪ (if Sum.inl p ∈ α.voc then φ.voc else {}) := by
@@ -185,12 +185,12 @@ lemma repl_in_P_voc_def p φ α :
     ext x
     have := repl_in_P_voc_def p φ α
     have := repl_in_P_voc_def p φ β
-    aesop
+    aesop (rule_sets := [-default])
   case union α β =>
     ext x
     have := repl_in_P_voc_def p φ α
     have := repl_in_P_voc_def p φ β
-    aesop
+    aesop (rule_sets := [-default])
   case test τ =>
     ext x
     have := repl_in_F_voc_def p φ τ
@@ -299,7 +299,7 @@ theorem repl_in_disMap x ρ (L : List α) (p : α → Prop) (f : α → Formula)
     dis (L.map (fun Fδ => if p Fδ then Formula.bottom else replInF x ρ (f Fδ))) := by
   rw [repl_in_dis, listEq_to_disEq]
   simp only [List.map_map]
-  aesop
+  aesop (rule_sets := [-default])
 
 /-! ## Cancellation of replacements -/
 
diff --git a/LeanPool/PDL/Syntax.lean b/LeanPool/PDL/Syntax.lean
index 5dc71f86a1..0e8781bd1d 100644
--- a/LeanPool/PDL/Syntax.lean
+++ b/LeanPool/PDL/Syntax.lean
@@ -179,7 +179,7 @@ lemma def_of_boxesOf_def {φ γ ψ} (h : boxesOf φ = (γ, ψ)) : φ = ⌈⌈γ
     cases φ <;> simp_all
   case cons α αs IH =>
     simp only [Formula.boxes_cons]
-    cases φ <;> grind [boxesOf]
+    cases φ <;> grind only [boxesOf]
 
 /-- Whether a formula has an outer box constructor. -/
 def Formula.isBox : Formula → Prop
@@ -190,7 +190,7 @@ lemma boxesOf_def_of_def_of_nonBox {φ γ ψ} (h : φ = ⌈⌈γ⌉⌉ψ) (nonBo
     boxesOf φ = (γ, ψ) := by
   induction γ generalizing φ
   · unfold boxesOf
-    cases φ <;> simp_all [Formula.isBox]; aesop
+    cases φ <;> simp_all [Formula.isBox]; aesop (rule_sets := [-default])
   case cons α αs IH =>
     subst h
     unfold boxesOf
@@ -459,7 +459,7 @@ lemma LoadFormula.split_boxes_cons {βs α φ} :
   · rw [List.cons_append]
     rw [LoadFormula.boxes_cons]
     simp only [split, AnyFormula.split, Prod.mk.injEq, List.cons.injEq, true_and]
-    grind
+    grind only []
 
 @[simp]
 theorem AnyFormula.split_normal (φ : Formula) : (AnyFormula.normal φ).split = ([],φ) := by
@@ -613,7 +613,7 @@ lemma loadMulti_eq_of_some (h : δ.head? = some d) :
 
 lemma loadMulti_eq_loadBoxes :
     AnyFormula.loaded (loadMulti δ α φ) = AnyFormula.loadBoxes (δ ++ [α]) φ := by
-  induction δ <;> aesop
+  induction δ <;> aesop (rule_sets := [-default])
 
 /-! ## splitLast -/
 
@@ -653,7 +653,7 @@ lemma splitLast_inj {α} {xs ys : List α} (h : splitLast xs = splitLast ys) :
     simp_all
   · exfalso
     simp_all
-  aesop
+  aesop (rule_sets := [-default])
 
 lemma LoadFormula.split_splitLast_to_loadBoxes {δs φ δs_ δ ξ}
     (ξsp_def : ξ.split = (δs, φ))
diff --git a/LeanPool/PDL/Tableau.lean b/LeanPool/PDL/Tableau.lean
index 1e1ebca087..bcf583a745 100644
--- a/LeanPool/PDL/Tableau.lean
+++ b/LeanPool/PDL/Tableau.lean
@@ -40,7 +40,7 @@ theorem proj : g ∈ projection A X ↔ (⌈·A⌉g) ∈ X :=
   case cons =>
     simp only [projection, formProjection, beq_iff_eq, List.map_cons, List.mem_cons]
     rw [List.reduceOption_mem_iff]
-    aesop
+    aesop (rule_sets := [-default])
 
 /-- Collect the continuations of matching atomic boxes in a formula finset. -/
 def _root_.Finset.pdlProjection : Nat → Finset Formula → Finset Formula
@@ -136,7 +136,7 @@ lemma LoadedPathRepeat.ext {Hist X} (lprA lprB : LoadedPathRepeat Hist X) :
     lprA.1 = lprB.1 → lprA = lprB := by
   rcases lprA with ⟨a, ha⟩
   rcases lprB with ⟨b, hb⟩
-  grind
+  grind only []
 
 instance {Hist X} : DecidableEq (LoadedPathRepeat Hist X) := Subtype.instDecidableEq
 
diff --git a/LeanPool/PDL/TableauPath.lean b/LeanPool/PDL/TableauPath.lean
index dd96774fe2..faeff95daf 100644
--- a/LeanPool/PDL/TableauPath.lean
+++ b/LeanPool/PDL/TableauPath.lean
@@ -390,8 +390,8 @@ theorem length_succ_eq_length_of_edge {Hist X} {tab : Tableau Hist X} {s t : Pat
 
 theorem edge_then_length_lt {Hist X} {tab : Tableau Hist X} {s t : PathIn tab} (s_t : s ⋖_ t) :
   s.length < t.length := by
-  have := length_succ_eq_length_of_edge s_t
-  linarith
+  rw [← length_succ_eq_length_of_edge s_t]
+  exact Nat.lt_succ_self _
 
 /-- Map tableau edges to strict increases in path length. -/
 def edgeNatLTRelHom {Hist X tab} : RelHom (@edge Hist X tab) Nat.lt :=
@@ -567,7 +567,7 @@ Lemmas developed for `tabToIntAt`.
 
 @[simp]
 lemma PathIn.cast_nil {Hist : History} {X : Sequent} {tab tab2 : Tableau Hist X} (h : tab = tab2) :
-    (h ▸ (.nil : PathIn tab)) = (.nil : PathIn tab2) := by grind
+    (h ▸ (.nil : PathIn tab)) = (.nil : PathIn tab2) := by grind only []
 
 lemma PathIn.tabAt_cast_nil {Hist : History} {X : Sequent} {tab tab2 : Tableau Hist X}
     (h : tab = tab2) :
@@ -644,7 +644,7 @@ lemma PathIn.lt_append_non_nil {Hist X pHist pX tabNew} {tab : Tableau Hist X}
         have := @PathIn.loc_append _ _ nflprep nbas lt nexts Y Y_in tail rfl
         convert this <;> try rw [h]
         · simp_all
-        · grind
+        · grind only []
       · simp only [tabAt_append]
         rw! [h]
         simp
@@ -668,7 +668,7 @@ lemma PathIn.lt_append_non_nil {Hist X pHist pX tabNew} {tab : Tableau Hist X}
         have := @PathIn.pdl_append _ _ _ next nflprep bas r tail rfl
         convert this <;> try rw [h]
         · simp_all
-        · grind
+        · grind only []
       · simp only [tabAt_append]
         rw! [h]
         simp
@@ -946,7 +946,7 @@ theorem path_then_length_lt {Hist X} {tab : Tableau Hist X} {s t : PathIn tab} (
   induction s_t
   case single set => exact edge_then_length_lt set
   case tail h ih => have := edge_then_length_lt h
-                    linarith
+                    omega
 
 theorem path_is_irreflexive {Hist X} {tab : Tableau Hist X} {a : PathIn tab} : ¬(Relation.TransGen
   edge a a) := by
@@ -1052,7 +1052,7 @@ theorem rewind_of_edge_is_eq {Hist X} {tab : Tableau Hist X} {a b : PathIn tab}
   b.rewind 1 = a := by
   induction tab
   case loc rest Y nrep nbas lt next IH =>
-    cases b <;> simp_all only [PathIn.rewind]
+    cases b <;> simp only [PathIn.rewind]
     case nil => simp_all [not_edge_nil]
     case loc Z nbas' nrep' Z_in tail =>
       cases a
@@ -1064,10 +1064,10 @@ theorem rewind_of_edge_is_eq {Hist X} {tab : Tableau Hist X} {a b : PathIn tab}
             apply PathIn.loc_injective
             rw [p_def]
             unfold tabAt at tabAt_def
-            aesop
+            aesop (rule_sets := [-default])
           · exfalso
             unfold tabAt at tabAt_def
-            aesop
+            aesop (rule_sets := [-default])
         subst t_nil
         rfl
       case loc X nbas'' nrep'' X_in tail' =>
@@ -1103,9 +1103,9 @@ theorem rewind_of_edge_is_eq {Hist X} {tab : Tableau Hist X} {a b : PathIn tab}
           Fin.val_castSucc, Fin.coe_ofNat_eq_mod, PathIn.loc_length_eq, Nat.one_mod, Fin.val_cast]
             at *
         rw [kdef, @Nat.one_mod_eq_one]
-        aesop
+        aesop (rule_sets := [-default])
   case pdl rest Y X nrep bas r tab IH =>
-    cases b <;> simp_all only [PathIn.rewind]
+    cases b <;> simp only [PathIn.rewind]
     case nil => simp_all [not_edge_nil]
     case pdl Z bas' nrep' tail =>
       cases a
@@ -1115,12 +1115,12 @@ theorem rewind_of_edge_is_eq {Hist X} {tab : Tableau Hist X} {a b : PathIn tab}
                           | ⟨_, _, _, _, _, _, _, tabAt_def, p_def⟩ )
           · exfalso
             unfold tabAt at tabAt_def
-            aesop
+            aesop (rule_sets := [-default])
           · simp only [PathIn.append] at p_def
             apply PathIn.pdl_injective
             rw [p_def]
             unfold tabAt at tabAt_def
-            aesop
+            aesop (rule_sets := [-default])
         subst t_nil
         rfl
       case pdl bas'' nrep'' tail' =>
@@ -1148,7 +1148,7 @@ theorem rewind_of_edge_is_eq {Hist X} {tab : Tableau Hist X} {a b : PathIn tab}
           Fin.val_castSucc, Fin.coe_ofNat_eq_mod, PathIn.pdl_length_eq, Nat.one_mod, Fin.val_cast]
             at *
         rw [kdef, @Nat.one_mod_eq_one]
-        aesop
+        aesop (rule_sets := [-default])
   case lrep => cases b; simp [not_edge_nil] at a_b
 
 theorem rewind_order_reversing_if_not_nil {Hist X} {tab : Tableau Hist X} {t : PathIn tab}
@@ -1379,10 +1379,10 @@ theorem rewind_helper {Hist X} {tab : Tableau Hist X} {a b : PathIn tab} {k : Fi
             apply PathIn.loc_injective
             rw [p_def]
             unfold tabAt at tabAt_def
-            aesop
+            aesop (rule_sets := [-default])
           · exfalso
             unfold tabAt at tabAt_def
-            aesop
+            aesop (rule_sets := [-default])
         subst t_nil
         simp_all [PathIn.rewind, Fin.lastCases, PathIn.toHistory]
         have ⟨k_val, k_pf⟩ := k
@@ -1434,12 +1434,12 @@ theorem rewind_helper {Hist X} {tab : Tableau Hist X} {a b : PathIn tab} {k : Fi
                         | ⟨_, _, _, _, _, _, _, tabAt_def, p_def⟩ )
           · exfalso
             unfold tabAt at tabAt_def
-            aesop
+            aesop (rule_sets := [-default])
           · simp only [PathIn.append] at p_def
             apply PathIn.pdl_injective
             rw [p_def]
             unfold tabAt at tabAt_def
-            aesop
+            aesop (rule_sets := [-default])
         subst t_nil
         simp_all [PathIn.rewind, PathIn.toHistory]
         have ⟨k_val, k_pf⟩ := k
@@ -1460,7 +1460,7 @@ theorem rewind_helper {Hist X} {tab : Tableau Hist X} {a b : PathIn tab} {k : Fi
             simp_all [Fin.last]
             simp [PathIn.toHistory] at i_pf
             have := edge_inc_length_by_one t'_t
-            linarith
+            omega
           rw [← Fin.exists_castSucc_eq] at h
           rcases h with ⟨k, kdef⟩
           simp only [Fin.cast_succ_eq, ← kdef, Fin.lastCases_castSucc, Function.comp_apply,
@@ -1544,31 +1544,19 @@ theorem allPaths_loc_cases {Hist X} {nrep : ¬ flprep Hist X} {nbas : ¬ X.basic
       ∨ ∃ (Y : Sequent) (Y_in : Y ∈ endNodesOf lt) (t :  PathIn (next Y Y_in)),
           t ∈ allPaths (next Y Y_in) ∧
           s = PathIn.loc Y_in t := by
-  constructor <;> intro hyp
-  · unfold allPaths at hyp
-    aesop
-  · unfold allPaths
-    aesop
+  simp only [allPaths, Finset.mem_union, Finset.mem_singleton, Finset.mem_sup,
+    Finset.mem_attach, true_and, Finset.mem_image, Subtype.exists, eq_comm]
 
 theorem PathIn.elem_allPaths {Hist X} {tab : Tableau Hist X} (p : PathIn tab) :
     p ∈ allPaths tab := by
-  induction tab
-  case loc Hist X lt nexts IH =>
-    induction p using init_inductionOn
-    case root =>
-      simp_all [allPaths]
-    case step t _ s t_s =>
-      rw [allPaths_loc_cases]
-      cases s
-      · tauto
-      case loc nrep nbas Y Y_in tail =>
-        right
-        simp_all
-  case pdl nrep bas r next =>
-    cases p <;> simp_all [allPaths]
-  case lrep lpr =>
-    cases p
-    simp_all [allPaths]
+  induction p with
+  | nil =>
+    rename_i tab
+    cases tab <;> simp only [allPaths, Finset.mem_union, Finset.mem_singleton, true_or]
+  | loc Y_in tail ih =>
+    exact (allPaths_loc_cases _).mpr (Or.inr ⟨_, Y_in, tail, ih, rfl⟩)
+  | pdl tail ih =>
+    exact Finset.mem_union_right _ (Finset.mem_image.mpr ⟨tail, ih, rfl⟩)
 
 /-- A Tableau is finite.
 Should be useful to get *converse* well-foundedness of `edge` -/
@@ -1582,15 +1570,29 @@ theorem Finite.wellfounded_of_irrefl_TC {α : Type} [Finite α] (r : α → α 
   ⟨fun a => acc_transGen_iff.mp <| wf.apply a⟩
 
 lemma nodeAt_mem_History_of_edge : p ⋖_ q → nodeAt p ∈ (tabAt q).1 := by
-  rintro ( ⟨Hist, XX, nrep, nbas, lt, next, Y, Y_in, tab_def, q_def⟩
-         | ⟨Hist, XX, nrep, bas, Y, r, next, tab_def, q_def⟩ )
-  <;> induction p <;> (simp at tab_def; try aesop)
+  rintro (⟨Hist, XX, nrep, nbas, lt, next, Y, Y_in, tab_def, q_def⟩ |
+    ⟨Hist, XX, nrep, bas, Y, rule, next, tab_def, q_def⟩)
+  all_goals
+    subst q_def
+    rw [tabAt_append, tabAt_cast_gen p _ tab_def]
+    simp only [tabAt]
+    have hnode : nodeAt p = XX := by
+      change (tabAt p).2.1 = XX
+      exact congrArg (fun value => value.2.1) tab_def
+    rw [hnode]
+    exact List.mem_cons_self
 
 lemma mem_History_of_edge : p ⋖_ q → x ∈ (tabAt p).1 → x ∈ (tabAt q).1 := by
-  intro hedge hmemp
-  rcases hedge with ( ⟨Hist, XX, nrep, nbas, lt, next, Y, Y_in, tab_def, q_def⟩
-                    | ⟨Hist, XX, nrep, bas, Y, r, next, tab_def, q_def⟩ )
-  <;> induction p <;> (simp at tab_def; try aesop)
+  intro hedge hx
+  rcases hedge with (⟨Hist, XX, nrep, nbas, lt, next, Y, Y_in, tab_def, q_def⟩ |
+    ⟨Hist, XX, nrep, bas, Y, rule, next, tab_def, q_def⟩)
+  all_goals
+    subst q_def
+    rw [tabAt_append, tabAt_cast_gen p _ tab_def]
+    simp only [tabAt]
+    have hhistory : (tabAt p).1 = Hist := congrArg (fun value => value.1) tab_def
+    rw [hhistory] at hx
+    exact List.mem_cons_of_mem XX hx
 
 lemma mem_History_append : X ∈ (tabAt p).1 → X ∈ (tabAt (p.append q)).1 := by
   intro h
@@ -1628,7 +1630,7 @@ lemma PathIn.length_lt_tab_size {H X} (tab : Tableau H X) (p : PathIn tab) :
     case pdl nrep bas tail =>
       simp only [length, Tableau.size]
       specialize IH tail
-      grind
+      grind only []
   · cases p
     simp [Tableau.size]
 
@@ -1645,9 +1647,9 @@ theorem flipEdge.wellFounded {H X} {tab : Tableau H X} :
     fun n => edge_then_length_lt (all_rel n)
   have : ∀ n, (f (n + 1)).length > n := by
     intro n
-    induction n <;> grind
+    induction n <;> grind only []
   absurd this tab.size
-  grind
+  grind only []
 
 /-- Induction principle going from the leaves (= childless nodes) to the root.
 Suppose whenever the `motive` holds at all children then it holds at the parent.