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
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
haveI := H.normalCore.fintypeQuotientOfFiniteIndex
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
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
obtain ⟨n, hn⟩ := iff_card.mp (hG.to_quotient H.normalCore)
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
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
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))
no goals
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
exact ⟨k, hk2⟩