-- Mathlib/GroupTheory/ClassEquation.lean
theorem Group.nat_card_center_add_sum_card_noncenter_eq_card [Finite G] :
    Nat.card (Subgroup.center G) + ∑ᶠ x ∈ noncenter G, Nat.card x.carrier = Nat.card G

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ Nat.card ↥(Subgroup.center G) + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑x.carrier = Nat.card G

Tactic:
cases nonempty_fintype G

Result:
case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Nat.card ↥(Subgroup.center G) + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑x.carrier = Nat.card G

Proof state:
case intro.e_a.mk
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : Quot.mk (⇑(IsConj.setoid G)) g ∈ Finset.univ \ (noncenter G).toFinset
⊢ 1 = Fintype.card ↑(carrier (Quot.mk (⇑(IsConj.setoid G)) g))

Tactic:
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

Result:
case intro.e_a.mk
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ 1 = Fintype.card ↑(carrier (Quot.mk (⇑(IsConj.setoid G)) g))

Proof state:
case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ x ∈ Finset.univ \ (noncenter G).toFinset, 1 = ∑ x ∈ Finset.univ \ (noncenter G).toFinset, Fintype.card ↑x.carrier

Tactic:
refine Finset.sum_congr rfl ?_

Result:
case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∀ x ∈ Finset.univ \ (noncenter G).toFinset, 1 = Fintype.card ↑x.carrier

Proof state:
case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Fintype.card ↥(Subgroup.center G) + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Fintype.card ↑x.carrier =
    ∑ x ∈ Finset.univ \ (noncenter G).toFinset, Fintype.card ↑x.carrier +
      ∑ x ∈ (noncenter G).toFinset, Fintype.card ↑x.carrier

Tactic:
congr 1

Result:
case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Fintype.card ↥(Subgroup.center G) = ∑ x ∈ Finset.univ \ (noncenter G).toFinset, Fintype.card ↑x.carrier

case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Fintype.card ↑x.carrier =
    ∑ x ∈ (noncenter G).toFinset, Fintype.card ↑x.carrier

Proof state:
case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Fintype.card ↥(Subgroup.center G) = ∑ x ∈ Finset.univ \ (noncenter G).toFinset, Fintype.card ↑x.carrier

case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Fintype.card ↑x.carrier =
    ∑ x ∈ (noncenter G).toFinset, Fintype.card ↑x.carrier

Tactic:
swap

Result:
case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Fintype.card ↑x.carrier =
    ∑ x ∈ (noncenter G).toFinset, Fintype.card ↑x.carrier

case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Fintype.card ↥(Subgroup.center G) = ∑ x ∈ Finset.univ \ (noncenter G).toFinset, Fintype.card ↑x.carrier

Proof state:
case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Nat.card ↥(Subgroup.center G) + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑x.carrier =
    ∑ x ∈ Finset.univ \ (noncenter G).toFinset, x.carrier.toFinset.card +
      ∑ x ∈ (noncenter G).toFinset, x.carrier.toFinset.card

Tactic:
simp only [Nat.card_eq_fintype_card, Set.toFinset_card]

Result:
case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Fintype.card ↥(Subgroup.center G) + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Fintype.card ↑x.carrier =
    ∑ x ∈ Finset.univ \ (noncenter G).toFinset, Fintype.card ↑x.carrier +
      ∑ x ∈ (noncenter G).toFinset, Fintype.card ↑x.carrier

Proof state:
case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Nat.card ↥(Subgroup.center G) + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑x.carrier = Nat.card G

Tactic:
rw [@Nat.card_eq_fintype_card G, ← sum_conjClasses_card_eq_card, ←
  Finset.sum_sdiff (ConjClasses.noncenter G).toFinset.subset_univ]

Result:
case intro
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Nat.card ↥(Subgroup.center G) + ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Nat.card ↑x.carrier =
    ∑ x ∈ Finset.univ \ (noncenter G).toFinset, x.carrier.toFinset.card +
      ∑ x ∈ (noncenter G).toFinset, x.carrier.toFinset.card

Proof state:
case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ᶠ (x : ConjClasses G) (_ : x ∈ noncenter G), Fintype.card ↑x.carrier =
    ∑ x ∈ (noncenter G).toFinset, Fintype.card ↑x.carrier

Tactic:
convert finsum_cond_eq_sum_of_cond_iff _ _

Result:
case intro.e_a.convert_7
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∀ {x : ConjClasses G}, Fintype.card ↑x.carrier ≠ 0 → (x ∈ noncenter G ↔ x ∈ (noncenter G).toFinset)

Proof state:
case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∀ x ∈ Finset.univ \ (noncenter G).toFinset, 1 = Fintype.card ↑x.carrier

Tactic:
rintro ⟨g⟩ hg

Result:
case intro.e_a.mk
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : Quot.mk (⇑(IsConj.setoid G)) g ∈ Finset.univ \ (noncenter G).toFinset
⊢ 1 = Fintype.card ↑(carrier (Quot.mk (⇑(IsConj.setoid G)) g))

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ ↑(carrier (Quot.mk (⇑(IsConj.setoid G)) g)).toFinset = ↑{g}

Tactic:
simpa using hg.eq_singleton_of_mem mem_carrier_mk

Result:
no goals

Proof state:
case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ (Finset.univ \ (noncenter G).toFinset).card = ∑ x ∈ Finset.univ \ (noncenter G).toFinset, Fintype.card ↑x.carrier

Tactic:
rw [Finset.card_eq_sum_ones]

Result:
case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ ∑ x ∈ Finset.univ \ (noncenter G).toFinset, 1 = ∑ x ∈ Finset.univ \ (noncenter G).toFinset, Fintype.card ↑x.carrier

Proof state:
case intro.e_a.mk
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ 1 = Fintype.card ↑(carrier (Quot.mk (⇑(IsConj.setoid G)) g))

Tactic:
rw [eq_comm, ← Set.toFinset_card, Finset.card_eq_one]

Result:
case intro.e_a.mk
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ ∃ a, (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).toFinset = {a}

Proof state:
case intro.e_a.mk
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
x✝ : ConjClasses G
g : G
hg : (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).Subsingleton
⊢ ∃ a, (carrier (Quot.mk (⇑(IsConj.setoid G)) g)).toFinset = {a}

Tactic:
exact ⟨g, Finset.coe_injective <| by simpa using hg.eq_singleton_of_mem mem_carrier_mk⟩

Result:
no goals

Proof state:
case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ Fintype.card ↥(Subgroup.center G) = ∑ x ∈ Finset.univ \ (noncenter G).toFinset, Fintype.card ↑x.carrier

Tactic:
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]
  _ = _ := ?_

Result:
case intro.e_a
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
val✝ : Fintype G
⊢ (Finset.univ \ (noncenter G).toFinset).card = ∑ x ∈ Finset.univ \ (noncenter G).toFinset, Fintype.card ↑x.carrier