internlm/Lean-Github huggingface dataset:
Theorem: Imo2006P3.lhs_ineq
Proof state before:
x y : ℝ
hxy : 0 ≤ x * y
⊢ 16 * x ^ 2 * y ^ 2 * (x + y) ^ 2 ≤ ((x + y) ^ 2) ^ 3
Tactic:
have : (x - y) ^ 2 * ((x + y) ^ 2 + 4 * (x * y)) ≥ 0 := by positivity
Proof state after:
x y : ℝ
hxy : 0 ≤ x * y
this : (x - y) ^ 2 * ((x + y) ^ 2 + 4 * (x * y)) ≥ 0
⊢ 16 * x ^ 2 * y ^ 2 * (x + y) ^ 2 ≤ ((x + y) ^ 2) ^ 3
Theorem: Imo2006P3.lhs_ineq
Proof state before:
x y : ℝ
hxy : 0 ≤ x * y
this : (x - y) ^ 2 * ((x + y) ^ 2 + 4 * (x * y)) ≥ 0
⊢ 16 * x ^ 2 * y ^ 2 * (x + y) ^ 2 ≤ ((x + y) ^ 2) ^ 3
Tactic:
calc 16 * x ^ 2 * y ^ 2 * (x + y) ^ 2 ≤ ((x + y) ^ 2) ^ 2 * (x + y) ^ 2 := by gcongr; linarith
  _ = ((x + y) ^ 2) ^ 3 := by ring
