feat(SetTheory/Cardinal/Cofinality): cofinality of Iio interval (leanprover-community#37021)

Author: vihdzp

Mathlib/SetTheory/Cardinal/Cofinality.lean

@@ -256,9 +256,13 @@ theorem lift_cof (o : Ordinal.{u}) : Cardinal.lift.{v} (cof o) = cof (Ordinal.li
   rw [cof_type, ← type_lt_ulift, cof_type, ← Cardinal.lift_id'.{u, v} (Order.cof (ULift _)),
     ← Cardinal.lift_umax, ← ULift.orderIso.lift_cof_congr]
 
+theorem _root_.Order.cof_Iio [LinearOrder α] [WellFoundedLT α] (x : α) :
+    Order.cof (Iio x) = cof (typein (α := α) (· < ·) x) :=
+  (cof_type _).symm
+
 @[simp]
 theorem cof_Iio (o : Ordinal.{u}) : Order.cof (Iio o) = cof (lift.{u + 1} o) := by
-  rw [← lift_cof, ← cof_toType, ← (@ToType.mk o).lift_cof_congr, Cardinal.lift_id'.{u, u + 1}]
+  rw [Order.cof_Iio, typein_ordinal]
 
 theorem cof_le_card (o : Ordinal) : cof o ≤ card o := by
   simpa using cof_le_cardinalMk o.ToType