Commit 2025-06-13 14:34 dfb6ce9d

View on Github →

chore(grewrite): import gcongr and grewrite in Tactic.Common (#25773) This PR rearranges the gcongr attributes so that gcongr and grewrite have minimal imports. This means that it can be imported in Mathlib.Tactic.Common. There was also an unused import in Tactic.Hint that I removed positivity now gets tagged as the discharger for gcongr immediately, which makes some proofs shorter. Nat.succ_le_succ was tagged twice with gcongr, so I removed the loose tag.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Field.lean

Modified Mathlib/Algebra/Order/Floor/Ring.lean

Modified Mathlib/Algebra/Order/Floor/Semiring.lean

Modified Mathlib/Algebra/Order/Module/OrderedSMul.lean

Modified Mathlib/Analysis/Normed/Group/Seminorm.lean

Modified Mathlib/Data/Finset/Density.lean

Modified Mathlib/Data/Int/CardIntervalMod.lean

Modified Mathlib/Data/Nat/Basic.lean

Modified Mathlib/Data/Nat/Factorial/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/AbsoluteValue.lean

Modified Mathlib/Order/Basic.lean

added def GCongr.exactLeOfLt

added theorem GCongr.gt_imp_gt

added theorem GCongr.gt_imp_gt_left

added theorem GCongr.gt_imp_gt_right

added theorem GCongr.le_imp_le

added theorem GCongr.lt_imp_lt

Modified Mathlib/Order/Lattice.lean

deleted def exactSubsetOfSSubset

Modified Mathlib/Order/RelClasses.lean

added def GCongr.exactSubsetOfSSubset

added theorem GCongr.ssubset_imp_ssubset

added theorem GCongr.ssubset_imp_ssubset_right

added theorem GCongr.ssuperset_imp_ssuperset

added theorem GCongr.ssuperset_imp_ssuperset_left

added theorem GCongr.ssuperset_imp_ssuperset_right

Modified Mathlib/Tactic/Common.lean

Modified Mathlib/Tactic/GCongr.lean

deleted theorem Mathlib.Tactic.GCongr.gt_imp_gt

deleted theorem Mathlib.Tactic.GCongr.gt_imp_gt_left

deleted theorem Mathlib.Tactic.GCongr.gt_imp_gt_right

deleted theorem Mathlib.Tactic.GCongr.le_imp_le

deleted theorem Mathlib.Tactic.GCongr.lt_imp_lt

deleted theorem Mathlib.Tactic.GCongr.ssubset_imp_ssubset

deleted theorem Mathlib.Tactic.GCongr.ssubset_imp_ssubset_right

deleted theorem Mathlib.Tactic.GCongr.ssuperset_imp_ssuperset

deleted theorem Mathlib.Tactic.GCongr.ssuperset_imp_ssuperset_left

deleted theorem Mathlib.Tactic.GCongr.ssuperset_imp_ssuperset_right

Modified Mathlib/Tactic/GCongr/Core.lean

deleted def Mathlib.Tactic.GCongr.exactLeOfLt

Modified Mathlib/Tactic/GCongr/CoreAttrs.lean

Modified Mathlib/Tactic/GRewrite.lean

Modified Mathlib/Tactic/Hint.lean

Modified Mathlib/Tactic/Positivity/Core.lean

Modified Mathlib/Tactic/Widget/GCongr.lean

Modified scripts/noshake.json