rw [Nat.card_eq_fintype_card, Fintype.card_pos_iff]
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
this : Fintype ↥H
⊢ 0 < Nat.card ↥H
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
this : Fintype ↥H
⊢ Nonempty ↥H