∀ (Γ : Type u_1) (R : Type u_2) (κ : Cardinal.{u_1}) [inst : PartialOrder Γ] [inst_1 : AddMonoid R]
  [hκ : Fact (Cardinal.aleph0 ≤ κ)], ↑(HahnSeries.cardSuppLTAddSubmonoid Γ R κ) = {x | x.cardSupp < κ}