Proof state after:
no goals
Theorem: Imo2006P3.lhs_ineq
Proof state before:
x y : ℝ
hxy : 0 ≤ x * y
⊢ (x - y) ^ 2 * ((x + y) ^ 2 + 4 * (x * y)) ≥ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: Imo2006P3.lhs_ineq
Proof state before:
x y : ℝ
hxy : 0 ≤ x * y
this : (x - y) ^ 2 * ((x + y) ^ 2 + 4 * (x * y)) ≥ 0
⊢ 16 * x ^ 2 * y ^ 2 * (x + y) ^ 2 ≤ ((x + y) ^ 2) ^ 2 * (x + y) ^ 2
Tactic:
gcongr
Proof state after:
case h
x y : ℝ
hxy : 0 ≤ x * y
this : (x - y) ^ 2 * ((x + y) ^ 2 + 4 * (x * y)) ≥ 0
⊢ 16 * x ^ 2 * y ^ 2 ≤ ((x + y) ^ 2) ^ 2
Theorem: Imo2006P3.lhs_ineq
Proof state before:
case h
x y : ℝ
hxy : 0 ≤ x * y
this : (x - y) ^ 2 * ((x + y) ^ 2 + 4 * (x * y)) ≥ 0
⊢ 16 * x ^ 2 * y ^ 2 ≤ ((x + y) ^ 2) ^ 2
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo2006P3.lhs_ineq
Proof state before:
x y : ℝ
hxy : 0 ≤ x * y
this : (x - y) ^ 2 * ((x + y) ^ 2 + 4 * (x * y)) ≥ 0
⊢ ((x + y) ^ 2) ^ 2 * (x + y) ^ 2 = ((x + y) ^ 2) ^ 3
Tactic:
ring
Proof state after:
no goals
Theorem: Imo2006P3.four_pow_four_pos
Proof state before:
⊢ 0 < 4 ^ 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: Imo2006P3.mid_ineq
Proof state before:
s t : ℝ
⊢ s * t ^ 3 ≤ (3 * t + s) ^ 4 / 4 ^ 4
Tactic:
rw [le_div_iff four_pow_four_pos]
Proof state after:
s t : ℝ
⊢ s * t ^ 3 * 4 ^ 4 ≤ (3 * t + s) ^ 4
Theorem: Imo2006P3.mid_ineq
Proof state before:
s t : ℝ
⊢ s * t ^ 3 * 4 ^ 4 ≤ (3 * t + s) ^ 4
Tactic:
have : 0 ≤ (s - t) ^ 2 * ((s + 7 * t) ^ 2 + 2 * (4 * t) ^ 2) := by positivity
Proof state after:
s t : ℝ
this : 0 ≤ (s - t) ^ 2 * ((s + 7 * t) ^ 2 + 2 * (4 * t) ^ 2)
⊢ s * t ^ 3 * 4 ^ 4 ≤ (3 * t + s) ^ 4
Theorem: Imo2006P3.mid_ineq
Proof state before:
s t : ℝ
this : 0 ≤ (s - t) ^ 2 * ((s + 7 * t) ^ 2 + 2 * (4 * t) ^ 2)
⊢ s * t ^ 3 * 4 ^ 4 ≤ (3 * t + s) ^ 4
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo2006P3.mid_ineq
Proof state before:
s t : ℝ
⊢ 0 ≤ (s - t) ^ 2 * ((s + 7 * t) ^ 2 + 2 * (4 * t) ^ 2)
Tactic:
positivity
Proof state after:
no goals
Theorem: Imo2006P3.rhs_ineq
Proof state before:
x y : ℝ
⊢ 3 * (x + y) ^ 2 ≤ 2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2)
Tactic:
have : 0 ≤ (x - y) ^ 2 := by positivity
Proof state after:
x y : ℝ
this : 0 ≤ (x - y) ^ 2
⊢ 3 * (x + y) ^ 2 ≤ 2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2)
Theorem: Imo2006P3.rhs_ineq
Proof state before:
x y : ℝ
this : 0 ≤ (x - y) ^ 2
⊢ 3 * (x + y) ^ 2 ≤ 2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2)
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo2006P3.rhs_ineq
Proof state before:
x y : ℝ
⊢ 0 ≤ (x - y) ^ 2
Tactic:
positivity
Proof state after:
no goals
Theorem: Imo2006P3.zero_lt_32
Proof state before:
⊢ 0 < 32
Tactic:
norm_num
Proof state after:
no goals
Theorem: Imo2006P3.subst_wlog
Proof state before:
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
⊢ 32 * |x * y * z * s| ≤ √2 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
Tactic:
have hz : (x + y) ^ 2 = z ^ 2 := by linear_combination (x + y - z) * hxyz
Proof state after:
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
⊢ 32 * |x * y * z * s| ≤ √2 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
Theorem: Imo2006P3.subst_wlog
Proof state before:
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
⊢ 32 * |x * y * z * s| ≤ √2 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
Tactic:
have this :=
  calc
    2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2)
      ≤ _ * _ ^ 3 := by gcongr; exact lhs_ineq hxy
    _ ≤ (3 * (x + y) ^ 2 + 2 * s ^ 2) ^ 4 / 4 ^ 4 := mid_ineq
    _ ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4 := by
        gcongr (?_ + _) ^ 4 / _
        apply rhs_ineq
