α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
this : Perm α ⧸ MonoidHom.ker sign ≃ ℤˣ :=
  (QuotientGroup.quotientKerEquivOfSurjective sign (_ : Function.Surjective ↑sign)).toEquiv
⊢ 2 * card { x // x ∈ alternatingGroup α } = card (Perm α)
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
⊢ 2 * card { x // x ∈ alternatingGroup α } = card (Perm α)
let this := (QuotientGroup.quotientKerEquivOfSurjective _ (sign_surjective α)).toEquiv
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
this : Perm α ⧸ MonoidHom.ker sign ≃ ℤˣ :=
  (QuotientGroup.quotientKerEquivOfSurjective sign (_ : Function.Surjective ↑sign)).toEquiv
⊢ card (Perm α ⧸ MonoidHom.ker sign) * card { x // x ∈ alternatingGroup α } = card (Perm α)
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
this : Perm α ⧸ MonoidHom.ker sign ≃ ℤˣ :=
  (QuotientGroup.quotientKerEquivOfSurjective sign (_ : Function.Surjective ↑sign)).toEquiv
⊢ 2 * card { x // x ∈ alternatingGroup α } = card (Perm α)
rw [← Fintype.card_units_int, ← Fintype.card_congr this]
no goals
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
this : Perm α ⧸ MonoidHom.ker sign ≃ ℤˣ :=
  (QuotientGroup.quotientKerEquivOfSurjective sign (_ : Function.Surjective ↑sign)).toEquiv
⊢ card (Perm α ⧸ MonoidHom.ker sign) * card { x // x ∈ alternatingGroup α } = card (Perm α)
apply (Subgroup.card_eq_card_quotient_mul_card_subgroup _).symm