Theorem: Imo2006P3.subst_proof₁ (Compfiles/Imo2006P3.lean)

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

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

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

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

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

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

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