awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
Goal:
p : ℕ
G : Type u_1
inst : Group G
hG : IsPGroup p G
H : Type u_2
inst_1 : Group H
ϕ : H →* G
hϕ : Function.Injective.{u_2 + 1, u_1 + 1} (α := H) (β := G) (⇑ϕ : (a : H) → G)
⊢ IsPGroup p H
have simp_rw : ∀ (g : H), ∃ (k : ℕ), HPow.hPow (α := G) ((ϕ : (a : H) → G) g : G) (p ^ k) = 1
Tactic: simp_rw [IsPGroup, ← hϕ.eq_iff, ϕ.map_pow, ϕ.map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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
have refine : ∀ (h : H) (g : G) (hg : (ϕ : (a : G) → H) g = h) (k : ℕ) (hk : g ^ p ^ k = 1), h ^ p ^ k = 1
Tactic: refine fun h => Exists.elim (hϕ h) fun g hg => Exists.imp (fun k hk => ?_) (hG g)
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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
⊢ h ^ p ^ k = 1
have rw : HPow.hPow (α := H) ((ϕ : (a : G) → H) g : H) (p ^ k) = 1
Tactic: rw [← hg, ← ϕ.map_pow, hk, ϕ.map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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
⊢ h ^ p ^ k = 1
have rw₁ : Eq.{u_2 + 1} (α := H) ((ϕ : (a : G) → H) (g ^ p ^ k) : H) (1 : H)
Tactic: rw [← hg, ← ϕ.map_pow, hk, ϕ.map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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)
⊢ h ^ p ^ k = 1
have rw₂ : Eq.{u_2 + 1} (α := H) ((ϕ : (a : G) → H) 1 : H) (1 : H)
Tactic: rw [← hg, ← ϕ.map_pow, hk, ϕ.map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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)
⊢ h ^ p ^ k = 1
have rw₃ : Eq.{u_2 + 1} (α := H) 1 1
Tactic: rw [← hg, ← ϕ.map_pow, hk, ϕ.map_one]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (goal)
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 ^ (orderOf g).gcdB n
have rw : ((hG.powEquiv hn).symm : (a : G) → G) g = g ^ (Nat.card.{u_1} ↥(Subgroup.zpowers g)).gcdB n
Tactic: rw [← Nat.card_zpowers]
-- 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)
H : Subgroup G
inst_1 : H.FiniteIndex
⊢ ∃ (n : ℕ), H.index = p ^ n
have obtain : ∀ (n : ℕ) (hn : Nat.card.{u_1} (G ⧸ H.normalCore) = p ^ n), ∃ (n : ℕ), H.index = p ^ n
Tactic: obtain ⟨n, hn⟩ := iff_card.mp (hG.to_quotient H.normalCore)
-- 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)
H : Subgroup G
inst_1 : H.FiniteIndex
n : ℕ
hn : Nat.card.{u_1} (G ⧸ H.normalCore) = p ^ n
⊢ ∃ (n : ℕ), H.index = p ^ n
have obtain : ∀ k ≤ n, ∀ (hk2 : H.index = p ^ k), ∃ (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))
-- 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)
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G
have inl : Finite G → Nat.card G = 1 ∨ p ∣ Nat.card G
Tactic: cases finite_or_infinite G
-- 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)
inl : Finite G → Nat.card G = 1 ∨ p ∣ Nat.card G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G
have inr : Infinite G → Nat.card G = 1 ∨ p ∣ Nat.card G
Tactic: cases finite_or_infinite G
-- 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)
h : Finite G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G
have inl : ∀ (n : ℕ) (hn : Nat.card G = p ^ n), Nat.card G = 1 ∨ p ∣ Nat.card G
Tactic: obtain ⟨n, hn⟩ := iff_card.mp hG
-- 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)
h : Finite G
n : ℕ
hn : Nat.card G = p ^ n
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G
have inl : p ^ n = 1 ∨ p ∣ p ^ n
Tactic: rw [hn]
-- 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)
h : Finite G
n : ℕ
hn : Nat.card G = p ^ n
⊢ p ^ n = 1 ∨ p ∣ p ^ n
have inl : ∀ (hn : Nat.card G = HPow.hPow (β := ℕ) p 0), HPow.hPow (β := ℕ) p 0 = 1 ∨ p ∣ HPow.hPow (β := ℕ) p 0
Tactic: rcases n with - | n
Cleared hypotheses: n, hn
-- 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)
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
⊢ p ^ n = 1 ∨ p ∣ p ^ n
have inl₁ : ∀ (n : ℕ) (hn : Nat.card G = p ^ (n + 1)), p ^ (n + 1) = 1 ∨ p ∣ p ^ (n + 1)
Tactic: rcases n with - | n
Cleared hypotheses: n, hn
-- 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)
h : Finite G
n : ℕ
hn : Nat.card G = p ^ (n + 1)
⊢ p ^ (n + 1) = p * p ^ n
have rw : p * p ^ n = p * p ^ n
Tactic: rw [pow_succ']
-- 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)
h : Infinite G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G
have inr : Eq (α := ℕ) 0 1 ∨ p ∣ 0
Tactic: rw [Nat.card_eq_zero_of_infinite]
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
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
⊢ False
have hk₁ : Nat.card G = 1
Tactic: rw [hk0, pow_zero] at hk
Cleared hypotheses: hk, hk0
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
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
⊢ ∃ (n : ℕ), Nat.card.{u_2} (↑(orbit G a) : Type u_2) = p ^ n
have this : Finite.{u_1 + 1} (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G a))
Tactic: haveI := Finite.of_equiv (orbit G a) ϕ
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
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))
⊢ ∃ (n : ℕ), Nat.card.{u_2} (↑(orbit G a) : Type u_2) = p ^ n
have this₁ : Subgroup.FiniteIndex (stabilizer G a)
Tactic: haveI := (stabilizer G a).finiteIndex_of_finite_quotient
-- 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 α
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_2} (↑(orbit G a) : Type u_2) = p ^ n
have rw : ∃ (n : ℕ), Nat.card.{u_1} (HasQuotient.Quotient G (B := Subgroup G) (stabilizer G a)) = p ^ n
Tactic: rw [Nat.card_congr ϕ]
-- 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 α
⊢ Nat.card α ≡ Nat.card.{u_2} (↑(fixedPoints G α) : Type u_2) [MOD p]
have have : ∀ (this : Fintype α), Nat.card α ≡ Nat.card.{u_2} (↑(fixedPoints G α) : Type u_2) [MOD p]
Tactic: have := Fintype.ofFinite α
-- 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 : Fintype α
⊢ Nat.card α ≡ Nat.card.{u_2} (↑(fixedPoints G α) : Type u_2) [MOD p]
have have : ∀ (this : Fintype (↑(fixedPoints G α) : Type u_2)), Nat.card α ≡ Nat.card.{u_2} (↑(fixedPoints G α) : Type u_2) [MOD p]
Tactic: have := Fintype.ofFinite (fixedPoints G α)
-- 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)
⊢ Nat.card α ≡ Nat.card.{u_2} (↑(fixedPoints G α) : Type u_2) [MOD p]
have rw : card α ≡ card.{u_2} (↑(fixedPoints G α) : Type u_2) [MOD p]
Tactic: rw [Nat.card_eq_fintype_card, Nat.card_eq_fintype_card]
-- 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 α ≡ card.{u_2} (↑(fixedPoints G α) : Type u_2) [MOD p]
have card : ∑ a : Quotient (orbitRel G α), card.{u_2} { x : α // Quotient.mk'' x = a } ≡
  ∑ _a : (↑(fixedPoints G α) : Type u_2), 1 [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
-- 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)
⊢ ∑ a : Quotient (orbitRel G α), card.{u_2} { x : α // Quotient.mk'' x = a } ≡
    ∑ _a : (↑(fixedPoints G α) : Type u_2), 1 [MOD p]
have 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))
Tactic: rw [← ZMod.natCast_eq_natCast_iff _ _ p, Nat.cast_sum, Nat.cast_sum]
-- 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)
x : α
⊢ card.{u_2} { y : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' y) (Quotient.mk'' x) } =
    card.{u_2} (↑(orbit G x) : Type u_2)
have simp : card.{u_2} { y : α // (orbitRel G α : α → α → Prop) y x } = card.{u_2} (↑(orbit G x) : Type u_2)
Tactic: simp only [Quotient.eq'']
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
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)
⊢ 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))
have 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)
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
-- 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)
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
⊢ 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)
have rw : Eq (α := ZMod p) (↑1 : ZMod p) (↑(card.{u_2} (↑(orbit G (↑a : α)) : Type u_2)) : ZMod p)
Tactic: rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2]
-- 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)
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)
⊢ 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)
have rw₁ : Eq (α := ZMod p) (↑1 : ZMod p) (↑1 : ZMod p)
Tactic: rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2]
-- 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)
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)
⊢ 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))
have 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)
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])
-- 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)
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
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨k, hk⟩ := hG.card_orbit b
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
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
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)
have hk₁ : card.{u_2} (↑(orbit G b) : Type u_2) = p ^ k
Tactic: rw [Nat.card_eq_fintype_card] at hk
Cleared hypotheses: hk
-- 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)
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
k : ℕ
hk : card.{u_2} (↑(orbit G b) : Type u_2) = p ^ k
⊢ k = 0
have contrapose! : ∀ (hb : k ≠ 0),
  Eq (α := ZMod p)
    (↑(card.{u_2} { x : α // Eq (α := Quotient (orbitRel G α)) (Quotient.mk'' x) (Quotient.mk'' b) }) : ZMod p) 0
Tactic: contrapose! hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.GroupTheory.PGroup (hypothesis)
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
k : ℕ
hk : 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)
have this₁ : k = 0
Tactic: have : k = 0 := by
      contrapose! hb
      simp [key, hk, hb]
-- 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_2 : 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
k : ℕ
hk : card.{u_2} (↑(orbit G b) : Type u_2) = p ^ k
this : k = 0
⊢ card.{u_2} (↑(orbit G b) : Type u_2) = 1
have rw : p ^ k = 1
Tactic: rw [hk, this, pow_zero]