English
If p^n ≤ |G|, then there exists a Sylow p-subgroup of G contained in a subgroup of suitable order p^m with m ≥ n.
Русский
Если p^n ≤ |G|, существует подгруппа Шилова p-подгруппы, содержащая её в подпгруппе порядка p^m с m ≥ n.
LaTeX
$$∃ H' ≤ G, card H' = p^m ∧ card H ≤ card H'$$
Lean4
/-- If `H` is a subgroup of `G` of cardinality `p ^ n`,
then `H` is contained in a subgroup of cardinality `p ^ m`
if `n ≤ m` and `p ^ m` divides the cardinality of `G` -/
theorem exists_subgroup_card_pow_prime_le [Finite G] (p : ℕ) :
∀ {n m : ℕ} [_hp : Fact p.Prime] (_hdvd : p ^ m ∣ Nat.card G) (H : Subgroup G) (_hH : Nat.card H = p ^ n)
(_hnm : n ≤ m), ∃ K : Subgroup G, Nat.card K = p ^ m ∧ H ≤ K
| n, m => fun {hdvd H hH hnm} =>
(lt_or_eq_of_le hnm).elim
(fun hnm : n < m =>
have h0m : 0 < m := lt_of_le_of_lt n.zero_le hnm
have hnm1 : n ≤ m - 1 := le_tsub_of_add_le_right hnm
let ⟨K, hK⟩ :=
@exists_subgroup_card_pow_prime_le _ _ n (m - 1) _ (Nat.pow_dvd_of_le_of_pow_dvd tsub_le_self hdvd) H hH hnm1
have hdvd' : p ^ (m - 1 + 1) ∣ Nat.card G := by rwa [tsub_add_cancel_of_le h0m.nat_succ_le]
let ⟨K', hK'⟩ := @exists_subgroup_card_pow_succ _ _ _ _ _ _ hdvd' K hK.1
⟨K', by rw [hK'.1, tsub_add_cancel_of_le h0m.nat_succ_le], le_trans hK.2 hK'.2⟩)
fun hnm : n = m => ⟨H, by simp [hH, hnm]⟩
