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

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

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

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) ?_
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

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

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

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

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

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 / _
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)

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

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

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

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

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

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

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

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