simp only [Finset.mem_insert, Finset.mem_singleton] at hx hy
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 : ℕ
hx : x ∈ {a, b, c}
y : ℕ
hy : y ∈ {a, b, c}
hxy : x ≠ y
⊢ ∃ k, x + y = k ^ 2
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