dsimp
case mk
a b c : ℤα
x y : ℝ
⊢ |({ re := x, im := y } -
          OneHom.toFun (↑↑inclusion)
            (let y_1 := round (2 * rt7⁻¹ * { re := x, im := y }.im);
            { z := round ({ re := x, im := y }.re - 2⁻¹ * ↑y_1), w := y_1 })).im| ≤
    |4⁻¹ * rt7|
case mk
a b c : ℤα
x y : ℝ
⊢ |y - (↑inclusion { z := round (x - 2⁻¹ * ↑(round (2 * rt7⁻¹ * y))), w := round (2 * rt7⁻¹ * y) }).im| ≤ |4⁻¹ * rt7|