exact dvd_pow hkdvdleft (by norm_num)
case intro.intro.intro.intro.refine'_3.H.ha.h₁
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ k ∣ a ^ 3
no goals