Commit 2023-03-03 08:54 b46c2e36

feat: tactic congr! and improvement to convert (#2566) This introduces a tactic congr! that is an analogue to mathlib 3's congr'. It is a more insistent version of congr that makes use of more congruence lemmas (including user congruence lemmas), propext, funext, and Subsingleton instances. It also has a feature to lift reflexive relations to equalities. Along with funext, the tactic does intros, allowing congr! to get access to function bodies; the introduced variables can be named using rename_i if needed. This also modifies convert to use congr! rather than congr, which makes it work more like the mathlib3 version of the tactic.