rw [← mul_lt_mul_left (by norm_num : (0 : ℤ) < 4)]
case intro.intro.intro.intro.intro.intro.refine'_2
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
c' : ℤ√(-3) := { re := c, im := d }
⊢ c'.norm < x ^ 2
case intro.intro.intro.intro.intro.intro.refine'_2
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
c' : ℤ√(-3) := { re := c, im := d }
⊢ 4 * c'.norm < 4 * x ^ 2