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

State before:
s t : ℝ
⊢ s * t ^ 3 ≤ (3 * t + s) ^ 4 / 4 ^ 4
Tactic:
rw [le_div_iff four_pow_four_pos]
State after:
s t : ℝ
⊢ s * t ^ 3 * 4 ^ 4 ≤ (3 * t + s) ^ 4

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

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

State before:
s t : ℝ
⊢ 0 ≤ (s - t) ^ 2 * ((s + 7 * t) ^ 2 + 2 * (4 * t) ^ 2)
Tactic:
positivity
State after:
no goals