Commit 2026-04-29 13:03 d65ebabb

View on Github →

chore(*): triage adaptation notes (#38470) This PR, along with my to previous ones, goes through the current adaptation notes in Mathlib and reverts the changes if possible, or commits to the changes if they are harmless anyway.

Estimated changes

Modified Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

Modified Mathlib/CategoryTheory/Filtered/Small.lean

Modified Mathlib/CategoryTheory/Monoidal/OfHasFiniteProducts.lean

Modified Mathlib/Data/Int/SuccPred.lean

Modified Mathlib/Data/List/Basic.lean

deleted theorem List.filter_subset'

added theorem List.filter_subset_self

Modified Mathlib/Data/List/Lattice.lean

Modified Mathlib/Data/List/MinMax.lean

Modified Mathlib/Data/Nat/SuccPred.lean

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

Modified Mathlib/SetTheory/Lists.lean

deleted def Lists.Equiv.decidable

deleted def Lists.Subset.decidable

deleted def Lists.mem.decidable

Modified Mathlib/Tactic/Translate/Core.lean

Modified Mathlib/Topology/Order/DenselyOrdered.lean

Modified MathlibTest/grind/pairwise_disjoint.lean

deleted theorem LawfulSingleton.insert_empty_eq'

Modified MathlibTest/zmod.lean