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