-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst_1 : MulAction G α
inst_2 : Finite α
this_1 : Fintype α
this : Fintype (↑(fixedPoints G α) : Type u_2)
card : ∑ _a : (↑(fixedPoints G α) : Type u_2), 1 = Fintype.card.{u_2} (↑(fixedPoints G α) : Type u_2)
card₁ :
  ∑ a : Quotient (orbitRel G α), Fintype.card.{u_2} { x : α // Quotient.mk'' x = a } ≡
    ∑ _a : (↑(fixedPoints G α) : Type u_2), 1 [MOD p]
card₂ :
  Eq (α := ZMod p)
    (∑ x : Quotient (orbitRel G α), (↑(Fintype.card.{u_2} { x_1 : α // Quotient.mk'' x_1 = x }) : ZMod p))
    (∑ x : (↑(fixedPoints G α) : Type u_2), (↑1 : ZMod p))
card₃ :
  ∀
    (key :
      ∀ (x : α),
        Fintype.card.{u_2} { y : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' y) (Quotient.mk'' x) } =
          Fintype.card.{u_2} (↑(orbit G x) : Type u_2)),
    Eq (α := ZMod p)
      (∑ x : Quotient (orbitRel G α), (↑(Fintype.card.{u_2} { x_1 : α // Quotient.mk'' x_1 = x }) : ZMod p))
      (∑ x : (↑(fixedPoints G α) : Type u_2), (↑1 : ZMod p))
⊢ Fintype.card α ≡ Fintype.card.{u_2} (↑(fixedPoints G α) : Type u_2) [MOD p]
have card₄ : ∀
  (key :
    ∀ (x : α),
      Fintype.card.{u_2} { y : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' y) (Quotient.mk'' x) } =
        Fintype.card.{u_2} (↑(orbit G x) : Type u_2))
  (b : Quotient (orbitRel G α)) (b : α),
  Membership.mem (γ := Finset (Quotient (orbitRel G α))) Finset.univ (Quotient.mk'' b) →
    ∀
      (hb :
        Ne (α := ZMod p)
          (↑(Fintype.card.{u_2} { x : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' x) (Quotient.mk'' b) }) :
            ZMod p)
          0),
      ∃ (a : (↑(fixedPoints G α) : Type u_2)) (h₁ :
        Membership.mem (γ := Finset (↑(fixedPoints G α) : Type u_2)) Finset.univ a) (h₂ :
        Ne (α := ZMod p) (↑1 : ZMod p) 0),
        Eq (α := Quotient (orbitRel G α))
          ((fun (a : (↑(fixedPoints G α) : Type u_2))
                (x : Membership.mem (γ := Finset (↑(fixedPoints G α) : Type u_2)) Finset.univ a)
                (x_1 : Ne (α := ZMod p) (↑1 : ZMod p) 0) ↦
              (Quotient.mk'' (↑a : α) : Quotient (orbitRel G α)))
            a h₁ h₂)
          (Quotient.mk'' b)
Tactic: classical
    calc
      card α = card (Σ y : Quotient (orbitRel G α), { x // Quotient.mk'' x = y }) :=
        card_congr (Equiv.sigmaFiberEquiv (@Quotient.mk'' _ (orbitRel G α))).symm
      _ = ∑ a : Quotient (orbitRel G α), card { x // Quotient.mk'' x = a } := card_sigma
      _ ≡ ∑ _a : fixedPoints G α, 1 [MOD p] := ?_
      _ = _ := by simp
    rw [← ZMod.natCast_eq_natCast_iff _ _ p, Nat.cast_sum, Nat.cast_sum]
    have key :
      ∀ x,
        card { y // (Quotient.mk'' y : Quotient (orbitRel G α)) = Quotient.mk'' x } =
          card (orbit G x) :=
      fun x => by simp only [Quotient.eq'']; congr
    refine
      Eq.symm
        (Finset.sum_bij_ne_zero (fun a _ _ => Quotient.mk'' a.1) (fun _ _ _ => Finset.mem_univ _)
          (fun a₁ _ _ a₂ _ _ h =>
            Subtype.ext (mem_fixedPoints'.mp a₂.2 a₁.1 (Quotient.exact' h)))
          (fun b => Quotient.inductionOn' b fun b _ hb => ?_) fun a ha _ => by
          rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2])
    obtain ⟨k, hk⟩ := hG.card_orbit b
    rw [Nat.card_eq_fintype_card] at hk
    have : k = 0 := by
      contrapose! hb
      simp [key, hk, hb]
    exact
      ⟨⟨b, mem_fixedPoints_iff_card_orbit_eq_one.2 <| by rw [hk, this, pow_zero]⟩,
        Finset.mem_univ _, ne_of_eq_of_ne Nat.cast_one one_ne_zero, rfl⟩