no goals
α : Type u_1
inst✝² : Group α
s✝ t : Subgroup α
inst✝¹ : Fintype α
s : Subgroup α
inst✝ : Fintype { x // x ∈ s }
⊢ Fintype.card { x // x ∈ s } ∣ Fintype.card α
classical simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_left ℕ]
no goals
α : Type u_1
inst✝² : Group α
s✝ t : Subgroup α
inst✝¹ : Fintype α
s : Subgroup α
inst✝ : Fintype { x // x ∈ s }
⊢ Fintype.card { x // x ∈ s } ∣ Fintype.card α
simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_left ℕ]