From 7c3f2bd35615f6f19b4bee3c1ea3dcb8de17088b Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 26 Oct 2025 08:57:58 -0400
Subject: [PATCH 01/12] chore: golfing in BehaviouralTheory

---
 Cslib/Languages/CCS/BehaviouralTheory.lean | 263 ++++++++-------------
 1 file changed, 96 insertions(+), 167 deletions(-)

diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean
index 17e4bd41..52c6cf14 100644
--- a/Cslib/Languages/CCS/BehaviouralTheory.lean
+++ b/Cslib/Languages/CCS/BehaviouralTheory.lean
@@ -31,7 +31,7 @@ open CCS CCS.Process CCS.Act
 
 namespace CCS
 
-@[grind]
+@[scoped grind]
 private inductive ParNil : (Process Name Constant) → (Process Name Constant) → Prop where
 | parNil : ParNil (par p nil) p
 
@@ -47,7 +47,7 @@ theorem bisimilarity_par_nil : (par p nil) ~[lts (defs := defs)] p := by
     grind [cases Tr]
   case right =>
     intro s2' htr
-    exists (par s2' nil)
+    exists par s2' nil
     grind [Tr.parL]
 
 private inductive ParComm : (Process Name Constant) → (Process Name Constant) → Prop where
@@ -58,50 +58,37 @@ private inductive ParComm : (Process Name Constant) → (Process Name Constant)
 theorem bisimilarity_par_comm : (par p q) ~[lts (defs := defs)] (par q p) := by
   exists ParComm
   constructor
-  case left =>
-    constructor
+  case left => constructor
   case right =>
-    simp only [LTS.IsBisimulation]
     intro s1 s2 hr μ
     cases hr
+    unfold lts at *
     case parComm p q =>
       constructor
       case left =>
         intro t htr
         cases htr
         case parL p' htr' =>
-          exists (par q p')
-          constructor
-          · apply Tr.parR htr'
-          · constructor
+          exists par q p'
+          grind [Tr.parR, ParComm]
         case parR q' htr' =>
-          exists (par q' p)
-          constructor
-          · apply Tr.parL htr'
-          · constructor
+          exists par q' p
+          grind [Tr.parL, ParComm]
         case com μ p' μ' q' hco htrp htrq =>
-          exists (par q' p')
-          constructor
-          · apply Tr.com hco.symm htrq htrp
-          · constructor
+          exists par q' p'
+          grind [Tr.com, ParComm]
       case right =>
         intro t htr
         cases htr
         case parL q' htr' =>
-          exists (par p q')
-          constructor
-          · apply Tr.parR htr'
-          · constructor
+          exists par p q'
+          grind [Tr.parR, ParComm]
         case parR p' htr' =>
-          exists (par p' q)
-          constructor
-          · apply Tr.parL htr'
-          · constructor
+          exists par p' q
+          grind [Tr.parL, ParComm]
         case com μ p' μ' q' hco htrp htrq =>
-          exists (par q' p')
-          constructor
-          · apply Tr.com hco.symm htrq htrp
-          · constructor
+          exists par q' p'
+          grind [Tr.com, ParComm]
 
 /-- 𝟎 | P ~ P -/
 @[simp, scoped grind .]
@@ -110,7 +97,6 @@ theorem bisimilarity_nil_par : (par nil p) ~[lts (defs := defs)] p :=
     (par nil p) ~[lts (defs := defs)] (par p nil) := by grind
     _ ~[lts (defs := defs)] p := by simp
 
-
 private inductive ParAssoc : (Process Name Constant) → (Process Name Constant) → Prop where
   | assoc : ParAssoc (par p (par q r)) (par (par p q) r)
   | id : ParAssoc p p
@@ -118,7 +104,7 @@ private inductive ParAssoc : (Process Name Constant) → (Process Name Constant)
 /-- P | (Q | R) ~ (P | Q) | R -/
 theorem bisimilarity_par_assoc :
   (par p (par q r)) ~[lts (defs := defs)] (par (par p q) r) := by
-  refine ⟨ParAssoc, ParAssoc.assoc, ?_⟩
+  use ParAssoc, ParAssoc.assoc
   intro s1 s2 hr μ
   apply And.intro <;> cases hr
   case right.assoc =>
@@ -135,7 +121,7 @@ theorem bisimilarity_par_assoc :
         grind [Tr.parL, Tr.parR, ParAssoc]
       case com μ p' μ' q' _ htrp htrq =>
         exists p'.par (q'.par r)
-        have htrq' : Tr (defs := defs) (q.par r) μ' (q'.par r) := by apply Tr.parL; assumption
+        have htrq' : Tr (defs := defs) (q.par r) μ' (q'.par r) := by grind [Tr.parL]
         grind [Tr.com, Tr.parL, ParAssoc]
     case parR p q r r' htr =>
       exists p.par (q.par r')
@@ -143,14 +129,12 @@ theorem bisimilarity_par_assoc :
     case com p q r μ p' μ' r' _ htr htr' =>
       cases htr
       case parL p' _ =>
-        refine ⟨ p'.par (q.par r'), ?_, ParAssoc.assoc⟩
-        apply Tr.com (μ := μ) (μ' := μ') <;> grind [Tr.parR]
+        use p'.par (q.par r')
+        grind [Tr.parR, Tr.com, ParAssoc.assoc]
       case parR q' _ =>
         use p.par (q'.par r')
         grind [Tr.parR, Tr.com, ParAssoc.assoc]
-      case com μ p' q' _ _ =>
-        unfold Act.Co at *
-        grind
+      case com => grind
   case left.assoc =>
     intro s2' htr
     unfold lts at *
@@ -164,8 +148,8 @@ theorem bisimilarity_par_assoc :
         exists (p.par q).par r'
         grind [Tr.parL, Tr.parR, ParAssoc]
       case com p q r μ q' μ' r' _ htrp htrq =>
-        refine ⟨(p.par q').par r', ?_, ParAssoc.assoc⟩
-        apply Tr.com (μ := μ) (μ' := μ') <;> grind [Tr.parR]
+        use (p.par q').par r'
+        grind [Tr.parR, Tr.com, ParAssoc.assoc]
     case parL p q r p' htr =>
       exists (p'.par q).par r
       grind [Tr.parL, ParAssoc]
@@ -175,11 +159,9 @@ theorem bisimilarity_par_assoc :
         use (p'.par q').par r
         grind [Tr.parL, Tr.com, ParAssoc.assoc]
       case parR r' _ =>
-        refine ⟨ (p'.par q).par r', ?_, ParAssoc.assoc⟩
-        apply Tr.com (μ := μ) (μ' := μ') <;> grind [Tr.parL]
-      case com =>
-        unfold Act.Co at *
-        grind
+        use (p'.par q).par r'
+        grind [Tr.parL, Tr.com, ParAssoc.assoc]
+      case com => grind
   all_goals grind [ParAssoc]
 
 private inductive ChoiceNil : (Process Name Constant) → (Process Name Constant) → Prop where
@@ -188,7 +170,7 @@ private inductive ChoiceNil : (Process Name Constant) → (Process Name Constant
 
 /-- P + 𝟎 ~ P -/
 theorem bisimilarity_choice_nil : (choice p nil) ~[lts (defs := defs)] p := by
-  refine ⟨ChoiceNil, ChoiceNil.nil, ?_⟩
+  use ChoiceNil, ChoiceNil.nil
   intro s1 s2 hr μ
   apply And.intro <;> cases hr
   case left.nil =>
@@ -215,16 +197,14 @@ theorem bisimilarity_choice_idem :
   case left => grind [ChoiceIdem]
   case right =>
     intro s1 s2 hr μ
-    apply And.intro <;> cases hr
+    apply And.intro <;> cases hr <;> unfold lts
     case left.idem =>
-      unfold lts
       grind [cases Tr, ChoiceIdem]
     case left.id =>
       grind [ChoiceIdem]
     case right.idem =>
       intro s1' htr
       exists s1'
-      unfold lts at *
       grind [Tr, ChoiceIdem]
     case right.id =>
       grind [ChoiceIdem]
@@ -237,11 +217,9 @@ private inductive ChoiceComm : (Process Name Constant) → (Process Name Constan
 theorem bisimilarity_choice_comm : (choice p q) ~[lts (defs := defs)] (choice q p) := by
   exists @ChoiceComm Name Constant defs
   repeat constructor
-  simp only [LTS.IsBisimulation]
   intro s1 s2 hr μ
   cases hr
-  case choiceComm =>
-    rename_i p q
+  case choiceComm p q =>
     constructor
     case left =>
       intro s1' htr
@@ -249,8 +227,7 @@ theorem bisimilarity_choice_comm : (choice p q) ~[lts (defs := defs)] (choice q
       constructor
       · unfold lts
         cases htr with grind [Tr.choiceR, Tr.choiceL]
-      · constructor
-        grind
+      · grind [ChoiceComm]
     case right =>
       intro s1' htr
       exists s1'
@@ -268,7 +245,7 @@ private inductive ChoiceAssoc : (Process Name Constant) → (Process Name Consta
 /-- P + (Q + R) ~ (P + Q) + R -/
 theorem bisimilarity_choice_assoc :
     (choice p (choice q r)) ~[lts (defs := defs)] (choice (choice p q) r) := by
-  refine ⟨ChoiceAssoc, ChoiceAssoc.assoc, ?_⟩
+  use ChoiceAssoc, ChoiceAssoc.assoc
   intro s1 s2 hr μ
   apply And.intro <;> cases hr
   case left.assoc p q r =>
@@ -301,49 +278,29 @@ theorem bisimilarity_congr_pre :
   intro hpq
   exists @PreBisim _ _ defs
   constructor
-  · constructor; assumption
-  simp only [LTS.IsBisimulation]
+  · grind [PreBisim]
   intro s1 s2 hr μ'
   cases hr
-  case pre =>
-    rename_i p' q' μ hbis
-    constructor
-    case left =>
-      intro s1' htr
-      cases htr
-      exists q'
-      constructor; constructor
-      apply PreBisim.bisim hbis
-    case right =>
-      intro s2' htr
-      cases htr
-      exists p'
-      constructor; constructor
-      apply PreBisim.bisim hbis
+  case pre p' q' μ hbis =>
+    unfold lts
+    constructor <;> intro _ _ <;> [exists q'; exists p'] <;> grind [cases Tr, Tr.pre, PreBisim]
   case bisim hbis =>
     constructor
     case left =>
       intro s1' htr
-      obtain ⟨r, hr, hb⟩ := hbis
-      let hbisim := hb
-      obtain ⟨s2', htr2, hr2⟩ := hb.follow_fst hr htr
+      obtain ⟨_, hr, hb⟩ := hbis
+      obtain ⟨s2', _⟩ := hb.follow_fst hr htr
       exists s2'
-      apply And.intro htr2
-      constructor
-      apply Bisimilarity.largest_bisimulation hbisim hr2
+      grind [PreBisim, Bisimilarity.largest_bisimulation]
     case right =>
       intro s2' htr
-      obtain ⟨r, hr, hb⟩ := hbis
-      let hbisim := hb
-      specialize hb hr μ'
-      obtain ⟨hb1, hb2⟩ := hb
-      specialize hb2 _ htr
-      obtain ⟨s1', htr1, hr1⟩ := hb2
+      obtain ⟨_, hr, hb⟩ := hbis
+      have ⟨_, hb2⟩ := hb hr μ'
+      obtain ⟨s1', _⟩ := hb2 _ htr
       exists s1'
-      apply And.intro htr1
-      constructor
-      apply Bisimilarity.largest_bisimulation hbisim hr1
+      grind [PreBisim, Bisimilarity.largest_bisimulation]
 
+@[scoped grind]
 private inductive ResBisim : (Process Name Constant) → (Process Name Constant) → Prop where
 | res : (p ~[lts (defs := defs)] q) → ResBisim (res a p) (res a q)
 -- | bisim : (p ~[lts (defs := defs)] q) → ResBisim p q
@@ -354,30 +311,25 @@ theorem bisimilarity_congr_res :
   intro hpq
   exists @ResBisim _ _ defs
   constructor
-  · constructor; assumption
-  simp only [LTS.IsBisimulation]
+  · grind
   intro s1 s2 hr μ'
   cases hr
   rename_i p q a h
   constructor
   case left =>
     intro s1' htr
-    cases htr
-    rename_i p' h1 h2 htr
-    have h := Bisimilarity.is_bisimulation.follow_fst h htr
-    obtain ⟨q', htrq, h⟩ := h
-    exists (res a q')
-    constructor; constructor; repeat assumption
-    constructor; assumption
+    cases htr with | res _ _ htr =>
+    obtain ⟨q', _⟩ := Bisimilarity.is_bisimulation.follow_fst h htr
+    exists res a q'
+    unfold lts at *
+    grind [Tr]
   case right =>
     intro s2' htr
-    cases htr
-    rename_i q' h1 h2 htr
-    have h := Bisimilarity.is_bisimulation.follow_snd h htr
-    obtain ⟨p', htrq, h⟩ := h
-    exists (res a p')
-    constructor; constructor; repeat assumption
-    constructor; assumption
+    cases htr with | res _ _ htr =>
+    obtain ⟨p', _⟩ := Bisimilarity.is_bisimulation.follow_snd h htr
+    exists res a p'
+    unfold lts at *
+    grind [Tr]
 
 private inductive ChoiceBisim : (Process Name Constant) → (Process Name Constant) → Prop where
 | choice : (p ~[lts (defs := defs)] q) → ChoiceBisim (choice p r) (choice q r)
@@ -390,7 +342,6 @@ theorem bisimilarity_congr_choice :
   exists @ChoiceBisim _ _ defs
   constructor
   · constructor; assumption
-  simp only [LTS.IsBisimulation]
   intro s1 s2 r μ
   constructor
   case left =>
@@ -448,6 +399,7 @@ theorem bisimilarity_congr_choice :
       · constructor
         apply Bisimilarity.largest_bisimulation hb hr1
 
+@[scoped grind]
 private inductive ParBisim : (Process Name Constant) → (Process Name Constant) → Prop where
 | par : (p ~[lts (defs := defs)] q) → ParBisim (par p r) (par q r)
 
@@ -457,88 +409,65 @@ theorem bisimilarity_congr_par :
   intro h
   exists @ParBisim _ _ defs
   constructor
-  · constructor; assumption
-  simp only [LTS.IsBisimulation]
+  · grind
   intro s1 s2 r μ
   constructor
   case left =>
     intro s1' htr
     cases r
+    unfold lts at *
+    have : {Tr :=  Tr (defs := defs)} = lts (defs := defs) := by rfl
     case par p q r hbisim =>
       obtain ⟨rel, hr, hb⟩ := hbisim
       cases htr
-      case parL _ _ p' htr =>
-        obtain ⟨q', htr2, hr2⟩ := hb.follow_fst hr htr
-        exists (par q' r)
-        constructor
-        · apply Tr.parL htr2
-        · constructor
-          apply Bisimilarity.largest_bisimulation hb hr2
-      case parR _ _ r' htr =>
-        exists (par q r')
-        constructor
-        · apply Tr.parR htr
-        · constructor
-          apply Bisimilarity.largest_bisimulation hb hr
-      case com _ p' _ r' hco htrp htrr =>
-        obtain ⟨q', htr2, hr2⟩ := hb.follow_fst hr htrp
-        exists (par q' r')
-        constructor
-        · apply Tr.com hco htr2 htrr
-        · constructor
-          apply Bisimilarity.largest_bisimulation hb hr2
+      case parL p' htr =>
+        obtain ⟨q', _⟩ := hb.follow_fst hr htr
+        exists par q' r
+        grind [Tr.parL]
+      case parR r' htr =>
+        exists par q r'
+        grind [Tr.parR]
+      case com r' _ htrp _ =>
+        obtain ⟨q', _⟩ := hb.follow_fst hr htrp
+        exists par q' r'
+        grind [Tr.com]
   case right =>
     intro s2' htr
     cases r
-    case par p q r hbisim =>
-      obtain ⟨rel, hr, hb⟩ := hbisim
+    unfold lts at *
+    have : {Tr :=  Tr (defs := defs)} = lts (defs := defs) := by rfl
+    case par p _ r hbisim =>
+      obtain ⟨_, hr, hb⟩ := hbisim
       cases htr
-      case parL _ _ p' htr =>
-        obtain ⟨p', htr2, hr2⟩ := hb.follow_snd hr htr
-        exists (par p' r)
-        constructor
-        · apply Tr.parL htr2
-        · constructor
-          apply Bisimilarity.largest_bisimulation hb hr2
+      case parL htr =>
+        obtain ⟨p', _⟩ := hb.follow_snd hr htr
+        exists par p' r
+        grind [Tr.parL]
       case parR _ _ r' htr =>
-        exists (par p r')
-        constructor
-        · apply Tr.parR htr
-        · constructor
-          apply Bisimilarity.largest_bisimulation hb hr
-      case com _ p' _ r' hco htrq htrr =>
-        obtain ⟨q', htr2, hr2⟩ := hb.follow_snd hr htrq
-        exists (par q' r')
-        constructor
-        · apply Tr.com hco htr2 htrr
-        · constructor
-          apply Bisimilarity.largest_bisimulation hb hr2
+        exists par p r'
+        grind [Tr.parR]
+      case com r' hco htrq htrr =>
+        obtain ⟨q', _⟩ := hb.follow_snd hr htrq
+        exists par q' r'
+        grind [Tr.com]
 
 /-- Bisimilarity is a congruence in CCS. -/
 theorem bisimilarity_congr
   (c : Context Name Constant) (p q : Process Name Constant) (h : p ~[lts (defs := defs)] q) :
   (c.fill p) ~[lts (defs := defs)] (c.fill q) := by
-  induction c
-  case hole => exact h
-  case pre _ _  ih => exact bisimilarity_congr_pre ih
-  case parL _ _ ih => exact bisimilarity_congr_par ih
-  case parR r c ih =>
-    apply Bisimilarity.trans
-    · apply bisimilarity_par_comm
-    · apply Bisimilarity.trans
-      · apply bisimilarity_congr_par
-        exact ih
-      · apply bisimilarity_par_comm
-  case choiceL _ _ ih => exact bisimilarity_congr_choice ih
-  case choiceR r c ih =>
-    apply Bisimilarity.trans
-    · apply bisimilarity_choice_comm
-    · apply Bisimilarity.trans
-      · exact bisimilarity_congr_choice ih
-      · exact bisimilarity_choice_comm
-  case res =>
-    apply bisimilarity_congr_res
-    assumption
+  induction c with
+  | parR r c ih =>
+    calc
+      _ ~[lts (defs := defs)] (c.fill p |>.par r)  := by grind
+      _ ~[lts (defs := defs)] (c.fill q |>.par r)  := by grind [bisimilarity_congr_par]
+      _ ~[lts (defs := defs)] (c.parR r |>.fill q) := by grind
+  | choiceR r c _ =>
+    calc
+      _ ~[lts (defs := defs)] (c.fill p |>.choice r)  := by grind [bisimilarity_choice_comm]
+      _ ~[lts (defs := defs)] (c.fill q |>.choice r)  := by grind [bisimilarity_congr_choice]
+      _ ~[lts (defs := defs)] (c.choiceR r |>.fill q) := by grind [bisimilarity_choice_comm]
+  | _ => grind [bisimilarity_congr_pre, bisimilarity_congr_par, 
+                bisimilarity_congr_choice, bisimilarity_congr_res]
 
 end CCS
 

From d327f6b7860d44437731352b1b90a6a8e4f26789 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 26 Oct 2025 09:11:34 -0400
Subject: [PATCH 02/12] locally grind Tr

---
 Cslib/Languages/CCS/BehaviouralTheory.lean | 86 +++++++++++-----------
 1 file changed, 43 insertions(+), 43 deletions(-)

diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean
index 52c6cf14..89b4c706 100644
--- a/Cslib/Languages/CCS/BehaviouralTheory.lean
+++ b/Cslib/Languages/CCS/BehaviouralTheory.lean
@@ -31,6 +31,8 @@ open CCS CCS.Process CCS.Act
 
 namespace CCS
 
+attribute [local grind] Tr
+
 @[scoped grind]
 private inductive ParNil : (Process Name Constant) → (Process Name Constant) → Prop where
 | parNil : ParNil (par p nil) p
@@ -48,8 +50,9 @@ theorem bisimilarity_par_nil : (par p nil) ~[lts (defs := defs)] p := by
   case right =>
     intro s2' htr
     exists par s2' nil
-    grind [Tr.parL]
+    grind
 
+@[scoped grind]
 private inductive ParComm : (Process Name Constant) → (Process Name Constant) → Prop where
 | parComm : ParComm (par p q) (par q p)
 
@@ -70,25 +73,25 @@ theorem bisimilarity_par_comm : (par p q) ~[lts (defs := defs)] (par q p) := by
         cases htr
         case parL p' htr' =>
           exists par q p'
-          grind [Tr.parR, ParComm]
+          grind
         case parR q' htr' =>
           exists par q' p
-          grind [Tr.parL, ParComm]
+          grind
         case com μ p' μ' q' hco htrp htrq =>
           exists par q' p'
-          grind [Tr.com, ParComm]
+          grind
       case right =>
         intro t htr
         cases htr
         case parL q' htr' =>
           exists par p q'
-          grind [Tr.parR, ParComm]
+          grind
         case parR p' htr' =>
           exists par p' q
-          grind [Tr.parL, ParComm]
+          grind
         case com μ p' μ' q' hco htrp htrq =>
           exists par q' p'
-          grind [Tr.com, ParComm]
+          grind
 
 /-- 𝟎 | P ~ P -/
 @[simp, scoped grind .]
@@ -97,6 +100,7 @@ theorem bisimilarity_nil_par : (par nil p) ~[lts (defs := defs)] p :=
     (par nil p) ~[lts (defs := defs)] (par p nil) := by grind
     _ ~[lts (defs := defs)] p := by simp
 
+@[scoped grind]
 private inductive ParAssoc : (Process Name Constant) → (Process Name Constant) → Prop where
   | assoc : ParAssoc (par p (par q r)) (par (par p q) r)
   | id : ParAssoc p p
@@ -115,25 +119,24 @@ theorem bisimilarity_par_assoc :
       cases htr
       case parL p q r p' _ =>
         exists p'.par (q.par r)
-        grind [Tr.parL, ParAssoc]
+        grind
       case parR p q r q' _ =>
         exists p.par (q'.par r)
-        grind [Tr.parL, Tr.parR, ParAssoc]
+        grind
       case com μ p' μ' q' _ htrp htrq =>
         exists p'.par (q'.par r)
-        have htrq' : Tr (defs := defs) (q.par r) μ' (q'.par r) := by grind [Tr.parL]
-        grind [Tr.com, Tr.parL, ParAssoc]
+        grind
     case parR p q r r' htr =>
       exists p.par (q.par r')
-      grind [Tr.parR, ParAssoc]
+      grind
     case com p q r μ p' μ' r' _ htr htr' =>
       cases htr
       case parL p' _ =>
         use p'.par (q.par r')
-        grind [Tr.parR, Tr.com, ParAssoc.assoc]
+        grind
       case parR q' _ =>
         use p.par (q'.par r')
-        grind [Tr.parR, Tr.com, ParAssoc.assoc]
+        grind
       case com => grind
   case left.assoc =>
     intro s2' htr
@@ -143,26 +146,26 @@ theorem bisimilarity_par_assoc :
       cases htr
       case parL p q r q' _ =>
         exists (p.par q').par r
-        grind [Tr.parL, Tr.parR, ParAssoc]
+        grind
       case parR p q r r' _ =>
         exists (p.par q).par r'
-        grind [Tr.parL, Tr.parR, ParAssoc]
+        grind
       case com p q r μ q' μ' r' _ htrp htrq =>
         use (p.par q').par r'
-        grind [Tr.parR, Tr.com, ParAssoc.assoc]
+        grind
     case parL p q r p' htr =>
       exists (p'.par q).par r
-      grind [Tr.parL, ParAssoc]
+      grind
     case com p q r μ p' μ' q' _ htr htr' =>
       cases htr'
       case parL q' _ =>
         use (p'.par q').par r
-        grind [Tr.parL, Tr.com, ParAssoc.assoc]
+        grind
       case parR r' _ =>
         use (p'.par q).par r'
-        grind [Tr.parL, Tr.com, ParAssoc.assoc]
+        grind
       case com => grind
-  all_goals grind [ParAssoc]
+  all_goals grind
 
 private inductive ChoiceNil : (Process Name Constant) → (Process Name Constant) → Prop where
   | nil : ChoiceNil (choice p nil) p
@@ -185,6 +188,7 @@ theorem bisimilarity_choice_nil : (choice p nil) ~[lts (defs := defs)] p := by
     · exact ChoiceNil.id
   all_goals grind [ChoiceNil]
 
+@[scoped grind]
 private inductive ChoiceIdem : (Process Name Constant) → (Process Name Constant) → Prop where
   | idem : ChoiceIdem (choice p p) p
   | id : ChoiceIdem p p
@@ -194,20 +198,15 @@ theorem bisimilarity_choice_idem :
   (choice p p) ~[lts (defs := defs)] p := by
   exists ChoiceIdem
   apply And.intro
-  case left => grind [ChoiceIdem]
+  case left => grind
   case right =>
     intro s1 s2 hr μ
     apply And.intro <;> cases hr <;> unfold lts
-    case left.idem =>
-      grind [cases Tr, ChoiceIdem]
-    case left.id =>
-      grind [ChoiceIdem]
     case right.idem =>
       intro s1' htr
       exists s1'
-      grind [Tr, ChoiceIdem]
-    case right.id =>
-      grind [ChoiceIdem]
+      grind
+    all_goals grind
 
 private inductive ChoiceComm : (Process Name Constant) → (Process Name Constant) → Prop where
   | choiceComm : ChoiceComm (choice p q) (choice q p)
@@ -226,14 +225,14 @@ theorem bisimilarity_choice_comm : (choice p q) ~[lts (defs := defs)] (choice q
       exists s1'
       constructor
       · unfold lts
-        cases htr with grind [Tr.choiceR, Tr.choiceL]
+        cases htr with grind
       · grind [ChoiceComm]
     case right =>
       intro s1' htr
       exists s1'
       constructor
       · unfold lts
-        cases htr with grind [Tr.choiceR, Tr.choiceL]
+        cases htr with grind
       · grind [ChoiceComm]
   case bisim h =>
     grind [ChoiceComm]
@@ -268,6 +267,7 @@ theorem bisimilarity_choice_assoc :
     case choiceR htr => apply Tr.choiceR; apply Tr.choiceR; assumption
   all_goals grind [ChoiceAssoc.id]
 
+@[scoped grind]
 private inductive PreBisim : (Process Name Constant) → (Process Name Constant) → Prop where
 | pre : (p ~[lts (defs := defs)] q) → PreBisim (pre μ p) (pre μ q)
 | bisim : (p ~[lts (defs := defs)] q) → PreBisim p q
@@ -278,12 +278,12 @@ theorem bisimilarity_congr_pre :
   intro hpq
   exists @PreBisim _ _ defs
   constructor
-  · grind [PreBisim]
+  · grind
   intro s1 s2 hr μ'
   cases hr
   case pre p' q' μ hbis =>
     unfold lts
-    constructor <;> intro _ _ <;> [exists q'; exists p'] <;> grind [cases Tr, Tr.pre, PreBisim]
+    constructor <;> intro _ _ <;> [exists q'; exists p'] <;> grind [cases Tr]
   case bisim hbis =>
     constructor
     case left =>
@@ -291,14 +291,14 @@ theorem bisimilarity_congr_pre :
       obtain ⟨_, hr, hb⟩ := hbis
       obtain ⟨s2', _⟩ := hb.follow_fst hr htr
       exists s2'
-      grind [PreBisim, Bisimilarity.largest_bisimulation]
+      grind [Bisimilarity.largest_bisimulation]
     case right =>
       intro s2' htr
       obtain ⟨_, hr, hb⟩ := hbis
       have ⟨_, hb2⟩ := hb hr μ'
       obtain ⟨s1', _⟩ := hb2 _ htr
       exists s1'
-      grind [PreBisim, Bisimilarity.largest_bisimulation]
+      grind [Bisimilarity.largest_bisimulation]
 
 @[scoped grind]
 private inductive ResBisim : (Process Name Constant) → (Process Name Constant) → Prop where
@@ -322,14 +322,14 @@ theorem bisimilarity_congr_res :
     obtain ⟨q', _⟩ := Bisimilarity.is_bisimulation.follow_fst h htr
     exists res a q'
     unfold lts at *
-    grind [Tr]
+    grind
   case right =>
     intro s2' htr
     cases htr with | res _ _ htr =>
     obtain ⟨p', _⟩ := Bisimilarity.is_bisimulation.follow_snd h htr
     exists res a p'
     unfold lts at *
-    grind [Tr]
+    grind
 
 private inductive ChoiceBisim : (Process Name Constant) → (Process Name Constant) → Prop where
 | choice : (p ~[lts (defs := defs)] q) → ChoiceBisim (choice p r) (choice q r)
@@ -423,14 +423,14 @@ theorem bisimilarity_congr_par :
       case parL p' htr =>
         obtain ⟨q', _⟩ := hb.follow_fst hr htr
         exists par q' r
-        grind [Tr.parL]
+        grind
       case parR r' htr =>
         exists par q r'
-        grind [Tr.parR]
+        grind
       case com r' _ htrp _ =>
         obtain ⟨q', _⟩ := hb.follow_fst hr htrp
         exists par q' r'
-        grind [Tr.com]
+        grind
   case right =>
     intro s2' htr
     cases r
@@ -442,14 +442,14 @@ theorem bisimilarity_congr_par :
       case parL htr =>
         obtain ⟨p', _⟩ := hb.follow_snd hr htr
         exists par p' r
-        grind [Tr.parL]
+        grind
       case parR _ _ r' htr =>
         exists par p r'
-        grind [Tr.parR]
+        grind
       case com r' hco htrq htrr =>
         obtain ⟨q', _⟩ := hb.follow_snd hr htrq
         exists par q' r'
-        grind [Tr.com]
+        grind
 
 /-- Bisimilarity is a congruence in CCS. -/
 theorem bisimilarity_congr

From e796f9c4f54f8d5f3aece0b742f7fb63ff1fbea2 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 26 Oct 2025 09:20:17 -0400
Subject: [PATCH 03/12] unused cases

---
 Cslib/Languages/CCS/BehaviouralTheory.lean | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean
index 89b4c706..c0634872 100644
--- a/Cslib/Languages/CCS/BehaviouralTheory.lean
+++ b/Cslib/Languages/CCS/BehaviouralTheory.lean
@@ -45,8 +45,7 @@ theorem bisimilarity_par_nil : (par p nil) ~[lts (defs := defs)] p := by
   constructor; constructor
   intro s1 s2 hr μ
   constructor
-  case left =>
-    grind [cases Tr]
+  case left => grind
   case right =>
     intro s2' htr
     exists par s2' nil
@@ -178,7 +177,7 @@ theorem bisimilarity_choice_nil : (choice p nil) ~[lts (defs := defs)] p := by
   apply And.intro <;> cases hr
   case left.nil =>
     unfold lts
-    grind [cases Tr, ChoiceNil]
+    grind [ChoiceNil]
   case right.nil =>
     intro s2' htr
     exists s2'
@@ -283,7 +282,7 @@ theorem bisimilarity_congr_pre :
   cases hr
   case pre p' q' μ hbis =>
     unfold lts
-    constructor <;> intro _ _ <;> [exists q'; exists p'] <;> grind [cases Tr]
+    constructor <;> intro _ _ <;> [exists q'; exists p'] <;> grind
   case bisim hbis =>
     constructor
     case left =>

From dec5954feb17b4bbf5ec35f53cb51f19b9c2b5fd Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 26 Oct 2025 09:24:37 -0400
Subject: [PATCH 04/12] style

---
 Cslib/Languages/CCS/BehaviouralTheory.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean
index c0634872..1cfcb7c3 100644
--- a/Cslib/Languages/CCS/BehaviouralTheory.lean
+++ b/Cslib/Languages/CCS/BehaviouralTheory.lean
@@ -455,7 +455,7 @@ theorem bisimilarity_congr
   (c : Context Name Constant) (p q : Process Name Constant) (h : p ~[lts (defs := defs)] q) :
   (c.fill p) ~[lts (defs := defs)] (c.fill q) := by
   induction c with
-  | parR r c ih =>
+  | parR r c _ =>
     calc
       _ ~[lts (defs := defs)] (c.fill p |>.par r)  := by grind
       _ ~[lts (defs := defs)] (c.fill q |>.par r)  := by grind [bisimilarity_congr_par]

From 2ea292d412b57809424bfd153260671a64d01acf Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 26 Oct 2025 09:27:56 -0400
Subject: [PATCH 05/12] extra parens

---
 Cslib/Languages/CCS/BehaviouralTheory.lean | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean
index 1cfcb7c3..1c80bcd1 100644
--- a/Cslib/Languages/CCS/BehaviouralTheory.lean
+++ b/Cslib/Languages/CCS/BehaviouralTheory.lean
@@ -34,7 +34,7 @@ namespace CCS
 attribute [local grind] Tr
 
 @[scoped grind]
-private inductive ParNil : (Process Name Constant) → (Process Name Constant) → Prop where
+private inductive ParNil : Process Name Constant → Process Name Constant → Prop where
 | parNil : ParNil (par p nil) p
 
 /-- P | 𝟎 ~ P -/
@@ -52,7 +52,7 @@ theorem bisimilarity_par_nil : (par p nil) ~[lts (defs := defs)] p := by
     grind
 
 @[scoped grind]
-private inductive ParComm : (Process Name Constant) → (Process Name Constant) → Prop where
+private inductive ParComm : Process Name Constant → Process Name Constant → Prop where
 | parComm : ParComm (par p q) (par q p)
 
 /-- P | Q ~ Q | P -/
@@ -100,7 +100,7 @@ theorem bisimilarity_nil_par : (par nil p) ~[lts (defs := defs)] p :=
     _ ~[lts (defs := defs)] p := by simp
 
 @[scoped grind]
-private inductive ParAssoc : (Process Name Constant) → (Process Name Constant) → Prop where
+private inductive ParAssoc : Process Name Constant → Process Name Constant → Prop where
   | assoc : ParAssoc (par p (par q r)) (par (par p q) r)
   | id : ParAssoc p p
 
@@ -166,7 +166,7 @@ theorem bisimilarity_par_assoc :
       case com => grind
   all_goals grind
 
-private inductive ChoiceNil : (Process Name Constant) → (Process Name Constant) → Prop where
+private inductive ChoiceNil : Process Name Constant → Process Name Constant → Prop where
   | nil : ChoiceNil (choice p nil) p
   | id : ChoiceNil p p
 
@@ -188,7 +188,7 @@ theorem bisimilarity_choice_nil : (choice p nil) ~[lts (defs := defs)] p := by
   all_goals grind [ChoiceNil]
 
 @[scoped grind]
-private inductive ChoiceIdem : (Process Name Constant) → (Process Name Constant) → Prop where
+private inductive ChoiceIdem : Process Name Constant → Process Name Constant → Prop where
   | idem : ChoiceIdem (choice p p) p
   | id : ChoiceIdem p p
 
@@ -207,7 +207,7 @@ theorem bisimilarity_choice_idem :
       grind
     all_goals grind
 
-private inductive ChoiceComm : (Process Name Constant) → (Process Name Constant) → Prop where
+private inductive ChoiceComm : Process Name Constant → Process Name Constant → Prop where
   | choiceComm : ChoiceComm (choice p q) (choice q p)
   | bisim : (p ~[lts (defs := defs)] q) → ChoiceComm p q
 
@@ -236,7 +236,7 @@ theorem bisimilarity_choice_comm : (choice p q) ~[lts (defs := defs)] (choice q
   case bisim h =>
     grind [ChoiceComm]
 
-private inductive ChoiceAssoc : (Process Name Constant) → (Process Name Constant) → Prop where
+private inductive ChoiceAssoc : Process Name Constant → Process Name Constant → Prop where
   | assoc : ChoiceAssoc (choice p (choice q r)) (choice (choice p q) r)
   | id : ChoiceAssoc p p
 
@@ -267,7 +267,7 @@ theorem bisimilarity_choice_assoc :
   all_goals grind [ChoiceAssoc.id]
 
 @[scoped grind]
-private inductive PreBisim : (Process Name Constant) → (Process Name Constant) → Prop where
+private inductive PreBisim : Process Name Constant → Process Name Constant → Prop where
 | pre : (p ~[lts (defs := defs)] q) → PreBisim (pre μ p) (pre μ q)
 | bisim : (p ~[lts (defs := defs)] q) → PreBisim p q
 
@@ -300,7 +300,7 @@ theorem bisimilarity_congr_pre :
       grind [Bisimilarity.largest_bisimulation]
 
 @[scoped grind]
-private inductive ResBisim : (Process Name Constant) → (Process Name Constant) → Prop where
+private inductive ResBisim : Process Name Constant → Process Name Constant → Prop where
 | res : (p ~[lts (defs := defs)] q) → ResBisim (res a p) (res a q)
 -- | bisim : (p ~[lts (defs := defs)] q) → ResBisim p q
 
@@ -330,7 +330,7 @@ theorem bisimilarity_congr_res :
     unfold lts at *
     grind
 
-private inductive ChoiceBisim : (Process Name Constant) → (Process Name Constant) → Prop where
+private inductive ChoiceBisim : Process Name Constant → Process Name Constant → Prop where
 | choice : (p ~[lts (defs := defs)] q) → ChoiceBisim (choice p r) (choice q r)
 | bisim : (p ~[lts (defs := defs)] q) → ChoiceBisim p q
 
@@ -399,7 +399,7 @@ theorem bisimilarity_congr_choice :
         apply Bisimilarity.largest_bisimulation hb hr1
 
 @[scoped grind]
-private inductive ParBisim : (Process Name Constant) → (Process Name Constant) → Prop where
+private inductive ParBisim : Process Name Constant → Process Name Constant → Prop where
 | par : (p ~[lts (defs := defs)] q) → ParBisim (par p r) (par q r)
 
 /-- P ~ Q → P | R ~ Q | R -/

From b4d42f8e8d953c480f96d8da37e4f2d65ed1ea5d Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 26 Oct 2025 09:28:52 -0400
Subject: [PATCH 06/12] one more paren

---
 Cslib/Languages/CCS/BehaviouralTheory.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean
index 1c80bcd1..7f354de6 100644
--- a/Cslib/Languages/CCS/BehaviouralTheory.lean
+++ b/Cslib/Languages/CCS/BehaviouralTheory.lean
@@ -25,7 +25,7 @@ namespace Cslib
 
 section CCS.BehaviouralTheory
 
-variable {Name : Type u} {Constant : Type v} {defs : Constant → (CCS.Process Name Constant) → Prop}
+variable {Name : Type u} {Constant : Type v} {defs : Constant → CCS.Process Name Constant → Prop}
 
 open CCS CCS.Process CCS.Act
 

From b20c5771acd982e211a8370b2735ce53934c5640 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 26 Oct 2025 09:40:48 -0400
Subject: [PATCH 07/12] defParComm

---
 Cslib/Languages/CCS/BehaviouralTheory.lean | 35 +++++-----------------
 1 file changed, 7 insertions(+), 28 deletions(-)

diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean
index 7f354de6..e12cf35b 100644
--- a/Cslib/Languages/CCS/BehaviouralTheory.lean
+++ b/Cslib/Languages/CCS/BehaviouralTheory.lean
@@ -55,6 +55,11 @@ theorem bisimilarity_par_nil : (par p nil) ~[lts (defs := defs)] p := by
 private inductive ParComm : Process Name Constant → Process Name Constant → Prop where
 | parComm : ParComm (par p q) (par q p)
 
+@[scoped grind]
+def defParComm : Process Name Constant → Process Name Constant
+| par p q => par q p
+| _ => nil
+
 /-- P | Q ~ Q | P -/
 @[scoped grind .]
 theorem bisimilarity_par_comm : (par p q) ~[lts (defs := defs)] (par q p) := by
@@ -62,35 +67,9 @@ theorem bisimilarity_par_comm : (par p q) ~[lts (defs := defs)] (par q p) := by
   constructor
   case left => constructor
   case right =>
-    intro s1 s2 hr μ
-    cases hr
+    intro _ _ _ _
     unfold lts at *
-    case parComm p q =>
-      constructor
-      case left =>
-        intro t htr
-        cases htr
-        case parL p' htr' =>
-          exists par q p'
-          grind
-        case parR q' htr' =>
-          exists par q' p
-          grind
-        case com μ p' μ' q' hco htrp htrq =>
-          exists par q' p'
-          grind
-      case right =>
-        intro t htr
-        cases htr
-        case parL q' htr' =>
-          exists par p q'
-          grind
-        case parR p' htr' =>
-          exists par p' q
-          grind
-        case com μ p' μ' q' hco htrp htrq =>
-          exists par q' p'
-          grind
+    split_ands <;> intro p _ <;> exists defParComm p <;> grind
 
 /-- 𝟎 | P ~ P -/
 @[simp, scoped grind .]

From d9a297367ca7478b9937bfeb94c358882182c9b6 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 26 Oct 2025 15:26:19 -0400
Subject: [PATCH 08/12] style

---
 Cslib/Languages/CCS/BehaviouralTheory.lean | 11 ++++-------
 1 file changed, 4 insertions(+), 7 deletions(-)

diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean
index e12cf35b..24c52ce6 100644
--- a/Cslib/Languages/CCS/BehaviouralTheory.lean
+++ b/Cslib/Languages/CCS/BehaviouralTheory.lean
@@ -63,13 +63,10 @@ def defParComm : Process Name Constant → Process Name Constant
 /-- P | Q ~ Q | P -/
 @[scoped grind .]
 theorem bisimilarity_par_comm : (par p q) ~[lts (defs := defs)] (par q p) := by
-  exists ParComm
-  constructor
-  case left => constructor
-  case right =>
-    intro _ _ _ _
-    unfold lts at *
-    split_ands <;> intro p _ <;> exists defParComm p <;> grind
+  use ParComm, ParComm.parComm
+  intro _ _ _ _
+  unfold lts at *
+  split_ands <;> intro p _ <;> exists defParComm p <;> grind
 
 /-- 𝟎 | P ~ P -/
 @[simp, scoped grind .]

From 9b7f360cad735947902a428c7bf86d7d1cea5147 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Sun, 26 Oct 2025 16:02:48 -0400
Subject: [PATCH 09/12] style

---
 Cslib/Languages/CCS/BehaviouralTheory.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean
index 24c52ce6..00c77b28 100644
--- a/Cslib/Languages/CCS/BehaviouralTheory.lean
+++ b/Cslib/Languages/CCS/BehaviouralTheory.lean
@@ -41,9 +41,8 @@ private inductive ParNil : Process Name Constant → Process Name Constant → P
 @[simp, scoped grind .]
 theorem bisimilarity_par_nil : (par p nil) ~[lts (defs := defs)] p := by
   unfold lts at *
-  exists ParNil
-  constructor; constructor
-  intro s1 s2 hr μ
+  exists ParNil, .parNil
+  intro _ _ _ _
   constructor
   case left => grind
   case right =>

From 3b8331dd4fef2a1620ec805cbe29ef9450be0ab3 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 27 Oct 2025 03:47:51 -0400
Subject: [PATCH 10/12] mergeWithGrind linter

---
 lakefile.toml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/lakefile.toml b/lakefile.toml
index 63c88bda..b6e6928d 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -6,6 +6,7 @@ testDriver = "CslibTests"
 [leanOptions]
 weak.linter.mathlibStandardSet = true
 weak.linter.flexible = true
+weak.linter.tacticAnalysis.mergeWithGrind = true
 # The next three linters are provided by Mathlib, but don't work here.
 # This should be fixed, see discussion at https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/weak.2Elinter.2EmathlibStandardSet.20and.20lint-style-action/with/544726745
 weak.linter.pythonStyle = false

From 0da1f595081a00994c868c30f0764e4dfd6a0c92 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 27 Oct 2025 15:34:19 -0400
Subject: [PATCH 11/12] inline defParComm

---
 Cslib/Languages/CCS/BehaviouralTheory.lean | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean
index 00c77b28..4c415205 100644
--- a/Cslib/Languages/CCS/BehaviouralTheory.lean
+++ b/Cslib/Languages/CCS/BehaviouralTheory.lean
@@ -54,14 +54,12 @@ theorem bisimilarity_par_nil : (par p nil) ~[lts (defs := defs)] p := by
 private inductive ParComm : Process Name Constant → Process Name Constant → Prop where
 | parComm : ParComm (par p q) (par q p)
 
-@[scoped grind]
-def defParComm : Process Name Constant → Process Name Constant
-| par p q => par q p
-| _ => nil
-
 /-- P | Q ~ Q | P -/
 @[scoped grind .]
 theorem bisimilarity_par_comm : (par p q) ~[lts (defs := defs)] (par q p) := by
+  let defParComm : Process Name Constant → Process Name Constant
+    | par p q => par q p
+    | _ => nil
   use ParComm, ParComm.parComm
   intro _ _ _ _
   unfold lts at *

From b1b136a6b98cc727dc86e0c5d5294cdbe9db3005 Mon Sep 17 00:00:00 2001
From: Chris Henson <chrishenson.net@gmail.com>
Date: Mon, 27 Oct 2025 15:43:48 -0400
Subject: [PATCH 12/12] make grind annotations local for private inductives

---
 Cslib/Languages/CCS/BehaviouralTheory.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean
index 4c415205..fa5e7a6e 100644
--- a/Cslib/Languages/CCS/BehaviouralTheory.lean
+++ b/Cslib/Languages/CCS/BehaviouralTheory.lean
@@ -33,7 +33,7 @@ namespace CCS
 
 attribute [local grind] Tr
 
-@[scoped grind]
+@[local grind]
 private inductive ParNil : Process Name Constant → Process Name Constant → Prop where
 | parNil : ParNil (par p nil) p
 
@@ -50,7 +50,7 @@ theorem bisimilarity_par_nil : (par p nil) ~[lts (defs := defs)] p := by
     exists par s2' nil
     grind
 
-@[scoped grind]
+@[local grind]
 private inductive ParComm : Process Name Constant → Process Name Constant → Prop where
 | parComm : ParComm (par p q) (par q p)
 
@@ -72,7 +72,7 @@ theorem bisimilarity_nil_par : (par nil p) ~[lts (defs := defs)] p :=
     (par nil p) ~[lts (defs := defs)] (par p nil) := by grind
     _ ~[lts (defs := defs)] p := by simp
 
-@[scoped grind]
+@[local grind]
 private inductive ParAssoc : Process Name Constant → Process Name Constant → Prop where
   | assoc : ParAssoc (par p (par q r)) (par (par p q) r)
   | id : ParAssoc p p
@@ -160,7 +160,7 @@ theorem bisimilarity_choice_nil : (choice p nil) ~[lts (defs := defs)] p := by
     · exact ChoiceNil.id
   all_goals grind [ChoiceNil]
 
-@[scoped grind]
+@[local grind]
 private inductive ChoiceIdem : Process Name Constant → Process Name Constant → Prop where
   | idem : ChoiceIdem (choice p p) p
   | id : ChoiceIdem p p
@@ -239,7 +239,7 @@ theorem bisimilarity_choice_assoc :
     case choiceR htr => apply Tr.choiceR; apply Tr.choiceR; assumption
   all_goals grind [ChoiceAssoc.id]
 
-@[scoped grind]
+@[local grind]
 private inductive PreBisim : Process Name Constant → Process Name Constant → Prop where
 | pre : (p ~[lts (defs := defs)] q) → PreBisim (pre μ p) (pre μ q)
 | bisim : (p ~[lts (defs := defs)] q) → PreBisim p q
@@ -272,7 +272,7 @@ theorem bisimilarity_congr_pre :
       exists s1'
       grind [Bisimilarity.largest_bisimulation]
 
-@[scoped grind]
+@[local grind]
 private inductive ResBisim : Process Name Constant → Process Name Constant → Prop where
 | res : (p ~[lts (defs := defs)] q) → ResBisim (res a p) (res a q)
 -- | bisim : (p ~[lts (defs := defs)] q) → ResBisim p q
@@ -371,7 +371,7 @@ theorem bisimilarity_congr_choice :
       · constructor
         apply Bisimilarity.largest_bisimulation hb hr1
 
-@[scoped grind]
+@[local grind]
 private inductive ParBisim : Process Name Constant → Process Name Constant → Prop where
 | par : (p ~[lts (defs := defs)] q) → ParBisim (par p r) (par q r)