Commit 2025-11-18 12:49 f9532ff3

View on Github →

feat: grind golfing in Topology/Path (#31305) This is not as exhaustive as I would have liked; there's plenty more cleanup to do here. But I need to pause on this for now and I think it's an improvement.

Estimated changes

Modified Mathlib/Algebra/Order/Interval/Set/Instances.lean

Modified Mathlib/AlgebraicTopology/FundamentalGroupoid/Basic.lean

modified theorem Path.Homotopy.continuous_reflTransSymmAux

modified theorem Path.Homotopy.continuous_transAssocReparamAux

modified theorem Path.Homotopy.continuous_transReflReparamAux

Modified Mathlib/Topology/Homotopy/Path.lean

Modified Mathlib/Topology/Path.lean

added theorem Path.extend_apply

deleted theorem Path.extend_extends

modified theorem Path.symm_symm

Modified Mathlib/Topology/UnitInterval.lean