diff --git a/Cslib/Algorithms/CCS/VendingMachine.lean b/Cslib/Algorithms/CCS/VendingMachine.lean
index dc964d4ad..601d173b8 100644
--- a/Cslib/Algorithms/CCS/VendingMachine.lean
+++ b/Cslib/Algorithms/CCS/VendingMachine.lean
@@ -84,8 +84,7 @@ theorem vm_ltsD_ltsND_not_bisim : ¬(vm ~[ltsD, ltsND] vm) := by
   let p₁ := `(CCS| (Tea. const Constant.vm) + (Coffee. const Constant.vm))
   let q₁ := `(CCS| Tea. const Constant.vm)
   have ltsD_vm_deterministic : ltsD.DeterministicStateLabel vm Coin := by
-    intro _ _ htr₁ htr₂
-    grind [const_tr htr₁, const_tr htr₂]
+    grind
   have h : r p₁ q₁ :=
     match_deterministic
       hbisim hr
diff --git a/Cslib/Algorithms/Lean/Query/Sort/LowerBound.lean b/Cslib/Algorithms/Lean/Query/Sort/LowerBound.lean
index d514b7203..cf8dec5c6 100644
--- a/Cslib/Algorithms/Lean/Query/Sort/LowerBound.lean
+++ b/Cslib/Algorithms/Lean/Query/Sort/LowerBound.lean
@@ -53,8 +53,8 @@ private theorem finPrefix_injective (h : ↑n ≤ #α) :
   (finEmbedding h).injective.extend_of_disjoint Sum.inl_injective Sum.inr_injective
     Set.isCompl_range_inl_range_inr.disjoint
 
-/-- A total order on an type `α` with at least `n` elements, that orders `n` embedded elements
-    (via `finEmbedding) according to `σ⁻¹`, with embedded elements
+/-- A total order on a type `α` with at least `n` elements, that orders `n` embedded elements
+    (via `finEmbedding`) according to `σ⁻¹`, with embedded elements
     preceding all others, and a well-ordering among non-embedded elements. -/
 private noncomputable def PrefixPermOrder (h : ↑n ≤ #α)
     (σ : Equiv.Perm (Fin n)) : α → α → Prop :=
diff --git a/Cslib/Computability/Circuit/Full.lean b/Cslib/Computability/Circuit/Full.lean
index 20377cf48..9450d2041 100644
--- a/Cslib/Computability/Circuit/Full.lean
+++ b/Cslib/Computability/Circuit/Full.lean
@@ -124,8 +124,7 @@ private theorem exists_full_synthesis_finset [DecidableEq U]
     obtain ⟨a, ha⟩ := exists_full_synthesis_point (f point) default point
     obtain ⟨b, hb⟩ := ih
     have hstep := ha.full_binary hb (fun v acc => if v = default then acc else v)
-    use a + b + 1
-    grind only [= Finset.mem_insert]
+    grind
 
 private theorem fullInterpretation_isComplete_two [Finite U] :
     (fullInterpretation (k := 2) (Carrier := U)).IsComplete where