Commit 2026-09-13 13:07 f508fa49

View on Github →

chore(Tactic/GCongr): deprecate Tactic/GCongr/CoreAttrs (#43594) This PR moves the @[gcongr] attributes that are in Mathlib.Tactic.GCongr.CoreAttrs to Mathlib.Tactic.GCongr and deprecates the former file. This follows the same pattern as e.g. to_additive of putting the basic attributes/setup in the root file of the tactic implementation.

Estimated changes

Modified Mathlib/Tactic/GCongr.lean

added theorem Mathlib.Tactic.GCongr.and_mono

added theorem Mathlib.Tactic.GCongr.imp_mono

Modified Mathlib/Tactic/GCongr/CoreAttrs.lean

deleted theorem Mathlib.Tactic.GCongr.and_mono

deleted theorem Mathlib.Tactic.GCongr.imp_mono