apply IsCoprime.dvd_of_dvd_mul_left _ this
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
this : ↑g ^ 2 ∣ x * y
⊢ ↑g ^ 2 ∣ y
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
this : ↑g ^ 2 ∣ x * y
⊢ IsCoprime (↑g ^ 2) x