p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
h : p ∣ index ↑P
⊢ False
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
⊢ ¬p ∣ index ↑P
intro h
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
h : p ∣ index ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
⊢ False
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
h : p ∣ index ↑P
⊢ False
letI : Fintype (G ⧸ (P : Subgroup G)) := (P : Subgroup G).fintypeQuotientOfFiniteIndex
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h : p ∣ card (G ⧸ ↑P)
⊢ False
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
h : p ∣ index ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
⊢ False
rw [index_eq_card (P : Subgroup G)] at h
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
⊢ False
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h : p ∣ card (G ⧸ ↑P)
⊢ False
obtain ⟨x, hx⟩ := exists_prime_orderOf_dvd_card (G := G ⧸ (P : Subgroup G)) p h
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
⊢ False
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
⊢ False
have h := IsPGroup.of_card ((orderOf_eq_card_zpowers.symm.trans hx).trans (pow_one p).symm)
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ False
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
⊢ False
let Q := (zpowers x).comap (QuotientGroup.mk' (P : Subgroup G))
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p { x // x ∈ Q }
⊢ False
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ False
have hQ : IsPGroup p Q := by
  apply h.comap_of_ker_isPGroup
  rw [QuotientGroup.ker_mk']
  exact P.2
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p { x // x ∈ Q }
hp : ¬x = 1
⊢ False
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p { x // x ∈ Q }
⊢ False
replace hp := mt orderOf_eq_one_iff.mpr (ne_of_eq_of_ne hx hp.1.ne_one)
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p { x // x ∈ Q }
hp : ↑P < comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ False
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p { x // x ∈ Q }
hp : ¬x = 1
⊢ False
rw [← zpowers_eq_bot, ← Ne, ← bot_lt_iff_ne_bot, ←
  comap_lt_comap_of_surjective (QuotientGroup.mk'_surjective _), MonoidHom.comap_bot,
  QuotientGroup.ker_mk'] at hp
no goals
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p { x // x ∈ Q }
hp : ↑P < comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ False
exact hp.ne' (P.3 hQ hp.le)
case hϕ
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ IsPGroup p { x // x ∈ MonoidHom.ker (QuotientGroup.mk' ↑P) }
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ IsPGroup p { x // x ∈ Q }
apply h.comap_of_ker_isPGroup
case hϕ
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ IsPGroup p { x // x ∈ ↑P }
case hϕ
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ IsPGroup p { x // x ∈ MonoidHom.ker (QuotientGroup.mk' ↑P) }
rw [QuotientGroup.ker_mk']
no goals
case hϕ
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Sylow p G
inst✝ : Normal ↑P
fP : FiniteIndex ↑P
this : Fintype (G ⧸ ↑P) := fintypeQuotientOfFiniteIndex ↑P
h✝ : p ∣ card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p { x_1 // x_1 ∈ zpowers x }
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ IsPGroup p { x // x ∈ ↑P }
exact P.2