Commit 2024-05-25 13:23 857573d7

View on Github →

style: remove last isolated where (#13202) Discovered when tweaking the rewritten style linter in #13199.

Estimated changes

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

modified def CategoryTheory.Limits.WalkingPair.equivBool

modified def CategoryTheory.Limits.WalkingPair.swap

modified def CategoryTheory.Limits.prod.braiding

Modified Mathlib/Tactic/CC/Addition.lean

Modified Mathlib/Topology/Homotopy/Product.lean

Modified test/FBinop.lean