Theorem: IMOSL.IMO2021N2.good_cond2_k_witness (IMOSLLean4/IMO2021/N2/N2.lean)

State before:
n : ℕ
h : 99 ≤ n
h0 : ∃ k, n ≤ 2 * k ^ 2 + 4 * k ∧ k ^ 2 + 6 * k + 8 ≤ n
⊢ ∃ k, n + 1 ≤ 2 * k ^ 2 + 4 * k ∧ k ^ 2 + 6 * k + 8 ≤ n + 1
Tactic:
rcases h0 with ⟨k, h0, h1⟩
State after:
case intro.intro
n : ℕ
h : 99 ≤ n
k : ℕ
h0 : n ≤ 2 * k ^ 2 + 4 * k
h1 : k ^ 2 + 6 * k + 8 ≤ n
⊢ ∃ k, n + 1 ≤ 2 * k ^ 2 + 4 * k ∧ k ^ 2 + 6 * k + 8 ≤ n + 1

State before:
case intro.intro
n : ℕ
h : 99 ≤ n
k : ℕ
h0 : n ≤ 2 * k ^ 2 + 4 * k
h1 : k ^ 2 + 6 * k + 8 ≤ n
⊢ ∃ k, n + 1 ≤ 2 * k ^ 2 + 4 * k ∧ k ^ 2 + 6 * k + 8 ≤ n + 1
Tactic:
rw [le_iff_lt_or_eq] at h0
State after:
case intro.intro
n : ℕ
h : 99 ≤ n
k : ℕ
h0 : n < 2 * k ^ 2 + 4 * k ∨ n = 2 * k ^ 2 + 4 * k
h1 : k ^ 2 + 6 * k + 8 ≤ n
⊢ ∃ k, n + 1 ≤ 2 * k ^ 2 + 4 * k ∧ k ^ 2 + 6 * k + 8 ≤ n + 1

State before:
case intro.intro
n : ℕ
h : 99 ≤ n
k : ℕ
h0 : n < 2 * k ^ 2 + 4 * k ∨ n = 2 * k ^ 2 + 4 * k
h1 : k ^ 2 + 6 * k + 8 ≤ n
⊢ ∃ k, n + 1 ≤ 2 * k ^ 2 + 4 * k ∧ k ^ 2 + 6 * k + 8 ≤ n + 1
Tactic:
rcases h0 with h0 | rfl
State after:
case intro.intro.inl
n : ℕ
h : 99 ≤ n
k : ℕ
h1 : k ^ 2 + 6 * k + 8 ≤ n
h0 : n < 2 * k ^ 2 + 4 * k
⊢ ∃ k, n + 1 ≤ 2 * k ^ 2 + 4 * k ∧ k ^ 2 + 6 * k + 8 ≤ n + 1

case intro.intro.inr
k : ℕ
h : 99 ≤ 2 * k ^ 2 + 4 * k
h1 : k ^ 2 + 6 * k + 8 ≤ 2 * k ^ 2 + 4 * k
⊢ ∃ k_1, 2 * k ^ 2 + 4 * k + 1 ≤ 2 * k_1 ^ 2 + 4 * k_1 ∧ k_1 ^ 2 + 6 * k_1 + 8 ≤ 2 * k ^ 2 + 4 * k + 1

State before:
case intro.intro.inr
k : ℕ
h : 99 ≤ 2 * k ^ 2 + 4 * k
h1 : k ^ 2 + 6 * k + 8 ≤ 2 * k ^ 2 + 4 * k
⊢ ∃ k_1, 2 * k ^ 2 + 4 * k + 1 ≤ 2 * k_1 ^ 2 + 4 * k_1 ∧ k_1 ^ 2 + 6 * k_1 + 8 ≤ 2 * k ^ 2 + 4 * k + 1
Tactic:
refine ⟨k + 1, ?_, ?_⟩
State after:
case intro.intro.inr.refine_1
k : ℕ
h : 99 ≤ 2 * k ^ 2 + 4 * k
h1 : k ^ 2 + 6 * k + 8 ≤ 2 * k ^ 2 + 4 * k
⊢ 2 * k ^ 2 + 4 * k + 1 ≤ 2 * (k + 1) ^ 2 + 4 * (k + 1)

case intro.intro.inr.refine_2
k : ℕ
h : 99 ≤ 2 * k ^ 2 + 4 * k
h1 : k ^ 2 + 6 * k + 8 ≤ 2 * k ^ 2 + 4 * k
⊢ (k + 1) ^ 2 + 6 * (k + 1) + 8 ≤ 2 * k ^ 2 + 4 * k + 1

