internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2014A4.final_solution_case2
Proof state before:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
⊢ f = fun x => (b - 1) * x + (b - 1) * k / (b - 1)
Tactic:
have h1 := c_eq_b_sub_one_mul_map_zero h2 h h0
Proof state after:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
h1 : (b - 1) * k = (b - 1) * f 0
⊢ f = fun x => (b - 1) * x + (b - 1) * k / (b - 1)
Theorem: IMOSL.IMO2014A4.final_solution_case2
Proof state before:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
h1 : (b - 1) * k = (b - 1) * f 0
⊢ f = fun x => (b - 1) * x + (b - 1) * k / (b - 1)
Tactic:
have h3 := (mul_ne_zero_iff.mp h0).1
Proof state after:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
h1 : (b - 1) * k = (b - 1) * f 0
h3 : b - 1 ≠ 0
⊢ f = fun x => (b - 1) * x + (b - 1) * k / (b - 1)
Theorem: IMOSL.IMO2014A4.final_solution_case2
Proof state before:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
h1 : (b - 1) * k = (b - 1) * f 0
h3 : b - 1 ≠ 0
⊢ f = fun x => (b - 1) * x + (b - 1) * k / (b - 1)
Tactic:
rw [Int.mul_ediv_cancel_left _ h3]
Proof state after:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
h1 : (b - 1) * k = (b - 1) * f 0
h3 : b - 1 ≠ 0
⊢ f = fun x => (b - 1) * x + k
Theorem: IMOSL.IMO2014A4.final_solution_case2
Proof state before:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
h1 : (b - 1) * k = (b - 1) * f 0
h3 : b - 1 ≠ 0
⊢ f = fun x => (b - 1) * x + k
Tactic:
rw [mul_eq_mul_left_iff, or_iff_left h3] at h1
Proof state after:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
h1 : k = f 0
h3 : b - 1 ≠ 0
⊢ f = fun x => (b - 1) * x + k
Theorem: IMOSL.IMO2014A4.final_solution_case2
Proof state before:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
h1 : k = f 0
h3 : b - 1 ≠ 0
⊢ f = fun x => (b - 1) * x + k
Tactic:
rw [h1]
Proof state after:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
h1 : k = f 0
h3 : b - 1 ≠ 0
⊢ f = fun x => (b - 1) * x + f 0
Theorem: IMOSL.IMO2014A4.final_solution_case2
Proof state before:
case intro
b : ℤ
h : 1 < b.natAbs
f : ℤ → ℤ
k : ℤ
h0 : (b - 1) * k ≠ 0
h2 : good b ((b - 1) * k) f
h1 : k = f 0
h3 : b - 1 ≠ 0
⊢ f = fun x => (b - 1) * x + f 0
Tactic:
exact funext (map_is_linear h2 h h0)
Proof state after:
no goals
Theorem: IMOSL.IMO2021N2.good_cond1
Proof state before:
n a b c k l m : ℕ
h : n ≤ a
h0 : a < b
h1 : b < c
h2 : c ≤ 2 * n
h3 : a + b = k ^ 2
h4 : a + c = l ^ 2
h5 : b + c = m ^ 2
x : ℕ → Bool
⊢ ∃ a b, n ≤ a ∧ a < b ∧ b ≤ 2 * n ∧ x a = x b ∧ ∃ k, a + b = k ^ 2
Tactic:
rcases (x a).eq_or_eq_not (x b) with h6 | h6
Proof state after:
case inl
n a b c k l m : ℕ
h : n ≤ a
h0 : a < b
h1 : b < c
h2 : c ≤ 2 * n
h3 : a + b = k ^ 2
h4 : a + c = l ^ 2
h5 : b + c = m ^ 2
x : ℕ → Bool
h6 : x a = x b
⊢ ∃ a b, n ≤ a ∧ a < b ∧ b ≤ 2 * n ∧ x a = x b ∧ ∃ k, a + b = k ^ 2

case inr
n a b c k l m : ℕ
h : n ≤ a
h0 : a < b
h1 : b < c
h2 : c ≤ 2 * n
h3 : a + b = k ^ 2
h4 : a + c = l ^ 2
h5 : b + c = m ^ 2
x : ℕ → Bool
h6 : x a = !x b
⊢ ∃ a b, n ≤ a ∧ a < b ∧ b ≤ 2 * n ∧ x a = x b ∧ ∃ k, a + b = k ^ 2
Theorem: IMOSL.IMO2021N2.good_cond1
Proof state before:
case inr
n a b c k l m : ℕ
h : n ≤ a
h0 : a < b
h1 : b < c
h2 : c ≤ 2 * n
h3 : a + b = k ^ 2
h4 : a + c = l ^ 2
h5 : b + c = m ^ 2
x : ℕ → Bool
h6 : x a = !x b
⊢ ∃ a b, n ≤ a ∧ a < b ∧ b ≤ 2 * n ∧ x a = x b ∧ ∃ k, a + b = k ^ 2
Tactic:
rcases (x c).eq_or_eq_not (x b) with h7 | h7
Proof state after:
case inr.inl
n a b c k l m : ℕ
h : n ≤ a
h0 : a < b
h1 : b < c
h2 : c ≤ 2 * n
h3 : a + b = k ^ 2
h4 : a + c = l ^ 2
h5 : b + c = m ^ 2
x : ℕ → Bool
h6 : x a = !x b
h7 : x c = x b
⊢ ∃ a b, n ≤ a ∧ a < b ∧ b ≤ 2 * n ∧ x a = x b ∧ ∃ k, a + b = k ^ 2

