Commit 2026-10-19 01:27 a0173d26

View on Github →

chore: remove unnecessary set_option lines (#45012) I removed 41 unnecessary set_option line(s) across 24 file(s).

Estimated changes

Modified Mathlib/Algebra/Group/End.lean

Modified Mathlib/Algebra/Homology/DerivedCategory/Ext/Map.lean

Modified Mathlib/Algebra/Homology/DerivedCategory/ShortExact.lean

Modified Mathlib/Algebra/Homology/Embedding/ExtendHomotopy.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean

Modified Mathlib/Algebra/Homology/HomotopyCategory/Triangulated.lean

Modified Mathlib/Analysis/Calculus/ContDiff/Basic.lean

Modified Mathlib/CategoryTheory/Monad/Adjunction.lean

Modified Mathlib/CategoryTheory/Monad/Coequalizer.lean

Modified Mathlib/CategoryTheory/Monad/Limits.lean

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

Modified Mathlib/Computability/Reduce.lean

Modified Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean

Modified Mathlib/MeasureTheory/OuterMeasure/AE.lean

Modified Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean

Modified Mathlib/Order/Filter/Prod.lean

Modified Mathlib/Order/Filter/Ultrafilter/Basic.lean

Modified Mathlib/Order/Int/ConditionallyCompleteOrder.lean

Modified Mathlib/SetTheory/Cardinal/HasCardinalLT.lean

Modified Mathlib/Topology/CompactOpen.lean

Modified Mathlib/Topology/Constructions.lean

Modified Mathlib/Topology/Homeomorph/Lemmas.lean

Modified Mathlib/Topology/OmegaCompletePartialOrder.lean