Lemmas about Nat.card and ENNReal

@[simp]

theorem ENNReal.toReal_enatCard (α : Type u_1) : (↑(ENat.card α)).toReal = ↑(Nat.card α)