feat(Set): API for subset restriction and coercion to/from subtypes (#9940)

Api for subset restriction and coercion to/from subtypes

Co-authored-by: Miguel Marco <mmarco@unizar.es>



Co-authored-by: Miguel Marco <mmarco@unizar.es>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: mmarco <mmarco@kali>
Co-authored-by: Winston Yin <winstonyin@gmail.com>

Author: 5 people

Mathlib.lean

@@ -2092,6 +2092,7 @@ import Mathlib.Data.Set.Pointwise.Support
 import Mathlib.Data.Set.Prod
 import Mathlib.Data.Set.Semiring
 import Mathlib.Data.Set.Sigma
+import Mathlib.Data.Set.Subset
 import Mathlib.Data.Set.Sups
 import Mathlib.Data.Set.UnionLift
 import Mathlib.Data.SetLike.Basic

Mathlib/Data/Set/Functor.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 import Mathlib.Data.Set.Lattice
 import Mathlib.Init.Set
 import Mathlib.Control.Basic
+import Mathlib.Lean.Expr.ExtraRecognizers
 
 #align_import data.set.functor from "leanprover-community/mathlib"@"207cfac9fcd06138865b5d04f7091e46d9320432"
 
@@ -115,6 +116,23 @@ 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
+
 /-- The coercion from `Set.monad` as an instance is equal to the coercion defined above. -/
 theorem coe_eq_image_val (t : Set s) :
     @Lean.Internal.coeM Set s α _ Set.monad t = (t : Set α) := by

Mathlib/Data/Set/Image.lean

@@ -1444,6 +1444,14 @@ theorem preimage_val_eq_preimage_val_iff (s t u : Set α) :
   preimage_coe_eq_preimage_coe_iff
 #align subtype.preimage_val_eq_preimage_val_iff Subtype.preimage_val_eq_preimage_val_iff
 
+lemma preimage_val_subset_preimage_val_iff (s t u : Set α) :
+    (Subtype.val ⁻¹' t : Set s) ⊆ Subtype.val ⁻¹' u ↔ s ∩ t ⊆ s ∩ u := by
+  constructor
+  · rw [← image_preimage_coe, ← image_preimage_coe]
+    exact image_subset _
+  · intro h x a
+    exact (h ⟨x.2, a⟩).2
+
 theorem exists_set_subtype {t : Set α} (p : Set α → Prop) :
     (∃ s : Set t, p (((↑) : t → α) '' s)) ↔ ∃ s : Set α, s ⊆ t ∧ p s := by
   rw [← exists_subset_range_and_iff, range_coe]

Mathlib/Data/Set/Subset.lean

@@ -0,0 +1,163 @@
+/-
+Copyright (c) 2024 Miguel Marco. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Miguel Marco
+-/
+import Mathlib.Data.Set.Function
+import Mathlib.Data.Set.Functor
+
+/-!
+# Sets in subtypes
+
+This file is about sets in `Set A` when `A` is a set.
+
+It defines notation `↓∩` for sets in a type pulled down to sets in a subtype, as an inverse
+operation to the coercion that lifts sets in a subtype up to sets in the ambient type.
+
+This module also provides lemmas for `↓∩` and this coercion.
+
+## Notation
+
+Let `α` be a `Type`, `A B : Set α` two sets in `α`, and `C : Set A` a set in the subtype `↑A`.
+
+- `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.
+To enable it, use `open Set.Notation`.
+
+
+## Naming conventions
+
+Theorem names refer to `↓∩` as `preimage_val`.
+
+## Tags
+
+subsets
+-/
+
+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
+
+lemma preimage_val_eq_univ_of_subset (h : A ⊆ B) : A ↓∩ B = univ := by
+  rw [eq_univ_iff_forall, Subtype.forall]
+  exact h
+
+lemma preimage_val_sUnion : A ↓∩ (⋃₀ S) = ⋃₀ { (A ↓∩ B) | B ∈ S } := by
+  erw [sUnion_image]
+  simp_rw [sUnion_eq_biUnion, preimage_iUnion]
+
+@[simp]
+lemma preimage_val_iInter : A ↓∩ (⋂ i, s i) = ⋂ i, A ↓∩ s i := preimage_iInter
+
+lemma preimage_val_sInter : A ↓∩ (⋂₀ S) = ⋂₀ { (A ↓∩ B) | B ∈ S } := by
+  erw [sInter_image]
+  simp_rw [sInter_eq_biInter, preimage_iInter]
+
+lemma preimage_val_sInter_eq_sInter : A ↓∩ (⋂₀ S) = ⋂₀ ((A ↓∩ .) '' S) := by
+  simp only [preimage_sInter, sInter_image]
+
+lemma eq_of_preimage_val_eq_of_subset (hB : B ⊆ A) (hC : C ⊆ A) (h : A ↓∩ B = A ↓∩ C) : B = C := by
+  simp only [← inter_eq_right] at hB hC
+  simp only [Subtype.preimage_val_eq_preimage_val_iff, hB, hC] at h
+  exact h
+
+/-!
+The following simp lemmas try to transform operations in the subtype into operations in the ambient
+type, if possible.
+-/
+
+@[simp]
+lemma image_val_union : (↑(D ∪ E) : Set α) = ↑D ∪ ↑E := image_union _ _ _
+
+@[simp]
+lemma image_val_inter : (↑(D ∩ E) : Set α) = ↑D ∩ ↑E := image_inter Subtype.val_injective
+
+@[simp]
+lemma image_val_diff : (↑(D \ E) : Set α) = ↑D \ ↑E := image_diff Subtype.val_injective _ _
+
+@[simp]
+lemma image_val_compl : ↑(Dᶜ) = A \ ↑D := by
+  rw [compl_eq_univ_diff, image_val_diff, image_univ, Subtype.range_coe_subtype, setOf_mem_eq]
+
+@[simp]
+lemma image_val_sUnion : ↑(⋃₀ T) = ⋃₀ { (B : Set α) | B ∈ T} := by
+  -- TODO: missing `image_sUnion` lemma
+  erw [sUnion_image]
+  simp_rw [sUnion_eq_biUnion, image_iUnion]
+
+@[simp]
+lemma image_val_iUnion : ↑(⋃ i, t i) = ⋃ i, (t i : Set α) := image_iUnion
+
+@[simp]
+lemma image_val_sInter (hT : T.Nonempty) : (↑(⋂₀ T) : Set α) = ⋂₀ { (↑B : Set α) | B ∈ T } := by
+  erw [sInter_image]
+  rw [sInter_eq_biInter, (Subtype.val_injective.injOn _).image_biInter_eq hT]
+
+@[simp]
+lemma image_val_iInter [Nonempty ι] : (↑(⋂ i, t i) : Set α) = ⋂ i, (↑(t i) : Set α) :=
+  (Subtype.val_injective.injOn _).image_iInter_eq
+
+@[simp]
+lemma image_val_union_self_right_eq : A ∪ ↑D = A :=
+  union_eq_left.2 image_val_subset
+
+@[simp]
+lemma image_val_union_self_left_eq : ↑D ∪ A = A :=
+  union_eq_right.2 image_val_subset
+
+@[simp]
+lemma cou_inter_self_right_eq_coe : A ∩ ↑D = ↑D :=
+  inter_eq_right.2 image_val_subset
+
+@[simp]
+lemma image_val_inter_self_left_eq_coe : ↑D ∩ A = ↑D :=
+  inter_eq_left.2 image_val_subset
+
+lemma subset_preimage_val_image_val_iff : D ⊆ A ↓∩ ↑E ↔ D ⊆ E := by
+  rw [preimage_image_eq _ Subtype.val_injective]
+
+@[simp]
+lemma image_val_inj : (D : Set α) = ↑E ↔ D = E := Subtype.val_injective.image_injective.eq_iff
+
+lemma image_val_injective : Function.Injective ((↑) : Set A → Set α) :=
+  Subtype.val_injective.image_injective
+
+lemma subset_of_image_val_subset_image_val (h : (↑D : Set α) ⊆ ↑E) : D ⊆ E :=
+  (image_subset_image_iff Subtype.val_injective).1 h
+
+@[mono]
+lemma image_val_mono (h : D ⊆ E) : (↑D : Set α) ⊆ ↑E :=
+  (image_subset_image_iff Subtype.val_injective).2 h
+
+/-!
+Relations between restriction and coercion.
+-/
+
+lemma image_val_preimage_val_subset_self : ↑(A ↓∩ B) ⊆ B :=
+  image_preimage_subset _ _
+
+lemma preimage_val_image_val_eq_self : A ↓∩ ↑D = D :=
+  Function.Injective.preimage_image Subtype.val_injective _
+
+end Set