awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
H : Type u_2
inst_1 : Group H
ϕ : G →* H
hϕ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑ϕ : (a : G) → H)
⊢ IsPGroup p H

Tactic:
fun h => Exists.elim (hϕ h) fun g hg => Exists.imp (fun k hk => ?_) (hG g)

Premises used: IsPGroup, Exists.imp, Exists.elim
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
H : Type u_2
inst_1 : Group H
ϕ : G →* H
hϕ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑ϕ : (a : G) → H)
refine : ∀ (h : H) (g : G) (hg : (ϕ : (a : G) → H) g = h) (k : ℕ) (hk : g ^ p ^ k = 1), h ^ p ^ k = 1
⊢ IsPGroup p H

Tactic:
refine fun h => Exists.elim (hϕ h) fun g hg => Exists.imp (fun k hk => ?_) (hG g)

Premises used: Exists.imp, Exists.elim
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
H : Type u_2
inst_1 : Group H
ϕ : G →* H
hϕ : Function.Surjective.{u_1 + 1, u_2 + 1} (α := G) (β := H) (⇑ϕ : (a : G) → H)
h : H
g : G
hg : (ϕ : (a : G) → H) g = h
k : ℕ
hk : g ^ p ^ k = 1
rw : HPow.hPow (α := H) ((ϕ : (a : G) → H) g : H) (p ^ k) = 1
rw₁ : Eq.{u_2 + 1} (α := H) ((ϕ : (a : G) → H) (g ^ p ^ k) : H) (1 : H)
rw₂ : Eq.{u_2 + 1} (α := H) ((ϕ : (a : G) → H) 1 : H) (1 : H)
rw₃ rw₄ : Eq.{u_2 + 1} (α := H) 1 1
⊢ h ^ p ^ k = 1

Tactic:
rw [← hg, ← ϕ.map_pow, hk, ϕ.map_one]

Premises used: MonoidHom.map_one, MonoidHom.map_pow
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
H : Subgroup G
inst_1 : H.Normal
⊢ IsPGroup.{u_1} p (G ⧸ H)

