simp only [Finset.mem_insert, Finset.mem_singleton]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_3
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
⊢ ∀ c_1 ∈ {a, b, c}, n ≤ c_1 ∧ c_1 ≤ 2 * n
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_3
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
⊢ ∀ (c_1 : ℕ), c_1 = a ∨ c_1 = b ∨ c_1 = c → n ≤ c_1 ∧ c_1 ≤ 2 * n