Commit 2026-09-28 14:01 87e20d7d

View on Github →

chore: golf proofs with grw/gcongr/gconvert (#44245)

Estimated changes

Modified Mathlib/Algebra/Order/CompleteField.lean

modified theorem ConditionallyCompleteLinearOrderedField.inducedMap_nonneg

modified theorem LinearOrderedField.cutMap_mono

Modified Mathlib/Computability/Ackermann.lean

Modified Mathlib/Data/Set/Pairwise/Basic.lean

added theorem Set.Pairwise.mono''

Modified Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean

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

Modified Mathlib/MeasureTheory/Integral/Average.lean

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

Modified Mathlib/MeasureTheory/Measure/Decomposition/Exhaustion.lean

Modified Mathlib/MeasureTheory/Measure/Regular.lean

Modified Mathlib/MeasureTheory/OuterMeasure/Basic.lean

modified theorem MeasureTheory.pos_mono

Modified Mathlib/Probability/Martingale/Upcrossing.lean

Modified Mathlib/SetTheory/Ordinal/Enum.lean

Modified Mathlib/SetTheory/ZFC/VonNeumann.lean

Modified Mathlib/Topology/MetricSpace/CoveringExponent.lean

Modified Mathlib/Topology/MetricSpace/MetricSeparated.lean