feat: small_iUnion and small_sUnion (#10921)

Also moves the other results about `Small` on sets to their own file.

Author: TwoFX

Mathlib.lean

@@ -2666,6 +2666,7 @@ import Mathlib.Logic.Small.Group
 import Mathlib.Logic.Small.List
 import Mathlib.Logic.Small.Module
 import Mathlib.Logic.Small.Ring
+import Mathlib.Logic.Small.Set
 import Mathlib.Logic.Unique
 import Mathlib.Logic.UnivLE
 import Mathlib.Mathport.Attributes

Mathlib/CategoryTheory/Comma/StructuredArrow.lean

@@ -7,6 +7,7 @@ import Mathlib.CategoryTheory.Comma.Basic
 import Mathlib.CategoryTheory.PUnit
 import Mathlib.CategoryTheory.Limits.Shapes.Terminal
 import Mathlib.CategoryTheory.EssentiallySmall
+import Mathlib.Logic.Small.Set
 
 #align_import category_theory.structured_arrow from "leanprover-community/mathlib"@"8a318021995877a44630c898d0b2bc376fceef3b"
 

Mathlib/Logic/Small/Basic.lean

@@ -37,11 +37,6 @@ theorem small_of_surjective {α : Type v} {β : Type w} [Small.{u} α] {f : α 
   small_of_injective (Function.injective_surjInv hf)
 #align small_of_surjective small_of_surjective
 
-theorem small_subset {α : Type v} {s t : Set α} (hts : t ⊆ s) [Small.{u} s] : Small.{u} t :=
-  let f : t → s := fun x => ⟨x, hts x.prop⟩
-  @small_of_injective _ _ _ f fun _ _ hxy => Subtype.ext (Subtype.mk.inj hxy)
-#align small_subset small_subset
-
 instance (priority := 100) small_subsingleton (α : Type v) [Subsingleton α] : Small.{w} α := by
   rcases isEmpty_or_nonempty α with ⟨⟩ <;> skip
   · apply small_map (Equiv.equivPEmpty α)
@@ -84,14 +79,4 @@ instance small_set {α} [Small.{w} α] : Small.{w} (Set α) :=
   ⟨⟨Set (Shrink α), ⟨Equiv.Set.congr (equivShrink α)⟩⟩⟩
 #align small_set small_set
 
-instance small_range {α : Type v} {β : Type w} (f : α → β) [Small.{u} α] :
-    Small.{u} (Set.range f) :=
-  small_of_surjective Set.surjective_onto_range
-#align small_range small_range
-
-instance small_image {α : Type v} {β : Type w} (f : α → β) (S : Set α) [Small.{u} S] :
-    Small.{u} (f '' S) :=
-  small_of_surjective Set.surjective_onto_image
-#align small_image small_image
-
 end

Mathlib/Logic/Small/Set.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2024 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel
+-/
+import Mathlib.Data.Set.Lattice
+import Mathlib.Logic.Small.Basic
+
+/-!
+# Results about `Small` on coerced sets
+-/
+
+universe u v w
+
+theorem small_subset {α : Type v} {s t : Set α} (hts : t ⊆ s) [Small.{u} s] : Small.{u} t :=
+  let f : t → s := fun x => ⟨x, hts x.prop⟩
+  @small_of_injective _ _ _ f fun _ _ hxy => Subtype.ext (Subtype.mk.inj hxy)
+#align small_subset small_subset
+
+instance small_range {α : Type v} {β : Type w} (f : α → β) [Small.{u} α] :
+    Small.{u} (Set.range f) :=
+  small_of_surjective Set.surjective_onto_range
+#align small_range small_range
+
+instance small_image {α : Type v} {β : Type w} (f : α → β) (S : Set α) [Small.{u} S] :
+    Small.{u} (f '' S) :=
+  small_of_surjective Set.surjective_onto_image
+#align small_image small_image
+
+instance small_union {α : Type v} (s t : Set α) [Small.{u} s] [Small.{u} t] :
+    Small.{u} (s ∪ t : Set α) := by
+  rw [← Subtype.range_val (s := s), ← Subtype.range_val (s := t), ← Set.Sum.elim_range]
+  infer_instance
+
+instance small_iUnion {α : Type v} {ι : Type w} [Small.{u} ι] (s : ι → Set α)
+    [∀ i, Small.{u} (s i)] : Small.{u} (⋃ i, s i) :=
+  small_of_surjective <| Set.sigmaToiUnion_surjective _
+
+instance small_sUnion {α : Type v} (s : Set (Set α)) [Small.{u} s] [∀ t : s, Small.{u} t] :
+    Small.{u} (⋃₀ s) :=
+  Set.sUnion_eq_iUnion ▸ small_iUnion _

Mathlib/SetTheory/Cardinal/Basic.lean

@@ -7,7 +7,7 @@ import Mathlib.Algebra.Module.Basic
 import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Data.Finsupp.Defs
 import Mathlib.Data.Set.Countable
-import Mathlib.Logic.Small.Basic
+import Mathlib.Logic.Small.Set
 import Mathlib.Order.ConditionallyCompleteLattice.Basic
 import Mathlib.Order.SuccPred.CompleteLinearOrder
 import Mathlib.SetTheory.Cardinal.SchroederBernstein