Commit 2026-03-13 11:18 21011521

View on Github →

feat(CategoryTheory/Limits): IsPullback.mono_fst_of_mono and similar (#35871) This lemma is more convenient than going through MorphismProperty.IsStableUnderBasechange. We use (inst : Mono f := by infer_instance) instead of [Mono f] because on occasion, these proof arguments are not by inferInstance, and this design lets us more easily use the lemma in such cases.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean

modified theorem CategoryTheory.IsPullback.isIso_fst_of_isIso

modified theorem CategoryTheory.IsPullback.isIso_fst_of_mono

modified theorem CategoryTheory.IsPullback.isIso_snd_iso_of_mono

modified theorem CategoryTheory.IsPullback.isIso_snd_of_isIso

added theorem CategoryTheory.IsPullback.mono_fst_of_mono

added theorem CategoryTheory.IsPullback.mono_snd_of_mono

added theorem CategoryTheory.IsPushout.epi_inl_of_epi

added theorem CategoryTheory.IsPushout.epi_inr_of_epi

modified theorem CategoryTheory.IsPushout.isIso_inl_iso_of_epi

modified theorem CategoryTheory.IsPushout.isIso_inl_of_isIso

modified theorem CategoryTheory.IsPushout.isIso_inr_iso_of_epi

modified theorem CategoryTheory.IsPushout.isIso_inr_of_isIso

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean