-- Module: Mathlib.GroupTheory.PGroup
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))
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)
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)
        (k : ℕ) (hk : Nat.card.{u_2} (↑(orbit G b) : Type u_2) = p ^ k),
        ∃ (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)
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)
        (k : ℕ) (hk : Fintype.card.{u_2} (↑(orbit G b) : Type u_2) = p ^ k),
        ∃ (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)
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)
        (k : ℕ) (hk : Fintype.card.{u_2} (↑(orbit G b) : Type u_2) = p ^ k) (this_2 : k = 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)
⊢ Fintype.card α ≡ Fintype.card.{u_2} (↑(fixedPoints G α) : Type u_2) [MOD p]

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⟩

Premises used: Finset.mem_univ, Quotient.mk'', Fintype.card_sigma, Quotient.inductionOn', Fintype.card, MulAction.orbitRel, Nat.cast_sum, Quotient, Iff.mp, ZMod.natCast_eq_natCast_iff, MulAction.fixedPoints, Finset.sum_bij_ne_zero, MulAction.mem_fixedPoints', Eq.symm, Subtype.val, Nat.card_eq_fintype_card, Subtype.property, Subtype.ext