Theorem: Imo2006P3.rhs_ineq (Compfiles/Imo2006P3.lean)

State before:
x y : ℝ
⊢ 3 * (x + y) ^ 2 ≤ 2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2)
Tactic:
have : 0 ≤ (x - y) ^ 2 := by positivity
State after:
x y : ℝ
this : 0 ≤ (x - y) ^ 2
⊢ 3 * (x + y) ^ 2 ≤ 2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2)

State before:
x y : ℝ
this : 0 ≤ (x - y) ^ 2
⊢ 3 * (x + y) ^ 2 ≤ 2 * (x ^ 2 + y ^ 2 + (x + y) ^ 2)
Tactic:
linarith
State after:
no goals

State before:
x y : ℝ
⊢ 0 ≤ (x - y) ^ 2
Tactic:
positivity
State after:
no goals