-- Mathlib/GroupTheory/Sylow.lean
theorem exists_subgroup_card_pow_succ [Finite G] {p : ℕ} {n : ℕ} [hp : Fact p.Prime]
    (hdvd : p ^ (n + 1) ∣ Nat.card G) {H : Subgroup G} (hH : Nat.card H = p ^ n) :
    ∃ K : Subgroup G, Nat.card K = p ^ (n + 1) ∧ H ≤ K :=
  let ⟨s, hs⟩ := exists_eq_mul_left_of_dvd hdvd
  have hcard : Nat.card (G ⧸ H) = s * p :=
    (mul_left_inj' (show Nat.card H ≠ 0 from Nat.card_pos.ne')).1
      (by
        rw [← card_eq_card_quotient_mul_card_subgroup H, hH, hs, pow_succ', mul_assoc, mul_comm p])
  have hm : s * p % p = Nat.card (normalizer H ⧸ H.subgroupOf H.normalizer) % p :=
    Nat.card_congr (fixedPointsMulLeftCosetsEquivQuotient H) ▸
      hcard ▸ (IsPGroup.of_card hH).card_modEq_card_fixedPoints _
  have hm' : p ∣ Nat.card (normalizer H ⧸ H.subgroupOf H.normalizer) :=
    Nat.dvd_of_mod_eq_zero (by rwa [Nat.mod_eq_zero_of_dvd (dvd_mul_left _ _), eq_comm] at hm)
  let ⟨x, hx⟩ := @exists_prime_orderOf_dvd_card' _ (QuotientGroup.Quotient.group _) _ _ hp hm'
  have hequiv : H ≃ H.subgroupOf H.normalizer := (subgroupOfEquivOfLe le_normalizer).symm.toEquiv
  ⟨Subgroup.map (normalizer H).subtype
      (Subgroup.comap (mk' (H.subgroupOf H.normalizer)) (zpowers x)), by
    show Nat.card (Subgroup.map H.normalizer.subtype
              (comap (mk' (H.subgroupOf H.normalizer)) (Subgroup.zpowers x))) = p ^ (n + 1)
    suffices Nat.card (Subtype.val ''
              (Subgroup.comap (mk' (H.subgroupOf H.normalizer)) (zpowers x) : Set H.normalizer)) =
        p ^ (n + 1)
      by convert this using 2
    rw [Nat.card_image_of_injective Subtype.val_injective
        (Subgroup.comap (mk' (H.subgroupOf H.normalizer)) (zpowers x) : Set H.normalizer),
      pow_succ, ← hH, Nat.card_congr hequiv, ← hx, ← Nat.card_zpowers, ←
      Nat.card_prod]
    exact Nat.card_congr
      (preimageMkEquivSubgroupProdSet (H.subgroupOf H.normalizer) (zpowers x)), by
    intro y hy
    simp only [exists_prop, Subgroup.coe_subtype, mk'_apply, Subgroup.mem_map, Subgroup.mem_comap]
    refine ⟨⟨y, le_normalizer hy⟩, ⟨0, ?_⟩, rfl⟩
    dsimp only
    rw [zpow_zero, eq_comm, QuotientGroup.eq_one_iff]
    simpa using hy⟩

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) % p
hm' : p ∣ Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer)
x : ↥H.normalizer ⧸ H.subgroupOf H.normalizer
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf H.normalizer)
y : G
hy : y ∈ H
⊢ ⟨y, ⋯⟩ ∈ H.subgroupOf H.normalizer

Tactic:
simpa using hy

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
⊢ Nat.card (G ⧸ H) * Nat.card ↥H = s * p * Nat.card ↥H

Tactic:
rw [← card_eq_card_quotient_mul_card_subgroup H, hH, hs, pow_succ', mul_assoc, mul_comm p]

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) % p
hm' : p ∣ Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer)
x : ↥H.normalizer ⧸ H.subgroupOf H.normalizer
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf H.normalizer)
⊢ Nat.card ↑↑(comap (mk' (H.subgroupOf H.normalizer)) (zpowers x)) =
    Nat.card (↥(H.subgroupOf H.normalizer) × ↥(zpowers x))

Tactic:
exact Nat.card_congr
  (preimageMkEquivSubgroupProdSet (H.subgroupOf H.normalizer) (zpowers x))

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) % p
⊢ Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) % p = 0

Tactic:
rwa [Nat.mod_eq_zero_of_dvd (dvd_mul_left _ _), eq_comm] at hm

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) % p
hm' : p ∣ Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer)
x : ↥H.normalizer ⧸ H.subgroupOf H.normalizer
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf H.normalizer)
y : G
hy : y ∈ H
⊢ ∃ x_1, ↑x_1 ∈ zpowers x ∧ ↑x_1 = y

Tactic:
refine ⟨⟨y, le_normalizer hy⟩, ⟨0, ?_⟩, rfl⟩

Result:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) % p
hm' : p ∣ Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer)
x : ↥H.normalizer ⧸ H.subgroupOf H.normalizer
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf H.normalizer)
y : G
hy : y ∈ H
⊢ (fun x_1 => x ^ x_1) 0 = ↑⟨y, ⋯⟩

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) % p
hm' : p ∣ Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer)
x : ↥H.normalizer ⧸ H.subgroupOf H.normalizer
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf H.normalizer)
this : Nat.card ↑(Subtype.val '' ↑(comap (mk' (H.subgroupOf H.normalizer)) (zpowers x))) = p ^ (n + 1)
⊢ Nat.card ↥(Subgroup.map H.normalizer.subtype (comap (mk' (H.subgroupOf H.normalizer)) (zpowers x))) = p ^ (n + 1)

Tactic:
convert this using 2

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) % p
hm' : p ∣ Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer)
x : ↥H.normalizer ⧸ H.subgroupOf H.normalizer
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf H.normalizer)
⊢ Nat.card ↥(Subgroup.map H.normalizer.subtype (comap (mk' (H.subgroupOf H.normalizer)) (zpowers x))) = p ^ (n + 1)

Tactic:
suffices Nat.card (Subtype.val ''
          (Subgroup.comap (mk' (H.subgroupOf H.normalizer)) (zpowers x) : Set H.normalizer)) =
    p ^ (n + 1)
  by convert this using 2

Result:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
p n : ℕ
hp : Fact (Nat.Prime p)
hdvd : p ^ (n + 1) ∣ Nat.card G
H : Subgroup G
hH : Nat.card ↥H = p ^ n
s : ℕ
hs : Nat.card G = s * p ^ (n + 1)
hcard : Nat.card (G ⧸ H) = s * p
hm : s * p % p = Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer) % p
hm' : p ∣ Nat.card (↥H.normalizer ⧸ H.subgroupOf H.normalizer)
x : ↥H.normalizer ⧸ H.subgroupOf H.normalizer
hx : orderOf x = p
hequiv : ↥H ≃ ↥(H.subgroupOf H.normalizer)
⊢ Nat.card ↑(Subtype.val '' ↑(comap (mk' (H.subgroupOf H.normalizer)) (zpowers x))) = p ^ (n + 1)