Commit 2023-11-17 00:15 a2ca43e5

View on Github →

refactor(CategoryTheory): simplify the proof of the characterisation of regular sheaves using the new arrows API (#8443)

Estimated changes

Modified Mathlib/CategoryTheory/Sites/RegularExtensive.lean

deleted def CategoryTheory.EqualizerFirstObjIso

deleted def CategoryTheory.EqualizerSecondObjIso

deleted theorem CategoryTheory.IsSheafForRegular.equalizerCondition

added theorem CategoryTheory.equalizerCondition_of_regular