rcases hx with (rfl | rfl | rfl) <;> rcases hy with (rfl | rfl | rfl)
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
n : ℕ
hn : 100 ≤ n
a b c : ℕ
hna : n ≤ a
hab : a < b
hbc : b < c
hcn : c ≤ 2 * n
h₁ : ∃ k, a + b = k ^ 2
h₂ : ∃ l, c + a = l ^ 2
h₃ : ∃ m, b + c = m ^ 2
x y : ℕ
hxy : x ≠ y
hx : x = a ∨ x = b ∨ x = c
hy : y = a ∨ y = b ∨ y = c
⊢ ∃ k, x + y = k ^ 2
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inl.inl
n : ℕ
hn : 100 ≤ n
b c : ℕ
hbc : b < c
hcn : c ≤ 2 * n
h₃ : ∃ m, b + c = m ^ 2
y : ℕ
hxy : y ≠ y
hna : n ≤ y
hab : y < b
h₁ : ∃ k, y + b = k ^ 2
h₂ : ∃ l, c + y = l ^ 2
⊢ ∃ k, y + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inl.inr.inl
n : ℕ
hn : 100 ≤ n
c : ℕ
hcn : c ≤ 2 * n
x y : ℕ
hxy : x ≠ y
hna : n ≤ x
h₂ : ∃ l, c + x = l ^ 2
hbc : y < c
h₃ : ∃ m, y + c = m ^ 2
hab : x < y
h₁ : ∃ k, x + y = k ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inl.inr.inr
n : ℕ
hn : 100 ≤ n
b x y : ℕ
hxy : x ≠ y
hna : n ≤ x
hab : x < b
h₁ : ∃ k, x + b = k ^ 2
hbc : b < y
hcn : y ≤ 2 * n
h₃ : ∃ m, b + y = m ^ 2
h₂ : ∃ l, y + x = l ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inl.inl
n : ℕ
hn : 100 ≤ n
c : ℕ
hcn : c ≤ 2 * n
x y : ℕ
hxy : x ≠ y
hbc : x < c
h₃ : ∃ m, x + c = m ^ 2
hna : n ≤ y
h₂ : ∃ l, c + y = l ^ 2
hab : y < x
h₁ : ∃ k, y + x = k ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inl.inr.inl
n : ℕ
hn : 100 ≤ n
a c : ℕ
hna : n ≤ a
hcn : c ≤ 2 * n
h₂ : ∃ l, c + a = l ^ 2
y : ℕ
hxy : y ≠ y
hab : a < y
hbc : y < c
h₁ : ∃ k, a + y = k ^ 2
h₃ : ∃ m, y + c = m ^ 2
⊢ ∃ k, y + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inl.inr.inr
n : ℕ
hn : 100 ≤ n
a : ℕ
hna : n ≤ a
x y : ℕ
hxy : x ≠ y
hab : a < x
h₁ : ∃ k, a + x = k ^ 2
hcn : y ≤ 2 * n
h₂ : ∃ l, y + a = l ^ 2
hbc : x < y
h₃ : ∃ m, x + y = m ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inl
n : ℕ
hn : 100 ≤ n
b x y : ℕ
hxy : x ≠ y
hbc : b < x
hcn : x ≤ 2 * n
h₃ : ∃ m, b + x = m ^ 2
hna : n ≤ y
hab : y < b
h₁ : ∃ k, y + b = k ^ 2
h₂ : ∃ l, x + y = l ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inr.inl
n : ℕ
hn : 100 ≤ n
a : ℕ
hna : n ≤ a
x y : ℕ
hxy : x ≠ y
hcn : x ≤ 2 * n
h₂ : ∃ l, x + a = l ^ 2
hab : a < y
h₁ : ∃ k, a + y = k ^ 2
hbc : y < x
h₃ : ∃ m, y + x = m ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inr.inr
n : ℕ
hn : 100 ≤ n
a b : ℕ
hna : n ≤ a
hab : a < b
h₁ : ∃ k, a + b = k ^ 2
y : ℕ
hxy : y ≠ y
hbc : b < y
hcn : y ≤ 2 * n
h₂ : ∃ l, y + a = l ^ 2
h₃ : ∃ m, b + y = m ^ 2
⊢ ∃ k, y + y = k ^ 2