feat: make Set.monad not an instance and add (Subtype.val '' ·) c…

…oercion (#8413)

The monad instance on `Set` isn't computationally relevant, and it causes Lean's monad lifting coercion logic to activate. We introduce a coercion instance for the case that's actually used in practice: when `s : Set X` and `t : Set s` then `(t : Set X)` ought to be `Subtype.val '' t`. This way we do not see `Lean.Internal.coeM` terms.

If the monad is still wanted, it can be activated using a local attribute or by using the `SetM.run` function.

Mathlib/Data/Set/Finite.lean

@@ -400,6 +400,9 @@ instance fintypeBiUnion' [DecidableEq α] {ι : Type*} (s : Set ι) [Fintype s]
   Fintype.ofFinset (s.toFinset.biUnion fun x => (t x).toFinset) <| by simp
 #align set.fintype_bUnion' Set.fintypeBiUnion'
 
+section monad
+attribute [local instance] Set.monad
+
 /-- If `s : Set α` is a set with `Fintype` instance and `f : α → Set β` is a function such that
 each `f a`, `a ∈ s`, has a `Fintype` structure, then `s >>= f` has a `Fintype` structure. -/
 def fintypeBind {α β} [DecidableEq β] (s : Set α) [Fintype s] (f : α → Set β)
@@ -412,6 +415,8 @@ instance fintypeBind' {α β} [DecidableEq β] (s : Set α) [Fintype s] (f : α
   Set.fintypeBiUnion' s f
 #align set.fintype_bind' Set.fintypeBind'
 
+end monad
+
 instance fintypeEmpty : Fintype (∅ : Set α) :=
   Fintype.ofFinset ∅ <| by simp
 #align set.fintype_empty Set.fintypeEmpty
@@ -828,11 +833,16 @@ theorem Finite.iUnion {ι : Type*} {s : ι → Set α} {t : Set ι} (ht : t.Fini
     contradiction
 #align set.finite.Union Set.Finite.iUnion
 
+section monad
+attribute [local instance] Set.monad
+
 theorem Finite.bind {α β} {s : Set α} {f : α → Set β} (h : s.Finite) (hf : ∀ a ∈ s, (f a).Finite) :
     (s >>= f).Finite :=
   h.biUnion hf
 #align set.finite.bind Set.Finite.bind
 
+end monad
+
 @[simp]
 theorem finite_empty : (∅ : Set α).Finite :=
   toFinite _

Mathlib/Data/Set/Functor.lean

@@ -25,12 +25,22 @@ namespace Set
 
 variable {α β : Type u} {s : Set α} {f : α → Set β} {g : Set (α → β)}
 
-instance monad : Monad.{u} Set where
+/-- The `Set` functor is a monad.
+
+This is not a global instance because it does not have computational content,
+so it does not make much sense using `do` notation in general.
+Plus, this would cause monad-related coercions and monad lifting logic to become activated.
+Either use `attribute [local instance] Set.monad` to make it be a local instance
+or use `SetM.run do ...` when `do` notation is wanted. -/
+protected def monad : Monad.{u} Set where
   pure a := {a}
   bind s f := ⋃ i ∈ s, f i
   seq s t := Set.seq s (t ())
   map := Set.image
 
+section with_instance
+attribute [local instance] Set.monad
+
 @[simp]
 theorem bind_def : s >>= f = ⋃ i ∈ s, f i :=
   rfl
@@ -74,7 +84,7 @@ instance : Alternative Set :=
     orElse := fun s t => s ∪ (t ())
     failure := ∅ }
 
-/-! ## Monadic coercion lemmas -/
+/-! ### Monadic coercion lemmas -/
 
 variable {β : Set α} {γ : Set β}
 
@@ -94,4 +104,50 @@ theorem image_coe_eq_restrict_image {f : α → δ} : f '' γ = β.restrict f ''
   ext fun _ =>
     ⟨fun ⟨_, h, ha⟩ => ⟨_, mem_of_mem_coe h, ha⟩, fun ⟨_, h, ha⟩ => ⟨_, mem_coe_of_mem _ h, ha⟩⟩
 
+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)⟩
+
+/-- 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
+  change ⋃ (x ∈ t), {x.1} = _
+  ext
+  simp
+
+variable {β : Set α} {γ : Set β}
+
+theorem mem_image_val_of_mem (ha : a ∈ β) (ha' : ⟨a, ha⟩ ∈ γ) : a ∈ (γ : Set α) :=
+  ⟨_, ha', rfl⟩
+
+theorem image_val_subset : (γ : Set α) ⊆ β := by
+  rintro _ ⟨⟨_, ha⟩, _, rfl⟩; exact ha
+
+theorem mem_of_mem_image_val (ha : a ∈ (γ : Set α)) : ⟨a, image_val_subset ha⟩ ∈ γ := by
+  rcases ha with ⟨_, ha, rfl⟩; exact ha
+
+theorem eq_univ_of_image_val_eq (hγ : (γ : Set α) = β) : γ = univ :=
+  eq_univ_of_forall fun ⟨_, ha⟩ => mem_of_mem_image_val <| hγ.symm ▸ ha
+
+theorem image_image_val_eq_restrict_image {f : α → δ} : f '' γ = β.restrict f '' γ := by
+  ext; simp
+
 end Set
+
+/-! ### Wrapper to enable the `Set` monad -/
+
+/-- This is `Set` but with a `Monad` instance. -/
+def SetM (α : Type u) := Set α
+
+instance : Monad SetM := Set.monad
+
+/-- Evaluates the `SetM` monad, yielding a `Set`.
+Implementation note: this is the identity function. -/
+protected def SetM.run (s : SetM α) : Set α := s

Mathlib/RingTheory/Polynomial/Dickson.lean

@@ -231,7 +231,7 @@ theorem dickson_one_one_zmod_p (p : ℕ) [Fact p.Prime] : dickson 1 (1 : ZMod p)
     -- For every `x`, that set is finite (since it is governed by a quadratic equation).
     -- For the moment, we claim that all these sets together cover `K`.
     suffices (Set.univ : Set K) =
-        { x : K | ∃ y : K, x = y + y⁻¹ ∧ y ≠ 0 } >>= fun x => { y | x = y + y⁻¹ ∨ y = 0 } by
+        ⋃ x ∈ { x : K | ∃ y : K, x = y + y⁻¹ ∧ y ≠ 0 }, { y | x = y + y⁻¹ ∨ y = 0 }  by
       rw [this]
       clear this
       refine' h.biUnion fun x _ => _

Mathlib/Topology/Constructions.lean

@@ -1676,14 +1676,12 @@ variable [TopologicalSpace α] {β : Set α} {γ : Set β}
 
 theorem IsOpen.trans (hγ : IsOpen γ) (hβ : IsOpen β) : IsOpen (γ : Set α) := by
   rcases isOpen_induced_iff.mp hγ with ⟨δ, hδ, rfl⟩
-  convert IsOpen.inter hβ hδ
-  ext
-  exact ⟨fun h => ⟨coe_subset h, mem_of_mem_coe h⟩, fun ⟨hβ, hδ⟩ => mem_coe_of_mem hβ hδ⟩
+  rw [Subtype.image_preimage_coe]
+  exact IsOpen.inter hδ hβ
 
 theorem IsClosed.trans (hγ : IsClosed γ) (hβ : IsClosed β) : IsClosed (γ : Set α) := by
   rcases isClosed_induced_iff.mp hγ with ⟨δ, hδ, rfl⟩
-  convert IsClosed.inter hβ hδ
-  ext
-  exact ⟨fun h => ⟨coe_subset h, mem_of_mem_coe h⟩, fun ⟨hβ, hδ⟩ => mem_coe_of_mem hβ hδ⟩
+  rw [Subtype.image_preimage_coe]
+  convert IsClosed.inter hδ hβ
 
 end Monad

Mathlib/Topology/ExtremallyDisconnected.lean

@@ -151,8 +151,9 @@ lemma exists_compact_surjective_zorn_subset [T1Space A] [CompactSpace D] {π : D
     refine ⟨E, isCompact_iff_compactSpace.mp E_closed.isCompact, E_surj, ?_⟩
     intro E₀ E₀_min E₀_closed
     contrapose! E₀_min
-    exact eq_univ_of_coe_eq <|
-      E_min E₀ ⟨E₀_closed.trans E_closed, image_coe_eq_restrict_image ▸ E₀_min⟩ coe_subset
+    exact eq_univ_of_image_val_eq <|
+      E_min E₀ ⟨E₀_closed.trans E_closed, image_image_val_eq_restrict_image ▸ E₀_min⟩
+        image_val_subset
   -- suffices to prove intersection of chain is minimal
   intro C C_sub C_chain
   -- prove intersection of chain is closed