case inr.inr
n a b c k l m : ℕ
h : n ≤ a
h0 : a < b
h1 : b < c
h2 : c ≤ 2 * n
h3 : a + b = k ^ 2
h4 : a + c = l ^ 2
h5 : b + c = m ^ 2
x : ℕ → Bool
h6 : x a = !x b
h7 : x c = !x b
⊢ ∃ a b, n ≤ a ∧ a < b ∧ b ≤ 2 * n ∧ x a = x b ∧ ∃ k, a + b = k ^ 2
Theorem: IMOSL.IMO2021N2.good_cond1
Proof state before:
case inl
n a b c k l m : ℕ
h : n ≤ a
h0 : a < b
h1 : b < c
h2 : c ≤ 2 * n
h3 : a + b = k ^ 2
h4 : a + c = l ^ 2
h5 : b + c = m ^ 2
x : ℕ → Bool
h6 : x a = x b
⊢ ∃ a b, n ≤ a ∧ a < b ∧ b ≤ 2 * n ∧ x a = x b ∧ ∃ k, a + b = k ^ 2
Tactic:
exact ⟨a, b, h, h0, h1.le.trans h2, h6, k, h3⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2021N2.good_cond1
Proof state before:
case inr.inl
n a b c k l m : ℕ
h : n ≤ a
h0 : a < b
h1 : b < c
h2 : c ≤ 2 * n
h3 : a + b = k ^ 2
h4 : a + c = l ^ 2
h5 : b + c = m ^ 2
x : ℕ → Bool
h6 : x a = !x b
h7 : x c = x b
⊢ ∃ a b, n ≤ a ∧ a < b ∧ b ≤ 2 * n ∧ x a = x b ∧ ∃ k, a + b = k ^ 2
Tactic:
exact ⟨b, c, h.trans h0.le, h1, h2, h7.symm, m, h5⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2021N2.good_cond1
Proof state before:
case inr.inr
n a b c k l m : ℕ
h : n ≤ a
h0 : a < b
h1 : b < c
h2 : c ≤ 2 * n
h3 : a + b = k ^ 2
h4 : a + c = l ^ 2
h5 : b + c = m ^ 2
x : ℕ → Bool
h6 : x a = !x b
h7 : x c = !x b
⊢ ∃ a b, n ≤ a ∧ a < b ∧ b ≤ 2 * n ∧ x a = x b ∧ ∃ k, a + b = k ^ 2
Tactic:
exact ⟨a, c, h, h0.trans h1, h2, h6.trans h7.symm, l, h4⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2021N2.good_cond2
Proof 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) ?_ ?_ ?_
Proof 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
Theorem: IMOSL.IMO2021N2.good_cond2
Proof 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]
Proof 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
Theorem: IMOSL.IMO2021N2.good_cond2
Proof 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 _ _)
Proof state after:
case refine_1
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ 4 ≤ 8
Theorem: IMOSL.IMO2021N2.good_cond2
Proof 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)
Proof state after:
no goals
Theorem: IMOSL.IMO2021N2.good_cond2
Proof 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]
Proof 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
Theorem: IMOSL.IMO2021N2.good_cond2
Proof 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 _ _)
Proof state after:
case refine_2
n k : ℕ
h : n ≤ 2 * k ^ 2 + 4 * k
h0 : k ^ 2 + 6 * k + 8 ≤ n
⊢ 8 ≤ 2 * 6
Theorem: IMOSL.IMO2021N2.good_cond2
Proof 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)
Proof state after:
no goals
Theorem: IMOSL.IMO2021N2.good_cond2
Proof 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]
Proof 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
Theorem: IMOSL.IMO2021N2.good_cond2
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2021N2.good_cond2
Proof 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]
Proof 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
Theorem: IMOSL.IMO2021N2.good_cond2
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2021N2.good_cond2
Proof 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]
Proof 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
Theorem: IMOSL.IMO2021N2.good_cond2
Proof 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
Proof state after:
no goals
Theorem: IMOSL.IMO2021N2.good_cond2_k_witness
Proof 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⟩
Proof 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
Theorem: IMOSL.IMO2021N2.good_cond2_k_witness
Proof 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
Proof 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
Theorem: IMOSL.IMO2021N2.good_cond2_k_witness
Proof 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
Proof 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
Theorem: IMOSL.IMO2021N2.good_cond2_k_witness
Proof 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, ?_, ?_⟩
Proof 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
Theorem: IMOSL.IMO2021N2.good_cond2_k_witness
Proof 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⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2021N2.good_cond2_k_witness
Proof 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]
Proof 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
Theorem: IMOSL.IMO2021N2.good_cond2_k_witness
Proof 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)
Proof state after:
no goals
Theorem: IMOSL.IMO2021N2.good_cond2_k_witness
Proof 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
Proof 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
Theorem: IMOSL.IMO2021N2.good_cond2_k_witness
Proof 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
Proof 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
Theorem: IMOSL.IMO2021N2.good_cond2_k_witness
Proof 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
Proof 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
Theorem: IMOSL.IMO2021N2.good_cond2_k_witness
Proof 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]
Proof 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)
Theorem: IMOSL.IMO2021N2.good_cond2_k_witness
Proof 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'
Proof 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)
Theorem: IMOSL.IMO2021N2.good_cond2_k_witness
Proof 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]
Proof 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)
Theorem: IMOSL.IMO2021N2.good_cond2_k_witness
Proof 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)
Proof state after:
no goals
Theorem: IMOSL.IMO2021N2.good_cond2_k_witness
Proof 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]
Proof 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
Theorem: IMOSL.IMO2021N2.good_cond2_k_witness
Proof 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
Proof state after:
no goals
Theorem: IMOSL.Extra.SquareLike.map_zero
Proof state before:
G : Type u_2
H : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : AddCancelCommMonoid H
hH : ∀ (x y : H), 2 • x = 2 • y → x = y
f : G → H
h : ∀ (x y : G), f (x + y) + f (x - y) = 2 • (f x + f y)
⊢ f 0 = 0
Tactic:
specialize h 0 0
Proof state after:
G : Type u_2
H : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : AddCancelCommMonoid H
hH : ∀ (x y : H), 2 • x = 2 • y → x = y
f : G → H
h : f (0 + 0) + f (0 - 0) = 2 • (f 0 + f 0)
⊢ f 0 = 0
Theorem: IMOSL.Extra.SquareLike.map_zero
Proof state before:
G : Type u_2
H : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : AddCancelCommMonoid H
hH : ∀ (x y : H), 2 • x = 2 • y → x = y
f : G → H
h : f (0 + 0) + f (0 - 0) = 2 • (f 0 + f 0)
⊢ f 0 = 0
Tactic:
rw [add_zero, sub_zero, two_nsmul, self_eq_add_right, ← two_nsmul] at h
Proof state after:
G : Type u_2
H : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : AddCancelCommMonoid H
hH : ∀ (x y : H), 2 • x = 2 • y → x = y
f : G → H
h : 2 • f 0 = 0
⊢ f 0 = 0
Theorem: IMOSL.Extra.SquareLike.map_zero
Proof state before:
G : Type u_2
H : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : AddCancelCommMonoid H
hH : ∀ (x y : H), 2 • x = 2 • y → x = y
f : G → H
h : 2 • f 0 = 0
⊢ f 0 = 0
Tactic:
exact hH _ _ (h.trans (nsmul_zero 2).symm)
Proof state after:
no goals
Theorem: IMOSL.Extra.SquareLike.map_even
Proof state before:
G : Type u_2
H : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : AddCancelCommMonoid H
hH : ∀ (x y : H), 2 • x = 2 • y → x = y
f : G → H
h : ∀ (x y : G), f (x + y) + f (x - y) = 2 • (f x + f y)
x : G
⊢ f (-x) = f x
Tactic:
have h0 := h 0 x
Proof state after:
G : Type u_2
H : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : AddCancelCommMonoid H
hH : ∀ (x y : H), 2 • x = 2 • y → x = y
f : G → H
h : ∀ (x y : G), f (x + y) + f (x - y) = 2 • (f x + f y)
x : G
h0 : f (0 + x) + f (0 - x) = 2 • (f 0 + f x)
⊢ f (-x) = f x
Theorem: IMOSL.Extra.SquareLike.map_even
Proof state before:
G : Type u_2
H : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : AddCancelCommMonoid H
hH : ∀ (x y : H), 2 • x = 2 • y → x = y
f : G → H
h : ∀ (x y : G), f (x + y) + f (x - y) = 2 • (f x + f y)
x : G
h0 : f (0 + x) + f (0 - x) = 2 • (f 0 + f x)
⊢ f (-x) = f x
Tactic:
rwa [zero_add, zero_sub, map_zero hH h, zero_add, two_nsmul, add_right_inj] at h0
Proof state after:
no goals
Theorem: IMOSL.Extra.SquareLike.map_triple
Proof state before:
G : Type u_2
H : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : AddCancelCommMonoid H
hH : ∀ (x y : H), 2 • x = 2 • y → x = y
f : G → H
h : ∀ (x y : G), f (x + y) + f (x - y) = 2 • (f x + f y)
x y z : G
⊢ 2 • (f (x + y + z) + f x + (f y + f z)) = 2 • (f (x + y) + f (x + z) + f (y + z))
Tactic:
rw [nsmul_add, ← h, ← h, add_add_add_comm, add_assoc x, add_sub_cancel_left,
add_comm (f (y + z)), add_add_add_comm, ← two_nsmul, nsmul_add, add_left_inj, ← h,
add_sub_add_left_eq_sub, add_left_inj, add_right_comm, add_add_add_comm]
Proof state after:
no goals
Theorem: IMOSL.Extra.SquareLike.BilinMap_eq_two_nsmul
Proof state before:
G : Type u_2
H : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : AddCommGroup H
hH : ∀ (x y : H), 2 • x = 2 • y → x = y
f : G → H
h : ∀ (x y : G), f (x + y) + f (x - y) = 2 • (f x + f y)
x : G
⊢ ((BilinMap hH h) x) x = 2 • f x
Tactic:
rw [two_nsmul, ← neg_inj, ← map_neg, BilinMap_def,
  add_neg_self, map_zero hH h, map_even hH h, zero_sub]
