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

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
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

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
State after:
no goals

State before:
x y : ℝ
hxy : 0 ≤ x * y
⊢ (x - y) ^ 2 * ((x + y) ^ 2 + 4 * (x * y)) ≥ 0
Tactic:
positivity
State after:
no goals

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
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

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
State after:
no goals

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
State after:
no goals