no goals
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.343920
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
⊢ Nontrivial { x // x ∈ Subgroup.center G }
classical
  cases nonempty_fintype G
  have := (hG.of_equiv ConjAct.toConjAct).exists_fixed_point_of_prime_dvd_card_of_fixed_point G
  rw [ConjAct.fixedPoints_eq_center] at this
  have dvd : p ∣ card G := by
    obtain ⟨n, hn0, hn⟩ := hG.nontrivial_iff_card.mp inferInstance
    exact hn.symm ▸ dvd_pow_self _ (ne_of_gt hn0)
  obtain ⟨g, hg⟩ := this dvd (Subgroup.center G).one_mem
  exact ⟨⟨1, ⟨g, hg.1⟩, mt Subtype.ext_iff.mp hg.2⟩⟩
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.343920
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
⊢ Nontrivial { x // x ∈ Subgroup.center G }
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.343920
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
⊢ Nontrivial { x // x ∈ Subgroup.center G }
cases nonempty_fintype G
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.343920
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
this : p ∣ card G → ∀ {a : G}, a ∈ fixedPoints (ConjAct G) G → ∃ b, b ∈ fixedPoints (ConjAct G) G ∧ a ≠ b
⊢ Nontrivial { x // x ∈ Subgroup.center G }
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.343920
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
⊢ Nontrivial { x // x ∈ Subgroup.center G }
have := (hG.of_equiv ConjAct.toConjAct).exists_fixed_point_of_prime_dvd_card_of_fixed_point G
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.343920
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
this : p ∣ card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b, b ∈ ↑(Subgroup.center G) ∧ a ≠ b
⊢ Nontrivial { x // x ∈ Subgroup.center G }
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.343920
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
this : p ∣ card G → ∀ {a : G}, a ∈ fixedPoints (ConjAct G) G → ∃ b, b ∈ fixedPoints (ConjAct G) G ∧ a ≠ b
⊢ Nontrivial { x // x ∈ Subgroup.center G }
rw [ConjAct.fixedPoints_eq_center] at this
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.343920
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
this : p ∣ card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b, b ∈ ↑(Subgroup.center G) ∧ a ≠ b
dvd : p ∣ card G
⊢ Nontrivial { x // x ∈ Subgroup.center G }
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.343920
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
this : p ∣ card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b, b ∈ ↑(Subgroup.center G) ∧ a ≠ b
⊢ Nontrivial { x // x ∈ Subgroup.center G }
have dvd : p ∣ card G := by
  obtain ⟨n, hn0, hn⟩ := hG.nontrivial_iff_card.mp inferInstance
  exact hn.symm ▸ dvd_pow_self _ (ne_of_gt hn0)
case intro.intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.343920
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
this : p ∣ card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b, b ∈ ↑(Subgroup.center G) ∧ a ≠ b
dvd : p ∣ card G
g : G
hg : g ∈ ↑(Subgroup.center G) ∧ 1 ≠ g
⊢ Nontrivial { x // x ∈ Subgroup.center G }
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.343920
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
this : p ∣ card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b, b ∈ ↑(Subgroup.center G) ∧ a ≠ b
dvd : p ∣ card G
⊢ Nontrivial { x // x ∈ Subgroup.center G }
obtain ⟨g, hg⟩ := this dvd (Subgroup.center G).one_mem
no goals
case intro.intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.343920
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
this : p ∣ card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b, b ∈ ↑(Subgroup.center G) ∧ a ≠ b
dvd : p ∣ card G
g : G
hg : g ∈ ↑(Subgroup.center G) ∧ 1 ≠ g
⊢ Nontrivial { x // x ∈ Subgroup.center G }
exact ⟨⟨1, ⟨g, hg.1⟩, mt Subtype.ext_iff.mp hg.2⟩⟩
case intro.intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.343920
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
this : p ∣ card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b, b ∈ ↑(Subgroup.center G) ∧ a ≠ b
n : ℕ
hn0 : n > 0
hn : card G = p ^ n
⊢ p ∣ card G
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.343920
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
this : p ∣ card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b, b ∈ ↑(Subgroup.center G) ∧ a ≠ b
⊢ p ∣ card G
obtain ⟨n, hn0, hn⟩ := hG.nontrivial_iff_card.mp inferInstance
no goals
case intro.intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type ?u.343920
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
this : p ∣ card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b, b ∈ ↑(Subgroup.center G) ∧ a ≠ b
n : ℕ
hn0 : n > 0
hn : card G = p ^ n
⊢ p ∣ card G
exact hn.symm ▸ dvd_pow_self _ (ne_of_gt hn0)