chore: add exception for Data.Set.Subset to noshake.json. (#14196)

We add `Data.Set.Subset` to the set of files ignored by the shake linter, which gives a false positive when this file is just imported for the notation.

Author: apnelson1

Mathlib.lean

@@ -2329,6 +2329,7 @@ import Mathlib.Data.Set.List
 import Mathlib.Data.Set.MemPartition
 import Mathlib.Data.Set.MulAntidiagonal
 import Mathlib.Data.Set.NAry
+import Mathlib.Data.Set.Notation
 import Mathlib.Data.Set.Opposite
 import Mathlib.Data.Set.Pairwise.Basic
 import Mathlib.Data.Set.Pairwise.Lattice

Mathlib/Data/Matroid/Map.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Peter Nelson
 -/
 import Mathlib.Data.Matroid.Constructions
-import Mathlib.Data.Set.Subset
+import Mathlib.Data.Set.Notation
 
 /-!
 # Maps between matroids

Mathlib/Data/Set/Functor.lean

@@ -6,7 +6,7 @@ Authors: Leonardo de Moura
 import Mathlib.Data.Set.Lattice
 import Mathlib.Init.Set
 import Mathlib.Control.Basic
-import Mathlib.Lean.Expr.ExtraRecognizers
+import Mathlib.Data.Set.Notation
 
 #align_import data.set.functor from "leanprover-community/mathlib"@"207cfac9fcd06138865b5d04f7091e46d9320432"
 
@@ -18,7 +18,7 @@ This file defines the functor structure of `Set`.
 
 universe u
 
-open Function
+open Function Set.Notation
 
 namespace Set
 
@@ -106,32 +106,11 @@ theorem image_coe_eq_restrict_image {δ : Type*} {f : α → δ} : f '' γ = β.
 end with_instance
 
 /-! ### Coercion applying functoriality for `Subtype.val`
-
 The `Monad` instance gives a coercion using the internal function `Lean.Internal.coeM`.
-In practice this is only used for applying the `Set` functor to `Subtype.val`.
-We define this coercion here.  -/
-
-/-- Coercion using `(Subtype.val '' ·)` -/
-instance : CoeHead (Set s) (Set α) := ⟨fun t => (Subtype.val '' t)⟩
-
-namespace Notation
-
-open Lean PrettyPrinter Delaborator SubExpr in
-/--
-If the `Set.Notation` namespace is open, sets of a subtype coerced to the ambient type are
-represented with `↑`.
--/
-@[scoped delab app.Set.image]
-def delab_set_image_subtype : Delab := whenPPOption getPPCoercions do
-  let #[α, _, f, _] := (← getExpr).getAppArgs | failure
-  guard <| f.isAppOfArity ``Subtype.val 2
-  let some _ := α.coeTypeSet? | failure
-  let e ← withAppArg delab
-  `(↑$e)
-
-end Notation
+In practice this is only used for applying the `Set` functor to `Subtype.val`,
+as was defined in `Data.Set.Notation`. -/
 
-/-- The coercion from `Set.monad` as an instance is equal to the coercion defined above. -/
+/-- The coercion from `Set.monad` as an instance is equal to the coercion in `Data.Set.Notation`. -/
 theorem coe_eq_image_val (t : Set s) :
     @Lean.Internal.coeM Set s α _ Set.monad t = (t : Set α) := by
   change ⋃ (x ∈ t), {x.1} = _

Mathlib/Data/Set/Notation.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2024 Peter Nelson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Peter Nelson
+-/
+import Mathlib.Mathport.Notation
+import Mathlib.Lean.Expr.ExtraRecognizers
+
+/-!
+# Set Notation
+
+This file defines two pieces of scoped notation related to sets and subtypes.
+
+The first is a coercion; for each `α : Type*` and `s : Set α`, `(↑) : Set s → Set α`
+is the function coercing `t : Set s` into a set in the ambient type; i.e. `↑t = Subtype.val '' t`.
+
+The second, for `s t : Set α`, is the notation `s ↓∩ t`, which denotes the intersection
+of `s` and `t` as a set in `Set s`.
+
+These notations are developed further in `Data.Set.Functor` and `Data.Set.Subset` respectively.
+They are defined here separately so that this file can be added as an exception to the shake linter
+and can thus be imported without a linting false positive when only the notation is desired.
+-/
+
+namespace Set.Notation
+/--
+Given two sets `A` and `B`, `A ↓∩ B` denotes the intersection of `A` and `B` as a set in `Set A`.
+
+The notation is short for `((↑) ⁻¹' B : Set A)`, while giving hints to the elaborator
+that both `A` and `B` are terms of `Set α` for the same `α`.
+This set is the same as `{x : ↑A | ↑x ∈ B}`.
+-/
+scoped notation3 A:67 " ↓∩ " B:67 => (Subtype.val ⁻¹' (B : type_of% A) : Set (A : Set _))
+
+/-- Coercion using `(Subtype.val '' ·)` -/
+instance {α : Type*} {s : Set α} : CoeHead (Set s) (Set α) := ⟨fun t => (Subtype.val '' t)⟩
+
+open Lean PrettyPrinter Delaborator SubExpr in
+/--
+If the `Set.Notation` namespace is open, sets of a subtype coerced to the ambient type are
+represented with `↑`.
+-/
+@[scoped delab app.Set.image]
+def delab_set_image_subtype : Delab := whenPPOption getPPCoercions do
+  let #[α, _, f, _] := (← getExpr).getAppArgs | failure
+  guard <| f.isAppOfArity ``Subtype.val 2
+  let some _ := α.coeTypeSet? | failure
+  let e ← withAppArg delab
+  `(↑$e)
+
+end Set.Notation

Mathlib/Data/Set/Subset.lean

@@ -23,8 +23,8 @@ Let `α` be a `Type`, `A B : Set α` two sets in `α`, and `C : Set A` a set in
 - `A ↓∩ B` denotes `(Subtype.val ⁻¹' B : Set A)` (that is, `{x : ↑A | ↑x ∈ B}`).
 - `↑C` denotes `Subtype.val '' C` (that is, `{x : α | ∃ y ∈ C, ↑y = x}`).
 
-This notation, (together with the `↑` notation for `Set.CoeHead` in `Mathlib.Data.Set.Functor`)
-is scoped to the `Set.Notation` namespace.
+This notation, (together with the `↑` notation for `Set.CoeHead`)
+is defined in `Mathlib.Data.Set.Notation` and is scoped to the `Set.Notation` namespace.
 To enable it, use `open Set.Notation`.
 
 
@@ -42,19 +42,6 @@ open Set
 variable {ι : Sort*} {α : Type*} {A B C : Set α} {D E : Set A}
 variable {S : Set (Set α)} {T : Set (Set A)} {s : ι → Set α} {t : ι → Set A}
 
-namespace Set.Notation
-
-/--
-Given two sets `A` and `B`, `A ↓∩ B` denotes the intersection of `A` and `B` as a set in `Set A`.
-
-The notation is short for `((↑) ⁻¹' B : Set A)`, while giving hints to the elaborator
-that both `A` and `B` are terms of `Set α` for the same `α`.
-This set is the same as `{x : ↑A | ↑x ∈ B}`.
--/
-scoped notation3 A:67 " ↓∩ " B:67 => (Subtype.val ⁻¹' (B : type_of% A) : Set (A : Set _))
-
-end Set.Notation
-
 namespace Set
 
 open Notation

scripts/noshake.json

@@ -42,6 +42,7 @@
   "Mathlib.Data.Matrix.Notation",
   "Mathlib.Data.Matroid.Init",
   "Mathlib.Data.Rat.Init",
+  "Mathlib.Data.Set.Notation",
   "Mathlib.Data.Sym.Sym2.Init",
   "Mathlib.Data.Vector.Basic",
   "Mathlib.Geometry.Manifold.Instances.Real",
@@ -309,7 +310,6 @@
   "Mathlib.Data.Seq.Parallel": ["Mathlib.Init.Data.Prod"],
   "Mathlib.Data.Ordmap.Ordnode": ["Mathlib.Data.Option.Basic"],
   "Mathlib.Data.Multiset.Bind": ["Mathlib.GroupTheory.GroupAction.Defs"],
-  "Mathlib.Data.Matroid.Map": ["Mathlib.Data.Set.Subset"],
   "Mathlib.Data.List.TFAE": ["Batteries.Tactic.Classical"],
   "Mathlib.Data.List.ProdSigma": ["Mathlib.Data.List.Basic"],
   "Mathlib.Data.List.Lemmas": ["Mathlib.Data.List.InsertNth"],