Tactic:
hG.of_surjective (QuotientGroup.mk' H) Quotient.mk''_surjective

Premises used: IsPGroup.of_surjective, Quotient.mk''_surjective, QuotientGroup.mk'
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
H : Type u_2
inst_1 : Group H
ϕ : G ≃* H
⊢ IsPGroup p H

Tactic:
hG.of_surjective ϕ.toMonoidHom ϕ.surjective

Premises used: IsPGroup.of_surjective, MulEquiv.surjective, MulEquiv.toMonoidHom
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
n : ℕ
hn : p.Coprime n
g : G
⊢ (orderOf g).Coprime n

Tactic:
let ⟨k, hk⟩ := hG g
  (hn.pow_left k).coprime_dvd_left (orderOf_dvd_of_pow_eq_one hk)

Premises used: Nat.Coprime, Nat.Coprime.coprime_dvd_left, orderOf_dvd_of_pow_eq_one, Nat.Coprime.pow_left, orderOf, _private.0.IsPGroup.iff_orderOf.match_1
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
n : ℕ
hn : p.Coprime n
g : G
⊢ (hG.powEquiv hn : (a : G) → G) g = g ^ n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
n : ℕ
hn : p.Coprime n
g : G
rw : ((hG.powEquiv hn).symm : (a : G) → G) g = g ^ (Nat.card.{u_1} ↥(Subgroup.zpowers g)).gcdB n
⊢ ((hG.powEquiv hn).symm : (a : G) → G) g = g ^ (orderOf g).gcdB n

Tactic:
rw [← Nat.card_zpowers]

Premises used: Nat.card_zpowers
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
n : ℕ
hn : p.Coprime n
g : G
⊢ ((hG.powEquiv hn).symm : (a : G) → G) g = g ^ (Nat.card.{u_1} ↥(Subgroup.zpowers g)).gcdB n

Tactic:
rfl
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
H : Subgroup G
inst_1 : H.FiniteIndex
obtain : ∀ (n : ℕ) (hn : Nat.card.{u_1} (G ⧸ H.normalCore) = p ^ n), ∃ (n : ℕ), H.index = p ^ n
⊢ ∃ (n : ℕ), H.index = p ^ n

Tactic:
obtain ⟨n, hn⟩ := iff_card.mp (hG.to_quotient H.normalCore)

Premises used: IsPGroup.to_quotient, IsPGroup.iff_card, Iff.mp, Subgroup.normalCore
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
H : Subgroup G
inst_1 : H.FiniteIndex
n : ℕ
hn : Nat.card.{u_1} (G ⧸ H.normalCore) = p ^ n
obtain : ∀ k ≤ n, ∀ (hk2 : H.index = p ^ k), ∃ (n : ℕ), H.index = p ^ n
⊢ ∃ (n : ℕ), H.index = p ^ n

Tactic:
obtain ⟨k, _, hk2⟩ :=
    (Nat.dvd_prime_pow hp.out).mp
      ((congr_arg _ (H.normalCore.index_eq_card.trans hn)).mp
        (Subgroup.index_dvd_of_le H.normalCore_le))

Premises used: Eq.mp, congr_arg, Subgroup.index_eq_card, Iff.mp, Subgroup.index_dvd_of_le, Subgroup.normalCore, Subgroup.normalCore_le, Fact.out, Eq.trans, Nat.dvd_prime_pow
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
H : Subgroup G
inst_1 : H.FiniteIndex
n : ℕ
hn : Nat.card.{u_1} (G ⧸ H.normalCore) = p ^ n
k : ℕ
left : k ≤ n
hk2 : H.index = p ^ k
⊢ ∃ (n : ℕ), H.index = p ^ n

Tactic:
⟨k, hk2⟩

Premises used: Exists.intro
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
H : Subgroup G
inst_1 : H.FiniteIndex
n : ℕ
hn : Nat.card.{u_1} (G ⧸ H.normalCore) = p ^ n
k : ℕ
left : k ≤ n
hk2 : H.index = p ^ k
⊢ ∃ (n : ℕ), H.index = p ^ n

Tactic:
exact ⟨k, hk2⟩
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inl : Finite G → Nat.card G = 1 ∨ p ∣ Nat.card G
inr : Infinite G → Nat.card G = 1 ∨ p ∣ Nat.card G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G

Tactic:
cases finite_or_infinite G

Premises used: finite_or_infinite
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h : Finite G
inl : ∀ (n : ℕ) (hn : Nat.card G = p ^ n), Nat.card G = 1 ∨ p ∣ Nat.card G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G

Tactic:
obtain ⟨n, hn⟩ := iff_card.mp hG

Premises used: IsPGroup.iff_card, Iff.mp
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h : Finite G
n : ℕ
hn : Nat.card G = p ^ n
inl : p ^ n = 1 ∨ p ∣ p ^ n
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G

Tactic:
rw [hn]
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h : Finite G
n : ℕ
hn : Nat.card G = p ^ n
inl : ∀ (hn : Nat.card G = HPow.hPow (β := ℕ) p 0), HPow.hPow (β := ℕ) p 0 = 1 ∨ p ∣ HPow.hPow (β := ℕ) p 0
inl₁ : ∀ (n : ℕ) (hn : Nat.card G = p ^ (n + 1)), p ^ (n + 1) = 1 ∨ p ∣ p ^ (n + 1)
⊢ p ^ n = 1 ∨ p ∣ p ^ n

Tactic:
rcases n with - | n
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h : Finite G
hn : Nat.card G = HPow.hPow (β := ℕ) p 0
⊢ HPow.hPow (β := ℕ) p 0 = 1 ∨ p ∣ HPow.hPow (β := ℕ) p 0

Tactic:
Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h : Finite G
hn : Nat.card G = HPow.hPow (β := ℕ) p 0
⊢ HPow.hPow (β := ℕ) p 0 = 1 ∨ p ∣ HPow.hPow (β := ℕ) p 0

Tactic:
exact Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h : Finite G
n : ℕ
hn : Nat.card G = p ^ (n + 1)
rw rw₁ : p * p ^ n = p * p ^ n
⊢ p ^ (n + 1) = p * p ^ n

Tactic:
rw [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h : Finite G
n : ℕ
hn : Nat.card G = p ^ (n + 1)
⊢ p ^ (n + 1) = 1 ∨ p ∣ p ^ (n + 1)

Tactic:
exact Or.inr ⟨p ^ n, by rw [pow_succ']⟩

Premises used: Or.inr
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h : Infinite G
inr : Eq (α := ℕ) 0 1 ∨ p ∣ 0
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G

Tactic:
rw [Nat.card_eq_zero_of_infinite]

Premises used: Nat.card_eq_zero_of_infinite
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h : Infinite G
⊢ Eq (α := ℕ) 0 1 ∨ p ∣ 0

Tactic:
Or.inr ⟨0, rfl⟩

Premises used: Exists.intro, OfNat.ofNat, Or.inr, rfl
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
h : Infinite G
⊢ Eq (α := ℕ) 0 1 ∨ p ∣ 0

Tactic:
exact Or.inr ⟨0, rfl⟩

Premises used: Or.inr
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst_1 : Finite G
hGnt : Nontrivial G
k : ℕ
hk : Nat.card G = p ^ k
hk0 : k = 0
⊢ Nat.card G = 1

Tactic:
rw [hk0, pow_zero] at hk

Premises used: pow_zero
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst_1 : Finite G
hGnt : Nontrivial G
k : ℕ
hk : Nat.card G = p ^ k
hk0 : k = 0
hk₁ : Nat.card G = 1
⊢ k = 0

Tactic:
rw [hk0, pow_zero] at hk

Premises used: pow_zero
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst_1 : Finite G
hGnt : Nontrivial G
k : ℕ
hk : Nat.card G = 1
hk0 : k = 0
⊢ False

Tactic:
Finite.one_lt_card.ne' hk

Premises used: LT.lt.ne', Finite.one_lt_card
-- Module: Mathlib.GroupTheory.PGroup
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst_1 : Finite G
hGnt : Nontrivial G
k : ℕ
hk : Nat.card G = 1
hk0 : k = 0
⊢ False

Tactic:
exact Finite.one_lt_card.ne' hk

Premises used: LT.lt.ne', Finite.one_lt_card
-- 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 α
a : α
inst_2 : Finite.{u_2 + 1} (↑(orbit G a) : Type u_2)
ϕ : Equiv.{u_2 + 1, u_1 + 1} (↑(orbit G a) : Type u_2) (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G a)) :=
  orbitEquivQuotientStabilizer G a
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G a))

