feat: allow several identifiers in assert_not_exists (leanprover-community#15994)

Align the `assert_not_exists` syntax to `assert_not_imported`: they now both allow several identifiers.



Co-authored-by: Jon Eugster <eugster.jon@gmail.com>

Author: adomani

Mathlib/Algebra/Algebra/Defs.lean

@@ -80,9 +80,7 @@ the second approach only when you need to weaken a condition on either `R` or `A
 
 -/
 
-assert_not_exists Field
-assert_not_exists Finset
-assert_not_exists Module.End
+assert_not_exists Field Finset Module.End
 
 universe u v w u₁ v₁
 

Mathlib/Algebra/Associated/Basic.lean

@@ -21,8 +21,7 @@ Then we show that the quotient type `Associates` is a monoid
 and prove basic properties of this quotient.
 -/
 
-assert_not_exists OrderedCommMonoid
-assert_not_exists Multiset
+assert_not_exists OrderedCommMonoid Multiset
 
 variable {M : Type*}
 

Mathlib/Algebra/BigOperators/Group/Finset.lean

@@ -38,9 +38,7 @@ See the documentation of `to_additive.attr` for more information.
 
 -- TODO
 -- assert_not_exists AddCommMonoidWithOne
-assert_not_exists MonoidWithZero
-assert_not_exists MulAction
-assert_not_exists OrderedCommMonoid
+assert_not_exists MonoidWithZero MulAction OrderedCommMonoid
 
 variable {ι κ α β γ : Type*}
 

Mathlib/Algebra/CharP/Basic.lean

@@ -19,8 +19,7 @@ imports of `CharP/Lemmas.lean`.
 As such, we can probably reorganize and find a better home for most of these lemmas.
 -/
 
-assert_not_exists Finset
-assert_not_exists TwoSidedIdeal
+assert_not_exists Finset TwoSidedIdeal
 
 open Set
 

Mathlib/Algebra/CharP/Defs.lean

@@ -19,8 +19,7 @@ import Mathlib.Data.Nat.Prime.Defs
     prime characteristic `p`)
 -/
 
-assert_not_exists Field
-assert_not_exists Finset
+assert_not_exists Field Finset
 
 open Set
 

Mathlib/Algebra/CharP/Lemmas.lean

@@ -12,9 +12,7 @@ import Mathlib.Data.Nat.Choose.Sum
 # Characteristic of semirings
 -/
 
-assert_not_exists Algebra
-assert_not_exists LinearMap
-assert_not_exists orderOf
+assert_not_exists Algebra LinearMap orderOf
 
 open Finset
 

Mathlib/Algebra/CharP/Two.lean

@@ -15,8 +15,7 @@ The lemmas in this file with a `_sq` suffix are just special cases of the `_pow_
 elsewhere, with a shorter name for ease of discovery, and no need for a `[Fact (Prime 2)]` argument.
 -/
 
-assert_not_exists Algebra
-assert_not_exists LinearMap
+assert_not_exists Algebra LinearMap
 
 variable {R ι : Type*}
 

Mathlib/Algebra/Group/Action/Opposite.lean

@@ -26,8 +26,7 @@ With `open scoped RightActions`, this provides:
 * `p <+ᵥ v` as an alias for `AddOpposite.op v +ᵥ p`
 -/
 
-assert_not_exists MonoidWithZero
-assert_not_exists Units
+assert_not_exists MonoidWithZero Units
 
 variable {M N α β : Type*}
 

Mathlib/Algebra/Group/Basic.lean

@@ -19,8 +19,7 @@ one-liners from the corresponding axioms. For the definitions of semigroups, mon
 `Algebra/Group/Defs.lean`.
 -/
 
-assert_not_exists MonoidWithZero
-assert_not_exists DenselyOrdered
+assert_not_exists MonoidWithZero DenselyOrdered
 
 open Function
 

Mathlib/Algebra/Group/Center.lean

@@ -36,9 +36,7 @@ We provide `Monoid.centralizer`, `AddMonoid.centralizer`, `Subgroup.centralizer`
 `AddSubgroup.centralizer` in other files.
 -/
 
-assert_not_exists Finset
-assert_not_exists MonoidWithZero
-assert_not_exists Subsemigroup
+assert_not_exists Finset MonoidWithZero Subsemigroup
 
 variable {M : Type*} {S T : Set M}