Theorem: aux_card_eq (LeanCourse/MIL/C08_Groups_and_Rings/solutions/Solutions_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:
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]
State after:
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)

State before:
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)
Tactic:
exact Nat.eq_of_mul_eq_mul_right card_pos this
State after:
no goals

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 (↥H) = card G
Tactic:
rw [← H.index_eq_card, H.index_mul_card]
State after:
no goals

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 = card (↥K) * card (↥H)
Tactic:
rw [h', mul_comm]
State after:
no goals