chore(SetTheory/Cardinal/Arithmetic): generalize card_iSup_Iio_le_sum_card (leanprover-community#19727)

The theorem becomes strictly more general at zero cost by letting the domain of the function be `Iio o` rather than `Ordinal`.

Author: vihdzp

Mathlib/SetTheory/Cardinal/Arithmetic.lean

@@ -869,16 +869,16 @@ theorem card_iSup_le_sum_card {ι : Type u} (f : ι → Ordinal.{max u v}) :
   have := lift_card_iSup_le_sum_card f
   rwa [Cardinal.lift_id'] at this
 
-theorem card_iSup_Iio_le_sum_card {o : Ordinal.{u}} (f : Ordinal.{u} → Ordinal.{max u v}) :
+theorem card_iSup_Iio_le_sum_card {o : Ordinal.{u}} (f : Iio o → Ordinal.{max u v}) :
     (⨆ a : Iio o, f a).card ≤ Cardinal.sum fun i ↦ (f ((enumIsoToType o).symm i)).card := by
   apply le_of_eq_of_le (congr_arg _ _).symm (card_iSup_le_sum_card _)
-  simpa using (enumIsoToType o).symm.iSup_comp (g := fun x ↦ f x.1)
+  simpa using (enumIsoToType o).symm.iSup_comp (g := fun x ↦ f x)
 
-theorem card_iSup_Iio_le_card_mul_iSup {o : Ordinal.{u}} (f : Ordinal.{u} → Ordinal.{max u v}) :
+theorem card_iSup_Iio_le_card_mul_iSup {o : Ordinal.{u}} (f : Iio o → Ordinal.{max u v}) :
     (⨆ a : Iio o, f a).card ≤ Cardinal.lift.{v} o.card * ⨆ a : Iio o, (f a).card := by
   apply (card_iSup_Iio_le_sum_card f).trans
   convert ← sum_le_iSup_lift _
   · exact mk_toType o
-  · exact (enumIsoToType o).symm.iSup_comp (g := fun x ↦ (f x.1).card)
+  · exact (enumIsoToType o).symm.iSup_comp (g := fun x ↦ (f x).card)
 
 end Ordinal