internlm/Lean-Github huggingface dataset:
Theorem: Imo2005P3.key_insight
Proof state before:
x y z : ℝ
hx : x > 0
hy : y > 0
hz : z > 0
h : x * y * z ≥ 1
key :
  (x ^ 5 - x ^ 2) / (x ^ 5 + y ^ 2 + z ^ 2) - (x ^ 5 - x ^ 2 * 1) / (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)) =
    (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) / ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2)))
h₅ : (x ^ 3 - 1) ^ 2 * x ^ 2 * (y ^ 2 + z ^ 2) / ((x ^ 5 + y ^ 2 + z ^ 2) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2))) ≥ 0
⊢ (x ^ 5 - x ^ 2 * (x * y * z)) * (x ^ 2 + y ^ 2 + z ^ 2) = (x ^ 2 - y * z) * (x ^ 3 * (x ^ 2 + y ^ 2 + z ^ 2))
Tactic:
ring
Proof state after:
no goals
Theorem: Imo2021P1.exists_numbers_in_interval
Proof state before:
n : ℕ
hn : 100 ≤ n
⊢ ∃ l, n + 4 * l ≤ 2 * l ^ 2 ∧ 2 * l ^ 2 + 4 * l ≤ 2 * n
Tactic:
have hn' : 1 ≤ Nat.sqrt (n + 1) := by
  rw [Nat.le_sqrt]
  omega
Proof state after:
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
⊢ ∃ l, n + 4 * l ≤ 2 * l ^ 2 ∧ 2 * l ^ 2 + 4 * l ≤ 2 * n
Theorem: Imo2021P1.exists_numbers_in_interval
Proof state before:
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
⊢ ∃ l, n + 4 * l ≤ 2 * l ^ 2 ∧ 2 * l ^ 2 + 4 * l ≤ 2 * n
Tactic:
have h₁ := Nat.sqrt_le' (n + 1)
Proof state after:
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
h₁ : (n + 1).sqrt ^ 2 ≤ n + 1
⊢ ∃ l, n + 4 * l ≤ 2 * l ^ 2 ∧ 2 * l ^ 2 + 4 * l ≤ 2 * n
Theorem: Imo2021P1.exists_numbers_in_interval
Proof state before:
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
h₁ : (n + 1).sqrt ^ 2 ≤ n + 1
⊢ ∃ l, n + 4 * l ≤ 2 * l ^ 2 ∧ 2 * l ^ 2 + 4 * l ≤ 2 * n
Tactic:
have h₂ := Nat.succ_le_succ_sqrt' (n + 1)
Proof state after:
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
h₁ : (n + 1).sqrt ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ ((n + 1).sqrt + 1) ^ 2
⊢ ∃ l, n + 4 * l ≤ 2 * l ^ 2 ∧ 2 * l ^ 2 + 4 * l ≤ 2 * n
Theorem: Imo2021P1.exists_numbers_in_interval
Proof state before:
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
h₁ : (n + 1).sqrt ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ ((n + 1).sqrt + 1) ^ 2
⊢ ∃ l, n + 4 * l ≤ 2 * l ^ 2 ∧ 2 * l ^ 2 + 4 * l ≤ 2 * n
Tactic:
have h₃ : 10 ≤ (n + 1).sqrt := by
  rw [Nat.le_sqrt]
  omega
