Commit 2025-12-11 11:46 798365a9

View on Github →

chore: absorb steps into terminal grind (#32713) This PR takes existing proofs that end with grind, and absorbs steps before grind that aren't needed. From #mathlib4 > Weekly linting log @ 💬

Estimated changes

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

Modified Mathlib/Algebra/Polynomial/RuleOfSigns.lean

Modified Mathlib/Analysis/Analytic/Order.lean

Modified Mathlib/CategoryTheory/Filtered/Basic.lean

Modified Mathlib/Combinatorics/SimpleGraph/Walks/Maps.lean

Modified Mathlib/Data/Fin/Tuple/Basic.lean

Modified Mathlib/Data/Finset/Pi.lean

Modified Mathlib/Data/Nat/Sqrt.lean

Modified Mathlib/Data/PFun.lean

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

Modified Mathlib/Order/Interval/Finset/Basic.lean

modified theorem Finset.Ico_diff_Ico_left

modified theorem Finset.Ico_diff_Ico_right

modified theorem Finset.Ico_filter_le

modified theorem Finset.Ico_filter_lt

modified theorem Finset.Ioc_inter_Ioc

modified theorem Finset.Ioo_filter_lt

Modified Mathlib/Topology/Algebra/InfiniteSum/Defs.lean