Proof state after:
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
this : 2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2) ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4
⊢ 32 * |x * y * z * s| ≤ √2 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
Theorem: Imo2006P3.subst_wlog
Proof state before:
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
this : 2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2) ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4
⊢ 32 * |x * y * z * s| ≤ √2 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
Tactic:
refine le_of_pow_le_pow_left two_ne_zero (by positivity) ?_
Proof state after:
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
this : 2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2) ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4
⊢ (32 * |x * y * z * s|) ^ 2 ≤ (√2 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2) ^ 2
Theorem: Imo2006P3.subst_wlog
Proof state before:
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
this : 2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2) ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4
⊢ (32 * |x * y * z * s|) ^ 2 ≤ (√2 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2) ^ 2
Tactic:
calc
  (32 * |x * y * z * s|) ^ 2 = 32 * (2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2)) := by
    rw [mul_pow, sq_abs, hz]; ring
  _ ≤ 32 * ((2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4) := by gcongr
  _ = (sqrt 2 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2) ^ 2 := by
    field_simp
    rw [mul_pow, sq_sqrt zero_le_two, hz]
    ring
Proof state after:
no goals
Theorem: Imo2006P3.subst_wlog
Proof state before:
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
⊢ (x + y) ^ 2 = z ^ 2
Tactic:
linear_combination (x + y - z) * hxyz
Proof state after:
no goals
Theorem: Imo2006P3.subst_wlog
Proof state before:
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
⊢ 2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2) ≤ 2 * s ^ 2 * ((x + y) ^ 2) ^ 3
Tactic:
gcongr
Proof state after:
case h
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
⊢ 16 * x ^ 2 * y ^ 2 * (x + y) ^ 2 ≤ ((x + y) ^ 2) ^ 3
Theorem: Imo2006P3.subst_wlog
Proof state before:
case h
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
⊢ 16 * x ^ 2 * y ^ 2 * (x + y) ^ 2 ≤ ((x + y) ^ 2) ^ 3
Tactic:
exact lhs_ineq hxy
Proof state after:
no goals
Theorem: Imo2006P3.subst_wlog
Proof state before:
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
⊢ (3 * (x + y) ^ 2 + 2 * s ^ 2) ^ 4 / 4 ^ 4 ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4
Tactic:
gcongr (?_ + _) ^ 4 / _
Proof state after:
case hab.hab.bc
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
⊢ 3 * (x + y) ^ 2 ≤ 2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2)
Theorem: Imo2006P3.subst_wlog
Proof state before:
case hab.hab.bc
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
⊢ 3 * (x + y) ^ 2 ≤ 2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2)
Tactic:
apply rhs_ineq
Proof state after:
no goals
Theorem: Imo2006P3.subst_wlog
Proof state before:
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
this : 2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2) ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4
⊢ 0 ≤ √2 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
Tactic:
positivity
Proof state after:
no goals
Theorem: Imo2006P3.subst_wlog
Proof state before:
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
this : 2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2) ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4
⊢ (32 * |x * y * z * s|) ^ 2 = 32 * (2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2))
Tactic:
rw [mul_pow, sq_abs, hz]
Proof state after:
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
this : 2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2) ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4
⊢ 32 ^ 2 * (x * y * z * s) ^ 2 = 32 * (2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * z ^ 2))
Theorem: Imo2006P3.subst_wlog
Proof state before:
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
this : 2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2) ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4
⊢ 32 ^ 2 * (x * y * z * s) ^ 2 = 32 * (2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * z ^ 2))
Tactic:
ring
Proof state after:
no goals
Theorem: Imo2006P3.subst_wlog
Proof state before:
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
this : 2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2) ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4
⊢ 32 * (2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2)) ≤
    32 * ((2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4)
Tactic:
gcongr
Proof state after:
no goals
Theorem: Imo2006P3.subst_wlog
Proof state before:
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
this : 2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2) ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4
⊢ 32 * ((2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4) = (√2 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2) ^ 2
Tactic:
field_simp
Proof state after:
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
this : 2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2) ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4
⊢ 32 * (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 = (√2 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2) ^ 2 * 4 ^ 4
Theorem: Imo2006P3.subst_wlog
Proof state before:
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
this : 2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2) ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4
⊢ 32 * (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 = (√2 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2) ^ 2 * 4 ^ 4
Tactic:
rw [mul_pow, sq_sqrt zero_le_two, hz]
Proof state after:
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
this : 2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2) ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4
⊢ 32 * (2 * (x ^ 2 + y ^ 2 + z ^ 2) + 2 * s ^ 2) ^ 4 = 2 * ((x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2) ^ 2 * 4 ^ 4
Theorem: Imo2006P3.subst_wlog
Proof state before:
x y z s : ℝ
hxy : 0 ≤ x * y
hxyz : x + y + z = 0
hz : (x + y) ^ 2 = z ^ 2
this : 2 * s ^ 2 * (16 * x ^ 2 * y ^ 2 * (x + y) ^ 2) ≤ (2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2) + 2 * s ^ 2) ^ 4 / 4 ^ 4
⊢ 32 * (2 * (x ^ 2 + y ^ 2 + z ^ 2) + 2 * s ^ 2) ^ 4 = 2 * ((x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2) ^ 2 * 4 ^ 4
Tactic:
ring
Proof state after:
no goals
Theorem: Imo2006P3.subst_proof₁
Proof state before:
x y z s : ℝ
hxyz : x + y + z = 0
⊢ |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
Tactic:
wlog h' : 0 ≤ x * y generalizing x y z
Proof state after:
case inr
x y z s : ℝ
hxyz : x + y + z = 0
this : ∀ (x y z : ℝ), x + y + z = 0 → 0 ≤ x * y → |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
h' : ¬0 ≤ x * y
⊢ |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2

s x y z : ℝ
hxyz : x + y + z = 0
h' : 0 ≤ x * y
⊢ |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
Theorem: Imo2006P3.subst_proof₁
Proof state before:
case inr
x y z s : ℝ
hxyz : x + y + z = 0
this : ∀ (x y z : ℝ), x + y + z = 0 → 0 ≤ x * y → |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
h' : ¬0 ≤ x * y
⊢ |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2

s x y z : ℝ
hxyz : x + y + z = 0
h' : 0 ≤ x * y
⊢ |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
Tactic:
swap
Proof state after:
s x y z : ℝ
hxyz : x + y + z = 0
h' : 0 ≤ x * y
⊢ |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2

case inr
x y z s : ℝ
hxyz : x + y + z = 0
this : ∀ (x y z : ℝ), x + y + z = 0 → 0 ≤ x * y → |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
h' : ¬0 ≤ x * y
⊢ |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
Theorem: Imo2006P3.subst_proof₁
Proof state before:
case inr
x y z s : ℝ
hxyz : x + y + z = 0
this : ∀ (x y z : ℝ), x + y + z = 0 → 0 ≤ x * y → |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
h' : ¬0 ≤ x * y
⊢ |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
Tactic:
cases' (mul_nonneg_of_three x y z).resolve_left h' with h h
Proof state after:
case inr.inl
x y z s : ℝ
hxyz : x + y + z = 0
this : ∀ (x y z : ℝ), x + y + z = 0 → 0 ≤ x * y → |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
h' : ¬0 ≤ x * y
h : 0 ≤ y * z
⊢ |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2

case inr.inr
x y z s : ℝ
hxyz : x + y + z = 0
this : ∀ (x y z : ℝ), x + y + z = 0 → 0 ≤ x * y → |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
h' : ¬0 ≤ x * y
h : 0 ≤ z * x
⊢ |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
Theorem: Imo2006P3.subst_proof₁
Proof state before:
s x y z : ℝ
hxyz : x + y + z = 0
h' : 0 ≤ x * y
⊢ |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
Tactic:
rw [div_mul_eq_mul_div, le_div_iff' zero_lt_32]
Proof state after:
s x y z : ℝ
hxyz : x + y + z = 0
h' : 0 ≤ x * y
⊢ 32 * |x * y * z * s| ≤ √2 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
Theorem: Imo2006P3.subst_proof₁
Proof state before:
s x y z : ℝ
hxyz : x + y + z = 0
h' : 0 ≤ x * y
⊢ 32 * |x * y * z * s| ≤ √2 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
Tactic:
exact subst_wlog h' hxyz
Proof state after:
no goals
Theorem: Imo2006P3.subst_proof₁
Proof state before:
case inr.inl
x y z s : ℝ
hxyz : x + y + z = 0
this : ∀ (x y z : ℝ), x + y + z = 0 → 0 ≤ x * y → |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
h' : ¬0 ≤ x * y
h : 0 ≤ y * z
⊢ |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
Tactic:
convert this y z x _ h using 2 <;> linarith
Proof state after:
no goals
Theorem: Imo2006P3.subst_proof₁
Proof state before:
case inr.inr
x y z s : ℝ
hxyz : x + y + z = 0
this : ∀ (x y z : ℝ), x + y + z = 0 → 0 ≤ x * y → |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
h' : ¬0 ≤ x * y
h : 0 ≤ z * x
⊢ |x * y * z * s| ≤ √2 / 32 * (x ^ 2 + y ^ 2 + z ^ 2 + s ^ 2) ^ 2
Tactic:
convert this z x y _ h using 2 <;> linarith
Proof state after:
no goals
Theorem: Imo2006P3.proof₁
Proof state before:
a b c : ℝ
⊢ |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| =
    |(a - b) * (b - c) * (c - a) * -(a + b + c)|
Tactic:
ring_nf
Proof state after:
no goals
Theorem: Imo2006P3.proof₁
Proof state before:
a b c : ℝ
⊢ a - b + (b - c) + (c - a) = 0
Tactic:
ring
Proof state after:
no goals
Theorem: Imo2006P3.proof₁
Proof state before:
a b c : ℝ
⊢ √2 / 32 * ((a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2 + (-(a + b + c)) ^ 2) ^ 2 =
    9 * √2 / 32 * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: Imo2006P3.proof₂
Proof state before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
⊢ 9 * √2 / 32 ≤ M
Tactic:
set α := sqrt (2:ℝ)
Proof state after:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
⊢ 9 * α / 32 ≤ M
Theorem: Imo2006P3.proof₂
Proof state before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
⊢ 9 * α / 32 ≤ M
Tactic:
have hα : α ^ 2 = 2 := sq_sqrt (by norm_num)
Proof state after:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
⊢ 9 * α / 32 ≤ M
Theorem: Imo2006P3.proof₂
Proof state before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
⊢ 9 * α / 32 ≤ M
Tactic:
let a := 2 - 3 * α
Proof state after:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
⊢ 9 * α / 32 ≤ M
Theorem: Imo2006P3.proof₂
Proof state before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
⊢ 9 * α / 32 ≤ M
Tactic:
let c := 2 + 3 * α
Proof state after:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 9 * α / 32 ≤ M
Theorem: Imo2006P3.proof₂
Proof state before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 9 * α / 32 ≤ M
Tactic:
calc _ = 18 ^ 2 * 2 * α / 48 ^ 2 := by ring
  _ ≤ M := ?_
Proof state after:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 18 ^ 2 * 2 * α / 48 ^ 2 ≤ M
Theorem: Imo2006P3.proof₂
Proof state before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 18 ^ 2 * 2 * α / 48 ^ 2 ≤ M
Tactic:
rw [div_le_iff (by positivity)]
Proof state after:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 18 ^ 2 * 2 * α ≤ M * 48 ^ 2
Theorem: Imo2006P3.proof₂
Proof state before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 18 ^ 2 * 2 * α ≤ M * 48 ^ 2
Tactic:
calc 18 ^ 2 * 2 * α
    = 18 ^ 2 * α ^ 2 * α := by linear_combination -324 * α * hα
  _ = abs (-(18 ^ 2 * α ^ 2 * α)) := by rw [abs_neg, abs_of_nonneg]; positivity
  _ = |a * 2 * (a ^ 2 - 2 ^ 2) + 2 * c * (2 ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| := by ring_nf
  _ ≤ M * (a ^ 2 + 2 ^ 2 + c ^ 2) ^ 2 := by apply h
  _ = M * 48 ^ 2 := by linear_combination (324 * α ^ 2 + 1080) * M * hα
Proof state after:
no goals
Theorem: Imo2006P3.proof₂
Proof state before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
⊢ 0 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Imo2006P3.proof₂
Proof state before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 9 * α / 32 = 18 ^ 2 * 2 * α / 48 ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: Imo2006P3.proof₂
Proof state before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 0 < 48 ^ 2
Tactic:
positivity
Proof state after:
no goals
Theorem: Imo2006P3.proof₂
Proof state before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 18 ^ 2 * 2 * α = 18 ^ 2 * α ^ 2 * α
Tactic:
linear_combination -324 * α * hα
Proof state after:
no goals
Theorem: Imo2006P3.proof₂
Proof state before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 18 ^ 2 * α ^ 2 * α = |(-(18 ^ 2 * α ^ 2 * α))|
Tactic:
rw [abs_neg, abs_of_nonneg]
Proof state after:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 0 ≤ 18 ^ 2 * α ^ 2 * α
Theorem: Imo2006P3.proof₂
Proof state before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ 0 ≤ 18 ^ 2 * α ^ 2 * α
Tactic:
positivity
Proof state after:
no goals
Theorem: Imo2006P3.proof₂
Proof state before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ |(-(18 ^ 2 * α ^ 2 * α))| = |a * 2 * (a ^ 2 - 2 ^ 2) + 2 * c * (2 ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)|
Tactic:
ring_nf
Proof state after:
no goals
Theorem: Imo2006P3.proof₂
Proof state before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ |a * 2 * (a ^ 2 - 2 ^ 2) + 2 * c * (2 ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + 2 ^ 2 + c ^ 2) ^ 2
Tactic:
apply h
Proof state after:
no goals
Theorem: Imo2006P3.proof₂
Proof state before:
M : ℝ
h :
  ∀ (a b c : ℝ),
    |a * b * (a ^ 2 - b ^ 2) + b * c * (b ^ 2 - c ^ 2) + c * a * (c ^ 2 - a ^ 2)| ≤ M * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2
α : ℝ := √2
hα : α ^ 2 = 2
a : ℝ := 2 - 3 * α
c : ℝ := 2 + 3 * α
⊢ M * (a ^ 2 + 2 ^ 2 + c ^ 2) ^ 2 = M * 48 ^ 2
Tactic:
linear_combination (324 * α ^ 2 + 1080) * M * hα
Proof state after:
no goals
Theorem: Usa1998P3.lemma0
Proof state before:
⊢ Set.Icc (-Real.pi / 4) (Real.pi / 4) ⊆ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)
Tactic:
intro a ha
Proof state after:
a : ℝ
ha : a ∈ Set.Icc (-Real.pi / 4) (Real.pi / 4)
⊢ a ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)
Theorem: Usa1998P3.lemma0
Proof state before:
a : ℝ
ha : a ∈ Set.Icc (-Real.pi / 4) (Real.pi / 4)
⊢ a ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)
Tactic:
exact ⟨by linarith[ha.1, Real.pi_pos], by linarith[ha.2, Real.pi_pos]⟩
Proof state after:
no goals
Theorem: Usa1998P3.lemma0
Proof state before:
a : ℝ
ha : a ∈ Set.Icc (-Real.pi / 4) (Real.pi / 4)
⊢ -(Real.pi / 2) < a
Tactic:
linarith[ha.1, Real.pi_pos]
Proof state after:
no goals
Theorem: Usa1998P3.lemma0
Proof state before:
a : ℝ
ha : a ∈ Set.Icc (-Real.pi / 4) (Real.pi / 4)
⊢ a < Real.pi / 2
Tactic:
linarith[ha.2, Real.pi_pos]
Proof state after:
no goals
Theorem: Usa1998P3.lemma1
Proof state before:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
⊢ (x - Real.pi / 4).tan < 1
Tactic:
let y' x := Real.tan (x - Real.pi / 4)
Proof state after:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
⊢ (x - Real.pi / 4).tan < 1
Theorem: Usa1998P3.lemma1
Proof state before:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
⊢ (x - Real.pi / 4).tan < 1
Tactic:
have h4 : Real.tan (Real.pi / 4) = y' (Real.pi / 2) := by
  dsimp only [y']
  rw [Real.tan_pi_div_two_sub, Real.tan_pi_div_four, one_eq_inv]
Proof state after:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
⊢ (x - Real.pi / 4).tan < 1
Theorem: Usa1998P3.lemma1
Proof state before:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
⊢ (x - Real.pi / 4).tan < 1
Tactic:
rw [← Real.tan_pi_div_four]
Proof state after:
x : ℝ
hx : x ∈ Set.Ioo 0 (Real.pi / 2)
y' : ℝ → ℝ := fun x => (x - Real.pi / 4).tan
h4 : (Real.pi / 4).tan = y' (Real.pi / 2)
⊢ (x - Real.pi / 4).tan < (Real.pi / 4).tan