State before:
case intro.intro.inl
n : ℕ
h : 99 ≤ n
k : ℕ
h1 : k ^ 2 + 6 * k + 8 ≤ n
h0 : n < 2 * k ^ 2 + 4 * k
⊢ ∃ k, n + 1 ≤ 2 * k ^ 2 + 4 * k ∧ k ^ 2 + 6 * k + 8 ≤ n + 1
Tactic:
exact ⟨k, h0, Nat.le_succ_of_le h1⟩
State after:
no goals

State before:
case intro.intro.inr.refine_1
k : ℕ
h : 99 ≤ 2 * k ^ 2 + 4 * k
h1 : k ^ 2 + 6 * k + 8 ≤ 2 * k ^ 2 + 4 * k
⊢ 2 * k ^ 2 + 4 * k + 1 ≤ 2 * (k + 1) ^ 2 + 4 * (k + 1)
Tactic:
rw [Nat.mul_succ, ← Nat.add_assoc]
State after:
case intro.intro.inr.refine_1
k : ℕ
h : 99 ≤ 2 * k ^ 2 + 4 * k
h1 : k ^ 2 + 6 * k + 8 ≤ 2 * k ^ 2 + 4 * k
⊢ 2 * k ^ 2 + 4 * k + 1 ≤ 2 * (k + 1) ^ 2 + 4 * k + 4

State before:
case intro.intro.inr.refine_1
k : ℕ
h : 99 ≤ 2 * k ^ 2 + 4 * k
h1 : k ^ 2 + 6 * k + 8 ≤ 2 * k ^ 2 + 4 * k
⊢ 2 * k ^ 2 + 4 * k + 1 ≤ 2 * (k + 1) ^ 2 + 4 * k + 4
Tactic:
exact Nat.add_le_add (Nat.add_le_add_right (Nat.mul_le_mul_left 2 <|
  Nat.pow_le_pow_of_le_left k.le_succ 2) _) (Nat.le_add_left 1 3)
State after:
no goals

State before:
case intro.intro.inr.refine_2
k : ℕ
h : 99 ≤ 2 * k ^ 2 + 4 * k
h1 : k ^ 2 + 6 * k + 8 ≤ 2 * k ^ 2 + 4 * k
⊢ (k + 1) ^ 2 + 6 * (k + 1) + 8 ≤ 2 * k ^ 2 + 4 * k + 1
Tactic:
replace h1 : 2 * k ^ 2 + 4 * k + 2 = 2 * (k + 1) ^ 2 := by
  rw [add_sq, Nat.mul_add, Nat.mul_add, Nat.mul_one, ← Nat.mul_assoc]; rfl
State after:
case intro.intro.inr.refine_2
k : ℕ
h : 99 ≤ 2 * k ^ 2 + 4 * k
h1 : 2 * k ^ 2 + 4 * k + 2 = 2 * (k + 1) ^ 2
⊢ (k + 1) ^ 2 + 6 * (k + 1) + 8 ≤ 2 * k ^ 2 + 4 * k + 1