Proof state after:
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
h₁ : (n + 1).sqrt ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ ((n + 1).sqrt + 1) ^ 2
h₃ : 10 ≤ (n + 1).sqrt
⊢ ∃ l, n + 4 * l ≤ 2 * l ^ 2 ∧ 2 * l ^ 2 + 4 * l ≤ 2 * n
Theorem: Imo2021P1.exists_numbers_in_interval
Proof state before:
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
h₁ : (n + 1).sqrt ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ ((n + 1).sqrt + 1) ^ 2
h₃ : 10 ≤ (n + 1).sqrt
⊢ ∃ l, n + 4 * l ≤ 2 * l ^ 2 ∧ 2 * l ^ 2 + 4 * l ≤ 2 * n
Tactic:
rw [← Nat.sub_add_cancel hn'] at h₁ h₂ h₃
Proof state after:
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
h₁ : ((n + 1).sqrt - 1 + 1) ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ ((n + 1).sqrt - 1 + 1 + 1) ^ 2
h₃ : 10 ≤ (n + 1).sqrt - 1 + 1
⊢ ∃ l, n + 4 * l ≤ 2 * l ^ 2 ∧ 2 * l ^ 2 + 4 * l ≤ 2 * n
Theorem: Imo2021P1.exists_numbers_in_interval
Proof state before:
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
h₁ : ((n + 1).sqrt - 1 + 1) ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ ((n + 1).sqrt - 1 + 1 + 1) ^ 2
h₃ : 10 ≤ (n + 1).sqrt - 1 + 1
⊢ ∃ l, n + 4 * l ≤ 2 * l ^ 2 ∧ 2 * l ^ 2 + 4 * l ≤ 2 * n
Tactic:
set l := (n + 1).sqrt - 1
Proof state after:
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
l : ℕ := (n + 1).sqrt - 1
h₁ : (l + 1) ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ (l + 1 + 1) ^ 2
h₃ : 10 ≤ l + 1
⊢ ∃ l, n + 4 * l ≤ 2 * l ^ 2 ∧ 2 * l ^ 2 + 4 * l ≤ 2 * n
Theorem: Imo2021P1.exists_numbers_in_interval
Proof state before:
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
l : ℕ := (n + 1).sqrt - 1
h₁ : (l + 1) ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ (l + 1 + 1) ^ 2
h₃ : 10 ≤ l + 1
⊢ ∃ l, n + 4 * l ≤ 2 * l ^ 2 ∧ 2 * l ^ 2 + 4 * l ≤ 2 * n
Tactic:
refine ⟨l, ?_, ?_⟩
Proof state after:
case refine_1
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
l : ℕ := (n + 1).sqrt - 1
h₁ : (l + 1) ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ (l + 1 + 1) ^ 2
h₃ : 10 ≤ l + 1
⊢ n + 4 * l ≤ 2 * l ^ 2

case refine_2
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
l : ℕ := (n + 1).sqrt - 1
h₁ : (l + 1) ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ (l + 1 + 1) ^ 2
h₃ : 10 ≤ l + 1
⊢ 2 * l ^ 2 + 4 * l ≤ 2 * n
Theorem: Imo2021P1.exists_numbers_in_interval
Proof state before:
n : ℕ
hn : 100 ≤ n
⊢ 1 ≤ (n + 1).sqrt
Tactic:
rw [Nat.le_sqrt]
Proof state after:
n : ℕ
hn : 100 ≤ n
⊢ 1 * 1 ≤ n + 1
Theorem: Imo2021P1.exists_numbers_in_interval
Proof state before:
n : ℕ
hn : 100 ≤ n
⊢ 1 * 1 ≤ n + 1
Tactic:
omega
Proof state after:
no goals
Theorem: Imo2021P1.exists_numbers_in_interval
Proof state before:
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
h₁ : (n + 1).sqrt ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ ((n + 1).sqrt + 1) ^ 2
⊢ 10 ≤ (n + 1).sqrt
Tactic:
rw [Nat.le_sqrt]
Proof state after:
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
h₁ : (n + 1).sqrt ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ ((n + 1).sqrt + 1) ^ 2
⊢ 10 * 10 ≤ n + 1
Theorem: Imo2021P1.exists_numbers_in_interval
Proof state before:
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
h₁ : (n + 1).sqrt ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ ((n + 1).sqrt + 1) ^ 2
⊢ 10 * 10 ≤ n + 1
Tactic:
omega
Proof state after:
no goals
Theorem: Imo2021P1.exists_numbers_in_interval
Proof state before:
case refine_1
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
l : ℕ := (n + 1).sqrt - 1
h₁ : (l + 1) ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ (l + 1 + 1) ^ 2
h₃ : 10 ≤ l + 1
⊢ n + 4 * l ≤ 2 * l ^ 2
Tactic:
calc n + 4 * l ≤ (l ^ 2 + 4 * l + 2) + 4 * l := by linarith only [h₂]
  _ ≤ 2 * l ^ 2 := by nlinarith only [h₃]
Proof state after:
no goals
Theorem: Imo2021P1.exists_numbers_in_interval
Proof state before:
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
l : ℕ := (n + 1).sqrt - 1
h₁ : (l + 1) ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ (l + 1 + 1) ^ 2
h₃ : 10 ≤ l + 1
⊢ n + 4 * l ≤ l ^ 2 + 4 * l + 2 + 4 * l
Tactic:
linarith only [h₂]
Proof state after:
no goals
Theorem: Imo2021P1.exists_numbers_in_interval
Proof state before:
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
l : ℕ := (n + 1).sqrt - 1
h₁ : (l + 1) ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ (l + 1 + 1) ^ 2
h₃ : 10 ≤ l + 1
⊢ l ^ 2 + 4 * l + 2 + 4 * l ≤ 2 * l ^ 2
Tactic:
nlinarith only [h₃]
Proof state after:
no goals
Theorem: Imo2021P1.exists_numbers_in_interval
Proof state before:
case refine_2
n : ℕ
hn : 100 ≤ n
hn' : 1 ≤ (n + 1).sqrt
l : ℕ := (n + 1).sqrt - 1
h₁ : (l + 1) ^ 2 ≤ n + 1
h₂ : n + 1 + 1 ≤ (l + 1 + 1) ^ 2
h₃ : 10 ≤ l + 1
⊢ 2 * l ^ 2 + 4 * l ≤ 2 * n
Tactic:
linarith only [h₁]
Proof state after:
no goals
Theorem: Imo2021P1.exists_triplet_summing_to_squares
Proof state before:
n : ℕ
hn : 100 ≤ n
⊢ ∃ a b c, n ≤ a ∧ a < b ∧ b < c ∧ c ≤ 2 * n ∧ (∃ k, a + b = k ^ 2) ∧ (∃ l, c + a = l ^ 2) ∧ ∃ m, b + c = m ^ 2
Tactic:
obtain ⟨l, hl1, hl2⟩ := exists_numbers_in_interval n hn
Proof state after:
case intro.intro
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
⊢ ∃ a b c, n ≤ a ∧ a < b ∧ b < c ∧ c ≤ 2 * n ∧ (∃ k, a + b = k ^ 2) ∧ (∃ l, c + a = l ^ 2) ∧ ∃ m, b + c = m ^ 2
Theorem: Imo2021P1.exists_triplet_summing_to_squares
Proof state before:
case intro.intro
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
⊢ ∃ a b c, n ≤ a ∧ a < b ∧ b < c ∧ c ≤ 2 * n ∧ (∃ k, a + b = k ^ 2) ∧ (∃ l, c + a = l ^ 2) ∧ ∃ m, b + c = m ^ 2
Tactic:
have p : 1 < l := by contrapose! hl1; interval_cases l <;> linarith
Proof state after:
case intro.intro
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
⊢ ∃ a b c, n ≤ a ∧ a < b ∧ b < c ∧ c ≤ 2 * n ∧ (∃ k, a + b = k ^ 2) ∧ (∃ l, c + a = l ^ 2) ∧ ∃ m, b + c = m ^ 2
Theorem: Imo2021P1.exists_triplet_summing_to_squares
Proof state before:
case intro.intro
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
⊢ ∃ a b c, n ≤ a ∧ a < b ∧ b < c ∧ c ≤ 2 * n ∧ (∃ k, a + b = k ^ 2) ∧ (∃ l, c + a = l ^ 2) ∧ ∃ m, b + c = m ^ 2
Tactic:
have h₁ : 4 * l ≤ 2 * l ^ 2 := by omega
Proof state after:
case intro.intro
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
⊢ ∃ a b c, n ≤ a ∧ a < b ∧ b < c ∧ c ≤ 2 * n ∧ (∃ k, a + b = k ^ 2) ∧ (∃ l, c + a = l ^ 2) ∧ ∃ m, b + c = m ^ 2
Theorem: Imo2021P1.exists_triplet_summing_to_squares
Proof state before:
case intro.intro
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
⊢ ∃ a b c, n ≤ a ∧ a < b ∧ b < c ∧ c ≤ 2 * n ∧ (∃ k, a + b = k ^ 2) ∧ (∃ l, c + a = l ^ 2) ∧ ∃ m, b + c = m ^ 2
Tactic:
have h₂ : 1 ≤ 2 * l := by omega
Proof state after:
case intro.intro
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ ∃ a b c, n ≤ a ∧ a < b ∧ b < c ∧ c ≤ 2 * n ∧ (∃ k, a + b = k ^ 2) ∧ (∃ l, c + a = l ^ 2) ∧ ∃ m, b + c = m ^ 2
Theorem: Imo2021P1.exists_triplet_summing_to_squares
Proof state before:
case intro.intro
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ ∃ a b c, n ≤ a ∧ a < b ∧ b < c ∧ c ≤ 2 * n ∧ (∃ k, a + b = k ^ 2) ∧ (∃ l, c + a = l ^ 2) ∧ ∃ m, b + c = m ^ 2
Tactic:
refine ⟨2 * l ^ 2 - 4 * l, 2 * l ^ 2 + 1, 2 * l ^ 2 + 4 * l, ?_, ?_, ?_,
  ⟨?_, ⟨2 * l - 1, ?_⟩, ⟨2 * l, ?_⟩, 2 * l + 1, ?_⟩⟩
Proof state after:
case intro.intro.refine_1
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ n ≤ 2 * l ^ 2 - 4 * l

case intro.intro.refine_2
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * l ^ 2 - 4 * l < 2 * l ^ 2 + 1

case intro.intro.refine_3
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * l ^ 2 + 1 < 2 * l ^ 2 + 4 * l

case intro.intro.refine_4
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * l ^ 2 + 4 * l ≤ 2 * n

case intro.intro.refine_5
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * l ^ 2 - 4 * l + (2 * l ^ 2 + 1) = (2 * l - 1) ^ 2

case intro.intro.refine_6
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * l ^ 2 + 4 * l + (2 * l ^ 2 - 4 * l) = (2 * l) ^ 2

case intro.intro.refine_7
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * l ^ 2 + 1 + (2 * l ^ 2 + 4 * l) = (2 * l + 1) ^ 2
Theorem: Imo2021P1.exists_triplet_summing_to_squares
Proof state before:
case intro.intro.refine_1
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ n ≤ 2 * l ^ 2 - 4 * l

case intro.intro.refine_2
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * l ^ 2 - 4 * l < 2 * l ^ 2 + 1

case intro.intro.refine_3
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * l ^ 2 + 1 < 2 * l ^ 2 + 4 * l

case intro.intro.refine_4
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * l ^ 2 + 4 * l ≤ 2 * n

case intro.intro.refine_5
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * l ^ 2 - 4 * l + (2 * l ^ 2 + 1) = (2 * l - 1) ^ 2

case intro.intro.refine_6
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * l ^ 2 + 4 * l + (2 * l ^ 2 - 4 * l) = (2 * l) ^ 2

case intro.intro.refine_7
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * l ^ 2 + 1 + (2 * l ^ 2 + 4 * l) = (2 * l + 1) ^ 2
Tactic:
all_goals zify [h₁, h₂]; linarith
Proof state after:
no goals
Theorem: Imo2021P1.exists_triplet_summing_to_squares
Proof state before:
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
⊢ 1 < l
Tactic:
contrapose! hl1
Proof state after:
n : ℕ
hn : 100 ≤ n
l : ℕ
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
hl1 : l ≤ 1
⊢ 2 * l ^ 2 < n + 4 * l
Theorem: Imo2021P1.exists_triplet_summing_to_squares
Proof state before:
n : ℕ
hn : 100 ≤ n
l : ℕ
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
hl1 : l ≤ 1
⊢ 2 * l ^ 2 < n + 4 * l
Tactic:
interval_cases l <;> linarith
Proof state after:
no goals
Theorem: Imo2021P1.exists_triplet_summing_to_squares
Proof state before:
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
⊢ 4 * l ≤ 2 * l ^ 2
Tactic:
omega
Proof state after:
no goals
Theorem: Imo2021P1.exists_triplet_summing_to_squares
Proof state before:
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
⊢ 1 ≤ 2 * l
Tactic:
omega
Proof state after:
no goals
Theorem: Imo2021P1.exists_triplet_summing_to_squares
Proof state before:
case intro.intro.refine_7
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * l ^ 2 + 1 + (2 * l ^ 2 + 4 * l) = (2 * l + 1) ^ 2
Tactic:
zify [h₁, h₂]
Proof state after:
case intro.intro.refine_7
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * ↑l ^ 2 + 1 + (2 * ↑l ^ 2 + 4 * ↑l) = (2 * ↑l + 1) ^ 2
Theorem: Imo2021P1.exists_triplet_summing_to_squares
Proof state before:
case intro.intro.refine_7
n : ℕ
hn : 100 ≤ n
l : ℕ
hl1 : n + 4 * l ≤ 2 * l ^ 2
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
p : 1 < l
h₁ : 4 * l ≤ 2 * l ^ 2
h₂ : 1 ≤ 2 * l
⊢ 2 * ↑l ^ 2 + 1 + (2 * ↑l ^ 2 + 4 * ↑l) = (2 * ↑l + 1) ^ 2
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares
Proof 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
Proof 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
Theorem: Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares
Proof 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}, ?_, ?_, ?_⟩
Proof 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
Theorem: Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares
Proof 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]
Proof 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
Theorem: Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares
Proof 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]
Proof 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}
Theorem: Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares
Proof 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]
Proof state after:
no goals
Theorem: Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares
Proof 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]
Proof state after:
no goals
Theorem: Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares
Proof 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]
Proof 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
Theorem: Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares
Proof 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
Proof 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
Theorem: Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares
Proof 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⟩
Proof state after:
no goals
Theorem: Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares
Proof 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
Proof 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
Theorem: Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares
Proof 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
Proof 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
Theorem: Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares
Proof 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)
Proof 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