obtain ⟨a, b, c, hna, hab, hbc, hcn, h₁, h₂, h₃⟩ := exists_triplet_summing_to_squares n hn
n : ℕ
hn : 100 ≤ n
⊢ ∃ 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
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