chore: rename mk_iUnion_Ordinal_le_of_le → mk_biUnion_le_of_le (leanprover-community#34452)

The former had bad capitalization, and referred to `iUnion` where `biUnion` would be more conventional.

Author: vihdzp

Mathlib/MeasureTheory/MeasurableSpace/Card.lean

@@ -176,7 +176,7 @@ theorem cardinal_generateMeasurableRec_le (s : Set (Set α)) (i : Ordinal.{v}) :
   have A : 𝔠 ≤ max #s 2 ^ ℵ₀ := power_le_power_right (le_max_right _ _)
   have B := aleph0_le_continuum.trans A
   have C : #(⋃ j < i, generateMeasurableRec s j) ≤ max #s 2 ^ ℵ₀ := by
-    apply mk_iUnion_Ordinal_lift_le_of_le _ B _
+    apply mk_biUnion_le_of_le_lift _ B _
     · intro j hj
       exact IH j hj (hj.trans_le hi).le
     · rw [lift_power, lift_aleph0]

Mathlib/SetTheory/Cardinal/Ordinal.lean

@@ -24,7 +24,7 @@ open Cardinal Ordinal Set
 namespace Cardinal
 
 /-- Bounds the cardinal of an ordinal-indexed union of sets. -/
-lemma mk_iUnion_Ordinal_lift_le_of_le {β : Type v} {o : Ordinal.{u}} {c : Cardinal.{v}}
+lemma mk_biUnion_le_of_le_lift {β : Type v} {o : Ordinal.{u}} {c : Cardinal.{v}}
     (ho : lift.{v} o.card ≤ lift.{u} c) (hc : ℵ₀ ≤ c) (A : Ordinal → Set β)
     (hA : ∀ j < o, #(A j) ≤ c) : #(⋃ j < o, A j) ≤ c := by
   simp_rw [← mem_Iio, biUnion_eq_iUnion, iUnion, iSup, ← ToType.mk.symm.surjective.range_comp]
@@ -35,12 +35,18 @@ lemma mk_iUnion_Ordinal_lift_le_of_le {β : Type v} {o : Ordinal.{u}} {c : Cardi
   intro i
   simpa using hA _ i.toOrd.prop
 
-lemma mk_iUnion_Ordinal_le_of_le {β : Type*} {o : Ordinal} {c : Cardinal}
+@[deprecated (since := "2026-01-26")]
+alias mk_iUnion_Ordinal_lift_le_of_le := mk_biUnion_le_of_le_lift
+
+lemma mk_biUnion_le_of_le {β : Type*} {o : Ordinal} {c : Cardinal}
     (ho : o.card ≤ c) (hc : ℵ₀ ≤ c) (A : Ordinal → Set β)
     (hA : ∀ j < o, #(A j) ≤ c) : #(⋃ j < o, A j) ≤ c := by
-  apply mk_iUnion_Ordinal_lift_le_of_le _ hc A hA
+  apply mk_biUnion_le_of_le_lift _ hc A hA
   rwa [Cardinal.lift_le]
 
+@[deprecated (since := "2026-01-26")]
+alias mk_iUnion_Ordinal_le_of_le := mk_biUnion_le_of_le
+
 end Cardinal
 
 /-! ### Cardinality of ordinals -/