rw [Finset.card_insert_of_not_mem this.1, Finset.card_insert_of_not_mem this.2,
  Finset.card_singleton]
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
this : a ∉ {b, c} ∧ b ∉ {c}
⊢ {a, b, c}.card = 3
no goals