no goals
α : Type u_1
inst✝³ : Group α
s t : Subgroup α
H : Type u_2
inst✝² : Group H
inst✝¹ : Fintype α
inst✝ : Fintype H
f : α →* H
hf : Injective ↑f
⊢ card α ∣ card H
classical calc
    card α = card (f.range : Subgroup H) := card_congr (Equiv.ofInjective f hf)
    _ ∣ card H := card_subgroup_dvd_card _
no goals
α : Type u_1
inst✝³ : Group α
s t : Subgroup α
H : Type u_2
inst✝² : Group H
inst✝¹ : Fintype α
inst✝ : Fintype H
f : α →* H
hf : Injective ↑f
⊢ card α ∣ card H
calc
card α = card (f.range : Subgroup H) := card_congr (Equiv.ofInjective f hf)
_ ∣ card H := card_subgroup_dvd_card _