have := calc
  card (G ⧸ H) * card H = card G := by rw [← H.index_eq_card, H.index_mul_card]
  _                     = card K * card H := by rw [h', mul_comm]
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : Fintype G
h' : card G = card ↥H * card ↥K
⊢ card (G ⧸ H) = card ↥K
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
inst✝ : Fintype G
h' : card G = card ↥H * card ↥K
this : card (G ⧸ H) * card ↥H = card ↥K * card ↥H
⊢ card (G ⧸ H) = card ↥K