dsimp only
case intro.inl.intro.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re = 4 * v - a.im
⊢ 4 * v - a.im =
      { re := 1, im := -1 }.re * { re := v - a.im, im := v }.re +
        -3 * { re := 1, im := -1 }.im * { re := v - a.im, im := v }.im ∧
    a.im =
      { re := 1, im := -1 }.re * { re := v - a.im, im := v }.im +
        { re := 1, im := -1 }.im * { re := v - a.im, im := v }.re
case intro.inl.intro.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
ha : Odd a.re
hb : Odd a.im
v : ℤ
hv : a.re = 4 * v - a.im
⊢ 4 * v - a.im = 1 * (v - a.im) + -3 * -1 * v ∧ a.im = 1 * v + -1 * (v - a.im)