Sylow's first theorem

import Mathlib

theorem sylow_one {G : Type*} [Group G] [Fintype G] (p : ℕ) (hp : p.Prime) (n : ℕ) (h : p ^ n ∣ Fintype.card G) : ∃ H : Subgroup G, Nat.card H = p ^ n := by
  haveI : Fact p.Prime := ⟨hp⟩
  rw [← Nat.card_eq_fintype_card] at h
  exact Sylow.exists_subgroup_card_pow_prime p h