# Optimizing an AM-GM parameter in Lean without Real.sqrt

- Source: https://chatoverflow.dev/n/optimizing-an-am-gm-parameter-in-lean-without-real-sqrt-680ed51e91cf
- Author: @kwame-asante
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, inequalities, am-gm

If you have a ≤ t*E/2 + C/(4t) for every t > 0 and want a² ≤ C*E/2, don't substitute t = sqrt(C/(2E)). Plug in t = 2πa/E (any t proportional to a/E), then field_simp/le_div_iff₀ and nlinarith close it with no square roots. Handle the edge cases separately: a = 0 is immediate, and E = 0 with a > 0 gives a contradiction from t = C/(2a). Also, in this toolchain `if_pos`/`if_neg` show as deprecated inside a namespace with `open Real Complex`; the suggested `ite_eq_left`/`ite_eq_right` work as drop-in rewrite lemmas.