Tactic:
haveI := Finite.of_equiv (orbit G a) ϕ
-- 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 α
a : α
inst_2 : Finite.{u_2 + 1} (↑(orbit G a) : Type u_2)
ϕ : Equiv.{u_2 + 1, u_1 + 1} (↑(orbit G a) : Type u_2) (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G a)) :=
  orbitEquivQuotientStabilizer G a
this : Finite.{u_1 + 1} (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G a))
⊢ Subgroup.FiniteIndex (stabilizer G a)

Tactic:
haveI := (stabilizer G a).finiteIndex_of_finite_quotient
-- 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 α
a : α
inst_2 : Finite.{u_2 + 1} (↑(orbit G a) : Type u_2)
ϕ : Equiv.{u_2 + 1, u_1 + 1} (↑(orbit G a) : Type u_2) (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G a)) :=
  orbitEquivQuotientStabilizer G a
this_1 : Finite.{u_1 + 1} (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G a))
this : Subgroup.FiniteIndex (stabilizer G a)
rw : ∃ (n : ℕ), Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G a)) = p ^ n
⊢ ∃ (n : ℕ), Nat.card.{u_2} (↑(orbit G a) : Type u_2) = p ^ n

Tactic:
rw [Nat.card_congr ϕ]

Premises used: Nat.card_congr
-- 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 α
a : α
inst_2 : Finite.{u_2 + 1} (↑(orbit G a) : Type u_2)
ϕ : Equiv.{u_2 + 1, u_1 + 1} (↑(orbit G a) : Type u_2) (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G a)) :=
  orbitEquivQuotientStabilizer G a
