Commit 2025-06-10 22:11 4523c8f5

feat: let gcongr deal with implications (#25534) This PR implements support for the _ → _ relation in the gcongr tactic. This can be useful in its own right, but the main reason for this is to later implement the grw and gconvert tactic using this infrastructure. To be more specific, _ → _ is now supported as a relation, and as a constant. Supporting it as a constant is not necessary for the purpose of grw, but it seems natural to add support for it in this PR, so that lemmas like imp_imp_imp can be used by gcongr. To make _ → _ in gcongr work more easily out of the box, I've built in support for goals of the form r a b → r c d where r is a transitive relation (i.e. it implements isTrans α r). This behaviour can be overridden with a @[gcongr] tag, and this is in particular done for the < relation, since we want the new goals to use ≤ instead of <. #mathlib4 > Rewrite with inequalities @ 💬