Commit 2025-11-05 11:15 7ddbcf0b

View on Github →

chore: golf some simp based proofs (#31266)

Estimated changes

Modified Mathlib/Algebra/FreeAbelianGroup/Finsupp.lean

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean

Modified Mathlib/Data/Stream/Init.lean

Modified Mathlib/Probability/Kernel/Composition/MapComap.lean

modified theorem ProbabilityTheory.Kernel.comap_id

Modified Mathlib/Topology/Category/TopCat/Opens.lean