leanprover-community · kim-em · Feb 25, 2024
diff --git a/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean b/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
@@ -535,7 +535,7 @@ theorem adjoin_toSubmodule (s : Set A) :
     (adjoin R s).toSubmodule = Submodule.span R (NonUnitalSubsemiring.closure s : Set A) :=
   rfl
 
-@[aesop safe 20 apply (rule_sets [SetLike])]
+@[aesop safe 20 apply (rule_sets := [SetLike])]
 theorem subset_adjoin {s : Set A} : s ⊆ adjoin R s :=
   NonUnitalSubsemiring.subset_closure.trans Submodule.subset_span
 

diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
@@ -104,7 +104,7 @@ variable (S : Subalgebra R A)
 instance instSMulMemClass : SMulMemClass (Subalgebra R A) R A where
   smul_mem {S} r x hx := (Algebra.smul_def r x).symm ▸ mul_mem (S.algebraMap_mem' r) hx
 
-@[aesop safe apply (rule_sets [SetLike])]
+@[aesop safe apply (rule_sets := [SetLike])]
 theorem _root_.algebraMap_mem {S R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A]
     [SetLike S A] [OneMemClass S A] [SMulMemClass S R A] (s : S) (r : R) :
     algebraMap R A r ∈ s :=

diff --git a/Mathlib/Algebra/Star/Basic.lean b/Mathlib/Algebra/Star/Basic.lean
@@ -65,7 +65,7 @@ class StarMemClass (S R : Type*) [Star R] [SetLike S R] : Prop where
 
 export StarMemClass (star_mem)
 
-attribute [aesop safe apply (rule_sets [SetLike])] star_mem
+attribute [aesop safe apply (rule_sets := [SetLike])] star_mem
 
 namespace StarMemClass
 

diff --git a/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean b/Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
@@ -633,7 +633,7 @@ theorem adjoin_toNonUnitalSubalgebra (s : Set A) :
     (adjoin R s).toNonUnitalSubalgebra = NonUnitalAlgebra.adjoin R (s ∪ star s) :=
   rfl
 
-@[aesop safe 20 apply (rule_sets [SetLike])]
+@[aesop safe 20 apply (rule_sets := [SetLike])]
 theorem subset_adjoin (s : Set A) : s ⊆ adjoin R s :=
   (Set.subset_union_left s (star s)).trans <| NonUnitalAlgebra.subset_adjoin R
 

diff --git a/Mathlib/Algebra/Star/SelfAdjoint.lean b/Mathlib/Algebra/Star/SelfAdjoint.lean
@@ -538,7 +538,7 @@ section SMul
 
 variable [Star R] [TrivialStar R] [AddCommGroup A] [StarAddMonoid A]
 
-@[aesop safe apply (rule_sets [SetLike])]
+@[aesop safe apply (rule_sets := [SetLike])]
 theorem smul_mem [Monoid R] [DistribMulAction R A] [StarModule R A] (r : R) {x : A}
     (h : x ∈ skewAdjoint A) : r • x ∈ skewAdjoint A := by
   rw [mem_iff, star_smul, star_trivial, mem_iff.mp h, smul_neg r]

diff --git a/Mathlib/Algebra/Star/Subalgebra.lean b/Mathlib/Algebra/Star/Subalgebra.lean
@@ -445,7 +445,7 @@ theorem adjoin_toSubalgebra (s : Set A) :
   rfl
 #align star_subalgebra.adjoin_to_subalgebra StarSubalgebra.adjoin_toSubalgebra
 
-@[aesop safe 20 apply (rule_sets [SetLike])]
+@[aesop safe 20 apply (rule_sets := [SetLike])]
 theorem subset_adjoin (s : Set A) : s ⊆ adjoin R s :=
   (Set.subset_union_left s (star s)).trans Algebra.subset_adjoin
 #align star_subalgebra.subset_adjoin StarSubalgebra.subset_adjoin

diff --git a/Mathlib/Analysis/Convex/Cone/Basic.lean b/Mathlib/Analysis/Convex/Cone/Basic.lean
@@ -95,7 +95,7 @@ theorem ext {S T : ConvexCone 𝕜 E} (h : ∀ x, x ∈ S ↔ x ∈ T) : S = T :
   SetLike.ext h
 #align convex_cone.ext ConvexCone.ext
 
-@[aesop safe apply (rule_sets [SetLike])]
+@[aesop safe apply (rule_sets := [SetLike])]
 theorem smul_mem {c : 𝕜} {x : E} (hc : 0 < c) (hx : x ∈ S) : c • x ∈ S :=
   S.smul_mem' hc hx
 #align convex_cone.smul_mem ConvexCone.smul_mem

diff --git a/Mathlib/CategoryTheory/Category/Basic.lean b/Mathlib/CategoryTheory/Category/Basic.lean
@@ -118,15 +118,15 @@ macro (name := aesop_cat) "aesop_cat" c:Aesop.tactic_clause* : tactic =>
 `(tactic|
   aesop $c* (config := { introsTransparency? := some .default, terminal := true })
             (simp_config := { decide := true })
-  (rule_sets [$(Lean.mkIdent `CategoryTheory):ident]))
+  (rule_sets := [$(Lean.mkIdent `CategoryTheory):ident]))
 
 /--
 We also use `aesop_cat?` to pass along a `Try this` suggestion when using `aesop_cat`
 -/
 macro (name := aesop_cat?) "aesop_cat?" c:Aesop.tactic_clause* : tactic =>
 `(tactic|
   aesop? $c* (config := { introsTransparency? := some .default, terminal := true })
-  (rule_sets [$(Lean.mkIdent `CategoryTheory):ident]))
+  (rule_sets := [$(Lean.mkIdent `CategoryTheory):ident]))
 /--
 A variant of `aesop_cat` which does not fail when it is unable to solve the
 goal. Use this only for exploration! Nonterminal `aesop` is even worse than
@@ -135,19 +135,19 @@ nonterminal `simp`.
 macro (name := aesop_cat_nonterminal) "aesop_cat_nonterminal" c:Aesop.tactic_clause* : tactic =>
   `(tactic|
     aesop $c* (config := { introsTransparency? := some .default, warnOnNonterminal := false })
-    (rule_sets [$(Lean.mkIdent `CategoryTheory):ident]))
+    (rule_sets := [$(Lean.mkIdent `CategoryTheory):ident]))
 
 
 -- We turn on `ext` inside `aesop_cat`.
-attribute [aesop safe tactic (rule_sets [CategoryTheory])] Std.Tactic.Ext.extCore'
+attribute [aesop safe tactic (rule_sets := [CategoryTheory])] Std.Tactic.Ext.extCore'
 
 -- We turn on the mathlib version of `rfl` inside `aesop_cat`.
-attribute [aesop safe tactic (rule_sets [CategoryTheory])] Mathlib.Tactic.rflTac
+attribute [aesop safe tactic (rule_sets := [CategoryTheory])] Mathlib.Tactic.rflTac
 
 -- Porting note:
 -- Workaround for issue discussed at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Failure.20of.20TC.20search.20in.20.60simp.60.20with.20.60etaExperiment.60.2E
 -- now that etaExperiment is always on.
-attribute [aesop safe (rule_sets [CategoryTheory])] Subsingleton.elim
+attribute [aesop safe (rule_sets := [CategoryTheory])] Subsingleton.elim
 
 /-- The typeclass `Category C` describes morphisms associated to objects of type `C`.
 The universe levels of the objects and morphisms are unconstrained, and will often need to be

diff --git a/Mathlib/CategoryTheory/Category/Pairwise.lean b/Mathlib/CategoryTheory/Category/Pairwise.lean
@@ -89,7 +89,7 @@ open Lean Elab Tactic in
 def pairwiseCases : TacticM Unit := do
   evalTactic (← `(tactic| casesm* (_ : Pairwise _) ⟶ (_ : Pairwise _)))
 
-attribute [local aesop safe tactic (rule_sets [CategoryTheory])] pairwiseCases in
+attribute [local aesop safe tactic (rule_sets := [CategoryTheory])] pairwiseCases in
 instance : Category (Pairwise ι) where
   Hom := Hom
   id := id

diff --git a/Mathlib/CategoryTheory/DiscreteCategory.lean b/Mathlib/CategoryTheory/DiscreteCategory.lean
@@ -45,7 +45,7 @@ universe v₁ v₂ v₃ u₁ u₁' u₂ u₃
 /-- A wrapper for promoting any type to a category,
 with the only morphisms being equalities.
 -/
-@[ext, aesop safe cases (rule_sets [CategoryTheory])]
+@[ext, aesop safe cases (rule_sets := [CategoryTheory])]
 structure Discrete (α : Type u₁) where
   /-- A wrapper for promoting any type to a category,
   with the only morphisms being equalities. -/
@@ -110,7 +110,7 @@ open Lean Elab Tactic in
 /--
 Use:
 ```
-attribute [local aesop safe tactic (rule_sets [CategoryTheory])]
+attribute [local aesop safe tactic (rule_sets := [CategoryTheory])]
   CategoryTheory.Discrete.discreteCases
 ```
 to locally gives `aesop_cat` the ability to call `cases` on
@@ -121,9 +121,9 @@ def discreteCases : TacticM Unit := do
 
 -- Porting note:
 -- investigate turning on either
--- `attribute [aesop safe cases (rule_sets [CategoryTheory])] Discrete`
+-- `attribute [aesop safe cases (rule_sets := [CategoryTheory])] Discrete`
 -- or
--- `attribute [aesop safe tactic (rule_sets [CategoryTheory])] discreteCases`
+-- `attribute [aesop safe tactic (rule_sets := [CategoryTheory])] discreteCases`
 -- globally.
 
 instance [Unique α] : Unique (Discrete α) :=
@@ -166,7 +166,7 @@ variable {C : Type u₂} [Category.{v₂} C]
 instance {I : Type u₁} {i j : Discrete I} (f : i ⟶ j) : IsIso f :=
   ⟨⟨Discrete.eqToHom (eq_of_hom f).symm, by aesop_cat⟩⟩
 
-attribute [local aesop safe tactic (rule_sets [CategoryTheory])]
+attribute [local aesop safe tactic (rule_sets := [CategoryTheory])]
   CategoryTheory.Discrete.discreteCases
 
 /-- Any function `I → C` gives a functor `Discrete I ⥤ C`.-/

diff --git a/Mathlib/CategoryTheory/EpiMono.lean b/Mathlib/CategoryTheory/EpiMono.lean
@@ -45,7 +45,7 @@ Every split monomorphism is a monomorphism.
 -/
 /- Porting note: @[nolint has_nonempty_instance] -/
 /- Porting note: `@[ext]` used to accept lemmas like this. Now we add an aesop rule -/
-@[aesop apply safe (rule_sets [CategoryTheory])]
+@[aesop apply safe (rule_sets := [CategoryTheory])]
 structure SplitMono {X Y : C} (f : X ⟶ Y) where
   /-- The map splitting `f` -/
   retraction : Y ⟶ X
@@ -75,7 +75,7 @@ Every split epimorphism is an epimorphism.
 -/
 /- Porting note: @[nolint has_nonempty_instance] -/
 /- Porting note: `@[ext]` used to accept lemmas like this. Now we add an aesop rule -/
-@[aesop apply safe (rule_sets [CategoryTheory])]
+@[aesop apply safe (rule_sets := [CategoryTheory])]
 structure SplitEpi {X Y : C} (f : X ⟶ Y) where
   /-- The map splitting `f` -/
   section_ : Y ⟶ X

diff --git a/Mathlib/CategoryTheory/Iso.lean b/Mathlib/CategoryTheory/Iso.lean
@@ -340,7 +340,7 @@ instance (priority := 100) mono_of_iso (f : X ⟶ Y) [IsIso f] : Mono f where
 #align category_theory.is_iso.mono_of_iso CategoryTheory.IsIso.mono_of_iso
 
 -- Porting note: `@[ext]` used to accept lemmas like this. Now we add an aesop rule
-@[aesop apply safe (rule_sets [CategoryTheory])]
+@[aesop apply safe (rule_sets := [CategoryTheory])]
 theorem inv_eq_of_hom_inv_id {f : X ⟶ Y} [IsIso f] {g : Y ⟶ X} (hom_inv_id : f ≫ g = 𝟙 X) :
     inv f = g := by
   apply (cancel_epi f).mp
@@ -354,7 +354,7 @@ theorem inv_eq_of_inv_hom_id {f : X ⟶ Y} [IsIso f] {g : Y ⟶ X} (inv_hom_id :
 #align category_theory.is_iso.inv_eq_of_inv_hom_id CategoryTheory.IsIso.inv_eq_of_inv_hom_id
 
 -- Porting note: `@[ext]` used to accept lemmas like this.
-@[aesop apply safe (rule_sets [CategoryTheory])]
+@[aesop apply safe (rule_sets := [CategoryTheory])]
 theorem eq_inv_of_hom_inv_id {f : X ⟶ Y} [IsIso f] {g : Y ⟶ X} (hom_inv_id : f ≫ g = 𝟙 X) :
     g = inv f :=
   (inv_eq_of_hom_inv_id hom_inv_id).symm
@@ -506,13 +506,13 @@ theorem isIso_of_comp_hom_eq_id (g : X ⟶ Y) [IsIso g] {f : Y ⟶ X} (h : f ≫
 namespace Iso
 
 -- Porting note: `@[ext]` used to accept lemmas like this.
-@[aesop apply safe (rule_sets [CategoryTheory])]
+@[aesop apply safe (rule_sets := [CategoryTheory])]
 theorem inv_ext {f : X ≅ Y} {g : Y ⟶ X} (hom_inv_id : f.hom ≫ g = 𝟙 X) : f.inv = g :=
   ((hom_comp_eq_id f).1 hom_inv_id).symm
 #align category_theory.iso.inv_ext CategoryTheory.Iso.inv_ext
 
 -- Porting note: `@[ext]` used to accept lemmas like this.
-@[aesop apply safe (rule_sets [CategoryTheory])]
+@[aesop apply safe (rule_sets := [CategoryTheory])]
 theorem inv_ext' {f : X ≅ Y} {g : Y ⟶ X} (hom_inv_id : f.hom ≫ g = 𝟙 X) : g = f.inv :=
   (hom_comp_eq_id f).1 hom_inv_id
 #align category_theory.iso.inv_ext' CategoryTheory.Iso.inv_ext'

diff --git a/Mathlib/CategoryTheory/Limits/Cones.lean b/Mathlib/CategoryTheory/Limits/Cones.lean
@@ -315,7 +315,7 @@ namespace Cones
   isomorphism between their vertices which commutes with the cone
   maps. -/
 -- Porting note: `@[ext]` used to accept lemmas like this. Now we add an aesop rule
-@[aesop apply safe (rule_sets [CategoryTheory]), simps]
+@[aesop apply safe (rule_sets := [CategoryTheory]), simps]
 def ext {c c' : Cone F} (φ : c.pt ≅ c'.pt)
     (w : ∀ j, c.π.app j = φ.hom ≫ c'.π.app j := by aesop_cat) : c ≅ c' where
   hom := { hom := φ.hom }
@@ -514,7 +514,7 @@ namespace Cocones
   isomorphism between their vertices which commutes with the cocone
   maps. -/
 -- Porting note: `@[ext]` used to accept lemmas like this. Now we add an aesop rule
-@[aesop apply safe (rule_sets [CategoryTheory]), simps]
+@[aesop apply safe (rule_sets := [CategoryTheory]), simps]
 def ext {c c' : Cocone F} (φ : c.pt ≅ c'.pt)
     (w : ∀ j, c.ι.app j ≫ φ.hom = c'.ι.app j := by aesop_cat) : c ≅ c' where
   hom := { hom := φ.hom }

diff --git a/Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean b/Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean
@@ -75,7 +75,7 @@ def conesEquivInverse (B : C) {J : Type w} (F : Discrete J ⥤ Over B) :
 
 -- Porting note: this should help with the additional `naturality` proof we now have to give in
 -- `conesEquivFunctor`, but doesn't.
--- attribute [local aesop safe cases (rule_sets [CategoryTheory])] Discrete
+-- attribute [local aesop safe cases (rule_sets := [CategoryTheory])] Discrete
 
 /-- (Impl) A preliminary definition to avoid timeouts. -/
 @[simps]
@@ -92,7 +92,7 @@ def conesEquivFunctor (B : C) {J : Type w} (F : Discrete J ⥤ Over B) :
 
 -- Porting note: unfortunately `aesop` can't cope with a `cases` rule here for the type synonym
 -- `WidePullbackShape`.
--- attribute [local aesop safe cases (rule_sets [CategoryTheory])] WidePullbackShape
+-- attribute [local aesop safe cases (rule_sets := [CategoryTheory])] WidePullbackShape
 -- If this worked we could avoid the `rintro` in `conesEquivUnitIso`.
 
 /-- (Impl) A preliminary definition to avoid timeouts. -/

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
@@ -147,7 +147,7 @@ section
 variable {F G : Discrete WalkingPair ⥤ C} (f : F.obj ⟨left⟩ ⟶ G.obj ⟨left⟩)
   (g : F.obj ⟨right⟩ ⟶ G.obj ⟨right⟩)
 
-attribute [local aesop safe tactic (rule_sets [CategoryTheory])]
+attribute [local aesop safe tactic (rule_sets := [CategoryTheory])]
   CategoryTheory.Discrete.discreteCases
 
 /-- The natural transformation between two functors out of the
@@ -290,10 +290,10 @@ variable {X Y : C}
 
 section
 
-attribute [local aesop safe tactic (rule_sets [CategoryTheory])]
+attribute [local aesop safe tactic (rule_sets := [CategoryTheory])]
   CategoryTheory.Discrete.discreteCases
 -- Porting note: would it be okay to use this more generally?
-attribute [local aesop safe cases (rule_sets [CategoryTheory])] Eq
+attribute [local aesop safe cases (rule_sets := [CategoryTheory])] Eq
 
 /-- A binary fan with vertex `P` consists of the two projections `π₁ : P ⟶ X` and `π₂ : P ⟶ Y`. -/
 @[simps pt]

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
@@ -130,7 +130,7 @@ namespace Bicones
   isomorphism between their vertices which commutes with the cocone
   maps. -/
 -- Porting note: `@[ext]` used to accept lemmas like this. Now we add an aesop rule
-@[aesop apply safe (rule_sets [CategoryTheory]), simps]
+@[aesop apply safe (rule_sets := [CategoryTheory]), simps]
 def ext {c c' : Bicone F} (φ : c.pt ≅ c'.pt)
     (wι : ∀ j, c.ι j ≫ φ.hom = c'.ι j := by aesop_cat)
     (wπ : ∀ j, φ.hom ≫ c'.π j = c.π j := by aesop_cat) : c ≅ c' where
@@ -161,10 +161,10 @@ end Bicones
 
 namespace Bicone
 
-attribute [local aesop safe tactic (rule_sets [CategoryTheory])]
+attribute [local aesop safe tactic (rule_sets := [CategoryTheory])]
   CategoryTheory.Discrete.discreteCases
 -- Porting note: would it be okay to use this more generally?
-attribute [local aesop safe cases (rule_sets [CategoryTheory])] Eq
+attribute [local aesop safe cases (rule_sets := [CategoryTheory])] Eq
 
 /-- Extract the cone from a bicone. -/
 def toConeFunctor : Bicone F ⥤ Cone (Discrete.functor F) where

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean b/Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
@@ -90,7 +90,7 @@ def evalCasesBash : TacticM Unit := do
     (← `(tactic| casesm* WidePullbackShape _,
       (_: WidePullbackShape _) ⟶ (_ : WidePullbackShape _) ))
 
-attribute [local aesop safe tactic (rule_sets [CategoryTheory])] evalCasesBash
+attribute [local aesop safe tactic (rule_sets := [CategoryTheory])] evalCasesBash
 
 instance subsingleton_hom : Quiver.IsThin (WidePullbackShape J) := fun _ _ => by
   constructor
@@ -206,7 +206,7 @@ def evalCasesBash' : TacticM Unit := do
     (← `(tactic| casesm* WidePushoutShape _,
       (_: WidePushoutShape _) ⟶ (_ : WidePushoutShape _) ))
 
-attribute [local aesop safe tactic (rule_sets [CategoryTheory])] evalCasesBash'
+attribute [local aesop safe tactic (rule_sets := [CategoryTheory])] evalCasesBash'
 
 instance subsingleton_hom : Quiver.IsThin (WidePushoutShape J) := fun _ _ => by
   constructor

diff --git a/Mathlib/CategoryTheory/Monoidal/Mon_.lean b/Mathlib/CategoryTheory/Monoidal/Mon_.lean
@@ -277,7 +277,7 @@ def monToLaxMonoidal : Mon_ C ⥤ LaxMonoidalFunctor (Discrete PUnit.{u + 1}) C
       tensor := fun _ _ => f.mul_hom }
 #align Mon_.equiv_lax_monoidal_functor_punit.Mon_to_lax_monoidal Mon_.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal
 
-attribute [local aesop safe tactic (rule_sets [CategoryTheory])]
+attribute [local aesop safe tactic (rule_sets := [CategoryTheory])]
   CategoryTheory.Discrete.discreteCases
 
 attribute [local simp] eqToIso_map

diff --git a/Mathlib/CategoryTheory/Sums/Basic.lean b/Mathlib/CategoryTheory/Sums/Basic.lean
@@ -58,11 +58,11 @@ instance sum : Category.{v₁} (Sum C D) where
     | inr X, inr Y, inr Z, inr W => Category.assoc f g h
 #align category_theory.sum CategoryTheory.sum
 
-@[aesop norm -10 destruct (rule_sets [CategoryTheory])]
+@[aesop norm -10 destruct (rule_sets := [CategoryTheory])]
 theorem hom_inl_inr_false {X : C} {Y : D} (f : Sum.inl X ⟶ Sum.inr Y) : False := by
   cases f
 
-@[aesop norm -10 destruct (rule_sets [CategoryTheory])]
+@[aesop norm -10 destruct (rule_sets := [CategoryTheory])]
 theorem hom_inr_inl_false {X : C} {Y : D} (f : Sum.inr X ⟶ Sum.inl Y) : False := by
   cases f
 

diff --git a/Mathlib/CategoryTheory/WithTerminal.lean b/Mathlib/CategoryTheory/WithTerminal.lean
@@ -51,7 +51,7 @@ inductive WithTerminal : Type u
   deriving Inhabited
 #align category_theory.with_terminal CategoryTheory.WithTerminal
 
-attribute [local aesop safe cases (rule_sets [CategoryTheory])] WithTerminal
+attribute [local aesop safe cases (rule_sets := [CategoryTheory])] WithTerminal
 
 /-- Formally adjoin an initial object to a category. -/
 inductive WithInitial : Type u
@@ -60,7 +60,7 @@ inductive WithInitial : Type u
   deriving Inhabited
 #align category_theory.with_initial CategoryTheory.WithInitial
 
-attribute [local aesop safe cases (rule_sets [CategoryTheory])] WithInitial
+attribute [local aesop safe cases (rule_sets := [CategoryTheory])] WithInitial
 
 namespace WithTerminal
 
@@ -114,7 +114,7 @@ def down {X Y : C} (f : of X ⟶ of Y) : X ⟶ Y := f
     down (f ≫ g) = down f ≫ down g :=
   rfl
 
-@[aesop safe destruct (rule_sets [CategoryTheory])]
+@[aesop safe destruct (rule_sets := [CategoryTheory])]
 lemma false_of_from_star {X : C} (f : star ⟶ of X) : False := (f : PEmpty).elim
 
 /-- The inclusion from `C` into `WithTerminal C`. -/
@@ -412,7 +412,7 @@ def down {X Y : C} (f : of X ⟶ of Y) : X ⟶ Y := f
     down (f ≫ g) = down f ≫ down g :=
   rfl
 
-@[aesop safe destruct (rule_sets [CategoryTheory])]
+@[aesop safe destruct (rule_sets := [CategoryTheory])]
 lemma false_of_to_star {X : C} (f : of X ⟶ star) : False := (f : PEmpty).elim
 
 /-- The inclusion of `C` into `WithInitial C`. -/