Commit 2026-08-04 16:35 881e56ce

View on Github →

chore: golf some proofs with grw (#42440) Use grw/gcongr to golf some proofs. Additionally, deprecate ENNReal.coe_le_coe_of_le/ENNReal.coe_lt_coe_of_lt, as gcongr can now be used on iff lemmas.

Estimated changes

Modified Mathlib/Analysis/Calculus/FDeriv/Extend.lean

Modified Mathlib/Analysis/Normed/Algebra/Spectrum.lean

Modified Mathlib/Data/ENNReal/Basic.lean

modified theorem ENNReal.coe_le_coe

modified theorem ENNReal.coe_lt_coe

Modified Mathlib/Data/Set/NAry.lean

Modified Mathlib/Dynamics/OmegaLimit.lean

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

Modified Mathlib/MeasureTheory/Measure/Stieltjes.lean

Modified Mathlib/MeasureTheory/VectorMeasure/Integral.lean