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

State before:
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ good n
Tactic:
refine good_cond1 (b := 2 * k ^ 2 + 8 * k + 9) (k := 2 * k + 3)
  (l := 2 * k + 4) (m := 2 * k + 5) h ?_ ?_
  (Nat.mul_le_mul_left 2 h0) ?_ ?_ ?_
State after:
case refine_1
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ 2 * k ^ 2 + 4 * k < 2 * k ^ 2 + 8 * k + 9

case refine_2
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ 2 * k ^ 2 + 8 * k + 9 < 2 * (k ^ 2 + 6 * k + 8)

case refine_3
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ 2 * k ^ 2 + 4 * k + (2 * k ^ 2 + 8 * k + 9) = (2 * k + 3) ^ 2

case refine_4
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ 2 * k ^ 2 + 4 * k + 2 * (k ^ 2 + 6 * k + 8) = (2 * k + 4) ^ 2

case refine_5
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ 2 * k ^ 2 + 8 * k + 9 + 2 * (k ^ 2 + 6 * k + 8) = (2 * k + 5) ^ 2

State before:
case refine_1
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ 2 * k ^ 2 + 4 * k < 2 * k ^ 2 + 8 * k + 9
Tactic:
rw [Nat.add_assoc, Nat.add_lt_add_iff_left, Nat.lt_succ_iff]
State after:
case refine_1
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ 4 * k ≤ 8 * k + 8

State before:
case refine_1
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ 4 * k ≤ 8 * k + 8
Tactic:
refine (Nat.mul_le_mul_right k ?_).trans (Nat.le_add_right _ _)
State after:
case refine_1
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ 4 ≤ 8

State before:
case refine_1
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ 4 ≤ 8
Tactic:
exact Nat.le_mul_of_pos_left 4 (Nat.succ_pos 1)
State after:
no goals

State before:
case refine_2
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ 2 * k ^ 2 + 8 * k + 9 < 2 * (k ^ 2 + 6 * k + 8)
Tactic:
rw [Nat.mul_add, Nat.mul_add, ← Nat.mul_assoc,
  Nat.lt_succ_iff, Nat.add_assoc, Nat.add_assoc,
  Nat.add_le_add_iff_left, Nat.add_le_add_iff_right]
State after:
case refine_2
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ 8 * k ≤ 2 * 6 * k + 6

State before:
case refine_2
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ 8 * k ≤ 2 * 6 * k + 6
Tactic:
refine (Nat.mul_le_mul_right k ?_).trans (Nat.le_add_right _ _)
State after:
case refine_2
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ 8 ≤ 2 * 6

State before:
case refine_2
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ 8 ≤ 2 * 6
Tactic:
exact Nat.mul_le_mul_left 4 (Nat.le_succ 2)
State after:
no goals

State before:
case refine_3
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ 2 * k ^ 2 + 4 * k + (2 * k ^ 2 + 8 * k + 9) = (2 * k + 3) ^ 2
Tactic:
rw [← Nat.add_assoc, Nat.add_add_add_comm, ← Nat.add_mul, ← Nat.add_mul,
  add_sq, Nat.mul_pow, Nat.mul_right_comm, ← Nat.mul_assoc]
State after:
case refine_3
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ (2 + 2) * k ^ 2 + (4 + 8) * k + 9 = 2 ^ 2 * k ^ 2 + 2 * 3 * 2 * k + 3 ^ 2

State before:
case refine_3
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ (2 + 2) * k ^ 2 + (4 + 8) * k + 9 = 2 ^ 2 * k ^ 2 + 2 * 3 * 2 * k + 3 ^ 2
Tactic:
rfl
State after:
no goals

State before:
case refine_4
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ 2 * k ^ 2 + 4 * k + 2 * (k ^ 2 + 6 * k + 8) = (2 * k + 4) ^ 2
Tactic:
rw [Nat.mul_add, ← Nat.add_assoc, Nat.mul_add, Nat.add_add_add_comm,
  ← Nat.add_mul, ← Nat.mul_assoc, ← Nat.add_mul, add_sq, Nat.mul_pow,
  Nat.mul_right_comm, ← Nat.mul_assoc]
State after:
case refine_4
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ (2 + 2) * k ^ 2 + (4 + 2 * 6) * k + 2 * 8 = 2 ^ 2 * k ^ 2 + 2 * 4 * 2 * k + 4 ^ 2

State before:
case refine_4
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ (2 + 2) * k ^ 2 + (4 + 2 * 6) * k + 2 * 8 = 2 ^ 2 * k ^ 2 + 2 * 4 * 2 * k + 4 ^ 2
Tactic:
rfl
State after:
no goals

State before:
case refine_5
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ 2 * k ^ 2 + 8 * k + 9 + 2 * (k ^ 2 + 6 * k + 8) = (2 * k + 5) ^ 2
Tactic:
rw [Nat.mul_add, Nat.add_add_add_comm, Nat.mul_add, ← Nat.mul_assoc,
  Nat.add_add_add_comm (2 * k ^ 2), ← Nat.add_mul, ← Nat.add_mul,
  add_sq, Nat.mul_pow, Nat.mul_right_comm, ← Nat.mul_assoc]
State after:
case refine_5
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ (2 + 2) * k ^ 2 + (8 + 2 * 6) * k + (9 + 2 * 8) = 2 ^ 2 * k ^ 2 + 2 * 5 * 2 * k + 5 ^ 2

State before:
case refine_5
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ (2 + 2) * k ^ 2 + (8 + 2 * 6) * k + (9 + 2 * 8) = 2 ^ 2 * k ^ 2 + 2 * 5 * 2 * k + 5 ^ 2
Tactic:
rfl
State after:
no goals