-- Mathlib/GroupTheory/PGroup.lean
theorem center_nontrivial [Nontrivial G] [Finite G] : Nontrivial (Subgroup.center G)

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : p ∣ Nat.card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b ∈ ↑(Subgroup.center G), a ≠ b
⊢ p ∣ Nat.card G

Tactic:
obtain ⟨n, hn0, hn⟩ := hG.nontrivial_iff_card.mp inferInstance

Result:
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : p ∣ Nat.card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b ∈ ↑(Subgroup.center G), a ≠ b
n : ℕ
hn0 : n > 0
hn : Nat.card G = p ^ n
⊢ p ∣ Nat.card G

Proof state:
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : p ∣ Nat.card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b ∈ ↑(Subgroup.center G), a ≠ b
n : ℕ
hn0 : n > 0
hn : Nat.card G = p ^ n
⊢ p ∣ Nat.card G

Tactic:
exact hn.symm ▸ dvd_pow_self _ (ne_of_gt hn0)

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
⊢ Nontrivial ↥(Subgroup.center G)

Tactic:
have := (hG.of_equiv ConjAct.toConjAct).exists_fixed_point_of_prime_dvd_card_of_fixed_point G

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : p ∣ Nat.card G → ∀ {a : G}, a ∈ fixedPoints (ConjAct G) G → ∃ b ∈ fixedPoints (ConjAct G) G, a ≠ b
⊢ Nontrivial ↥(Subgroup.center G)

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
⊢ Nontrivial ↥(Subgroup.center G)

Tactic:
classical
  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 ∣ Nat.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⟩⟩

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : p ∣ Nat.card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b ∈ ↑(Subgroup.center G), a ≠ b
⊢ Nontrivial ↥(Subgroup.center G)

Tactic:
have dvd : p ∣ Nat.card G := by
  obtain ⟨n, hn0, hn⟩ := hG.nontrivial_iff_card.mp inferInstance
  exact hn.symm ▸ dvd_pow_self _ (ne_of_gt hn0)

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : p ∣ Nat.card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b ∈ ↑(Subgroup.center G), a ≠ b
dvd : p ∣ Nat.card G
⊢ Nontrivial ↥(Subgroup.center G)

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : p ∣ Nat.card G → ∀ {a : G}, a ∈ fixedPoints (ConjAct G) G → ∃ b ∈ fixedPoints (ConjAct G) G, a ≠ b
⊢ Nontrivial ↥(Subgroup.center G)

Tactic:
rw [ConjAct.fixedPoints_eq_center] at this

Result:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : p ∣ Nat.card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b ∈ ↑(Subgroup.center G), a ≠ b
⊢ Nontrivial ↥(Subgroup.center G)

Proof state:
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : p ∣ Nat.card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b ∈ ↑(Subgroup.center G), a ≠ b
dvd : p ∣ Nat.card G
⊢ Nontrivial ↥(Subgroup.center G)

Tactic:
obtain ⟨g, hg⟩ := this dvd (Subgroup.center G).one_mem

Result:
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : p ∣ Nat.card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b ∈ ↑(Subgroup.center G), a ≠ b
dvd : p ∣ Nat.card G
g : G
hg : g ∈ ↑(Subgroup.center G) ∧ 1 ≠ g
⊢ Nontrivial ↥(Subgroup.center G)

Proof state:
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : p ∣ Nat.card G → ∀ {a : G}, a ∈ ↑(Subgroup.center G) → ∃ b ∈ ↑(Subgroup.center G), a ≠ b
dvd : p ∣ Nat.card G
g : G
hg : g ∈ ↑(Subgroup.center G) ∧ 1 ≠ g
⊢ Nontrivial ↥(Subgroup.center G)

Tactic:
exact ⟨⟨1, ⟨g, hg.1⟩, mt Subtype.ext_iff.mp hg.2⟩⟩

Result:
no goals