cases fintypeOrInfinite G
G : Type u_1
inst✝ : Group G
⊢ d1224 G ∣ Nat.card G
case inl
G : Type u_1
inst✝ : Group G
val✝ : Fintype G
⊢ d1224 G ∣ Nat.card G

case inr
G : Type u_1
inst✝ : Group G
val✝ : Infinite G
⊢ d1224 G ∣ Nat.card G