rcases ey with ⟨b, hb⟩
case intro
x y : ℤ
ey : ∃ k, y = 2 * k + 1
a : ℤ
ha : x = 2 * a + 1
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r
case intro.intro
x y a : ℤ
ha : x = 2 * a + 1
b : ℤ
hb : y = 2 * b + 1
⊢ ∃ r, x ^ 2 + y ^ 2 = r + r