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

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
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

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
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

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
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

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
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

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, ?_⟩⟩
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

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

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
State after:
n : ℕ
hn : 100 ≤ n
l : ℕ
hl2 : 2 * l ^ 2 + 4 * l ≤ 2 * n
hl1 : l ≤ 1
⊢ 2 * l ^ 2 < n + 4 * l

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

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

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

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₂]
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

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