Want to multiply ineq on both sides, apply_fun is hard

Stream: new members

[Daniel Vainsencher]

Hi, while trying to formalize a simple inequality (a variant of am-gm), I wanted to massage an inequality by multiplying both sides by a positive term.

apply_fun (see example below) felt like using a cannon to swat a fly.

Are there better tools for this elementary task (and the other term shuffling)?
Maybe specialized to ℝ with the usual ordering?

example (x y : ℝ )
  (hp : (x+y)^2 > 0)
  (h' : 4 * x * y ≤ (x + y) ^ 2) :
    x*y/(x+y)^2 ≤ 1 / 4 := by {
  -- h' is almost the goal, mathematically just need to
  -- "multiply both sides of the goal by 4 * (x + y) ^ 2, its fine because hp"
  have hpp : 4 * (x + y) ^ 2 > 0 := by positivity
  apply_fun OrderIso.mulRight₀ (4 * (x + y) ^ 2) hpp
  simp
  move_mul [← 4]
  field_simp
  rw [← mul_assoc]
  convert h'
}

[Yaël Dillies]

You could rewrite using docs#mul_le_mul_right

[Kevin Buzzard]

import Mathlib

example (x y : ℝ)
    (hp : (x+y)^2 > 0)
    (h' : 4 * x * y ≤ (x + y) ^ 2) :
    x*y/(x+y)^2 ≤ 1 / 4 := by
  rw [div_le_div_iff] <;> linarith

[Daniel Vainsencher]

@Kevin Buzzard thanks, (n)linarith is clearly a powerful tool and I need to better understand what cases it handles and what can block it.