Commit 2025-12-31 08:52 503f425a

View on Github →

chore: golf using grind. add grind annotations. (#33332)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

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

modified theorem SimpleGraph.Walk.nil_nil

Modified Mathlib/Data/Finset/Max.lean

Modified Mathlib/Order/Interval/Set/UnorderedInterval.lean

modified theorem Set.uIoc_of_ge

modified theorem Set.uIoc_of_le