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

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

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

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

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

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

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

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

State before:
n : ℕ
hn : 100 ≤ n
⊢ 1 ≤ (n + 1).sqrt
Tactic:
rw [Nat.le_sqrt]
State after:
n : ℕ
hn : 100 ≤ n
⊢ 1 * 1 ≤ n + 1

State before:
n : ℕ
hn : 100 ≤ n
⊢ 1 * 1 ≤ n + 1
Tactic:
omega
State after:
no goals

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

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

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

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

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

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