ext <;> dsimp <;> simp only [MulZeroClass.mul_zero, round_zero, algebraMap.coe_zero, sub_zero] <;>
norm_num
a b c : ℤα
this : OneHom.toFun (↑↑inclusion) 0 = 0
⊢ (let y := round (2 * rt7⁻¹ * 0.im);
    { z := round (0.re - 2⁻¹ * ↑y), w := y }) =
    0
no goals