-- Lean 4 proof step from Mathlib.GroupTheory.ClassEquation (goal)
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)
⊢ 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
have 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))
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⟩