Commit 2025-10-27 16:35 ef9ae2a4

View on Github →

feat(gcongr): support @[gcongr] for Monotone and friends (#28339) This PR adds the feature to gcongr that you can now tag lemmas whose conclusion is Monotone f, Antitone f, etc.

Estimated changes

modified theorem Int.floor_le_floor
modified theorem Nat.floor_le_floor
modified theorem algebraMap_mono
modified theorem algebraMap_strictMono
modified theorem EReal.exp_le_exp
modified theorem EReal.exp_lt_exp
modified theorem Multiset.card_strictMono
deleted theorem GCongr.natCast_le_natCast
deleted theorem GCongr.natCast_lt_natCast
modified theorem Module.Basis.flag_le_flag
deleted theorem GCongr.Filter.map_le_map