[Merged by Bors] - feat: assert_not_exists

Mathlib.lean

@@ -2373,6 +2373,7 @@ import Mathlib.Topology.UrysohnsLemma
 import Mathlib.Topology.VectorBundle.Basic
 import Mathlib.Topology.VectorBundle.Constructions
 import Mathlib.Util.AddRelatedDecl
+import Mathlib.Util.AssertExists
 import Mathlib.Util.AssertNoSorry
 import Mathlib.Util.AtomM
 import Mathlib.Util.Export

Mathlib/Algebra/Associated.lean

@@ -1230,5 +1230,4 @@ theorem dvd_prime_pow [CancelCommMonoidWithZero α] {p q : α} (hp : Prime p) (n
 
 end CancelCommMonoidWithZero
 
--- Porting note: `assert_not_exists` has not been ported yet.
--- assert_not_exists multiset
+assert_not_exists Multiset

Mathlib/Algebra/Group/Conj.lean

@@ -332,5 +332,4 @@ theorem carrier_eq_preimage_mk {a : ConjClasses α} : a.carrier = ConjClasses.mk
 
 end ConjClasses
 
--- porting notes: not implemented
--- assert_not_exists multiset
+assert_not_exists Multiset

Mathlib/Algebra/GroupWithZero/Units/Basic.lean

@@ -11,6 +11,7 @@ Authors: Johan Commelin
 import Mathlib.Algebra.GroupWithZero.Basic
 import Mathlib.Algebra.Group.Units
 import Mathlib.Tactic.Nontriviality
+import Mathlib.Util.AssertExists
 
 /-!
 # Lemmas about units in a `MonoidWithZero` or a `GroupWithZero`.
@@ -354,5 +355,4 @@ noncomputable def commGroupWithZeroOfIsUnitOrEqZero [hM : CommMonoidWithZero M]
 end NoncomputableDefs
 
 -- Guard against import creep
--- porting note: command not ported yet (added in mathlib#17416)
--- assert_not_exists multiplicative
+assert_not_exists Multiplicative

Mathlib/Algebra/Hom/GroupAction.lean

@@ -39,8 +39,7 @@ The above types have corresponding classes:
 
 -/
 
---Porting note: assert_not_exists is not yet implemented
---assert_not_exists Submonoid
+assert_not_exists Submonoid
 
 variable (M' : Type _)
 variable (X : Type _) [SMul M' X]

Mathlib/Algebra/Module/Basic.lean

@@ -767,5 +767,4 @@ theorem Int.smul_one_eq_coe {R : Type _} [Ring R] (m : ℤ) : m • (1 : R) = 
   rw [zsmul_eq_mul, mul_one]
 #align int.smul_one_eq_coe Int.smul_one_eq_coe
 
--- Porting note: `assert_not_exists` not implemented yet
--- assert_not_exists multiset
+assert_not_exists Multiset

Mathlib/Algebra/Module/LinearMap.lean

@@ -58,12 +58,8 @@ linear map
 -/
 
 
--- Porting note: `assert_not_exists` is not defined yet
-/-
 assert_not_exists Submonoid
-
-assert_not_exists finset
--/
+assert_not_exists Finset
 
 open Function
 

Mathlib/Algebra/Order/Field/Defs.lean

@@ -49,6 +49,5 @@ instance (priority := 100) LinearOrderedField.toLinearOrderedSemifield [LinearOr
   { LinearOrderedRing.toLinearOrderedSemiring, ‹LinearOrderedField α› with }
 #align linear_ordered_field.to_linear_ordered_semifield LinearOrderedField.toLinearOrderedSemifield
 
--- Porting note: assert_not_exists has not been ported yet.
 -- Guard against import creep.
--- assert_not_exists monoid_hom
+assert_not_exists MonoidHom

Mathlib/Algebra/Ring/Equiv.lean

@@ -12,6 +12,7 @@ Ported by: Anatole Dedecker
 import Mathlib.Algebra.Group.Opposite
 import Mathlib.Algebra.Hom.Ring
 import Mathlib.Logic.Equiv.Set
+import Mathlib.Util.AssertExists
 
 /-!
 # (Semi)ring equivs
@@ -880,5 +881,4 @@ protected theorem isDomain {A : Type _} (B : Type _) [Ring A] [Ring B] [IsDomain
 end RingEquiv
 
 -- guard against import creep
--- Porting note: not implemented yet
--- assert_not_exists fintype
+assert_not_exists Fintype

Mathlib/Algebra/Star/Basic.lean

@@ -43,9 +43,8 @@ positive cone which is the closure of the sums of elements `star r * r`. A weake
 advantage of not requiring a topology.
 -/
 
--- Porting note: `assert_not_exists` not implemented yet
---assert_not_exists finset
---assert_not_exists subgroup
+assert_not_exists Finset
+assert_not_exists Subgroup
 
 universe u v
 

Mathlib/Analysis/Complex/Basic.lean

@@ -38,7 +38,7 @@ We also register the fact that `ℂ` is an `IsROrC` field.
 -/
 
 
--- porting note: todo: restore assert_not_exists Absorbs
+assert_not_exists Absorbs
 
 noncomputable section
 

Mathlib/Analysis/Convex/Topology.lean

@@ -25,8 +25,7 @@ We prove the following facts:
 * `Set.Finite.isClosed_convexHull` : convex hull of a finite set is closed.
 -/
 
--- Porting note: this does not exist in Lean 4:
---assert_not_exists Norm
+assert_not_exists Norm
 
 open Metric Set Pointwise Convex
 

Mathlib/Analysis/Normed/Field/Basic.lean

@@ -1030,8 +1030,5 @@ instance toNormedCommRing [NormedCommRing R] [SubringClass S R] (s : S) : Normed
 
 end SubringClass
 
--- porting note: add this back in once `assert_not_exists` is ported
-/-
 -- Guard again import creep.
 assert_not_exists RestrictScalars
--/

Mathlib/Analysis/Seminorm.lean

@@ -1226,5 +1226,4 @@ theorem balanced_ball_zero : Balanced 𝕜 (Metric.ball (0 : E) r) := by
 
 end normSeminorm
 
--- Porting note: no guards here
--- assert_not_exists balancedCore
+assert_not_exists balancedCore

Mathlib/CategoryTheory/Limits/Yoneda.lean

@@ -9,6 +9,7 @@ Authors: Scott Morrison, Bhavik Mehta
 ! if you have ported upstream changes.
 -/
 import Mathlib.CategoryTheory.Limits.FunctorCategory
+import Mathlib.Util.AssertExists
 
 /-!
 # Limit properties relating to the (co)yoneda embedding.
@@ -176,9 +177,7 @@ instance coyonedaFunctorReflectsLimits : ReflectsLimits (@coyoneda D _) :=
 
 end CategoryTheory
 
--- Porting note: assert_not_exists doesn't exist in Lean 4 now. Is there value in keeping this?
--- We don't need to have developed any algebra or set theory to reach (at least) this point
--- in the category theory hierarchy.
--- assert_not_exists Set.range
+assert_not_exists Set.range
 
+-- Porting note: after the port see if this import can be removed
 -- assert_not_exists AddCommMonoid

Mathlib/CategoryTheory/Monoidal/Tor.lean

@@ -89,5 +89,4 @@ set_option linter.uppercaseLean3 false in
 
 end CategoryTheory
 
--- porting note: commented the following line
---assert_not_exists Module.abelian
+assert_not_exists Module.abelian

Mathlib/Data/Finset/Basic.lean

@@ -3805,8 +3805,7 @@ theorem disjoint_toFinset_iff_disjoint : _root_.Disjoint l.toFinset l'.toFinset
 
 end List
 
--- Porting note: `assert_not_exists` not yet available
 -- Assert that we define `Finset` without the material on `List.sublists`.
 -- Note that we cannot use `List.sublists` itself as that is defined very early.
--- assert_not_exists list.sublists_len
--- assert_not_exists multiset.powerset
+assert_not_exists List.sublistsLen
+assert_not_exists Multiset.powerset

Mathlib/Data/Int/Order/Basic.lean

@@ -553,6 +553,5 @@ theorem toNat_sub_of_le {a b : ℤ} (h : b ≤ a) : (toNat (a - b) : ℤ) = a -
 
 end Int
 
--- Porting note assert_not_exists not ported yet.
 -- We should need only a minimal development of sets in order to get here.
--- assert_not_exists set.range
+assert_not_exists Set.range

Mathlib/Data/List/Basic.lean

@@ -22,8 +22,7 @@ open Function
 
 open Nat hiding one_pos
 
--- Porting note: missing impl
--- assert_not_exists Set.range
+assert_not_exists Set.range
 
 namespace List
 

Mathlib/Data/Multiset/FinsetOps.lean

@@ -284,7 +284,6 @@ theorem ndinter_eq_zero_iff_disjoint {s t : Multiset α} : ndinter s t = 0 ↔ D
 
 end Multiset
 
--- Porting note: `assert_not_exists` has not been ported yet.
--- -- Assert that we define `finset` without the material on the set lattice.
--- -- Note that we cannot put this in `data.finset.basic` because we proved relevant lemmas there.
--- assert_not_exists set.sInter
+-- Assert that we define `Finset` without the material on the set lattice.
+-- Note that we cannot put this in `Data.Finset.Basic` because we proved relevant lemmas there.
+assert_not_exists Set.sInter

Mathlib/Data/Nat/Factors.lean

@@ -307,5 +307,4 @@ theorem eq_two_pow_or_exists_odd_prime_and_dvd (n : ℕ) :
 
 end Nat
 
--- Porting note: `assert_not_exists` is not implemented yet.
---assert_not_exists Multiset
+assert_not_exists Multiset

Mathlib/Data/Rat/Defs.lean

@@ -560,6 +560,5 @@ theorem mkRat_eq_div {n : ℤ} {d : ℕ} : mkRat n d = n / d := by
 
 end Rat
 
--- Porting note: `assert_not_exists` is not implemented yet.
 -- Guard against import creep.
--- assert_not_exists field
+assert_not_exists Field

Mathlib/Data/Rat/Order.lean

@@ -311,15 +311,13 @@ theorem abs_def (q : ℚ) : |q| = q.num.natAbs /. q.den := by
 
 end Rat
 
--- Porting note: `assert_not_exists` not yet implemented.
-
 -- We make some assertions here about declarations that do not need to be in the import dependencies
 -- for this file, but have been in the past.
--- assert_not_exists fintype
+assert_not_exists Fintype
 
--- assert_not_exists set.Icc
+assert_not_exists Set.Icc
 
--- assert_not_exists galois_connection
+assert_not_exists GaloisConnection
 
 -- These are less significant, but should not be relaxed until at least after port to Lean 4.
--- assert_not_exists LinearOrderedCommGroupWithZero
+assert_not_exists LinearOrderedCommGroupWithZero

Mathlib/Data/Real/Basic.lean

@@ -22,9 +22,9 @@ lifting everything to `ℚ`.
 -/
 
 
---assert_not_exists finset
---assert_not_exists Module
---assert_not_exists Submonoid
+assert_not_exists Finset
+assert_not_exists Module
+assert_not_exists Submonoid
 
 open Pointwise
 

Mathlib/GroupTheory/Subgroup/Basic.lean

@@ -3686,4 +3686,4 @@ theorem normalClosure_eq_top_of {N : Subgroup G} [hn : N.Normal] {g g' : G} {hg
 
 end IsConj
 
--- assert_not_exists Multiset
+assert_not_exists Multiset

Mathlib/GroupTheory/Submonoid/Center.lean

@@ -100,6 +100,5 @@ end
 
 end Submonoid
 
--- Porting note: `assert_not_exists` is not ported yet
 -- Guard against import creep
---assert_not_exists finset
+assert_not_exists Finset

Mathlib/GroupTheory/Submonoid/Centralizer.lean

@@ -91,6 +91,5 @@ end
 
 end Submonoid
 
--- Porting note: `assert_not_exists` not implemented yet
 -- Guard against import creep
---assert_not_exists finset
+assert_not_exists Finset

Mathlib/GroupTheory/Subsemigroup/Center.lean

@@ -194,5 +194,4 @@ end
 end Subsemigroup
 
 -- Guard against import creep
--- Porting note: Not implemented yet
--- assert_not_exists finset
+assert_not_exists Finset

Mathlib/GroupTheory/Subsemigroup/Centralizer.lean

@@ -192,6 +192,5 @@ end
 
 end Subsemigroup
 
--- porting note: This does not exist yet, however it is not relevant for functionality
 -- Guard against import creep
--- assert_not_exists finset
+assert_not_exists Finset

Mathlib/Mathport/Syntax.lean

@@ -333,8 +333,6 @@ namespace Command
 
 /- S -/ syntax (name := printSorryIn) "#print_sorry_in " ident : command
 
-/- E -/ syntax (name := assertExists) "assert_exists " ident : command
-/- E -/ syntax (name := assertNotExists) "assert_not_exists " ident : command
 /- E -/ syntax (name := assertInstance) "assert_instance " term : command
 /- E -/ syntax (name := assertNoInstance) "assert_no_instance " term : command
 

Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.lean

@@ -251,6 +251,6 @@ instance ENNReal.hasMeasurablePow : MeasurablePow ℝ≥0∞ ℝ := by
 end PowInstances
 
 -- Guard against import creep:
--- assert_not_exists InnerProductSpace
--- assert_not_exists Real.arctan
--- assert_not_exists FiniteDimensional.proper
+assert_not_exists InnerProductSpace
+assert_not_exists Real.arctan
+assert_not_exists FiniteDimensional.proper

Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

@@ -1549,5 +1549,4 @@ theorem WithTop.iSup_coe_lt_top {ι : Sort _} {α : Type _} [ConditionallyComple
 end WithTopBot
 
 -- Guard against import creep
--- Porting note: `assert_not_exists` has not been ported yet.
---assert_not_exists multiset
+assert_not_exists Multiset

Mathlib/Order/Hom/Basic.lean

@@ -13,6 +13,7 @@ import Mathlib.Order.RelIso.Basic
 import Mathlib.Order.Disjoint
 import Mathlib.Order.WithBot
 import Mathlib.Tactic.Monotonicity.Attr
+import Mathlib.Util.AssertExists
 
 /-!
 # Order homomorphisms
@@ -1388,6 +1389,5 @@ end BoundedOrder
 
 end LatticeIsos
 
--- Developments relating order homs and sets belong in `order.hom.set` or later.
--- porting note: command not ported yet (added in mathlib#17416)
--- assert_not_exists set.range
+-- Developments relating order homs and sets belong in `Order.Hom.Set` or later.
+assert_not_exists Set.range

Mathlib/Order/SemiconjSup.lean

@@ -133,5 +133,4 @@ theorem csSup_div_semiconj [ConditionallyCompleteLattice α] [Group G] (f₁ f
 #align function.cSup_div_semiconj Function.csSup_div_semiconj
 
 -- Guard against import creep
--- Porting note: not implemented yet
--- assert_not_exists finset
+assert_not_exists Finset

Mathlib/Util/AssertExists.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2022 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Patrick Massot, Scott Morrison
+-/
+import Lean
+
+/-!
+# User commands for assert the (non-)existence of declaration or instances.
+
+These commands are used to enforce the independence of different parts of mathlib.
+
+## TODO
+
+Potentially after the port reimplement the mathlib 3 linters to check that declarations asserted
+about do eventually exist.
+
+Implement `assert_instance` and `assert_no_instance`
+-/
+
+section
+open Lean Elab Meta
+
+/--
+`assert_exists n` is a user command that asserts that a declaration named `n` exists
+in the current import scope.
+
+Be careful to use names (e.g. `Rat`) rather than notations (e.g. `ℚ`).
+-/
+elab "assert_exists " n:ident : command => do
+  let _ ← resolveGlobalConstNoOverloadWithInfo n
+
+/--
+`assert_not_exists n` is a user command that asserts that a declaration named `n` *does not exist*
+in the current import scope.
+
+Be careful to use names (e.g. `Rat`) rather than notations (e.g. `ℚ`).
+
+It may be used (sparingly!) in mathlib to enforce plans that certain files
+are independent of each other.
+
+If you encounter an error on an `assert_not_exists` command while developing mathlib,
+it is probably because you have introduced new import dependencies to a file.
+
+In this case, you should refactor your work
+(for example by creating new files rather than adding imports to existing files).
+You should *not* delete the `assert_not_exists` statement without careful discussion ahead of time.
+-/
+elab "assert_not_exists " n:ident : command =>
+  do let [] ← try resolveGlobalConstWithInfos n catch _ => return
+      | throw <| Exception.error n m!"Declaration {n} is not allowed to exist in this file"