Commit 2026-02-06 13:36 c01b1d7d

feat(gcongr): beef up @[gcongr] tag to accept ↔ & any argument order (#33025) This PR modifies the @[gcongr] tag to accept lemmas in more forms.

• Iff-lemmas are now accepted, and are turned into an auxiliary lemma that is simply one of the two implications.
• Implicational gcongr lemmas now don't need to have their arguments given in the "correct" order. An auxiliary lemma is generated if necessary. The auxiliary lemma generation is done analogously to simp which creates little lemmas Foo._simp_1., I also went throught all lemmas that have GCongr. in the name, and removed all but one of them (the remaining one is GCongr.mem_of_le_of_mem) A future PR may introduce the gcongr at tactic, which does gcongr but at hypotheses. This would be using the reverse direction of the iff lemmas tagged with gcongr. For this reason it is preferred to tag the iff lemma if possible.