no goals
G✝ : Type ?u.118962
inst✝⁴ : Group G✝
H✝ K L : Subgroup G✝
G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : Fintype G
inst✝ : Fintype H
f : G →* H
hf : Function.Surjective ↑f
⊢ Fintype.card H ∣ Fintype.card G
simp only [← Nat.card_eq_fintype_card, nat_card_dvd_of_surjective f hf]