α : Type u_2
inst✝³ : Group α
s t : Subgroup α
H : Type u_1
inst✝² : Group H
K : Subgroup H
inst✝¹ : Fintype { x // x ∈ K }
f : α →* H
inst✝ : Fintype { x // x ∈ comap f K }
hf : Injective ↑f
this : Fintype { x // x ∈ map f (comap f K) }
⊢ card { x // x ∈ comap f K } ∣ card { x // x ∈ K }
α : Type u_2
inst✝³ : Group α
s t : Subgroup α
H : Type u_1
inst✝² : Group H
K : Subgroup H
inst✝¹ : Fintype { x // x ∈ K }
f : α →* H
inst✝ : Fintype { x // x ∈ comap f K }
hf : Injective ↑f
⊢ card { x // x ∈ comap f K } ∣ card { x // x ∈ K }
haveI : Fintype ((K.comap f).map f) :=
    Fintype.ofEquiv _ (equivMapOfInjective _ _ hf).toEquiv
no goals
α : Type u_2
inst✝³ : Group α
s t : Subgroup α
H : Type u_1
inst✝² : Group H
K : Subgroup H
inst✝¹ : Fintype { x // x ∈ K }
f : α →* H
inst✝ : Fintype { x // x ∈ comap f K }
hf : Injective ↑f
this : Fintype { x // x ∈ map f (comap f K) }
⊢ card { x // x ∈ comap f K } ∣ card { x // x ∈ K }
calc
  Fintype.card (K.comap f) = Fintype.card ((K.comap f).map f) :=
    Fintype.card_congr (equivMapOfInjective _ _ hf).toEquiv
  _ ∣ Fintype.card K := card_dvd_of_le (map_comap_le _ _)