---

$$\text{If }P\text{ is a finite simple }p\text{-group, show that }P\text{ has order }p.$$

Formalizing the Statement

import Mathlib

open Subgroup in
example {p : ℕ} {P : Type u_1} [Group P] (hP : IsPGroup p P) [hp : Fact (Nat.Prime p)]
  [Finite P] [IsSimpleGroup P]: Nat.card P = p := by sorry

Step-by-Step Solution

1. The center of $P$ must be nontrivial since it is a $p$-group.

have center_nontriv := hP.center_nontrivial

2. Since $P$ is simple, its center (which is a normal subgroup) must be either trivial or $P$ itself.

have center_bot_top := (center P).normal_of_characteristic.eq_bot_or_eq_top

3. The center is not trivial, therefore it is $P$ itself.

have center_not_bot := (center P).nontrivial_iff_ne_bot.mp center_nontriv
replace center_bot_top := center_bot_top.resolve_left center_not_bot

Which means that $P$ should be abelian.

letI : CommGroup P := Group.commGroupOfCenterEqTop center_bot_top

1. Of course $P$ is nontrivial since its center is nontrivial.

letI : Nontrivial P := Set.nontrivial_of_nontrivial_coe center_nontriv

2. And the cardinality of $P$ should be divisible by $p$ since $P$ has cardinality $p^n$ for some $n$ and $n \neq 0$ for: $P$ is nontrivial, and nontrivial implies a cardinality strictly greater than 1.

letI : Fintype P := Fintype.ofFinite P
have : p ∣ Fintype.card P := by
  /- since $P$ has cardinality $p^n$ for some $n$--/
  obtain ⟨n, hnp⟩ := IsPGroup.iff_card.1 hP
  rw [← Nat.card_eq_fintype_card, hnp]
  /- and $n \neq 0$--/
  have : n ≠ 0 := by
       by_contra nzero
       rw [nzero, pow_zero] at hnp
       /- for $P$ is nontrivial, and nontrivial implies a cardinality strictly greater than 1.--/
       have := hnp ▸ Finite.one_lt_card_iff_nontrivial (α := P)
       tauto
  exact Prime.dvd_pow_iff_dvd hp.out.prime this |>.2 p.dvd_refl

By Cauchy’s theorem, this admits the existence of an element whose order is $p$. We define the subgroup generated by the element as $sub$.

obtain ⟨x, hx⟩ := exists_prime_orderOf_dvd_card p this
set sub := zpowers x with hsub

1. It must be of cardinality $p$ since the element has order $p$.

have sub_card := hsub ▸ hx ▸ Nat.card_zpowers x

2. And it must be normal since $P$ is abelian.

have sub_normal : sub.Normal := sub.normal_of_comm

3. Furthermore it mustn’t be trivial since its generator is not the identity (identity won’t have order $p$).

have sub_ntriv : sub ≠ ⊥ := by
  /- since its generator is not the identity (identity won't have order $p$).--/
  refine zpowers_ne_bot.mpr ?_
  by_contra hx_one
  rw [hx_one, orderOf_one] at hx
  rw [← hx] at hp
  tauto

Thus, since $P$ is simple, $sub$ must be $P$ it self. Therefore the cardinality of $P$ is exactly $p$.

have sub_eq_top := sub_normal.eq_bot_or_eq_top.resolve_left sub_ntriv
exact card_top (G := P) ▸ sub_eq_top ▸ sub_card

Complete Code

import Mathlib

open Subgroup in
example {p : ℕ} {P : Type u_1} [Group P] (hP : IsPGroup p P) [hp : Fact (Nat.Prime p)]
  [Finite P] [IsSimpleGroup P]: Nat.card P = p := by
  have center_nontriv := hP.center_nontrivial
  have center_bot_top := (center P).normal_of_characteristic.eq_bot_or_eq_top
  have center_not_bot := (center P).nontrivial_iff_ne_bot.mp center_nontriv
  replace center_bot_top := center_bot_top.resolve_left center_not_bot
  letI : CommGroup P := Group.commGroupOfCenterEqTop center_bot_top
  letI : Fintype P := Fintype.ofFinite P
  letI : Nontrivial P := Set.nontrivial_of_nontrivial_coe center_nontriv
  have : p ∣ Fintype.card P := by
    obtain ⟨n, hnp⟩ := IsPGroup.iff_card.1 hP
    rw [← Nat.card_eq_fintype_card, hnp]
    have : n ≠ 0 := by
      by_contra nzero
      rw [nzero, pow_zero] at hnp
      have := hnp ▸ Finite.one_lt_card_iff_nontrivial (α := P)
      tauto
    exact Prime.dvd_pow_iff_dvd hp.out.prime this |>.2 p.dvd_refl
  obtain ⟨x, hx⟩ := exists_prime_orderOf_dvd_card p this
  set sub := zpowers x with hsub
  have sub_card := hsub ▸ hx ▸ Nat.card_zpowers x
  have sub_normal : sub.Normal := sub.normal_of_comm
  have sub_ntriv : sub ≠ ⊥ := by
    refine zpowers_ne_bot.mpr ?_
    by_contra hx_one
    rw [hx_one, orderOf_one] at hx
    rw [← hx] at hp
    tauto
  have sub_eq_top := sub_normal.eq_bot_or_eq_top.resolve_left sub_ntriv
  exact card_top (G := P) ▸ sub_eq_top ▸ sub_card