calc
  4 * c'.norm = (2 * c) ^ 2 + 3 * (2 * d) ^ 2 :=
    by
    rw [Zsqrtd.norm_def]
    ring
  _ < x ^ 2 + 3 * x ^ 2 := (add_lt_add ?_ ?_)
  _ = 4 * x ^ 2 := by ring
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 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ 4 * Zsqrtd.norm c' < 4 * x ^ 2
case intro.intro.intro.intro.intro.intro.refine'_2.calc_1
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ (2 * c) ^ 2 < x ^ 2

case intro.intro.intro.intro.intro.intro.refine'_2.calc_2
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ 3 * (2 * d) ^ 2 < 3 * x ^ 2