case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : relindex (↑P) (normalizer ↑P) ≠ 0
val✝ : Fintype (Sylow p G)
⊢ ¬p ∣ index ↑P
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : relindex (↑P) (normalizer ↑P) ≠ 0
⊢ ¬p ∣ index ↑P
cases nonempty_fintype (Sylow p G)
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : relindex (↑P) (normalizer ↑P) ≠ 0
val✝ : Fintype (Sylow p G)
⊢ ¬p ∣ relindex (↑P) (normalizer ↑P) * card (Sylow p G)
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : relindex (↑P) (normalizer ↑P) ≠ 0
val✝ : Fintype (Sylow p G)
⊢ ¬p ∣ index ↑P
rw [← relindex_mul_index le_normalizer, ← card_sylow_eq_index_normalizer]
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : relindex (↑P) (normalizer ↑P) ≠ 0
val✝ : Fintype (Sylow p G)
this : Normal ↑(Sylow.subtype P (_ : ↑P ≤ normalizer ↑P))
⊢ ¬p ∣ relindex (↑P) (normalizer ↑P) * card (Sylow p G)
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : relindex (↑P) (normalizer ↑P) ≠ 0
val✝ : Fintype (Sylow p G)
⊢ ¬p ∣ relindex (↑P) (normalizer ↑P) * card (Sylow p G)
haveI : (P.subtype le_normalizer : Subgroup (P : Subgroup G).normalizer).Normal :=
  Subgroup.normal_in_normalizer
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : relindex (↑P) (normalizer ↑P) ≠ 0
val✝ : Fintype (Sylow p G)
this✝ : Normal ↑(Sylow.subtype P (_ : ↑P ≤ normalizer ↑P))
this : FiniteIndex ↑(Sylow.subtype P (_ : ↑P ≤ normalizer ↑P))
⊢ ¬p ∣ relindex (↑P) (normalizer ↑P) * card (Sylow p G)
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : relindex (↑P) (normalizer ↑P) ≠ 0
val✝ : Fintype (Sylow p G)
this : Normal ↑(Sylow.subtype P (_ : ↑P ≤ normalizer ↑P))
⊢ ¬p ∣ relindex (↑P) (normalizer ↑P) * card (Sylow p G)
haveI : FiniteIndex ↑(P.subtype le_normalizer : Subgroup (P : Subgroup G).normalizer) := ⟨hP⟩
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
val✝ : Fintype (Sylow p G)
this✝ : Normal ↑(Sylow.subtype P (_ : ↑P ≤ normalizer ↑P))
this : FiniteIndex ↑(Sylow.subtype P (_ : ↑P ≤ normalizer ↑P))
hP : ¬p ∣ index ↑(Sylow.subtype P (_ : ↑P ≤ normalizer ↑P))
⊢ ¬p ∣ relindex (↑P) (normalizer ↑P) * card (Sylow p G)
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
hP : relindex (↑P) (normalizer ↑P) ≠ 0
val✝ : Fintype (Sylow p G)
this✝ : Normal ↑(Sylow.subtype P (_ : ↑P ≤ normalizer ↑P))
this : FiniteIndex ↑(Sylow.subtype P (_ : ↑P ≤ normalizer ↑P))
⊢ ¬p ∣ relindex (↑P) (normalizer ↑P) * card (Sylow p G)
replace hP := not_dvd_index_sylow' (P.subtype le_normalizer)
no goals
case intro
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
val✝ : Fintype (Sylow p G)
this✝ : Normal ↑(Sylow.subtype P (_ : ↑P ≤ normalizer ↑P))
this : FiniteIndex ↑(Sylow.subtype P (_ : ↑P ≤ normalizer ↑P))
hP : ¬p ∣ index ↑(Sylow.subtype P (_ : ↑P ≤ normalizer ↑P))
⊢ ¬p ∣ relindex (↑P) (normalizer ↑P) * card (Sylow p G)
exact hp.1.not_dvd_mul hP (not_dvd_card_sylow p G)