Proof state after:
no goals
Theorem: IMOSL.Extra.SquareLike.two_nsmul_BilinMap_eq
Proof state before:
G : Type u_2
H : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : AddCommGroup H
hH : ∀ (x y : H), 2 • x = 2 • y → x = y
f : G → H
h : ∀ (x y : G), f (x + y) + f (x - y) = 2 • (f x + f y)
x y : G
⊢ 2 • ((BilinMap hH h) x) y = f (x + y) - f (x - y)
Tactic:
rw [BilinMap_def, nsmul_sub, ← h, two_nsmul, add_sub_add_left_eq_sub]
Proof state after:
no goals
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
⊢ ∀ (x : R), x ≤ 0 → f x = 0
Tactic:
have h0 : ∀ t x : R, f (f t) - f (f x) ≤ (f t - x) * f x := λ t x ↦ by
  rw [sub_le_iff_le_add]
  apply (h _ _).trans_eq'
  rw [add_sub_cancel]
Proof state after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (t x : R), f (f t) - f (f x) ≤ (f t - x) * f x
⊢ ∀ (x : R), x ≤ 0 → f x = 0
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (t x : R), f (f t) - f (f x) ≤ (f t - x) * f x
⊢ ∀ (x : R), x ≤ 0 → f x = 0
Tactic:
replace h0 : ∀ t x : R, 0 ≤ (f t - x) * f x + (f x - t) * f t := λ t x ↦ by
  rw [← sub_self (f (f t)), ← sub_add_sub_cancel _ (f (f x))]
  exact add_le_add (h0 t x) (h0 x t)
