mathlib3
445be96e - fix(tactic/squeeze): `squeeze_simp` providing invalid suggestions (#11696)

Commit
3 years ago
fix(tactic/squeeze): `squeeze_simp` providing invalid suggestions (#11696) `squeeze_simp` was previously permuting the lemmas passed to `simp`, which caused failures in cases where the lemma order mattered. The fix is to ensure that `squeeze_simp` does not change the order of passed lemmas. Closes #3097
Author
Parents
Loading