have : 0 < Nat.card H := by
  rw [Nat.card_eq_fintype_card, Fintype.card_pos_iff]
  exact ⟨⟨1, one_mem _⟩⟩
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
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