Disprove $ f\mid e^2, e\gcd(e,f),\gcd(e,f)^2\Rightarrow f\mid e\ $

Question

(This has been cross-posted from a now-deleted MO question, per advice from Neil Strickland.)

Suppose we have natural numbers $E$ and $F$ such that all of $$G = \frac{\bigg(\gcd(E,F)\bigg)^2}{F}$$ $$H = \frac{E^2}{F}$$ $$I = \bigg(\frac{E}{F}\bigg)\cdot\gcd(E,F)$$ and $$J = \frac{E}{\gcd(E,F)}$$ are also natural numbers.

Here are my questions:

Is it possible to ask the theorem prover called Lean whether it follows from these combined premises that $F$ divides $E$? If so, what is Lean's answer?

(Caveat: I know that Lean is open source, however, I have not yet gotten down to studying it in detail, so any help is appreciated.)

Answer 1

Based on comments from Neil Strickland in MathOverflow here and there:

• The case $(E,F)=(2,4)$ is a counterexample.
• The case $(E,F)=(3,9)$ is also a counterexample.

Neil also advised that Lean is mostly for checking proofs, it is not very good at finding them.