mathlib

dbc4284c - feat(tactic/squeeze): improve suggestion of `cases x; squeeze_simp` (#2218)

feat(tactic/squeeze): improve suggestion of `cases x; squeeze_simp` (#2218) * feat(tactic/squeeze): improve produced argument list and format * feat(tactic/squeeze): combine suggestions of repeated executions * add documentation * remove dead code * suggestion from reviewers * Apply suggestions from code review Co-Authored-By: Gabriel Ebner <gebner@gebner.org> * Update squeeze.lean * Apply suggestions from code review Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * simplify and remove comparison of proof terms * simplify goal comparison data structure * add documentation and fix meta-variable handling * add example * fix tests * move tests * use binders with trivial names to abstract meta variables Co-authored-by: Gabriel Ebner <gebner@gebner.org> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>