Theorem: aux_card_eq (LeanCourse/MIL/C08_Groups_and_Rings/S01_Groups.lean)

State before:
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)
Tactic:
sorry
State after:
no goals