Commit 2025-07-31 09:17 8495a95a

feat(gcongr): also use more general lemmas, closing extra goals with rfl (#26907) This PR fixes an annoyance in tagging gcongr lemmas: if your function has n arguments in which to use congruence, then you would need to provide 2^n-1 gcongr lemmas. Now, it suffices to only tag the most general gcongr lemma, and in more specific cases, the extra goals will be closed using rfl. While working on this, more issues with gcongr came up, and these all needed to be dealt with in the same PR:

• When applying a gcongr lemma, this should be done in the reducible transparency. The transparency was already bumped form default to instances after a zulip discussion (#mathlib4 > gcongr unfold DFunLike.coe). But I found that the same issue appears at instances transparency instead of reducible. MWE:

import Mathlib
open MeasureTheory
variable {α : Type*} (a : Set α) {μ : OuterMeasure α} {μ' : OuterMeasure α}
@[gcongr] -- remove this tag to make the last example work
lemma mono_outerMeasure (h : μ ≤ μ') : μ a ≤ μ' a := h a
example (h : μ ≤ μ') : μ a ≤ μ' a := by gcongr
variable [MeasurableSpace α] {ν : Measure α} {ν' : Measure α}
@[gcongr]
lemma mono_measure (h : ν ≤ ν') : ν a ≤ ν' a := h a
example (h : ν ≤ ν') : ν a ≤ ν' a := by
  with_reducible apply mono_outerMeasure
  set_option trace.Meta.isDefEq true in
  with_reducible gcongr

This aligns with the congr! tactic

• Using reducible transparency is not compatible with the approach of matching varyingArgs, because when comparing instance arguments, we need to use at least instances transparency. So, instead of storing the lemmas by varyingArgs, we sort them by the number of varying arguments, and simply try applying all the lemmas (which should be cheap in reducible transparency). This aligns with congr/congr!(/simp) which also tries all of the lemmas for the given constant.
• As a result of sorting the lemmas in the same way as congr lemmas, more recently added lemmas are now tried before older ones. This causes an issue which has to be solved by implementing a priority argument for the gcongr tag (similar to how instance and simp work), e.g.@[gcongr high]. This aligns with the @[congr] tag.