mathlib3

5c851bdb - fix(tactic/squeeze_simp): make `squeeze_simp [←...]` work (#2961)

fix(tactic/squeeze_simp): make `squeeze_simp [←...]` work (#2961) `squeeze_simp` parses the argument list using a function in core Lean, and when support for backwards arguments was added to `simp`, it used a new function to parse the additional structure. This PR fixes the TODO left in the code to switch `squeeze_simp` to the new function by deleting the code that needed it - it wasn't used anyway! To add a test for the fix, I moved the single existing `squeeze_simp` test from the deprecated file `examples.lean` to a new file.