refine ⟨{a, b, c}, ?_, ?_, ?_⟩
case intro.intro.intro.intro.intro.intro.intro.intro.intro
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
⊢ ∃ B, 2 * 1 + 1 ≤ B.card ∧ (∀ a ∈ B, ∀ b ∈ B, a ≠ b → ∃ k, a + b = k ^ 2) ∧ ∀ c ∈ B, n ≤ c ∧ c ≤ 2 * n
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
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
⊢ 2 * 1 + 1 ≤ {a, b, c}.card

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
⊢ ∀ a_1 ∈ {a, b, c}, ∀ b_1 ∈ {a, b, c}, a_1 ≠ b_1 → ∃ k, a_1 + b_1 = k ^ 2

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