Commit 2026-01-13 15:36 ae275c9c

View on Github →

chore: golf using grind, reduce compilation time and imports (#33912)

Estimated changes

Modified Mathlib/Data/Finset/Defs.lean

modified theorem Finset.forall_mem_not_eq'

modified theorem Finset.forall_mem_not_eq

Modified Mathlib/Data/List/Triplewise.lean

Modified Mathlib/Data/Prod/Basic.lean

modified theorem Prod.swap_eq_iff_eq_swap

Modified Mathlib/Logic/Equiv/PartialEquiv.lean