rw [← Subgroup.card_mul_index H, Nat.mul_div_cancel_left _ this, Subgroup.index]
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
H : Subgroup G
this✝ : Fintype ↥H
this : 0 < Nat.card ↥H
⊢ Nat.card (G ⧸ H) = Nat.card G / Nat.card ↥H
no goals