feat(SetTheory/ZFC/Basic): generalize universes of range (#17016)

Author: vihdzp

Mathlib/SetTheory/ZFC/Basic.lean

@@ -1209,25 +1209,24 @@ theorem toSet_image (f : ZFSet → ZFSet) [Definable₁ f] (x : ZFSet) :
   ext
   simp
 
-/-- The range of an indexed family of sets. The universes allow for a more general index type
-  without manual use of `ULift`. -/
-noncomputable def range {α : Type u} (f : α → ZFSet.{max u v}) : ZFSet.{max u v} :=
-  ⟦⟨ULift.{v} α, Quotient.out ∘ f ∘ ULift.down⟩⟧
+/-- The range of a type-indexed family of sets. -/
+noncomputable def range {α} [Small.{u} α] (f : α → ZFSet.{u}) : ZFSet.{u} :=
+  ⟦⟨_, Quotient.out ∘ f ∘ (equivShrink α).symm⟩⟧
 
 @[simp]
-theorem mem_range {α : Type u} {f : α → ZFSet.{max u v}} {x : ZFSet.{max u v}} :
-    x ∈ range.{u, v} f ↔ x ∈ Set.range f :=
+theorem mem_range {α} [Small.{u} α] {f : α → ZFSet.{u}} {x : ZFSet.{u}} :
+    x ∈ range f ↔ x ∈ Set.range f :=
   Quotient.inductionOn x fun y => by
     constructor
     · rintro ⟨z, hz⟩
-      exact ⟨z.down, Quotient.eq_mk_iff_out.2 hz.symm⟩
+      exact ⟨(equivShrink α).symm z, Quotient.eq_mk_iff_out.2 hz.symm⟩
     · rintro ⟨z, hz⟩
-      use ULift.up z
+      use equivShrink α z
       simpa [hz] using PSet.Equiv.symm (Quotient.mk_out y)
 
 @[simp]
-theorem toSet_range {α : Type u} (f : α → ZFSet.{max u v}) :
-    (range.{u, v} f).toSet = Set.range f := by
+theorem toSet_range {α} [Small.{u} α] (f : α → ZFSet.{u}) :
+    (range f).toSet = Set.range f := by
   ext
   simp
 

Mathlib/SetTheory/ZFC/Rank.lean

@@ -3,6 +3,7 @@ Copyright (c) 2024 Dexin Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Dexin Zhang
 -/
+import Mathlib.Logic.UnivLE
 import Mathlib.SetTheory.Ordinal.Rank
 import Mathlib.SetTheory.ZFC.Basic
 
@@ -194,7 +195,7 @@ theorem le_succ_rank_sUnion (x : ZFSet) : rank x ≤ succ (rank (⋃₀ x)) := b
   exists z
 
 @[simp]
-theorem rank_range {α : Type u} (f : α → ZFSet.{max u v}) :
+theorem rank_range {α : Type*} [Small.{u} α] (f : α → ZFSet.{u}) :
     rank (range f) = ⨆ i, succ (rank (f i)) := by
   apply (Ordinal.iSup_le _).antisymm'
   · simpa [rank_le_iff, ← succ_le_iff] using Ordinal.le_iSup _