Prime Theorem Help

Stream: general

[Debendro Mookerjee]

Here is the theorem I am trying to prove:
Let n > 1. If n has no positive prime factor less than or equal to sqrt(n), then n is prime.

Here is a proof from Hungerford's Abstract Algebra:
Suppose n has the given property but assume that n is not prime. Then n has at least two positive prime factors, say p1 and p2, so that n = p1p2k for some positive integer k. By hypothesis, n has no positive prime divisors less than or equal to sqrt(n). Hence p1 > sqrt(n) and p2 > sqrt(n). Hence n = p1p2k >= p1*p2 >n. Contradiction.

I am new to lean, so I am trying to translate proofs in textbooks for practice. Can anyone please tell me how to translate this proof into Lean code?

[Kevin Buzzard]

Conversation moved to here