Replaced some cases instances with grind

InductiveVerification/Event.lean

@@ -11,10 +11,11 @@ inductive Event
 -- Define the `initState` function
 class HasInitState (α : Type) where
   initState : α → Set Msg
-
+  
 variable [ hasInitStateAgent : HasInitState Agent ]
   
 open HasInitState
+attribute [simp] initState
   
 -- Define the `bad` set
 abbrev DecidableMem ( A : Set Agent ) := (a : Agent) →  Decidable (a ∈ A)
@@ -27,8 +28,8 @@ class Bad where
 instance [Bad] : DecidableMem Bad.bad := Bad.decidableBad
 open Bad
 
--- attribute [simp] Spy_in_bad
--- attribute [simp] Server_not_bad
+attribute [simp, grind .] Spy_in_bad
+attribute [simp] Server_not_bad
 
 instance decidableAgentEq : DecidableEq Agent :=
   λ a b =>
@@ -60,9 +61,12 @@ def knows [Bad] : Agent → List Event → Set Msg
   if A = A' then insert X (knows A evs) else knows A evs
 | A, Event.Notes A' X :: evs =>
   if A = A' then insert X (knows A evs) else knows A evs
+  
+attribute [simp] knows
 
 -- Define the `spies` abbreviation
 abbrev spies (evs : List Event) [Bad] : Set Msg := knows Agent.Spy evs
+attribute [simp] spies
 
 -- Define the `used` function
 def used : List Event → Set Msg
@@ -172,6 +176,7 @@ lemma Notes_imp_knows_Spy [Bad] {A : Agent} {X : Msg} {evs : List Event} :
 
 -- Elimination rules: derive contradictions from old Says events containing
 -- items known to be fresh
+@[grind ., grind! .]
 lemma Says_imp_parts_knows_Spy [Bad] :
   ∀ {A B : Agent} {X : Msg} {evs : List Event},
     Event.Says A B X ∈ evs → X ∈ parts (knows Agent.Spy evs) := by
@@ -364,6 +369,7 @@ lemma knows_Spy_imp_Says_Notes_initState [Bad] {X : Msg} {evs : List Event} :
       · apply ih at h; aapply knows_Spy_imp_Says_Notes_initState_aux
 
 -- Parts of what the Spy knows are a subset of what is used
+@[grind! .]
 lemma parts_knows_Spy_subset_used [Bad] :
     parts (knows Agent.Spy evs) ⊆ used evs := by
   induction evs with