have : Fintype H := by classical infer_instance
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
⊢ Nat.card (G ⧸ H) = Nat.card G / Nat.card ↥H
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
this : Fintype ↥H
⊢ Nat.card (G ⧸ H) = Nat.card G / Nat.card ↥H