Commit 2025-03-11 22:28 a5860dae

View on Github →

chore: review of erw in CategoryTheory/ (#22815) This is just epsilon progress towards reviewing use of erw in CategoryTheory/. It barely scrapes the surface.

Estimated changes

Modified Mathlib/CategoryTheory/Adhesive.lean

Modified Mathlib/CategoryTheory/CatCommSq.lean

Modified Mathlib/CategoryTheory/ChosenFiniteProducts.lean

Modified Mathlib/CategoryTheory/ComposableArrows.lean

Modified Mathlib/CategoryTheory/ConnectedComponents.lean

Modified Mathlib/CategoryTheory/Core.lean

Modified Mathlib/CategoryTheory/DifferentialObject.lean

Modified Mathlib/CategoryTheory/EqToHom.lean

Modified Mathlib/CategoryTheory/Equivalence.lean

Modified Mathlib/CategoryTheory/FiberedCategory/BasedCategory.lean

Modified Mathlib/CategoryTheory/Iso.lean

Modified Mathlib/CategoryTheory/NatIso.lean

Modified Mathlib/CategoryTheory/Shift/Basic.lean

Modified Mathlib/CategoryTheory/Subobject/MonoOver.lean