English
If p^n ≤ |G|, there exists a Sylow p-subgroup of cardinality p^n in G.
Русский
Если p^n ≤ |G|, в G существует Sylow p-подгруппа кардинальности p^n.
LaTeX
$$∃ H: Subgroup G, card H = p^n$$
Lean4
/-- A special case of **Sylow's first theorem**. If `G` is a `p`-group and `H` a subgroup of size at
least `p ^ n` then there is a subgroup of `H` of cardinality `p ^ n`. -/
theorem exists_subgroup_le_card_pow_prime_of_le_card {n p : ℕ} (hp : p.Prime) (h : IsPGroup p G) {H : Subgroup G}
(hn : p ^ n ≤ Nat.card H) : ∃ H' ≤ H, Nat.card H' = p ^ n :=
by
obtain ⟨H', H'card⟩ := exists_subgroup_card_pow_prime_of_le_card hp (h.to_subgroup H) hn
refine ⟨H'.map H.subtype, map_subtype_le _, ?_⟩
rw [← H'card]
let e : H' ≃* H'.map H.subtype := H'.equivMapOfInjective (Subgroup.subtype H) H.subtype_injective
exact Nat.card_congr e.symm.toEquiv