this_1 : Finite.{u_1 + 1} (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G a))
this : Subgroup.FiniteIndex (stabilizer G a)
⊢ ∃ (n : ℕ), Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G a)) = p ^ n

Tactic:
hG.index (stabilizer G a)

Premises used: IsPGroup.index, Subgroup.index, MulAction.stabilizer
-- 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 α
a : α
inst_2 : Finite.{u_2 + 1} (↑(orbit G a) : Type u_2)
ϕ : Equiv.{u_2 + 1, u_1 + 1} (↑(orbit G a) : Type u_2) (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G a)) :=
  orbitEquivQuotientStabilizer G a
this_1 : Finite.{u_1 + 1} (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G a))
this : Subgroup.FiniteIndex (stabilizer G a)
⊢ ∃ (n : ℕ), Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G a)) = p ^ n

Tactic:
exact hG.index (stabilizer G a)

Premises used: IsPGroup.index, MulAction.stabilizer
-- 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 α
have : ∀ (this : Fintype α), Nat.card α ≡ Nat.card.{u_2} (↑(fixedPoints G α) : Type u_2) [MOD p]
⊢ Nat.card α ≡ Nat.card.{u_2} (↑(fixedPoints G α) : Type u_2) [MOD p]

Tactic:
have := Fintype.ofFinite α
-- 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 : Fintype α
have :
  ∀ (this : Fintype (↑(fixedPoints G α) : Type u_2)),
    Nat.card α ≡ Nat.card.{u_2} (↑(fixedPoints G α) : Type u_2) [MOD p]
⊢ Nat.card α ≡ Nat.card.{u_2} (↑(fixedPoints G α) : Type u_2) [MOD p]

Tactic:
have := Fintype.ofFinite (fixedPoints G α)
-- 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)
rw : card α ≡ card.{u_2} (↑(fixedPoints G α) : Type u_2) [MOD p]
⊢ Nat.card α ≡ Nat.card.{u_2} (↑(fixedPoints G α) : Type u_2) [MOD p]

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

