Commit 2025-11-13 17:14 64900984

feat(gcongr): use mdata instead of template (#30739) This PR changes the implementation of gcongr patterns. Instead of carrying around another expression of the same shape, we put a metadata annotation in the actual goal, in order to keep track of where we want to apply more gcongr lemmas. This makes the implementation neater, and this is a necessary step towards supporting more operations in gcongr, such as those from the congr! tactic. This also means that the pattern given to the gcongr tactic is checked to be fully correct. This helped fix one pattern in mathlib that was ∑ _ : α, ?_, but should have been ∑ _ : β, ?_. Another change that this PR makes is that if the goal relation is a → b, then we run reducible whnf on a and b before getting the two sides of the relation. This means that x > y is reduced to y < x. This is needed because this refactor now is keeping track of which side is which side, and to do this consistently, we need x > y to be swapped into y < x.