Commit 2025-09-15 22:46 2609d95a

chore: deprecate Real.add_lt_add_iff_left (#29676) _root_.add_lt_add_iff_left serves the same purpose, though the instance that provides it currently relies on the specialized theorem. By deprecating it, authors no longer need to make a meaningless choice between the two theorems. Making it protected should ensure no disambiguation is needed when the Real namespace is open, though I've not managed to reproduce a case where Lean errors rather than using the namespaced theorem silently.