Commit 2025-07-01 20:53 d31f1948

View on Github →

feat: initial use of @[grind] in Logic/Equiv (#26569) This PR begins using grind in Logic/Equiv.

Estimated changes

Modified Mathlib/Data/Prod/PProd.lean

Modified Mathlib/Logic/Equiv/Defs.lean

modified theorem Equiv.apply_symm_apply

modified theorem Equiv.coe_fn_mk

modified theorem Equiv.symm_apply_apply

Modified Mathlib/Logic/Equiv/Prod.lean

modified def Equiv.boolArrowEquivProd

Modified Mathlib/Logic/Function/Defs.lean

Modified scripts/noshake.json