no goals
α : Type u_1
inst✝² : Group α
s✝ t : Subgroup α
inst✝¹ : Fintype α
s : Subgroup α
inst✝ : DecidablePred fun x => x ∈ s
⊢ Fintype.card (α ⧸ s) ∣ Fintype.card α
simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_right ℕ]