-- Module: Mathlib.GroupTheory.ClassEquation
Goal:
G : Type u_1
inst : Group G
inst_1 : Finite G
intro :
  ∀ (val : Fintype G),
    Nat.card.{u_1} ↥(Subgroup.center G) +
        ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
          Nat.card.{u_1} (↑x.carrier : Type u_1) =
      Nat.card G
intro₁ :
  ∀ (val : Fintype G),
    Nat.card.{u_1} ↥(Subgroup.center G) +
        ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
          Nat.card.{u_1} (↑x.carrier : Type u_1) =
      HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), x.carrier.toFinset.card)
        (∑ x ∈ Set.toFinset (noncenter G), x.carrier.toFinset.card)
intro₂ :
  ∀ (val : Fintype G),
    Fintype.card.{u_1} ↥(Subgroup.center G) +
        ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
          Fintype.card.{u_1} (↑x.carrier : Type u_1) =
      HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
        (∑ x ∈ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
intro₃ :
  ∀ (val : Fintype G),
    Fintype.card.{u_1} ↥(Subgroup.center G) =
      ∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1)
intro₄ intro₅ :
  ∀ (val : Fintype G),
    Eq (α := ℕ)
      (∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
        Fintype.card.{u_1} (↑x.carrier : Type u_1))
      (∑ x ∈ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
intro₆ intro₇ :
  ∀ (val : Fintype G),
    Fintype.card.{u_1} ↥(Subgroup.center G) =
      ∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1)
intro₈ :
  ∀ (val : Fintype G),
    Finset.card (α := ConjClasses G) (Finset.univ \ Set.toFinset (noncenter G)) =
      ∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1)
intro₉ :
  ∀ (val : Fintype G),
    Eq (α := ℕ) (∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), 1)
      (∑ x ∈ Finset.univ \ Set.toFinset (noncenter G), Fintype.card.{u_1} (↑x.carrier : Type u_1))
intro₁₀ :
  ∀ (val : Fintype G) (x : ConjClasses G),
    Membership.mem (γ := Finset (ConjClasses G)) (Finset.univ \ Set.toFinset (noncenter G)) x →
      1 = Fintype.card.{u_1} (↑x.carrier : Type u_1)
intro₁₁ :
  ∀ (val : Fintype G) (x : ConjClasses G) (g : G)
    (hg :
      Membership.mem (γ := Finset (ConjClasses G)) (Finset.univ \ Set.toFinset (noncenter G))
        (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)),
    1 = Fintype.card.{u_1} (↑(carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)) : Type u_1)
intro₁₂ :
  ∀ (val : Fintype G) (x : ConjClasses G) (g : G)
    (hg : (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton),
    1 = Fintype.card.{u_1} (↑(carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)) : Type u_1)
intro₁₃ :
  ∀ (val : Fintype G) (x : ConjClasses G) (g : G)
    (hg : (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).Subsingleton),
    ∃ (a : G), (carrier (Quot.mk (⇑(IsConj.setoid G) : G → G → Prop) g)).toFinset = {a}
⊢ Nat.card.{u_1} ↥(Subgroup.center G) +
      ∑ᶠ (x : ConjClasses G) (_ : Membership.mem (γ := Set (ConjClasses G)) (noncenter G) x),
        Nat.card.{u_1} (↑x.carrier : Type u_1) =
    Nat.card G

Tactic:
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.toFinset_setOf, Finset.mem_univ, true_and,
             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⟩

Premises used: Finset.mem_univ, finsum_cond_eq_sum_of_cond_iff, Finset.card_eq_one, Finset.card_eq_sum_ones, sum_conjClasses_card_eq_card, Set.toFinset_card, eq_comm, Finset.mem_sdiff, nonempty_fintype, Set.not_nontrivial_iff, Finset.mem_filter, Set.mem_toFinset, Finset.sum_congr, Set.toFinset_setOf, ConjClasses.noncenter, rfl, true_and, Nat.card_eq_fintype_card