Commit 2025-10-28 10:18 6e294ac5

View on Github →

chore: use grw, gcongr even more (#30632) Also delete a redundant instance.

Estimated changes

Modified Archive/Imo/Imo1982Q1.lean

Modified Archive/Imo/Imo2013Q5.lean

Modified Mathlib/Algebra/Order/AbsoluteValue/Basic.lean

Modified Mathlib/Algebra/Order/GroupWithZero/WithZero.lean

Modified Mathlib/Algebra/Polynomial/BigOperators.lean

Modified Mathlib/Algebra/Polynomial/Degree/Definitions.lean

Modified Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/TrapezoidalRule.lean

Modified Mathlib/RingTheory/PowerSeries/Order.lean

Modified Mathlib/SetTheory/Ordinal/NaturalOps.lean

Modified Mathlib/Topology/EMetricSpace/PairReduction.lean