-- Mathlib/GroupTheory/PGroup.lean
theorem card_modEq_card_fixedPoints : Nat.card α ≡ Nat.card (fixedPoints G α) [MOD p]

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
x : α
⊢ card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)

Tactic:
simp only [Quotient.eq'']

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
x : α
⊢ card { y // (orbitRel G α) y x } = card ↑(orbit G x)

Proof state:
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝¹ : Fintype α
this✝ : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
k : ℕ
hk : card ↑(orbit G b) = p ^ k
this : k = 0
⊢ ∃ a, ∃ (h₁ : a ∈ Finset.univ) (h₂ : ↑1 ≠ 0), (fun a x x => Quotient.mk'' ↑a) a h₁ h₂ = Quotient.mk'' b

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

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
⊢ card α ≡ card ↑(fixedPoints G α) [MOD p]

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

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
⊢ ∑ a : Quotient (orbitRel G α), card { x // Quotient.mk'' x = a } ≡ ∑ _a : ↑(fixedPoints G α), 1 [MOD p]

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
⊢ ∑ a : Quotient (orbitRel G α), card { x // Quotient.mk'' x = a } ≡ ∑ _a : ↑(fixedPoints G α), 1 [MOD p]

Tactic:
rw [← ZMod.eq_iff_modEq_nat p, Nat.cast_sum, Nat.cast_sum]

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
⊢ ∑ x : Quotient (orbitRel G α), ↑(card { x_1 // Quotient.mk'' x_1 = x }) = ∑ x : ↑(fixedPoints G α), ↑1

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
⊢ ∑ x : Quotient (orbitRel G α), ↑(card { x_1 // Quotient.mk'' x_1 = x }) = ∑ x : ↑(fixedPoints G α), ↑1

Tactic:
refine
  Eq.symm
    (Finset.sum_bij_ne_zero (fun a _ _ => Quotient.mk'' a.1) (fun _ _ _ => Finset.mem_univ _)
      (fun a₁ _ _ a₂ _ _ h =>
        Subtype.eq (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])

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
⊢ ∃ a, ∃ (h₁ : a ∈ Finset.univ) (h₂ : ↑1 ≠ 0), (fun a x x => Quotient.mk'' ↑a) a h₁ h₂ = Quotient.mk'' b

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
⊢ ∃ a, ∃ (h₁ : a ∈ Finset.univ) (h₂ : ↑1 ≠ 0), (fun a x x => Quotient.mk'' ↑a) a h₁ h₂ = Quotient.mk'' b

Tactic:
obtain ⟨k, hk⟩ := hG.card_orbit b

Result:
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
k : ℕ
hk : Nat.card ↑(orbit G b) = p ^ k
⊢ ∃ a, ∃ (h₁ : a ∈ Finset.univ) (h₂ : ↑1 ≠ 0), (fun a x x => Quotient.mk'' ↑a) a h₁ h₂ = Quotient.mk'' b

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
⊢ Nat.card α ≡ Nat.card ↑(fixedPoints G α) [MOD p]

Tactic:
have := Fintype.ofFinite α

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this : Fintype α
⊢ Nat.card α ≡ Nat.card ↑(fixedPoints G α) [MOD p]

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
⊢ Nat.card α ≡ Nat.card ↑(fixedPoints G α) [MOD p]

Tactic:
rw [Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
⊢ card α ≡ card ↑(fixedPoints G α) [MOD p]

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
this✝ : Fintype α
this : Fintype ↑(fixedPoints G α)
⊢ card α ≡ card ↑(fixedPoints G α) [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.eq_iff_modEq_nat 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.eq (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 [-Quotient.eq, 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⟩

Result:
no goals