Commit 2025-06-14 00:25 121a0233

View on Github →

feat(gcongr): fix pattern elaborator and @[gcongr] for lemmas introducing binders (#25716) This PR adds @[gcongr] tags so that

gcongr can move inside Eventually and Frequently,
moving inside of ∀ ε > 0, or ∃ ε > 0, adds the hypothesis/condition to the local context.

Estimated changes

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.GCongr.eventually_mono

added theorem Filter.GCongr.frequently_mono

Modified Mathlib/Tactic/GCongr/Core.lean

Modified Mathlib/Tactic/GCongr/CoreAttrs.lean

added theorem GCongr.and_right_mono

added theorem GCongr.imp_right_mono

added theorem GCongr.imp_trans

deleted theorem imp_trans'

deleted theorem imp_trans

Modified MathlibTest/GCongr/inequalities.lean

Modified MathlibTest/peel.lean