State before:
case intro.intro.inr.refine_2
k : ℕ
h : 99 ≤ 2 * k ^ 2 + 4 * k
h1 : 2 * k ^ 2 + 4 * k + 2 = 2 * (k + 1) ^ 2
⊢ (k + 1) ^ 2 + 6 * (k + 1) + 8 ≤ 2 * k ^ 2 + 4 * k + 1
Tactic:
rw [← Nat.add_le_add_iff_right (n := 2), h1, Nat.succ_le_iff, Nat.mul_comm,
  ← Nat.div_lt_iff_lt_mul (Nat.succ_pos 1), ← Nat.sqrt_lt'] at h
State after:
case intro.intro.inr.refine_2
k : ℕ
h : ((99 + 1) / Nat.succ 1).sqrt < k + 1
h1 : 2 * k ^ 2 + 4 * k + 2 = 2 * (k + 1) ^ 2
⊢ (k + 1) ^ 2 + 6 * (k + 1) + 8 ≤ 2 * k ^ 2 + 4 * k + 1

State before:
case intro.intro.inr.refine_2
k : ℕ
h : ((99 + 1) / Nat.succ 1).sqrt < k + 1
h1 : 2 * k ^ 2 + 4 * k + 2 = 2 * (k + 1) ^ 2
⊢ (k + 1) ^ 2 + 6 * (k + 1) + 8 ≤ 2 * k ^ 2 + 4 * k + 1
Tactic:
change 8 ≤ k + 1 at h
State after:
case intro.intro.inr.refine_2
k : ℕ
h1 : 2 * k ^ 2 + 4 * k + 2 = 2 * (k + 1) ^ 2
h : 8 ≤ k + 1
⊢ (k + 1) ^ 2 + 6 * (k + 1) + 8 ≤ 2 * k ^ 2 + 4 * k + 1

State before:
case intro.intro.inr.refine_2
k : ℕ
h1 : 2 * k ^ 2 + 4 * k + 2 = 2 * (k + 1) ^ 2
h : 8 ≤ k + 1
⊢ (k + 1) ^ 2 + 6 * (k + 1) + 8 ≤ 2 * k ^ 2 + 4 * k + 1
Tactic:
rw [← Nat.add_le_add_iff_right (n := 1), h1, Nat.two_mul,
  Nat.add_assoc, Nat.add_assoc, Nat.add_le_add_iff_left, sq]
State after:
case intro.intro.inr.refine_2
k : ℕ
h1 : 2 * k ^ 2 + 4 * k + 2 = 2 * (k + 1) ^ 2
h : 8 ≤ k + 1
⊢ 6 * (k + 1) + (8 + 1) ≤ (k + 1) * (k + 1)

State before:
case intro.intro.inr.refine_2
k : ℕ
h1 : 2 * k ^ 2 + 4 * k + 2 = 2 * (k + 1) ^ 2
h : 8 ≤ k + 1
⊢ 6 * (k + 1) + (8 + 1) ≤ (k + 1) * (k + 1)
Tactic:
apply (Nat.mul_le_mul_right _ h).trans'
State after:
case intro.intro.inr.refine_2
k : ℕ
h1 : 2 * k ^ 2 + 4 * k + 2 = 2 * (k + 1) ^ 2
h : 8 ≤ k + 1
⊢ 6 * (k + 1) + (8 + 1) ≤ 8 * (k + 1)

State before:
case intro.intro.inr.refine_2
k : ℕ
h1 : 2 * k ^ 2 + 4 * k + 2 = 2 * (k + 1) ^ 2
h : 8 ≤ k + 1
⊢ 6 * (k + 1) + (8 + 1) ≤ 8 * (k + 1)
Tactic:
rw [Nat.add_mul 6 2, Nat.add_le_add_iff_left, Nat.two_mul]
State after:
case intro.intro.inr.refine_2
k : ℕ
h1 : 2 * k ^ 2 + 4 * k + 2 = 2 * (k + 1) ^ 2
h : 8 ≤ k + 1
⊢ 8 + 1 ≤ k + 1 + (k + 1)

State before:
case intro.intro.inr.refine_2
k : ℕ
h1 : 2 * k ^ 2 + 4 * k + 2 = 2 * (k + 1) ^ 2
h : 8 ≤ k + 1
⊢ 8 + 1 ≤ k + 1 + (k + 1)
Tactic:
exact Nat.add_le_add h (Nat.le_add_left 1 k)
State after:
no goals

State before:
k : ℕ
h : 99 ≤ 2 * k ^ 2 + 4 * k
h1 : k ^ 2 + 6 * k + 8 ≤ 2 * k ^ 2 + 4 * k
⊢ 2 * k ^ 2 + 4 * k + 2 = 2 * (k + 1) ^ 2
Tactic:
rw [add_sq, Nat.mul_add, Nat.mul_add, Nat.mul_one, ← Nat.mul_assoc]
State after:
k : ℕ
h : 99 ≤ 2 * k ^ 2 + 4 * k
h1 : k ^ 2 + 6 * k + 8 ≤ 2 * k ^ 2 + 4 * k
⊢ 2 * k ^ 2 + 4 * k + 2 = 2 * k ^ 2 + 2 * 2 * k + 2 * 1 ^ 2

State before:
k : ℕ
h : 99 ≤ 2 * k ^ 2 + 4 * k
h1 : k ^ 2 + 6 * k + 8 ≤ 2 * k ^ 2 + 4 * k
⊢ 2 * k ^ 2 + 4 * k + 2 = 2 * k ^ 2 + 2 * 2 * k + 2 * 1 ^ 2
Tactic:
rfl
State after:
no goals