Commit 2025-05-22 00:47 b9e54805

View on Github →

chore: fix some defeq abuse in theorem statements around the Id monad (#25098) Follows on from https://github.com/leanprover/lean4/pull/7352. This also deprecates:

id.mk, which looks like a porting error
Free(Add)(Magma|Semigroup).mul_map_seq, which is a garbage lemma that both is not meaningfully about the free objects and has defeq abuse everywhere.

Estimated changes

Modified Mathlib/Algebra/Free.lean

deleted theorem FreeMagma.map_pure

deleted theorem FreeSemigroup.map_pure

Modified Mathlib/Control/Bitraversable/Basic.lean

Modified Mathlib/Control/Bitraversable/Instances.lean

Modified Mathlib/Control/Functor.lean

Modified Mathlib/Control/Traversable/Basic.lean

Modified Mathlib/Control/Traversable/Equiv.lean

Modified Mathlib/Control/Traversable/Instances.lean

modified theorem Option.id_traverse

Modified Mathlib/Control/Traversable/Lemmas.lean

modified theorem Traversable.map_eq_traverse_id

Modified Mathlib/Data/Finset/Functor.lean

modified theorem Finset.id_traverse

Modified Mathlib/Data/Multiset/Functor.lean

modified theorem Multiset.id_traverse

Modified Mathlib/Data/Tree/Traversable.lean

Modified Mathlib/Data/Vector/Basic.lean

Modified Mathlib/Lean/Expr/ReplaceRec.lean