[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
hp : Fact (Nat.Prime p)
g : G
k : ℕ
hk : orderOf g = p ^ k
⊢ g ^ p ^ k = 1
[PROOFSTEP]
rw [← hk, pow_orderOf_eq_one]
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
n : ℕ
hG : card G = p ^ n
g : G
⊢ g ^ p ^ n = 1
[PROOFSTEP]
rw [← hG, pow_card_eq_one]
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
⊢ IsPGroup p G ↔ ∃ n, card G = p ^ n
[PROOFSTEP]
have hG : card G ≠ 0 := card_ne_zero
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
⊢ IsPGroup p G ↔ ∃ n, card G = p ^ n
[PROOFSTEP]
refine' ⟨fun h => _, fun ⟨n, hn⟩ => of_card hn⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
⊢ ∃ n, card G = p ^ n
[PROOFSTEP]
suffices ∀ q ∈ Nat.factors (card G), q = p by
  use(card G).factors.length
  rw [← List.prod_replicate, ← List.eq_replicate_of_mem this, Nat.prod_factors hG]
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
this : ∀ (q : ℕ), q ∈ Nat.factors (card G) → q = p
⊢ ∃ n, card G = p ^ n
[PROOFSTEP]
use(card G).factors.length
[GOAL]
case h
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
this : ∀ (q : ℕ), q ∈ Nat.factors (card G) → q = p
⊢ card G = p ^ List.length (Nat.factors (card G))
[PROOFSTEP]
rw [← List.prod_replicate, ← List.eq_replicate_of_mem this, Nat.prod_factors hG]
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
⊢ ∀ (q : ℕ), q ∈ Nat.factors (card G) → q = p
[PROOFSTEP]
intro q hq
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ Nat.factors (card G)
⊢ q = p
[PROOFSTEP]
obtain ⟨hq1, hq2⟩ := (Nat.mem_factors hG).mp hq
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ Nat.factors (card G)
hq1 : Nat.Prime q
hq2 : q ∣ card G
⊢ q = p
[PROOFSTEP]
haveI : Fact q.Prime := ⟨hq1⟩
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ Nat.factors (card G)
hq1 : Nat.Prime q
hq2 : q ∣ card G
this : Fact (Nat.Prime q)
⊢ q = p
[PROOFSTEP]
obtain ⟨g, hg⟩ := exists_prime_orderOf_dvd_card q hq2
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ Nat.factors (card G)
hq1 : Nat.Prime q
hq2 : q ∣ card G
this : Fact (Nat.Prime q)
g : G
hg : orderOf g = q
⊢ q = p
[PROOFSTEP]
obtain ⟨k, hk⟩ := (iff_orderOf.mp h) g
[GOAL]
case intro.intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fintype G
hG : card G ≠ 0
h : IsPGroup p G
q : ℕ
hq : q ∈ Nat.factors (card G)
hq1 : Nat.Prime q
hq2 : q ∣ card G
this : Fact (Nat.Prime q)
g : G
hg : orderOf g = q
k : ℕ
hk : orderOf g = p ^ k
⊢ q = p
[PROOFSTEP]
exact (hq1.pow_eq_iff.mp (hg.symm.trans hk).symm).1.symm
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : H →* G
hϕ : Function.Injective ↑ϕ
⊢ IsPGroup p H
[PROOFSTEP]
simp_rw [IsPGroup, ← hϕ.eq_iff, ϕ.map_pow, ϕ.map_one]
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : H →* G
hϕ : Function.Injective ↑ϕ
⊢ ∀ (g : H), ∃ k, ↑ϕ g ^ p ^ k = 1
[PROOFSTEP]
exact fun h => hG (ϕ h)
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : G →* H
hϕ : Function.Surjective ↑ϕ
⊢ IsPGroup p H
[PROOFSTEP]
refine' fun h => Exists.elim (hϕ h) fun g hg => Exists.imp (fun k hk => _) (hG g)
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : G →* H
hϕ : Function.Surjective ↑ϕ
h : H
g : G
hg : ↑ϕ g = h
k : ℕ
hk : g ^ p ^ k = 1
⊢ h ^ p ^ k = 1
[PROOFSTEP]
rw [← hg, ← ϕ.map_pow, hk, ϕ.map_one]
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
n : ℕ
hn : Nat.coprime p n
g : G
⊢ ↑(powEquiv hG hn).symm g = g ^ Nat.gcdB (orderOf g) n
[PROOFSTEP]
rw [order_eq_card_zpowers']
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
n : ℕ
hn : Nat.coprime p n
g : G
⊢ ↑(powEquiv hG hn).symm g = g ^ Nat.gcdB (Nat.card { x // x ∈ Subgroup.zpowers g }) n
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
H : Subgroup G
inst✝ : Subgroup.FiniteIndex H
⊢ ∃ n, Subgroup.index H = p ^ n
[PROOFSTEP]
haveI := H.normalCore.fintypeQuotientOfFiniteIndex
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
H : Subgroup G
inst✝ : Subgroup.FiniteIndex H
this : Fintype (G ⧸ Subgroup.normalCore H)
⊢ ∃ n, Subgroup.index H = p ^ n
[PROOFSTEP]
obtain ⟨n, hn⟩ := iff_card.mp (hG.to_quotient H.normalCore)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
H : Subgroup G
inst✝ : Subgroup.FiniteIndex H
this : Fintype (G ⧸ Subgroup.normalCore H)
n : ℕ
hn : card (G ⧸ Subgroup.normalCore H) = p ^ n
⊢ ∃ n, Subgroup.index H = p ^ n
[PROOFSTEP]
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))
[GOAL]
case intro.intro.intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
H : Subgroup G
inst✝ : Subgroup.FiniteIndex H
this : Fintype (G ⧸ Subgroup.normalCore H)
n : ℕ
hn : card (G ⧸ Subgroup.normalCore H) = p ^ n
k : ℕ
left✝ : k ≤ n
hk2 : Subgroup.index H = p ^ k
⊢ ∃ n, Subgroup.index H = p ^ n
[PROOFSTEP]
exact ⟨k, hk2⟩
[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
[PROOFSTEP]
cases fintypeOrInfinite G
[GOAL]
case inl
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G
[PROOFSTEP]
obtain ⟨n, hn⟩ := iff_card.mp hG
[GOAL]
case inl.intro
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
n : ℕ
hn : card G = p ^ n
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G
[PROOFSTEP]
rw [Nat.card_eq_fintype_card, hn]
[GOAL]
case inl.intro
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
n : ℕ
hn : card G = p ^ n
⊢ p ^ n = 1 ∨ p ∣ p ^ n
[PROOFSTEP]
cases' n with n n
[GOAL]
case inl.intro.zero
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
hn : card G = p ^ Nat.zero
⊢ p ^ Nat.zero = 1 ∨ p ∣ p ^ Nat.zero
[PROOFSTEP]
exact Or.inl rfl
[GOAL]
case inl.intro.succ
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
n : ℕ
hn : card G = p ^ Nat.succ n
⊢ p ^ Nat.succ n = 1 ∨ p ∣ p ^ Nat.succ n
[PROOFSTEP]
exact Or.inr ⟨p ^ n, by rw [pow_succ]⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Fintype G
n : ℕ
hn : card G = p ^ Nat.succ n
⊢ p ^ Nat.succ n = p * p ^ n
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case inr
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Infinite G
⊢ Nat.card G = 1 ∨ p ∣ Nat.card G
[PROOFSTEP]
rw [Nat.card_eq_zero_of_infinite]
[GOAL]
case inr
p : ℕ
G : Type u_1
inst✝ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
val✝ : Infinite G
⊢ 0 = 1 ∨ p ∣ 0
[PROOFSTEP]
exact Or.inr ⟨0, rfl⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝ : Fintype G
hGnt : Nontrivial G
k : ℕ
hk : card G = p ^ k
hk0 : k = 0
⊢ False
[PROOFSTEP]
rw [hk0, pow_zero] at hk 
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝ : Fintype G
hGnt : Nontrivial G
k : ℕ
hk : card G = 1
hk0 : k = 0
⊢ False
[PROOFSTEP]
exact Fintype.one_lt_card.ne' hk
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Fintype ↑(orbit G a)
⊢ ∃ n, card ↑(orbit G a) = p ^ n
[PROOFSTEP]
let ϕ := orbitEquivQuotientStabilizer G a
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Fintype ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
⊢ ∃ n, card ↑(orbit G a) = p ^ n
[PROOFSTEP]
haveI := Fintype.ofEquiv (orbit G a) ϕ
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Fintype ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
this : Fintype (G ⧸ stabilizer G a)
⊢ ∃ n, card ↑(orbit G a) = p ^ n
[PROOFSTEP]
haveI := (stabilizer G a).finiteIndex_of_finite_quotient
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Fintype ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
this✝ : Fintype (G ⧸ stabilizer G a)
this : Subgroup.FiniteIndex (stabilizer G a)
⊢ ∃ n, card ↑(orbit G a) = p ^ n
[PROOFSTEP]
rw [card_congr ϕ, ← Subgroup.index_eq_card]
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
a : α
inst✝ : Fintype ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
this✝ : Fintype (G ⧸ stabilizer G a)
this : Subgroup.FiniteIndex (stabilizer G a)
⊢ ∃ n, Subgroup.index (stabilizer G a) = p ^ n
[PROOFSTEP]
exact hG.index (stabilizer G a)
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
⊢ card α ≡ card ↑(fixedPoints G α) [MOD p]
[PROOFSTEP]
classical
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; rfl
rw [← ZMod.eq_iff_modEq_nat p, Nat.cast_sum, Nat.cast_sum]
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
refine'
  Eq.symm
    (Finset.sum_bij_ne_zero (fun a _ _ => Quotient.mk'' a.1) (fun _ _ _ => Finset.mem_univ _)
      (fun a₁ a₂ _ _ _ _ h => Subtype.eq ((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])
obtain ⟨k, hk⟩ := hG.card_orbit b
have : k = 0 :=
  le_zero_iff.1
    (Nat.le_of_lt_succ
      (lt_of_not_ge
        (mt (pow_dvd_pow p)
          (by rwa [pow_one, ← hk, ← Nat.modEq_zero_iff_dvd, ← ZMod.eq_iff_modEq_nat, ← key, Nat.cast_zero]))))
exact
  ⟨⟨b, mem_fixedPoints_iff_card_orbit_eq_one.2 <| by rw [hk, this, pow_zero]⟩, Finset.mem_univ _,
    ne_of_eq_of_ne Nat.cast_one one_ne_zero, rfl⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
⊢ card α ≡ card ↑(fixedPoints G α) [MOD p]
[PROOFSTEP]
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; rfl
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
⊢ ∑ _a : ↑(fixedPoints G α), 1 = card ↑(fixedPoints G α)
[PROOFSTEP]
simp
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
⊢ Finset.card Finset.univ = card ↑(fixedPoints G α)
[PROOFSTEP]
rfl
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
⊢ ∑ a : Quotient (orbitRel G α), card { x // Quotient.mk'' x = a } ≡ ∑ _a : ↑(fixedPoints G α), 1 [MOD p]
[PROOFSTEP]
rw [← ZMod.eq_iff_modEq_nat p, Nat.cast_sum, Nat.cast_sum]
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
⊢ ∑ x : Quotient (orbitRel G α), ↑(card { x_1 // Quotient.mk'' x_1 = x }) = ∑ x : ↑(fixedPoints G α), ↑1
[PROOFSTEP]
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
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
x : α
⊢ card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
[PROOFSTEP]
simp only [Quotient.eq'']
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
x : α
⊢ card { y // Setoid.r y x } = card ↑(orbit G x)
[PROOFSTEP]
congr
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
⊢ ∑ x : Quotient (orbitRel G α), ↑(card { x_1 // Quotient.mk'' x_1 = x }) = ∑ x : ↑(fixedPoints G α), ↑1
[PROOFSTEP]
refine'
  Eq.symm
    (Finset.sum_bij_ne_zero (fun a _ _ => Quotient.mk'' a.1) (fun _ _ _ => Finset.mem_univ _)
      (fun a₁ a₂ _ _ _ _ h => Subtype.eq ((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])
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
a : ↑(fixedPoints G α)
ha : a ∈ Finset.univ
x✝ : ↑1 ≠ 0
⊢ ↑1 = ↑(card { x // Quotient.mk'' x = (fun a x x => Quotient.mk'' ↑a) a ha x✝ })
[PROOFSTEP]
rw [key, mem_fixedPoints_iff_card_orbit_eq_one.mp a.2]
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
⊢ ∃ a h₁ h₂, Quotient.mk'' b = (fun a x x => Quotient.mk'' ↑a) a h₁ h₂
[PROOFSTEP]
obtain ⟨k, hk⟩ := hG.card_orbit b
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
k : ℕ
hk : card ↑(orbit G b) = p ^ k
⊢ ∃ a h₁ h₂, Quotient.mk'' b = (fun a x x => Quotient.mk'' ↑a) a h₁ h₂
[PROOFSTEP]
have : k = 0 :=
  le_zero_iff.1
    (Nat.le_of_lt_succ
      (lt_of_not_ge
        (mt (pow_dvd_pow p)
          (by rwa [pow_one, ← hk, ← Nat.modEq_zero_iff_dvd, ← ZMod.eq_iff_modEq_nat, ← key, Nat.cast_zero]))))
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
k : ℕ
hk : card ↑(orbit G b) = p ^ k
⊢ ¬p ^ Nat.succ 0 ∣ p ^ k
[PROOFSTEP]
rwa [pow_one, ← hk, ← Nat.modEq_zero_iff_dvd, ← ZMod.eq_iff_modEq_nat, ← key, Nat.cast_zero]
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
k : ℕ
hk : card ↑(orbit G b) = p ^ k
this : k = 0
⊢ ∃ a h₁ h₂, Quotient.mk'' b = (fun a x x => Quotient.mk'' ↑a) a h₁ h₂
[PROOFSTEP]
exact
  ⟨⟨b, mem_fixedPoints_iff_card_orbit_eq_one.2 <| by rw [hk, this, pow_zero]⟩, Finset.mem_univ _,
    ne_of_eq_of_ne Nat.cast_one one_ne_zero, rfl⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Fintype ↑(fixedPoints G α)
key : ∀ (x : α), card { y // Quotient.mk'' y = Quotient.mk'' x } = card ↑(orbit G x)
b✝ : Quotient (orbitRel G α)
b : α
x✝ : Quotient.mk'' b ∈ Finset.univ
hb : ↑(card { x // Quotient.mk'' x = Quotient.mk'' b }) ≠ 0
k : ℕ
hk : card ↑(orbit G b) = p ^ k
this : k = 0
⊢ card ↑(orbit G b) = 1
[PROOFSTEP]
rw [hk, this, pow_zero]
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
hpα : ¬p ∣ card α
inst✝ : Finite ↑(fixedPoints G α)
⊢ Nonempty ↑(fixedPoints G α)
[PROOFSTEP]
cases nonempty_fintype (fixedPoints G α)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
hpα : ¬p ∣ card α
inst✝ : Finite ↑(fixedPoints G α)
val✝ : Fintype ↑(fixedPoints G α)
⊢ Nonempty ↑(fixedPoints G α)
[PROOFSTEP]
rw [← card_pos_iff, pos_iff_ne_zero]
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
hpα : ¬p ∣ card α
inst✝ : Finite ↑(fixedPoints G α)
val✝ : Fintype ↑(fixedPoints G α)
⊢ card ↑(fixedPoints G α) ≠ 0
[PROOFSTEP]
contrapose! hpα
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Finite ↑(fixedPoints G α)
val✝ : Fintype ↑(fixedPoints G α)
hpα : card ↑(fixedPoints G α) = 0
⊢ p ∣ card α
[PROOFSTEP]
rw [← Nat.modEq_zero_iff_dvd, ← hpα]
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝³ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : Finite ↑(fixedPoints G α)
val✝ : Fintype ↑(fixedPoints G α)
hpα : card ↑(fixedPoints G α) = 0
⊢ card α ≡ card ↑(fixedPoints G α) [MOD p]
[PROOFSTEP]
exact hG.card_modEq_card_fixedPoints α
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Fintype α
hpα : p ∣ card α
a : α
ha : a ∈ fixedPoints G α
⊢ ∃ b, b ∈ fixedPoints G α ∧ a ≠ b
[PROOFSTEP]
cases nonempty_fintype (fixedPoints G α)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Fintype α
hpα : p ∣ card α
a : α
ha : a ∈ fixedPoints G α
val✝ : Fintype ↑(fixedPoints G α)
⊢ ∃ b, b ∈ fixedPoints G α ∧ a ≠ b
[PROOFSTEP]
have hpf : p ∣ card (fixedPoints G α) :=
  Nat.modEq_zero_iff_dvd.mp ((hG.card_modEq_card_fixedPoints α).symm.trans hpα.modEq_zero_nat)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Fintype α
hpα : p ∣ card α
a : α
ha : a ∈ fixedPoints G α
val✝ : Fintype ↑(fixedPoints G α)
hpf : p ∣ card ↑(fixedPoints G α)
⊢ ∃ b, b ∈ fixedPoints G α ∧ a ≠ b
[PROOFSTEP]
have hα : 1 < card (fixedPoints G α) :=
  (Fact.out (p := p.Prime)).one_lt.trans_le (Nat.le_of_dvd (card_pos_iff.2 ⟨⟨a, ha⟩⟩) hpf)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Fintype α
hpα : p ∣ card α
a : α
ha : a ∈ fixedPoints G α
val✝ : Fintype ↑(fixedPoints G α)
hpf : p ∣ card ↑(fixedPoints G α)
hα : 1 < card ↑(fixedPoints G α)
⊢ ∃ b, b ∈ fixedPoints G α ∧ a ≠ b
[PROOFSTEP]
exact
  let ⟨⟨b, hb⟩, hba⟩ := exists_ne_of_one_lt_card hα ⟨a, ha⟩
  ⟨b, hb, fun hab => hba (by simp_rw [hab])⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Fintype α
hpα : p ∣ card α
a : α
ha : a ∈ fixedPoints G α
val✝ : Fintype ↑(fixedPoints G α)
hpf : p ∣ card ↑(fixedPoints G α)
hα : 1 < card ↑(fixedPoints G α)
b : α
hb : b ∈ fixedPoints G α
hba : { val := b, property := hb } ≠ { val := a, property := ha }
hab : a = b
⊢ { val := b, property := hb } = { val := a, property := ha }
[PROOFSTEP]
simp_rw [hab]
[GOAL]
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
⊢ Nontrivial { x // x ∈ Subgroup.center G }
[PROOFSTEP]
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⟩⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
⊢ Nontrivial { x // x ∈ Subgroup.center G }
[PROOFSTEP]
cases nonempty_fintype G
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
val✝ : Fintype G
⊢ Nontrivial { x // x ∈ Subgroup.center G }
[PROOFSTEP]
have := (hG.of_equiv ConjAct.toConjAct).exists_fixed_point_of_prime_dvd_card_of_fixed_point G
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
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 }
[PROOFSTEP]
rw [ConjAct.fixedPoints_eq_center] at this 
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
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 }
[PROOFSTEP]
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)
[GOAL]
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
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
[PROOFSTEP]
obtain ⟨n, hn0, hn⟩ := hG.nontrivial_iff_card.mp inferInstance
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
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
[PROOFSTEP]
exact hn.symm ▸ dvd_pow_self _ (ne_of_gt hn0)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
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 }
[PROOFSTEP]
obtain ⟨g, hg⟩ := this dvd (Subgroup.center G).one_mem
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
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 }
[PROOFSTEP]
exact ⟨⟨1, ⟨g, hg.1⟩, mt Subtype.ext_iff.mp hg.2⟩⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
⊢ ⊥ < Subgroup.center G
[PROOFSTEP]
haveI := center_nontrivial hG
[GOAL]
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : Nontrivial { x // x ∈ Subgroup.center G }
⊢ ⊥ < Subgroup.center G
[PROOFSTEP]
cases nonempty_fintype G
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : Nontrivial { x // x ∈ Subgroup.center G }
val✝ : Fintype G
⊢ ⊥ < Subgroup.center G
[PROOFSTEP]
classical exact bot_lt_iff_ne_bot.mpr ((Subgroup.center G).one_lt_card_iff_ne_bot.mp Fintype.one_lt_card)
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝⁴ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_2
inst✝³ : MulAction G α
inst✝² : Fintype α
inst✝¹ : Nontrivial G
inst✝ : Finite G
this : Nontrivial { x // x ∈ Subgroup.center G }
val✝ : Fintype G
⊢ ⊥ < Subgroup.center G
[PROOFSTEP]
exact bot_lt_iff_ne_bot.mpr ((Subgroup.center G).one_lt_card_iff_ne_bot.mp Fintype.one_lt_card)
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : IsPGroup p { x // x ∈ K }
hHK : H ≤ K
a b : { x // x ∈ H }
h : ↑(Subgroup.inclusion hHK) a = ↑(Subgroup.inclusion hHK) b
⊢ ↑a = ↑b
[PROOFSTEP]
change ((Subgroup.inclusion hHK) a : G) = (Subgroup.inclusion hHK) b
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
H K : Subgroup G
hK : IsPGroup p { x // x ∈ K }
hHK : H ≤ K
a b : { x // x ∈ H }
h : ↑(Subgroup.inclusion hHK) a = ↑(Subgroup.inclusion hHK) b
⊢ ↑(↑(Subgroup.inclusion hHK) a) = ↑(↑(Subgroup.inclusion hHK) b)
[PROOFSTEP]
apply Subtype.ext_iff.mp h
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : G →* K
⊢ IsPGroup p { x // x ∈ Subgroup.map ϕ H }
[PROOFSTEP]
rw [← H.subtype_range, MonoidHom.map_range]
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : G →* K
⊢ IsPGroup p { x // x ∈ MonoidHom.range (MonoidHom.comp ϕ (Subgroup.subtype H)) }
[PROOFSTEP]
exact hH.of_surjective (ϕ.restrict H).rangeRestrict (ϕ.restrict H).rangeRestrict_surjective
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
⊢ IsPGroup p { x // x ∈ Subgroup.comap ϕ H }
[PROOFSTEP]
intro g
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
⊢ ∃ k, g ^ p ^ k = 1
[PROOFSTEP]
obtain ⟨j, hj⟩ := hH ⟨ϕ g.1, g.2⟩
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
j : ℕ
hj : { val := ↑ϕ ↑g, property := (_ : ↑g ∈ Subgroup.comap ϕ H) } ^ p ^ j = 1
⊢ ∃ k, g ^ p ^ k = 1
[PROOFSTEP]
rw [Subtype.ext_iff, H.coe_pow, Subtype.coe_mk, ← ϕ.map_pow] at hj 
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
j : ℕ
hj : ↑ϕ (↑g ^ p ^ j) = ↑1
⊢ ∃ k, g ^ p ^ k = 1
[PROOFSTEP]
obtain ⟨k, hk⟩ := hϕ ⟨g.1 ^ p ^ j, hj⟩
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
j : ℕ
hj : ↑ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : { val := ↑g ^ p ^ j, property := hj } ^ p ^ k = 1
⊢ ∃ k, g ^ p ^ k = 1
[PROOFSTEP]
rw [Subtype.ext_iff, ϕ.ker.coe_pow, Subtype.coe_mk, ← pow_mul, ← pow_add] at hk 
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
j : ℕ
hj : ↑ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : ↑g ^ p ^ (j + k) = ↑1
⊢ ∃ k, g ^ p ^ k = 1
[PROOFSTEP]
exact ⟨j + k, by rwa [Subtype.ext_iff, (H.comap ϕ).coe_pow]⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
hH : IsPGroup p { x // x ∈ H }
K : Type u_2
inst✝ : Group K
ϕ : K →* G
hϕ : IsPGroup p { x // x ∈ MonoidHom.ker ϕ }
g : { x // x ∈ Subgroup.comap ϕ H }
j : ℕ
hj : ↑ϕ (↑g ^ p ^ j) = ↑1
k : ℕ
hk : ↑g ^ p ^ (j + k) = ↑1
⊢ g ^ p ^ (j + k) = 1
[PROOFSTEP]
rwa [Subtype.ext_iff, (H.comap ϕ).coe_pow]
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p { x // x ∈ H }
hK : IsPGroup p { x // x ∈ K }
inst✝ : Subgroup.Normal K
⊢ IsPGroup p { x // x ∈ H ⊔ K }
[PROOFSTEP]
rw [← QuotientGroup.ker_mk' K, ← Subgroup.comap_map_eq]
[GOAL]
p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p { x // x ∈ H }
hK : IsPGroup p { x // x ∈ K }
inst✝ : Subgroup.Normal K
⊢ IsPGroup p { x // x ∈ Subgroup.comap (QuotientGroup.mk' K) (Subgroup.map (QuotientGroup.mk' K) H) }
[PROOFSTEP]
apply (hH.map (QuotientGroup.mk' K)).comap_of_ker_isPGroup
[GOAL]
case hϕ
p : ℕ
G : Type u_1
inst✝¹ : Group G
H K : Subgroup G
hH : IsPGroup p { x // x ∈ H }
hK : IsPGroup p { x // x ∈ K }
inst✝ : Subgroup.Normal K
⊢ IsPGroup p { x // x ∈ MonoidHom.ker (QuotientGroup.mk' K) }
[PROOFSTEP]
rwa [QuotientGroup.ker_mk']
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
⊢ Nat.coprime (card { x // x ∈ H₁ }) (card { x // x ∈ H₂ })
[PROOFSTEP]
obtain ⟨n₁, heq₁⟩ := iff_card.mp hH₁
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ : ℕ
heq₁ : card { x // x ∈ H₁ } = p₁ ^ n₁
⊢ Nat.coprime (card { x // x ∈ H₁ }) (card { x // x ∈ H₂ })
[PROOFSTEP]
rw [heq₁]
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ : ℕ
heq₁ : card { x // x ∈ H₁ } = p₁ ^ n₁
⊢ Nat.coprime (p₁ ^ n₁) (card { x // x ∈ H₂ })
[PROOFSTEP]
clear heq₁
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ : ℕ
⊢ Nat.coprime (p₁ ^ n₁) (card { x // x ∈ H₂ })
[PROOFSTEP]
obtain ⟨n₂, heq₂⟩ := iff_card.mp hH₂
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ n₂ : ℕ
heq₂ : card { x // x ∈ H₂ } = p₂ ^ n₂
⊢ Nat.coprime (p₁ ^ n₁) (card { x // x ∈ H₂ })
[PROOFSTEP]
rw [heq₂]
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ n₂ : ℕ
heq₂ : card { x // x ∈ H₂ } = p₂ ^ n₂
⊢ Nat.coprime (p₁ ^ n₁) (p₂ ^ n₂)
[PROOFSTEP]
clear heq₂
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝³ : Group G
G₂ : Type u_2
inst✝² : Group G₂
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ : Subgroup G
H₂ : Subgroup G₂
inst✝¹ : Fintype { x // x ∈ H₁ }
inst✝ : Fintype { x // x ∈ H₂ }
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
n₁ n₂ : ℕ
⊢ Nat.coprime (p₁ ^ n₁) (p₂ ^ n₂)
[PROOFSTEP]
exact Nat.coprime_pow_primes _ _ hp₁.elim hp₂.elim hne
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
⊢ Disjoint H₁ H₂
[PROOFSTEP]
rw [Subgroup.disjoint_def]
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
⊢ ∀ {x : G}, x ∈ H₁ → x ∈ H₂ → x = 1
[PROOFSTEP]
intro x hx₁ hx₂
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
⊢ x = 1
[PROOFSTEP]
obtain ⟨n₁, hn₁⟩ := iff_orderOf.mp hH₁ ⟨x, hx₁⟩
[GOAL]
case intro
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf { val := x, property := hx₁ } = p₁ ^ n₁
⊢ x = 1
[PROOFSTEP]
obtain ⟨n₂, hn₂⟩ := iff_orderOf.mp hH₂ ⟨x, hx₂⟩
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf { val := x, property := hx₁ } = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf { val := x, property := hx₂ } = p₂ ^ n₂
⊢ x = 1
[PROOFSTEP]
rw [← orderOf_subgroup, Subgroup.coe_mk] at hn₁ hn₂ 
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf x = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
⊢ x = 1
[PROOFSTEP]
have : p₁ ^ n₁ = p₂ ^ n₂ := by rw [← hn₁, ← hn₂]
[GOAL]
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf x = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
⊢ p₁ ^ n₁ = p₂ ^ n₂
[PROOFSTEP]
rw [← hn₁, ← hn₂]
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁ : orderOf x = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
this : p₁ ^ n₁ = p₂ ^ n₂
⊢ x = 1
[PROOFSTEP]
rcases n₁.eq_zero_or_pos with (rfl | hn₁)
[GOAL]
case intro.intro.inl
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
hn₁ : orderOf x = p₁ ^ 0
this : p₁ ^ 0 = p₂ ^ n₂
⊢ x = 1
[PROOFSTEP]
simpa using hn₁
[GOAL]
case intro.intro.inr
p : ℕ
G : Type u_1
inst✝ : Group G
p₁ p₂ : ℕ
hp₁ : Fact (Nat.Prime p₁)
hp₂ : Fact (Nat.Prime p₂)
hne : p₁ ≠ p₂
H₁ H₂ : Subgroup G
hH₁ : IsPGroup p₁ { x // x ∈ H₁ }
hH₂ : IsPGroup p₂ { x // x ∈ H₂ }
x : G
hx₁ : x ∈ H₁
hx₂ : x ∈ H₂
n₁ : ℕ
hn₁✝ : orderOf x = p₁ ^ n₁
n₂ : ℕ
hn₂ : orderOf x = p₂ ^ n₂
this : p₁ ^ n₁ = p₂ ^ n₂
hn₁ : n₁ > 0
⊢ x = 1
[PROOFSTEP]
exact absurd (eq_of_prime_pow_eq hp₁.out.prime hp₂.out.prime hn₁ this) hne
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hn : 0 < n
inst✝ : Fintype { x // x ∈ center G }
⊢ ∃ k, k > 0 ∧ card { x // x ∈ center G } = p ^ k
[PROOFSTEP]
have hcG := to_subgroup (of_card hGpn) (center G)
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hn : 0 < n
inst✝ : Fintype { x // x ∈ center G }
hcG : IsPGroup p { x // x ∈ center G }
⊢ ∃ k, k > 0 ∧ card { x // x ∈ center G } = p ^ k
[PROOFSTEP]
rcases iff_card.1 hcG with _
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hn : 0 < n
inst✝ : Fintype { x // x ∈ center G }
hcG : IsPGroup p { x // x ∈ center G }
x✝ : ∃ n, card { x // x ∈ center G } = p ^ n
⊢ ∃ k, k > 0 ∧ card { x // x ∈ center G } = p ^ k
[PROOFSTEP]
haveI : Nontrivial G := (nontrivial_iff_card <| of_card hGpn).2 ⟨n, hn, hGpn⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝³ : Group G
inst✝² : Fintype G
inst✝¹ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hn : 0 < n
inst✝ : Fintype { x // x ∈ center G }
hcG : IsPGroup p { x // x ∈ center G }
x✝ : ∃ n, card { x // x ∈ center G } = p ^ n
this : Nontrivial G
⊢ ∃ k, k > 0 ∧ card { x // x ∈ center G } = p ^ k
[PROOFSTEP]
exact (nontrivial_iff_card hcG).mp (center_nontrivial (of_card hGpn))
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hG : card G = p ^ 2
⊢ IsCyclic (G ⧸ center G)
[PROOFSTEP]
classical
rcases card_center_eq_prime_pow hG zero_lt_two with ⟨k, hk0, hk⟩
rw [card_eq_card_quotient_mul_card_subgroup (center G), mul_comm, hk] at hG 
have hk2 := (Nat.pow_dvd_pow_iff_le_right (Fact.out (p := p.Prime)).one_lt).1 ⟨_, hG.symm⟩
interval_cases k
· rw [sq, pow_one, mul_right_inj' (Fact.out (p := p.Prime)).ne_zero] at hG 
  exact isCyclic_of_prime_card hG
·
  exact
    @isCyclic_of_subsingleton _ _
      ⟨Fintype.card_le_one_iff.1
          (mul_right_injective₀ (pow_ne_zero 2 (NeZero.ne p)) (hG.trans (mul_one (p ^ 2)).symm)).le⟩
[GOAL]
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hG : card G = p ^ 2
⊢ IsCyclic (G ⧸ center G)
[PROOFSTEP]
rcases card_center_eq_prime_pow hG zero_lt_two with ⟨k, hk0, hk⟩
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
hG : card G = p ^ 2
k : ℕ
hk0 : k > 0
hk : card { x // x ∈ center G } = p ^ k
⊢ IsCyclic (G ⧸ center G)
[PROOFSTEP]
rw [card_eq_card_quotient_mul_card_subgroup (center G), mul_comm, hk] at hG 
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
k : ℕ
hG : p ^ k * card (G ⧸ center G) = p ^ 2
hk0 : k > 0
hk : card { x // x ∈ center G } = p ^ k
⊢ IsCyclic (G ⧸ center G)
[PROOFSTEP]
have hk2 := (Nat.pow_dvd_pow_iff_le_right (Fact.out (p := p.Prime)).one_lt).1 ⟨_, hG.symm⟩
[GOAL]
case intro.intro
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
k : ℕ
hG : p ^ k * card (G ⧸ center G) = p ^ 2
hk0 : k > 0
hk : card { x // x ∈ center G } = p ^ k
hk2 : k ≤ 2
⊢ IsCyclic (G ⧸ center G)
[PROOFSTEP]
interval_cases k
[GOAL]
case intro.intro.«1»
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
k : ℕ
hG : p ^ 1 * card (G ⧸ center G) = p ^ 2
hk0 : 1 > 0
hk : card { x // x ∈ center G } = p ^ 1
hk2 : 1 ≤ 2
⊢ IsCyclic (G ⧸ center G)
[PROOFSTEP]
rw [sq, pow_one, mul_right_inj' (Fact.out (p := p.Prime)).ne_zero] at hG 
[GOAL]
case intro.intro.«1»
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
k : ℕ
hG : card (G ⧸ center G) = p
hk0 : 1 > 0
hk : card { x // x ∈ center G } = p ^ 1
hk2 : 1 ≤ 2
⊢ IsCyclic (G ⧸ center G)
[PROOFSTEP]
exact isCyclic_of_prime_card hG
[GOAL]
case intro.intro.«2»
p : ℕ
G : Type u_1
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : card G = p ^ n
k : ℕ
hG : p ^ 2 * card (G ⧸ center G) = p ^ 2
hk0 : 2 > 0
hk : card { x // x ∈ center G } = p ^ 2
hk2 : 2 ≤ 2
⊢ IsCyclic (G ⧸ center G)
[PROOFSTEP]
exact
  @isCyclic_of_subsingleton _ _
    ⟨Fintype.card_le_one_iff.1
        (mul_right_injective₀ (pow_ne_zero 2 (NeZero.ne p)) (hG.trans (mul_one (p ^ 2)).symm)).le⟩
