Theorem: Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares (Compfiles/Imo2021P1.lean)

State before:
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
Tactic:
obtain ⟨a, b, c, hna, hab, hbc, hcn, h₁, h₂, h₃⟩ := exists_triplet_summing_to_squares n hn
State after:
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

State before:
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
Tactic:
refine ⟨{a, b, c}, ?_, ?_, ?_⟩
State after:
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

State before:
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
Tactic:
suffices ({a, b, c} : Finset ℕ).card = 3 by rw [this]
State after:
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
⊢ {a, b, c}.card = 3

State before:
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
⊢ {a, b, c}.card = 3
Tactic:
suffices a ∉ {b, c} ∧ b ∉ {c} by
  rw [Finset.card_insert_of_not_mem this.1, Finset.card_insert_of_not_mem this.2,
    Finset.card_singleton]
State after:
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
⊢ a ∉ {b, c} ∧ b ∉ {c}

State before:
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}.card = 3
⊢ 2 * 1 + 1 ≤ {a, b, c}.card
Tactic:
rw [this]
State after:
no goals

State before:
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
Tactic:
rw [Finset.card_insert_of_not_mem this.1, Finset.card_insert_of_not_mem this.2,
  Finset.card_singleton]
State after:
no goals

State before:
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
⊢ a ∉ {b, c} ∧ b ∉ {c}
Tactic:
rw [Finset.mem_insert, Finset.mem_singleton, Finset.mem_singleton]
State after:
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
⊢ ¬(a = b ∨ a = c) ∧ ¬b = c

State before:
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
⊢ ¬(a = b ∨ a = c) ∧ ¬b = c
Tactic:
push_neg
State after:
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
⊢ (a ≠ b ∧ a ≠ c) ∧ b ≠ c

State before:
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
⊢ (a ≠ b ∧ a ≠ c) ∧ b ≠ c
Tactic:
exact ⟨⟨hab.ne, (hab.trans hbc).ne⟩, hbc.ne⟩
State after:
no goals

State before:
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
Tactic:
intro x hx y hy hxy
State after:
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

State before:
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
Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton] at hx hy
State after:
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

State before:
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
Tactic:
rcases hx with (rfl | rfl | rfl) <;> rcases hy with (rfl | rfl | rfl)
State after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inl.inl
n : ℕ
hn : 100 ≤ n
b c : ℕ
hbc : b < c
hcn : c ≤ 2 * n
h₃ : ∃ m, b + c = m ^ 2
y : ℕ
hxy : y ≠ y
hna : n ≤ y
hab : y < b
h₁ : ∃ k, y + b = k ^ 2
h₂ : ∃ l, c + y = l ^ 2
⊢ ∃ k, y + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inl.inr.inl
n : ℕ
hn : 100 ≤ n
c : ℕ
hcn : c ≤ 2 * n
x y : ℕ
hxy : x ≠ y
hna : n ≤ x
h₂ : ∃ l, c + x = l ^ 2
hbc : y < c
h₃ : ∃ m, y + c = m ^ 2
hab : x < y
h₁ : ∃ k, x + y = k ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inl.inr.inr
n : ℕ
hn : 100 ≤ n
b x y : ℕ
hxy : x ≠ y
hna : n ≤ x
hab : x < b
h₁ : ∃ k, x + b = k ^ 2
hbc : b < y
hcn : y ≤ 2 * n
h₃ : ∃ m, b + y = m ^ 2
h₂ : ∃ l, y + x = l ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inl.inl
n : ℕ
hn : 100 ≤ n
c : ℕ
hcn : c ≤ 2 * n
x y : ℕ
hxy : x ≠ y
hbc : x < c
h₃ : ∃ m, x + c = m ^ 2
hna : n ≤ y
h₂ : ∃ l, c + y = l ^ 2
hab : y < x
h₁ : ∃ k, y + x = k ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inl.inr.inl
n : ℕ
hn : 100 ≤ n
a c : ℕ
hna : n ≤ a
hcn : c ≤ 2 * n
h₂ : ∃ l, c + a = l ^ 2
y : ℕ
hxy : y ≠ y
hab : a < y
hbc : y < c
h₁ : ∃ k, a + y = k ^ 2
h₃ : ∃ m, y + c = m ^ 2
⊢ ∃ k, y + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inl.inr.inr
n : ℕ
hn : 100 ≤ n
a : ℕ
hna : n ≤ a
x y : ℕ
hxy : x ≠ y
hab : a < x
h₁ : ∃ k, a + x = k ^ 2
hcn : y ≤ 2 * n
h₂ : ∃ l, y + a = l ^ 2
hbc : x < y
h₃ : ∃ m, x + y = m ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inl
n : ℕ
hn : 100 ≤ n
b x y : ℕ
hxy : x ≠ y
hbc : b < x
hcn : x ≤ 2 * n
h₃ : ∃ m, b + x = m ^ 2
hna : n ≤ y
hab : y < b
h₁ : ∃ k, y + b = k ^ 2
h₂ : ∃ l, x + y = l ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inr.inl
n : ℕ
hn : 100 ≤ n
a : ℕ
hna : n ≤ a
x y : ℕ
hxy : x ≠ y
hcn : x ≤ 2 * n
h₂ : ∃ l, x + a = l ^ 2
hab : a < y
h₁ : ∃ k, a + y = k ^ 2
hbc : y < x
h₃ : ∃ m, y + x = m ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inr.inr
n : ℕ
hn : 100 ≤ n
a b : ℕ
hna : n ≤ a
hab : a < b
h₁ : ∃ k, a + b = k ^ 2
y : ℕ
hxy : y ≠ y
hbc : b < y
hcn : y ≤ 2 * n
h₂ : ∃ l, y + a = l ^ 2
h₃ : ∃ m, b + y = m ^ 2
⊢ ∃ k, y + y = k ^ 2

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inl.inl
n : ℕ
hn : 100 ≤ n
b c : ℕ
hbc : b < c
hcn : c ≤ 2 * n
h₃ : ∃ m, b + c = m ^ 2
y : ℕ
hxy : y ≠ y
hna : n ≤ y
hab : y < b
h₁ : ∃ k, y + b = k ^ 2
h₂ : ∃ l, c + y = l ^ 2
⊢ ∃ k, y + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inl.inr.inl
n : ℕ
hn : 100 ≤ n
c : ℕ
hcn : c ≤ 2 * n
x y : ℕ
hxy : x ≠ y
hna : n ≤ x
h₂ : ∃ l, c + x = l ^ 2
hbc : y < c
h₃ : ∃ m, y + c = m ^ 2
hab : x < y
h₁ : ∃ k, x + y = k ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inl.inr.inr
n : ℕ
hn : 100 ≤ n
b x y : ℕ
hxy : x ≠ y
hna : n ≤ x
hab : x < b
h₁ : ∃ k, x + b = k ^ 2
hbc : b < y
hcn : y ≤ 2 * n
h₃ : ∃ m, b + y = m ^ 2
h₂ : ∃ l, y + x = l ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inl.inl
n : ℕ
hn : 100 ≤ n
c : ℕ
hcn : c ≤ 2 * n
x y : ℕ
hxy : x ≠ y
hbc : x < c
h₃ : ∃ m, x + c = m ^ 2
hna : n ≤ y
h₂ : ∃ l, c + y = l ^ 2
hab : y < x
h₁ : ∃ k, y + x = k ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inl.inr.inl
n : ℕ
hn : 100 ≤ n
a c : ℕ
hna : n ≤ a
hcn : c ≤ 2 * n
h₂ : ∃ l, c + a = l ^ 2
y : ℕ
hxy : y ≠ y
hab : a < y
hbc : y < c
h₁ : ∃ k, a + y = k ^ 2
h₃ : ∃ m, y + c = m ^ 2
⊢ ∃ k, y + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inl.inr.inr
n : ℕ
hn : 100 ≤ n
a : ℕ
hna : n ≤ a
x y : ℕ
hxy : x ≠ y
hab : a < x
h₁ : ∃ k, a + x = k ^ 2
hcn : y ≤ 2 * n
h₂ : ∃ l, y + a = l ^ 2
hbc : x < y
h₃ : ∃ m, x + y = m ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inl
n : ℕ
hn : 100 ≤ n
b x y : ℕ
hxy : x ≠ y
hbc : b < x
hcn : x ≤ 2 * n
h₃ : ∃ m, b + x = m ^ 2
hna : n ≤ y
hab : y < b
h₁ : ∃ k, y + b = k ^ 2
h₂ : ∃ l, x + y = l ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inr.inl
n : ℕ
hn : 100 ≤ n
a : ℕ
hna : n ≤ a
x y : ℕ
hxy : x ≠ y
hcn : x ≤ 2 * n
h₂ : ∃ l, x + a = l ^ 2
hab : a < y
h₁ : ∃ k, a + y = k ^ 2
hbc : y < x
h₃ : ∃ m, y + x = m ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inr.inr
n : ℕ
hn : 100 ≤ n
a b : ℕ
hna : n ≤ a
hab : a < b
h₁ : ∃ k, a + b = k ^ 2
y : ℕ
hxy : y ≠ y
hbc : b < y
hcn : y ≤ 2 * n
h₂ : ∃ l, y + a = l ^ 2
h₃ : ∃ m, b + y = m ^ 2
⊢ ∃ k, y + y = k ^ 2
Tactic:
all_goals
  first
  | contradiction
  | assumption
  | simpa only [add_comm x y]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inr.inr
n : ℕ
hn : 100 ≤ n
a b : ℕ
hna : n ≤ a
hab : a < b
h₁ : ∃ k, a + b = k ^ 2
y : ℕ
hxy : y ≠ y
hbc : b < y
hcn : y ≤ 2 * n
h₂ : ∃ l, y + a = l ^ 2
h₃ : ∃ m, b + y = m ^ 2
⊢ ∃ k, y + y = k ^ 2
Tactic:
first
| contradiction
| assumption
| simpa only [add_comm x y]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inr.inr
n : ℕ
hn : 100 ≤ n
a b : ℕ
hna : n ≤ a
hab : a < b
h₁ : ∃ k, a + b = k ^ 2
y : ℕ
hxy : y ≠ y
hbc : b < y
hcn : y ≤ 2 * n
h₂ : ∃ l, y + a = l ^ 2
h₃ : ∃ m, b + y = m ^ 2
⊢ ∃ k, y + y = k ^ 2
Tactic:
contradiction
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inl
n : ℕ
hn : 100 ≤ n
b x y : ℕ
hxy : x ≠ y
hbc : b < x
hcn : x ≤ 2 * n
h₃ : ∃ m, b + x = m ^ 2
hna : n ≤ y
hab : y < b
h₁ : ∃ k, y + b = k ^ 2
h₂ : ∃ l, x + y = l ^ 2
⊢ ∃ k, x + y = k ^ 2
Tactic:
assumption
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inr.inl
n : ℕ
hn : 100 ≤ n
a : ℕ
hna : n ≤ a
x y : ℕ
hxy : x ≠ y
hcn : x ≤ 2 * n
h₂ : ∃ l, x + a = l ^ 2
hab : a < y
h₁ : ∃ k, a + y = k ^ 2
hbc : y < x
h₃ : ∃ m, y + x = m ^ 2
⊢ ∃ k, x + y = k ^ 2
Tactic:
simpa only [add_comm x y]
State after:
no goals

State before:
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
Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton]
State after:
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

State before:
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
Tactic:
omega
State after:
no goals