Proof state after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (t x : R), 0 ≤ (f t - x) * f x + (f x - t) * f t
⊢ ∀ (x : R), x ≤ 0 → f x = 0
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (t x : R), 0 ≤ (f t - x) * f x + (f x - t) * f t
⊢ ∀ (x : R), x ≤ 0 → f x = 0
Tactic:
replace h0 : ∀ x : R, x * f x ≤ 0 := λ x ↦ by
  have h1 := h0 x (f x + f x)
  rwa [sub_add_cancel_left, sub_mul, neg_mul, mul_comm,
    ← add_sub_assoc, neg_add_self, zero_sub, neg_nonneg] at h1
Proof state after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (x : R), x * f x ≤ 0
⊢ ∀ (x : R), x ≤ 0 → f x = 0
Theorem: IMOSL.IMO2011A6.final_solution
Proof state before:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (x : R), x * f x ≤ 0
⊢ ∀ (x : R), x ≤ 0 → f x = 0
Tactic:
have h1 : ∀ x : R, f x ≤ f (f x) := λ x ↦ by
  have h1 := h x 0
  rwa [add_zero, zero_mul, zero_add] at h1
Proof state after:
R : Type u_1
inst✝ : LinearOrderedCommRing R
f : R → R
h : ∀ (x y : R), f (x + y) ≤ y * f x + f (f x)
h0 : ∀ (x : R), x * f x ≤ 0
h1 : ∀ (x : R), f x ≤ f (f x)
⊢ ∀ (x : R), x ≤ 0 → f x = 0