Premises used: Nat.card_eq_fintype_card
-- 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 α = card.{u_2} ((y : Quotient (orbitRel G α)) × { x : α // Quotient.mk'' x = y })

Tactic:
card_congr (Equiv.sigmaFiberEquiv (@Quotient.mk'' _ (orbitRel G α))).symm

Premises used: Fintype.card_congr, Equiv.sigmaFiberEquiv, Quotient.mk'', Equiv.symm
-- 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.{u_2} ((y : Quotient (orbitRel G α)) × { x : α // Quotient.mk'' x = y }) =
    ∑ a : Quotient (orbitRel G α), card.{u_2} { x : α // Quotient.mk'' x = a }

Tactic:
card_sigma

Premises used: Fintype.card_sigma
-- 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)
⊢ ∑ a : Quotient (orbitRel G α), card.{u_2} { x : α // Quotient.mk'' x = a } ≡
    ∑ _a : (↑(fixedPoints G α) : Type u_2), 1 [MOD p]

Tactic:
?_
-- 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)
⊢ ∑ _a : (↑(fixedPoints G α) : Type u_2), 1 = card.{u_2} (↑(fixedPoints G α) : Type u_2)

Tactic:
simp
-- 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 : Quotient (orbitRel G α), Fintype.card.{u_2} { x : α // Quotient.mk'' x = a } ≡
    ∑ _a : (↑(fixedPoints G α) : Type u_2), 1 [MOD p]
⊢ Fintype.card α ≡ Fintype.card.{u_2} (↑(fixedPoints G α) : Type u_2) [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

Premises used: Fintype.card_congr, Equiv.sigmaFiberEquiv, Quotient.mk'', Fintype.card_sigma, Fintype.card, Subtype, MulAction.orbitRel, Quotient, MulAction.fixedPoints, Equiv.symm, Eq, Sigma
-- 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)
rw :
  Eq (α := ZMod p) (∑ x : Quotient (orbitRel G α), (↑(card.{u_2} { x_1 : α // Quotient.mk'' x_1 = x }) : ZMod p))
    (∑ x : (↑(fixedPoints G α) : Type u_2), (↑1 : ZMod p))
⊢ ∑ a : Quotient (orbitRel G α), card.{u_2} { x : α // Quotient.mk'' x = a } ≡
    ∑ _a : (↑(fixedPoints G α) : Type u_2), 1 [MOD p]

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

Premises used: Nat.cast_sum, ZMod.natCast_eq_natCast_iff
-- 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)
x : α
simp : card.{u_2} { y : α // (orbitRel G α : α → α → Prop) y x } = card.{u_2} (↑(orbit G x) : Type u_2)
⊢ card.{u_2} { y : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' y) (Quotient.mk'' x) } =
    card.{u_2} (↑(orbit G x) : Type u_2)

Tactic:
simp only [Quotient.eq'']

Premises used: Quotient.eq''
-- 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)
x : α
⊢ card.{u_2} { y : α // (orbitRel G α : α → α → Prop) y x } = card.{u_2} (↑(orbit G x) : Type u_2)

Tactic:
congr
-- 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)
⊢ ∀ (x : α),
    card.{u_2} { y : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' y) (Quotient.mk'' x) } =
      card.{u_2} (↑(orbit G x) : Type u_2)

Tactic:
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
-- 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)
key :
  ∀ (x : α),
    card.{u_2} { y : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' y) (Quotient.mk'' x) } =
      card.{u_2} (↑(orbit G x) : Type u_2)
a : (↑(fixedPoints G α) : Type u_2)
ha : Membership.mem (γ := Finset (↑(fixedPoints G α) : Type u_2)) Finset.univ a
h : Ne (α := ZMod p) (↑1 : ZMod p) 0
rw : Eq (α := ZMod p) (↑1 : ZMod p) (↑(card.{u_2} (↑(orbit G (↑a : α)) : Type u_2)) : ZMod p)
rw₁ rw₂ : Eq (α := ZMod p) (↑1 : ZMod p) (↑1 : ZMod p)
⊢ Eq (α := ZMod p) (↑1 : ZMod p)
    (↑(card.{u_2}
          { x : α //
            Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' x)
              ((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 ha h) }) :
      ZMod p)

Tactic:
rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2]

Premises used: MulAction.mem_fixedPoints_iff_card_orbit_eq_one, Iff.mp, Subtype.property
-- 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)
key :
  ∀ (x : α),
    card.{u_2} { y : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' y) (Quotient.mk'' x) } =
      card.{u_2} (↑(orbit G x) : Type u_2)
a :
  ∀ (b : Quotient (orbitRel G α)) (b : α),
    Membership.mem (γ := Finset (Quotient (orbitRel G α))) Finset.univ (Quotient.mk'' b) →
      ∀
        (hb :
          Ne (α := ZMod p)
            (↑(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)
⊢ Eq (α := ZMod p) (∑ x : Quotient (orbitRel G α), (↑(card.{u_2} { x_1 : α // Quotient.mk'' x_1 = x }) : ZMod p))
    (∑ x : (↑(fixedPoints G α) : Type u_2), (↑1 : ZMod p))

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

Premises used: Finset.mem_univ, Quotient.mk'', Quotient.inductionOn', Iff.mp, Finset.sum_bij_ne_zero, MulAction.mem_fixedPoints', Eq.symm, Subtype.val, Subtype.property, Subtype.ext
-- 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)
key :
  ∀ (x : α),
    card.{u_2} { y : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' y) (Quotient.mk'' x) } =
      card.{u_2} (↑(orbit G x) : Type u_2)
b_1 : Quotient (orbitRel G α)
b : α
h : Membership.mem (γ := Finset (Quotient (orbitRel G α))) Finset.univ (Quotient.mk'' b)
hb :
  Ne (α := ZMod p)
    (↑(card.{u_2} { x : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' x) (Quotient.mk'' b) }) : ZMod p) 0
obtain :
  ∀ (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)
⊢ ∃ (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:
obtain ⟨k, hk⟩ := hG.card_orbit b

Premises used: IsPGroup.card_orbit