Commit 2025-12-05 11:03 2c4760b7

View on Github →

chore: golf using grind (#32333)

Estimated changes

Modified Mathlib/Data/Set/Image.lean

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

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

modified theorem Nat.Ico_succ_singleton

modified theorem Nat.Ioc_succ_singleton