[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype (ConjClasses G)
inst✝¹ : Fintype G
inst✝ : (x : ConjClasses G) → Fintype ↑(carrier x)
⊢ ∑ x : ConjClasses G, Finset.card (Set.toFinset (carrier x)) = Fintype.card G
[PROOFSTEP]
suffices : (Σ x : ConjClasses G, x.carrier) ≃ G
[GOAL]
G : Type u
inst✝³ : Group G
inst✝² : Fintype (ConjClasses G)
inst✝¹ : Fintype G
inst✝ : (x : ConjClasses G) → Fintype ↑(carrier x)
this : (x : ConjClasses G) × ↑(carrier x) ≃ G
⊢ ∑ x : ConjClasses G, Finset.card (Set.toFinset (carrier x)) = Fintype.card G
[PROOFSTEP]
simpa using (Fintype.card_congr this)
[GOAL]
case this
G : Type u
inst✝³ : Group G
inst✝² : Fintype (ConjClasses G)
inst✝¹ : Fintype G
inst✝ : (x : ConjClasses G) → Fintype ↑(carrier x)
⊢ (x : ConjClasses G) × ↑(carrier x) ≃ G
[PROOFSTEP]
simpa [carrier_eq_preimage_mk] using Equiv.sigmaFiberEquiv ConjClasses.mk
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
⊢ ∑ᶠ (x : ConjClasses G), Set.ncard (carrier x) = Nat.card G
[PROOFSTEP]
classical
cases nonempty_fintype G
rw [Nat.card_eq_fintype_card, ← sum_conjClasses_card_eq_card, finsum_eq_sum_of_fintype]
simp [Set.ncard_eq_toFinset_card']
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
⊢ ∑ᶠ (x : ConjClasses G), Set.ncard (carrier x) = Nat.card G
[PROOFSTEP]
cases nonempty_fintype G
[GOAL]
case intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ᶠ (x : ConjClasses G), Set.ncard (carrier x) = Nat.card G
[PROOFSTEP]
rw [Nat.card_eq_fintype_card, ← sum_conjClasses_card_eq_card, finsum_eq_sum_of_fintype]
[GOAL]
case intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ i : ConjClasses G, Set.ncard (carrier i) = ∑ x : ConjClasses G, Finset.card (Set.toFinset (carrier x))
[PROOFSTEP]
simp [Set.ncard_eq_toFinset_card']
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
⊢ Nat.card { x // x ∈ Subgroup.center G } + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑(carrier x) =
    Nat.card G
[PROOFSTEP]
classical
cases nonempty_fintype G
rw [@Nat.card_eq_fintype_card G, ← sum_conjClasses_card_eq_card, ←
  Finset.sum_sdiff (ConjClasses.noncenter G).toFinset.subset_univ]
simp only [Nat.card_eq_fintype_card, Set.toFinset_card]
congr 1
swap
· convert finsum_cond_eq_sum_of_cond_iff _ _
  simp [Set.mem_toFinset]
calc
  Fintype.card (Subgroup.center G) = Fintype.card ((noncenter G)ᶜ : Set _) := Fintype.card_congr ((mk_bijOn G).equiv _)
  _ = Finset.card (Finset.univ \ (noncenter G).toFinset) := by
    rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]
  _ = _ := ?_
rw [Finset.card_eq_sum_ones]
refine Finset.sum_congr rfl ?_
rintro ⟨g⟩ hg
simp only [noncenter, Set.not_subsingleton_iff, Set.toFinset_setOf, Finset.mem_univ, true_and, forall_true_left,
  Finset.mem_sdiff, Finset.mem_filter, Set.not_nontrivial_iff] at hg 
rw [eq_comm, ← Set.toFinset_card, Finset.card_eq_one]
exact ⟨g, Finset.coe_injective <| by simpa using hg.eq_singleton_of_mem mem_carrier_mk⟩
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
⊢ Nat.card { x // x ∈ Subgroup.center G } + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑(carrier x) =
    Nat.card G
[PROOFSTEP]
cases nonempty_fintype G
[GOAL]
case intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Nat.card { x // x ∈ Subgroup.center G } + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑(carrier x) =
    Nat.card G
[PROOFSTEP]
rw [@Nat.card_eq_fintype_card G, ← sum_conjClasses_card_eq_card, ←
  Finset.sum_sdiff (ConjClasses.noncenter G).toFinset.subset_univ]
[GOAL]
case intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Nat.card { x // x ∈ Subgroup.center G } + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑(carrier x) =
    ∑ x in Finset.univ \ Set.toFinset (noncenter G), Finset.card (Set.toFinset (carrier x)) +
      ∑ x in Set.toFinset (noncenter G), Finset.card (Set.toFinset (carrier x))
[PROOFSTEP]
simp only [Nat.card_eq_fintype_card, Set.toFinset_card]
[GOAL]
case intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Fintype.card { x // x ∈ Subgroup.center G } +
      ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Fintype.card ↑(carrier x) =
    ∑ x in Finset.univ \ Set.toFinset (noncenter G), Fintype.card ↑(carrier x) +
      ∑ x in Set.toFinset (noncenter G), Fintype.card ↑(carrier x)
[PROOFSTEP]
congr 1
[GOAL]
case intro.e_a
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Fintype.card { x // x ∈ Subgroup.center G } =
    ∑ x in Finset.univ \ Set.toFinset (noncenter G), Fintype.card ↑(carrier x)
case intro.e_a
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Fintype.card ↑(carrier x) =
    ∑ x in Set.toFinset (noncenter G), Fintype.card ↑(carrier x)
[PROOFSTEP]
swap
[GOAL]
case intro.e_a
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Fintype.card ↑(carrier x) =
    ∑ x in Set.toFinset (noncenter G), Fintype.card ↑(carrier x)
[PROOFSTEP]
convert finsum_cond_eq_sum_of_cond_iff _ _
[GOAL]
case intro.e_a.convert_7
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∀ {x : ConjClasses G}, Fintype.card ↑(carrier x) ≠ 0 → (x ∈ noncenter G ↔ x ∈ Set.toFinset (noncenter G))
[PROOFSTEP]
simp [Set.mem_toFinset]
[GOAL]
case intro.e_a
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Fintype.card { x // x ∈ Subgroup.center G } =
    ∑ x in Finset.univ \ Set.toFinset (noncenter G), Fintype.card ↑(carrier x)
[PROOFSTEP]
calc
  Fintype.card (Subgroup.center G) = Fintype.card ((noncenter G)ᶜ : Set _) := Fintype.card_congr ((mk_bijOn G).equiv _)
  _ = Finset.card (Finset.univ \ (noncenter G).toFinset) := by
    rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]
  _ = _ := ?_
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Fintype.card ↑(noncenter G)ᶜ = Finset.card (Finset.univ \ Set.toFinset (noncenter G))
[PROOFSTEP]
rw [← Set.toFinset_card, Set.toFinset_compl, Finset.compl_eq_univ_sdiff]
[GOAL]
case intro.e_a
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Finset.card (Finset.univ \ Set.toFinset (noncenter G)) =
    ∑ x in Finset.univ \ Set.toFinset (noncenter G), Fintype.card ↑(carrier x)
[PROOFSTEP]
rw [Finset.card_eq_sum_ones]
[GOAL]
case intro.e_a
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ x in Finset.univ \ Set.toFinset (noncenter G), 1 =
    ∑ x in Finset.univ \ Set.toFinset (noncenter G), Fintype.card ↑(carrier x)
[PROOFSTEP]
refine Finset.sum_congr rfl ?_
[GOAL]
case intro.e_a
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∀ (x : ConjClasses G), x ∈ Finset.univ \ Set.toFinset (noncenter G) → 1 = Fintype.card ↑(carrier x)
[PROOFSTEP]
rintro ⟨g⟩ hg
[GOAL]
case intro.e_a.mk
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : Quot.mk Setoid.r g ∈ Finset.univ \ Set.toFinset (noncenter G)
⊢ 1 = Fintype.card ↑(carrier (Quot.mk Setoid.r g))
[PROOFSTEP]
simp only [noncenter, Set.not_subsingleton_iff, Set.toFinset_setOf, Finset.mem_univ, true_and, forall_true_left,
  Finset.mem_sdiff, Finset.mem_filter, Set.not_nontrivial_iff] at hg 
[GOAL]
case intro.e_a.mk
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : Set.Subsingleton (carrier (Quot.mk Setoid.r g))
⊢ 1 = Fintype.card ↑(carrier (Quot.mk Setoid.r g))
[PROOFSTEP]
rw [eq_comm, ← Set.toFinset_card, Finset.card_eq_one]
[GOAL]
case intro.e_a.mk
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : Set.Subsingleton (carrier (Quot.mk Setoid.r g))
⊢ ∃ a, Set.toFinset (carrier (Quot.mk Setoid.r g)) = {a}
[PROOFSTEP]
exact ⟨g, Finset.coe_injective <| by simpa using hg.eq_singleton_of_mem mem_carrier_mk⟩
[GOAL]
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : Set.Subsingleton (carrier (Quot.mk Setoid.r g))
⊢ ↑(Set.toFinset (carrier (Quot.mk Setoid.r g))) = ↑{g}
[PROOFSTEP]
simpa using hg.eq_singleton_of_mem mem_carrier_mk
[GOAL]
G✝ : Type u
inst✝⁵ : Group G✝
G : Type u_1
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑(carrier x)
inst✝² : Fintype G
inst✝¹ : Fintype { x // x ∈ Subgroup.center G }
inst✝ : Fintype ↑(noncenter G)
⊢ Fintype.card { x // x ∈ Subgroup.center G } +
      ∑ x in Set.toFinset (noncenter G), Finset.card (Set.toFinset (carrier x)) =
    Fintype.card G
[PROOFSTEP]
convert Group.nat_card_center_add_sum_card_noncenter_eq_card G using 2
[GOAL]
case h.e'_2.h.e'_5
G✝ : Type u
inst✝⁵ : Group G✝
G : Type u_1
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑(carrier x)
inst✝² : Fintype G
inst✝¹ : Fintype { x // x ∈ Subgroup.center G }
inst✝ : Fintype ↑(noncenter G)
⊢ Fintype.card { x // x ∈ Subgroup.center G } = Nat.card { x // x ∈ Subgroup.center G }
[PROOFSTEP]
simp
[GOAL]
case h.e'_2.h.e'_6
G✝ : Type u
inst✝⁵ : Group G✝
G : Type u_1
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑(carrier x)
inst✝² : Fintype G
inst✝¹ : Fintype { x // x ∈ Subgroup.center G }
inst✝ : Fintype ↑(noncenter G)
⊢ ∑ x in Set.toFinset (noncenter G), Finset.card (Set.toFinset (carrier x)) =
    ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑(carrier x)
[PROOFSTEP]
rw [← finsum_set_coe_eq_finsum_mem (noncenter G), finsum_eq_sum_of_fintype, ← Finset.sum_set_coe]
[GOAL]
case h.e'_2.h.e'_6
G✝ : Type u
inst✝⁵ : Group G✝
G : Type u_1
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑(carrier x)
inst✝² : Fintype G
inst✝¹ : Fintype { x // x ∈ Subgroup.center G }
inst✝ : Fintype ↑(noncenter G)
⊢ ∑ i : ↑(noncenter G), Finset.card (Set.toFinset (carrier ↑i)) = ∑ i : ↑(noncenter G), Nat.card ↑(carrier ↑i)
[PROOFSTEP]
simp
[GOAL]
case h.e'_3
G✝ : Type u
inst✝⁵ : Group G✝
G : Type u_1
inst✝⁴ : Group G
inst✝³ : (x : ConjClasses G) → Fintype ↑(carrier x)
inst✝² : Fintype G
inst✝¹ : Fintype { x // x ∈ Subgroup.center G }
inst✝ : Fintype ↑(noncenter G)
⊢ Fintype.card G = Nat.card G
[PROOFSTEP]
simp
