Commit 2024-07-31 19:18 b66c970b

View on Github →

feat: gcongr works with eta and proofs (#15364)

gcongr now recognizes eta-expanded variables as variables
gcongr now recognizes all proofs as "defeq" even if the proofs have different types (in e.g. Finset.sup'_mono
Give a bit more information in the error message when not accepting a gcongr-lemma.

Estimated changes

Modified Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

deleted theorem GCongr.prod_le_prod'

deleted theorem GCongr.prod_lt_prod_of_nonempty'

Modified Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

deleted theorem GCongr.prod_le_prod

Modified Mathlib/Combinatorics/Schnirelmann.lean

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/Finset/Lattice.lean

deleted theorem GCongr.finset_inf'_mono

deleted theorem GCongr.finset_sup'_le

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

Modified Mathlib/Tactic/GCongr/Core.lean

Modified test/GCongr/inequalities.lean