no goals
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : Fintype G
⊢ index H ∣ Fintype.card G
classical exact ⟨Fintype.card H, H.index_mul_card.symm⟩
no goals
G : Type u_1
inst✝¹ : Group G
H K L : Subgroup G
inst✝ : Fintype G
⊢ index H ∣ Fintype.card G
exact ⟨Fintype.card H, H.index_mul_card.symm⟩