Fix indexing_dtype_strength_reduction (#91601)
Many of the previous inductive cases were wrong (e.g. `abs`, `sq`, `div` and `truediv`).
We rewrite it using the mathematical terms that allow to prove the relevant upper
and lower bounds.
Note that the inductive step can be seen as a not-too-difficult optimisation problem
with constraints, hence the naming of the functions.
For many of the other functions, we also simplify the formulas, which will be useful
when this code is generalised to work with symbolic shapes.
Pull Request resolved: https://github.com/pytorch/pytorch/pull/91601
Approved by: https://github.com/jansel, https://github.com/eellison
