Commit 2024-07-03 01:14 475fdf42

View on Github →

chore(CategoryTheory/Limits/Shapes/Pullbacks): split into multiple files and add documentation (#14344) In this PR we split the file CategoryTheory/Limits/Shapes/Pullbacks.lean into 7 (!) smaller files and add documentation. This contribution was inspired by the AIM workshop "Formalizing algebraic geometry" in June 2024.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/Ring/Constructions.lean

Modified Mathlib/AlgebraicGeometry/OpenImmersion.lean

Modified Mathlib/CategoryTheory/Adjunction/Over.lean

Modified Mathlib/CategoryTheory/EffectiveEpi/Coproduct.lean

Modified Mathlib/CategoryTheory/Extensive.lean

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

Modified Mathlib/CategoryTheory/Limits/Constructions/EpiMono.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/Pullbacks.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean

Modified Mathlib/CategoryTheory/Limits/EpiMono.lean

Modified Mathlib/CategoryTheory/Limits/Lattice.lean

Modified Mathlib/CategoryTheory/Limits/Over.lean

Modified Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean

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

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

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

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

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

Created Mathlib/CategoryTheory/Limits/Shapes/Pullback/Assoc.lean

added theorem CategoryTheory.Limits.hasPullback_assoc

added theorem CategoryTheory.Limits.hasPullback_assoc_symm

added theorem CategoryTheory.Limits.hasPushout_assoc

added theorem CategoryTheory.Limits.hasPushout_assoc_symm

added theorem CategoryTheory.Limits.inl_inl_pushoutAssoc_hom

added theorem CategoryTheory.Limits.inl_inr_pushoutAssoc_inv

added theorem CategoryTheory.Limits.inl_pushoutAssoc_inv

added theorem CategoryTheory.Limits.inr_inl_pushoutAssoc_hom

added theorem CategoryTheory.Limits.inr_inr_pushoutAssoc_inv

added theorem CategoryTheory.Limits.inr_pushoutAssoc_hom

added def CategoryTheory.Limits.pullbackAssocIsPullback

added def CategoryTheory.Limits.pullbackAssocSymmIsPullback

added theorem CategoryTheory.Limits.pullbackAssoc_hom_fst

added theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_fst

added theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_snd

added theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_fst

added theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_snd

added theorem CategoryTheory.Limits.pullbackAssoc_inv_snd

added def CategoryTheory.Limits.pullbackPullbackLeftIsPullback

added def CategoryTheory.Limits.pullbackPullbackRightIsPullback

added def CategoryTheory.Limits.pushoutAssocIsPushout

added def CategoryTheory.Limits.pushoutAssocSymmIsPushout

added def CategoryTheory.Limits.pushoutPushoutLeftIsPushout

added def CategoryTheory.Limits.pushoutPushoutRightIsPushout

Renamed Mathlib/CategoryTheory/Limits/Shapes/CommSq.lean to Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean

Created Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean

added def CategoryTheory.Limits.WalkingCospan.ext

added def CategoryTheory.Limits.WalkingSpan.ext

added def CategoryTheory.Limits.cospan

added def CategoryTheory.Limits.cospanCompIso

added theorem CategoryTheory.Limits.cospanCompIso_app_left

added theorem CategoryTheory.Limits.cospanCompIso_app_one

added theorem CategoryTheory.Limits.cospanCompIso_app_right

added theorem CategoryTheory.Limits.cospanCompIso_hom_app_left

added theorem CategoryTheory.Limits.cospanCompIso_hom_app_one

added theorem CategoryTheory.Limits.cospanCompIso_hom_app_right

added theorem CategoryTheory.Limits.cospanCompIso_inv_app_left

added theorem CategoryTheory.Limits.cospanCompIso_inv_app_one

added theorem CategoryTheory.Limits.cospanCompIso_inv_app_right

added def CategoryTheory.Limits.cospanExt

added theorem CategoryTheory.Limits.cospanExt_app_left

added theorem CategoryTheory.Limits.cospanExt_app_one

added theorem CategoryTheory.Limits.cospanExt_app_right

added theorem CategoryTheory.Limits.cospanExt_hom_app_left

added theorem CategoryTheory.Limits.cospanExt_hom_app_one

added theorem CategoryTheory.Limits.cospanExt_hom_app_right

added theorem CategoryTheory.Limits.cospanExt_inv_app_left

added theorem CategoryTheory.Limits.cospanExt_inv_app_one

added theorem CategoryTheory.Limits.cospanExt_inv_app_right

added theorem CategoryTheory.Limits.cospan_left

added theorem CategoryTheory.Limits.cospan_map_id

added theorem CategoryTheory.Limits.cospan_map_inl

added theorem CategoryTheory.Limits.cospan_map_inr

added theorem CategoryTheory.Limits.cospan_one

added theorem CategoryTheory.Limits.cospan_right

added def CategoryTheory.Limits.diagramIsoCospan

added def CategoryTheory.Limits.diagramIsoSpan

added def CategoryTheory.Limits.span

added def CategoryTheory.Limits.spanCompIso

added theorem CategoryTheory.Limits.spanCompIso_app_left

added theorem CategoryTheory.Limits.spanCompIso_app_right

added theorem CategoryTheory.Limits.spanCompIso_app_zero

added theorem CategoryTheory.Limits.spanCompIso_hom_app_left

added theorem CategoryTheory.Limits.spanCompIso_hom_app_right

added theorem CategoryTheory.Limits.spanCompIso_hom_app_zero

added theorem CategoryTheory.Limits.spanCompIso_inv_app_left

added theorem CategoryTheory.Limits.spanCompIso_inv_app_right

added theorem CategoryTheory.Limits.spanCompIso_inv_app_zero

added def CategoryTheory.Limits.spanExt

added theorem CategoryTheory.Limits.spanExt_app_left

added theorem CategoryTheory.Limits.spanExt_app_one

added theorem CategoryTheory.Limits.spanExt_app_right

added theorem CategoryTheory.Limits.spanExt_hom_app_left

added theorem CategoryTheory.Limits.spanExt_hom_app_right

added theorem CategoryTheory.Limits.spanExt_hom_app_zero

added theorem CategoryTheory.Limits.spanExt_inv_app_left

added theorem CategoryTheory.Limits.spanExt_inv_app_right

added theorem CategoryTheory.Limits.spanExt_inv_app_zero

added theorem CategoryTheory.Limits.span_left

added theorem CategoryTheory.Limits.span_map_fst

added theorem CategoryTheory.Limits.span_map_id

added theorem CategoryTheory.Limits.span_map_snd

added theorem CategoryTheory.Limits.span_right

added theorem CategoryTheory.Limits.span_zero

Created Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean

added theorem CategoryTheory.Limits.PullbackCone.fst_limit_cone

added theorem CategoryTheory.Limits.PullbackCone.snd_limit_cone

added theorem CategoryTheory.Limits.PushoutCocone.inl_colimit_cocone

added theorem CategoryTheory.Limits.PushoutCocone.inr_colimit_cocone

added theorem CategoryTheory.Limits.hasPullback_symmetry

added theorem CategoryTheory.Limits.hasPullbacks_of_hasLimit_cospan

added theorem CategoryTheory.Limits.hasPushout_symmetry

added theorem CategoryTheory.Limits.hasPushouts_of_hasColimit_span

added theorem CategoryTheory.Limits.inl_comp_pushoutComparison

added theorem CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom

added theorem CategoryTheory.Limits.inl_comp_pushoutSymmetry_inv

added theorem CategoryTheory.Limits.inr_comp_pushoutComparison

added theorem CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom

added theorem CategoryTheory.Limits.inr_comp_pushoutSymmetry_inv

added theorem CategoryTheory.Limits.map_lift_pullbackComparison

added theorem CategoryTheory.Limits.pullback.condition

added def CategoryTheory.Limits.pullback.congrHom

added theorem CategoryTheory.Limits.pullback.congrHom_inv

added def CategoryTheory.Limits.pullback.desc'

added theorem CategoryTheory.Limits.pullback.hom_ext

added def CategoryTheory.Limits.pullback.lift'

added theorem CategoryTheory.Limits.pullback.lift_fst

added theorem CategoryTheory.Limits.pullback.lift_snd

added theorem CategoryTheory.Limits.pullback.mapDesc_comp

added def CategoryTheory.Limits.pullbackComparison

added theorem CategoryTheory.Limits.pullbackComparison_comp_fst

added theorem CategoryTheory.Limits.pullbackComparison_comp_snd

added def CategoryTheory.Limits.pullbackIsPullback

added def CategoryTheory.Limits.pullbackSymmetry

added theorem CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst

added theorem CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd

added theorem CategoryTheory.Limits.pullbackSymmetry_inv_comp_fst

added theorem CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd

added theorem CategoryTheory.Limits.pushout.condition

added def CategoryTheory.Limits.pushout.congrHom

added theorem CategoryTheory.Limits.pushout.congrHom_inv

added theorem CategoryTheory.Limits.pushout.hom_ext

added theorem CategoryTheory.Limits.pushout.inl_desc

added theorem CategoryTheory.Limits.pushout.inr_desc

added theorem CategoryTheory.Limits.pushout.mapLift_comp

added def CategoryTheory.Limits.pushoutComparison

added theorem CategoryTheory.Limits.pushoutComparison_map_desc

added def CategoryTheory.Limits.pushoutIsPushout

added def CategoryTheory.Limits.pushoutSymmetry

added def CategoryTheory.Limits.walkingCospanOpEquiv

added def CategoryTheory.Limits.walkingSpanOpEquiv

Created Mathlib/CategoryTheory/Limits/Shapes/Pullback/Iso.lean

added theorem CategoryTheory.Limits.hasPullback_of_left_iso

added theorem CategoryTheory.Limits.hasPullback_of_right_iso

added theorem CategoryTheory.Limits.hasPushout_of_left_iso

added theorem CategoryTheory.Limits.hasPushout_of_right_iso

added def CategoryTheory.Limits.pullbackConeOfLeftIso

added def CategoryTheory.Limits.pullbackConeOfLeftIsoIsLimit

added theorem CategoryTheory.Limits.pullbackConeOfLeftIso_fst

added theorem CategoryTheory.Limits.pullbackConeOfLeftIso_snd

added theorem CategoryTheory.Limits.pullbackConeOfLeftIso_x

added theorem CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_left

added theorem CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_none

added theorem CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_right

added def CategoryTheory.Limits.pullbackConeOfRightIso

added def CategoryTheory.Limits.pullbackConeOfRightIsoIsLimit

added theorem CategoryTheory.Limits.pullbackConeOfRightIso_fst

added theorem CategoryTheory.Limits.pullbackConeOfRightIso_snd

added theorem CategoryTheory.Limits.pullbackConeOfRightIso_x

added theorem CategoryTheory.Limits.pullbackConeOfRightIso_π_app_left

added theorem CategoryTheory.Limits.pullbackConeOfRightIso_π_app_none

added theorem CategoryTheory.Limits.pullbackConeOfRightIso_π_app_right

added def CategoryTheory.Limits.pushoutCoconeOfLeftIso

added def CategoryTheory.Limits.pushoutCoconeOfLeftIsoIsLimit

added theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_inl

added theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_inr

added theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_x

added theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_left

added theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_none

added theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_right

added def CategoryTheory.Limits.pushoutCoconeOfRightIso

added def CategoryTheory.Limits.pushoutCoconeOfRightIsoIsLimit

added theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_inl

added theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_inr

added theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_x

added theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_left

added theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_none

added theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_right

Created Mathlib/CategoryTheory/Limits/Shapes/Pullback/Mono.lean

added def CategoryTheory.Limits.PullbackCone.isLimitMkIdId

added def CategoryTheory.Limits.PullbackCone.isLimitOfCompMono

added def CategoryTheory.Limits.PullbackCone.isLimitOfFactors

added theorem CategoryTheory.Limits.PullbackCone.mono_fst_of_is_pullback_of_mono

added theorem CategoryTheory.Limits.PullbackCone.mono_of_isLimitMkIdId

added theorem CategoryTheory.Limits.PullbackCone.mono_snd_of_is_pullback_of_mono

added theorem CategoryTheory.Limits.PushoutCocone.epi_inl_of_is_pushout_of_epi

added theorem CategoryTheory.Limits.PushoutCocone.epi_inr_of_is_pushout_of_epi

added theorem CategoryTheory.Limits.PushoutCocone.epi_of_isColimitMkIdId

added def CategoryTheory.Limits.PushoutCocone.isColimitMkIdId

added def CategoryTheory.Limits.PushoutCocone.isColimitOfEpiComp

added def CategoryTheory.Limits.PushoutCocone.isColimitOfFactors

added theorem CategoryTheory.Limits.fst_eq_snd_of_mono_eq

added theorem CategoryTheory.Limits.inl_eq_inr_of_epi_eq

added theorem CategoryTheory.Limits.pullbackSymmetry_hom_of_mono_eq

added theorem CategoryTheory.Limits.pullback_symmetry_hom_of_epi_eq

Created Mathlib/CategoryTheory/Limits/Shapes/Pullback/Pasting.lean

added def CategoryTheory.Limits.bigSquareIsPullback

added def CategoryTheory.Limits.bigSquareIsPushout

added theorem CategoryTheory.Limits.inl_inl_pushoutLeftPushoutInrIso_hom

added theorem CategoryTheory.Limits.inl_pushoutLeftPushoutInrIso_inv

added theorem CategoryTheory.Limits.inr_inl_pushoutLeftPushoutInrIso_hom

added theorem CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_hom

added theorem CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_inv

added def CategoryTheory.Limits.leftSquareIsPullback

added theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst

added theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd

added theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst

added theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst

added theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd

added def CategoryTheory.Limits.rightSquareIsPushout

Created Mathlib/CategoryTheory/Limits/Shapes/Pullback/PullbackCone.lean

added def CategoryTheory.Limits.Cocone.ofPushoutCocone

added def CategoryTheory.Limits.Cone.ofPullbackCone

added theorem CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext

added def CategoryTheory.Limits.PullbackCone.IsLimit.lift'

added def CategoryTheory.Limits.PullbackCone.IsLimit.lift

added theorem CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst

added theorem CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd

added def CategoryTheory.Limits.PullbackCone.IsLimit.mk

added theorem CategoryTheory.Limits.PullbackCone.condition

added theorem CategoryTheory.Limits.PullbackCone.condition_one

added theorem CategoryTheory.Limits.PullbackCone.equalizer_ext

added def CategoryTheory.Limits.PullbackCone.ext

added def CategoryTheory.Limits.PullbackCone.flip

added def CategoryTheory.Limits.PullbackCone.flipFlipIso

added def CategoryTheory.Limits.PullbackCone.flipIsLimit

added theorem CategoryTheory.Limits.PullbackCone.flip_fst

added theorem CategoryTheory.Limits.PullbackCone.flip_pt

added theorem CategoryTheory.Limits.PullbackCone.flip_snd

added def CategoryTheory.Limits.PullbackCone.isLimitAux'

added def CategoryTheory.Limits.PullbackCone.isLimitAux

added def CategoryTheory.Limits.PullbackCone.isLimitOfFlip

added def CategoryTheory.Limits.PullbackCone.isoMk

added def CategoryTheory.Limits.PullbackCone.mk

added theorem CategoryTheory.Limits.PullbackCone.mk_fst

added theorem CategoryTheory.Limits.PullbackCone.mk_snd

added theorem CategoryTheory.Limits.PullbackCone.mk_π_app_left

added theorem CategoryTheory.Limits.PullbackCone.mk_π_app_one

added theorem CategoryTheory.Limits.PullbackCone.mk_π_app_right

added def CategoryTheory.Limits.PullbackCone.ofCone

added theorem CategoryTheory.Limits.PullbackCone.π_app_left

added theorem CategoryTheory.Limits.PullbackCone.π_app_right

added def CategoryTheory.Limits.PushoutCocone.IsColimit.desc'

added def CategoryTheory.Limits.PushoutCocone.IsColimit.desc

added theorem CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext

added theorem CategoryTheory.Limits.PushoutCocone.IsColimit.inl_desc

added theorem CategoryTheory.Limits.PushoutCocone.IsColimit.inr_desc

added def CategoryTheory.Limits.PushoutCocone.IsColimit.mk

added theorem CategoryTheory.Limits.PushoutCocone.coequalizer_ext

added theorem CategoryTheory.Limits.PushoutCocone.condition

added theorem CategoryTheory.Limits.PushoutCocone.condition_zero

added def CategoryTheory.Limits.PushoutCocone.ext

added def CategoryTheory.Limits.PushoutCocone.flip

added def CategoryTheory.Limits.PushoutCocone.flipFlipIso

added def CategoryTheory.Limits.PushoutCocone.flipIsColimit

added theorem CategoryTheory.Limits.PushoutCocone.flip_inl

added theorem CategoryTheory.Limits.PushoutCocone.flip_inr

added theorem CategoryTheory.Limits.PushoutCocone.flip_pt

added def CategoryTheory.Limits.PushoutCocone.isColimitAux'

added def CategoryTheory.Limits.PushoutCocone.isColimitAux

added def CategoryTheory.Limits.PushoutCocone.isColimitOfFlip

added def CategoryTheory.Limits.PushoutCocone.isoMk

added def CategoryTheory.Limits.PushoutCocone.mk

added theorem CategoryTheory.Limits.PushoutCocone.mk_inl

added theorem CategoryTheory.Limits.PushoutCocone.mk_inr

added theorem CategoryTheory.Limits.PushoutCocone.mk_ι_app_left

added theorem CategoryTheory.Limits.PushoutCocone.mk_ι_app_right

added theorem CategoryTheory.Limits.PushoutCocone.mk_ι_app_zero

added def CategoryTheory.Limits.PushoutCocone.ofCocone

added theorem CategoryTheory.Limits.PushoutCocone.ι_app_left

added theorem CategoryTheory.Limits.PushoutCocone.ι_app_right

Deleted Mathlib/CategoryTheory/Limits/Shapes/Pullbacks.lean

deleted def CategoryTheory.Limits.Cocone.ofPushoutCocone

deleted def CategoryTheory.Limits.Cone.ofPullbackCone

deleted theorem CategoryTheory.Limits.PullbackCone.IsLimit.hom_ext

deleted def CategoryTheory.Limits.PullbackCone.IsLimit.lift'

deleted def CategoryTheory.Limits.PullbackCone.IsLimit.lift

deleted theorem CategoryTheory.Limits.PullbackCone.IsLimit.lift_fst

deleted theorem CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd

deleted def CategoryTheory.Limits.PullbackCone.IsLimit.mk

deleted theorem CategoryTheory.Limits.PullbackCone.condition

deleted theorem CategoryTheory.Limits.PullbackCone.condition_one

deleted theorem CategoryTheory.Limits.PullbackCone.equalizer_ext

deleted def CategoryTheory.Limits.PullbackCone.ext

deleted def CategoryTheory.Limits.PullbackCone.flip

deleted def CategoryTheory.Limits.PullbackCone.flipFlipIso

deleted def CategoryTheory.Limits.PullbackCone.flipIsLimit

deleted theorem CategoryTheory.Limits.PullbackCone.flip_fst

deleted theorem CategoryTheory.Limits.PullbackCone.flip_pt

deleted theorem CategoryTheory.Limits.PullbackCone.flip_snd

deleted theorem CategoryTheory.Limits.PullbackCone.fst_colimit_cocone

deleted def CategoryTheory.Limits.PullbackCone.isLimitAux'

deleted def CategoryTheory.Limits.PullbackCone.isLimitAux

deleted def CategoryTheory.Limits.PullbackCone.isLimitMkIdId

deleted def CategoryTheory.Limits.PullbackCone.isLimitOfCompMono

deleted def CategoryTheory.Limits.PullbackCone.isLimitOfFactors

deleted def CategoryTheory.Limits.PullbackCone.isLimitOfFlip

deleted def CategoryTheory.Limits.PullbackCone.isoMk

deleted def CategoryTheory.Limits.PullbackCone.mk

deleted theorem CategoryTheory.Limits.PullbackCone.mk_fst

deleted theorem CategoryTheory.Limits.PullbackCone.mk_snd

deleted theorem CategoryTheory.Limits.PullbackCone.mk_π_app_left

deleted theorem CategoryTheory.Limits.PullbackCone.mk_π_app_one

deleted theorem CategoryTheory.Limits.PullbackCone.mk_π_app_right

deleted theorem CategoryTheory.Limits.PullbackCone.mono_fst_of_is_pullback_of_mono

deleted theorem CategoryTheory.Limits.PullbackCone.mono_of_isLimitMkIdId

deleted theorem CategoryTheory.Limits.PullbackCone.mono_snd_of_is_pullback_of_mono

deleted def CategoryTheory.Limits.PullbackCone.ofCone

deleted theorem CategoryTheory.Limits.PullbackCone.snd_colimit_cocone

deleted theorem CategoryTheory.Limits.PullbackCone.π_app_left

deleted theorem CategoryTheory.Limits.PullbackCone.π_app_right

deleted def CategoryTheory.Limits.PushoutCocone.IsColimit.desc'

deleted def CategoryTheory.Limits.PushoutCocone.IsColimit.desc

deleted theorem CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext

deleted theorem CategoryTheory.Limits.PushoutCocone.IsColimit.inl_desc

deleted theorem CategoryTheory.Limits.PushoutCocone.IsColimit.inr_desc

deleted def CategoryTheory.Limits.PushoutCocone.IsColimit.mk

deleted theorem CategoryTheory.Limits.PushoutCocone.coequalizer_ext

deleted theorem CategoryTheory.Limits.PushoutCocone.condition

deleted theorem CategoryTheory.Limits.PushoutCocone.condition_zero

deleted theorem CategoryTheory.Limits.PushoutCocone.epi_inl_of_is_pushout_of_epi

deleted theorem CategoryTheory.Limits.PushoutCocone.epi_inr_of_is_pushout_of_epi

deleted theorem CategoryTheory.Limits.PushoutCocone.epi_of_isColimitMkIdId

deleted def CategoryTheory.Limits.PushoutCocone.ext

deleted def CategoryTheory.Limits.PushoutCocone.flip

deleted def CategoryTheory.Limits.PushoutCocone.flipFlipIso

deleted def CategoryTheory.Limits.PushoutCocone.flipIsColimit

deleted theorem CategoryTheory.Limits.PushoutCocone.flip_inl

deleted theorem CategoryTheory.Limits.PushoutCocone.flip_inr

deleted theorem CategoryTheory.Limits.PushoutCocone.flip_pt

deleted theorem CategoryTheory.Limits.PushoutCocone.inl_colimit_cocone

deleted theorem CategoryTheory.Limits.PushoutCocone.inr_colimit_cocone

deleted def CategoryTheory.Limits.PushoutCocone.isColimitAux'

deleted def CategoryTheory.Limits.PushoutCocone.isColimitAux

deleted def CategoryTheory.Limits.PushoutCocone.isColimitMkIdId

deleted def CategoryTheory.Limits.PushoutCocone.isColimitOfEpiComp

deleted def CategoryTheory.Limits.PushoutCocone.isColimitOfFactors

deleted def CategoryTheory.Limits.PushoutCocone.isColimitOfFlip

deleted def CategoryTheory.Limits.PushoutCocone.isoMk

deleted def CategoryTheory.Limits.PushoutCocone.mk

deleted theorem CategoryTheory.Limits.PushoutCocone.mk_inl

deleted theorem CategoryTheory.Limits.PushoutCocone.mk_inr

deleted theorem CategoryTheory.Limits.PushoutCocone.mk_ι_app_left

deleted theorem CategoryTheory.Limits.PushoutCocone.mk_ι_app_right

deleted theorem CategoryTheory.Limits.PushoutCocone.mk_ι_app_zero

deleted def CategoryTheory.Limits.PushoutCocone.ofCocone

deleted theorem CategoryTheory.Limits.PushoutCocone.ι_app_left

deleted theorem CategoryTheory.Limits.PushoutCocone.ι_app_right

deleted def CategoryTheory.Limits.WalkingCospan.ext

deleted def CategoryTheory.Limits.WalkingSpan.ext

deleted def CategoryTheory.Limits.bigSquareIsPullback

deleted def CategoryTheory.Limits.bigSquareIsPushout

deleted def CategoryTheory.Limits.cospan

deleted def CategoryTheory.Limits.cospanCompIso

deleted theorem CategoryTheory.Limits.cospanCompIso_app_left

deleted theorem CategoryTheory.Limits.cospanCompIso_app_one

deleted theorem CategoryTheory.Limits.cospanCompIso_app_right

deleted theorem CategoryTheory.Limits.cospanCompIso_hom_app_left

deleted theorem CategoryTheory.Limits.cospanCompIso_hom_app_one

deleted theorem CategoryTheory.Limits.cospanCompIso_hom_app_right

deleted theorem CategoryTheory.Limits.cospanCompIso_inv_app_left

deleted theorem CategoryTheory.Limits.cospanCompIso_inv_app_one

deleted theorem CategoryTheory.Limits.cospanCompIso_inv_app_right

deleted def CategoryTheory.Limits.cospanExt

deleted theorem CategoryTheory.Limits.cospanExt_app_left

deleted theorem CategoryTheory.Limits.cospanExt_app_one

deleted theorem CategoryTheory.Limits.cospanExt_app_right

deleted theorem CategoryTheory.Limits.cospanExt_hom_app_left

deleted theorem CategoryTheory.Limits.cospanExt_hom_app_one

deleted theorem CategoryTheory.Limits.cospanExt_hom_app_right

deleted theorem CategoryTheory.Limits.cospanExt_inv_app_left

deleted theorem CategoryTheory.Limits.cospanExt_inv_app_one

deleted theorem CategoryTheory.Limits.cospanExt_inv_app_right

deleted theorem CategoryTheory.Limits.cospan_left

deleted theorem CategoryTheory.Limits.cospan_map_id

deleted theorem CategoryTheory.Limits.cospan_map_inl

deleted theorem CategoryTheory.Limits.cospan_map_inr

deleted theorem CategoryTheory.Limits.cospan_one

deleted theorem CategoryTheory.Limits.cospan_right

deleted def CategoryTheory.Limits.diagramIsoCospan

deleted def CategoryTheory.Limits.diagramIsoSpan

deleted theorem CategoryTheory.Limits.fst_eq_snd_of_mono_eq

deleted theorem CategoryTheory.Limits.hasPullback_assoc

deleted theorem CategoryTheory.Limits.hasPullback_assoc_symm

deleted theorem CategoryTheory.Limits.hasPullback_of_left_iso

deleted theorem CategoryTheory.Limits.hasPullback_of_right_iso

deleted theorem CategoryTheory.Limits.hasPullback_symmetry

deleted theorem CategoryTheory.Limits.hasPullbacks_of_hasLimit_cospan

deleted theorem CategoryTheory.Limits.hasPushout_assoc

deleted theorem CategoryTheory.Limits.hasPushout_assoc_symm

deleted theorem CategoryTheory.Limits.hasPushout_of_left_iso

deleted theorem CategoryTheory.Limits.hasPushout_of_right_iso

deleted theorem CategoryTheory.Limits.hasPushout_symmetry

deleted theorem CategoryTheory.Limits.hasPushouts_of_hasColimit_span

deleted theorem CategoryTheory.Limits.inl_comp_pushoutComparison

deleted theorem CategoryTheory.Limits.inl_comp_pushoutSymmetry_hom

deleted theorem CategoryTheory.Limits.inl_comp_pushoutSymmetry_inv

deleted theorem CategoryTheory.Limits.inl_eq_inr_of_epi_eq

deleted theorem CategoryTheory.Limits.inl_inl_pushoutAssoc_hom

deleted theorem CategoryTheory.Limits.inl_inl_pushoutLeftPushoutInrIso_hom

deleted theorem CategoryTheory.Limits.inl_inr_pushoutAssoc_inv

deleted theorem CategoryTheory.Limits.inl_pushoutAssoc_inv

deleted theorem CategoryTheory.Limits.inl_pushoutLeftPushoutInrIso_inv

deleted theorem CategoryTheory.Limits.inr_comp_pushoutComparison

deleted theorem CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom

deleted theorem CategoryTheory.Limits.inr_comp_pushoutSymmetry_inv

deleted theorem CategoryTheory.Limits.inr_inl_pushoutAssoc_hom

deleted theorem CategoryTheory.Limits.inr_inl_pushoutLeftPushoutInrIso_hom

deleted theorem CategoryTheory.Limits.inr_inr_pushoutAssoc_inv

deleted theorem CategoryTheory.Limits.inr_pushoutAssoc_hom

deleted theorem CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_hom

deleted theorem CategoryTheory.Limits.inr_pushoutLeftPushoutInrIso_inv

deleted def CategoryTheory.Limits.leftSquareIsPullback

deleted theorem CategoryTheory.Limits.map_lift_pullbackComparison

deleted theorem CategoryTheory.Limits.pullback.condition

deleted def CategoryTheory.Limits.pullback.congrHom

deleted theorem CategoryTheory.Limits.pullback.congrHom_inv

deleted def CategoryTheory.Limits.pullback.desc'

deleted theorem CategoryTheory.Limits.pullback.hom_ext

deleted def CategoryTheory.Limits.pullback.lift'

deleted theorem CategoryTheory.Limits.pullback.lift_fst

deleted theorem CategoryTheory.Limits.pullback.lift_snd

deleted theorem CategoryTheory.Limits.pullback.mapDesc_comp

deleted def CategoryTheory.Limits.pullbackAssocIsPullback

deleted def CategoryTheory.Limits.pullbackAssocSymmIsPullback

deleted theorem CategoryTheory.Limits.pullbackAssoc_hom_fst

deleted theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_fst

deleted theorem CategoryTheory.Limits.pullbackAssoc_hom_snd_snd

deleted theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_fst

deleted theorem CategoryTheory.Limits.pullbackAssoc_inv_fst_snd

deleted theorem CategoryTheory.Limits.pullbackAssoc_inv_snd

deleted def CategoryTheory.Limits.pullbackComparison

deleted theorem CategoryTheory.Limits.pullbackComparison_comp_fst

deleted theorem CategoryTheory.Limits.pullbackComparison_comp_snd

deleted def CategoryTheory.Limits.pullbackConeOfLeftIso

deleted def CategoryTheory.Limits.pullbackConeOfLeftIsoIsLimit

deleted theorem CategoryTheory.Limits.pullbackConeOfLeftIso_fst

deleted theorem CategoryTheory.Limits.pullbackConeOfLeftIso_snd

deleted theorem CategoryTheory.Limits.pullbackConeOfLeftIso_x

deleted theorem CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_left

deleted theorem CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_none

deleted theorem CategoryTheory.Limits.pullbackConeOfLeftIso_π_app_right

deleted def CategoryTheory.Limits.pullbackConeOfRightIso

deleted def CategoryTheory.Limits.pullbackConeOfRightIsoIsLimit

deleted theorem CategoryTheory.Limits.pullbackConeOfRightIso_fst

deleted theorem CategoryTheory.Limits.pullbackConeOfRightIso_snd

deleted theorem CategoryTheory.Limits.pullbackConeOfRightIso_x

deleted theorem CategoryTheory.Limits.pullbackConeOfRightIso_π_app_left

deleted theorem CategoryTheory.Limits.pullbackConeOfRightIso_π_app_none

deleted theorem CategoryTheory.Limits.pullbackConeOfRightIso_π_app_right

deleted def CategoryTheory.Limits.pullbackIsPullback

deleted def CategoryTheory.Limits.pullbackPullbackLeftIsPullback

deleted def CategoryTheory.Limits.pullbackPullbackRightIsPullback

deleted theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_fst

deleted theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_hom_snd

deleted theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst

deleted theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_fst

deleted theorem CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd

deleted def CategoryTheory.Limits.pullbackSymmetry

deleted theorem CategoryTheory.Limits.pullbackSymmetry_hom_comp_fst

deleted theorem CategoryTheory.Limits.pullbackSymmetry_hom_comp_snd

deleted theorem CategoryTheory.Limits.pullbackSymmetry_hom_of_mono_eq

deleted theorem CategoryTheory.Limits.pullbackSymmetry_inv_comp_fst

deleted theorem CategoryTheory.Limits.pullbackSymmetry_inv_comp_snd

deleted theorem CategoryTheory.Limits.pullback_symmetry_hom_of_epi_eq

deleted theorem CategoryTheory.Limits.pushout.condition

deleted def CategoryTheory.Limits.pushout.congrHom

deleted theorem CategoryTheory.Limits.pushout.congrHom_inv

deleted theorem CategoryTheory.Limits.pushout.hom_ext

deleted theorem CategoryTheory.Limits.pushout.inl_desc

deleted theorem CategoryTheory.Limits.pushout.inr_desc

deleted theorem CategoryTheory.Limits.pushout.mapLift_comp

deleted def CategoryTheory.Limits.pushoutAssocIsPushout

deleted def CategoryTheory.Limits.pushoutAssocSymmIsPushout

deleted def CategoryTheory.Limits.pushoutCoconeOfLeftIso

deleted def CategoryTheory.Limits.pushoutCoconeOfLeftIsoIsLimit

deleted theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_inl

deleted theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_inr

deleted theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_x

deleted theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_left

deleted theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_none

deleted theorem CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_right

deleted def CategoryTheory.Limits.pushoutCoconeOfRightIso

deleted def CategoryTheory.Limits.pushoutCoconeOfRightIsoIsLimit

deleted theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_inl

deleted theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_inr

deleted theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_x

deleted theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_left

deleted theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_none

deleted theorem CategoryTheory.Limits.pushoutCoconeOfRightIso_ι_app_right

deleted def CategoryTheory.Limits.pushoutComparison

deleted theorem CategoryTheory.Limits.pushoutComparison_map_desc

deleted def CategoryTheory.Limits.pushoutIsPushout

deleted def CategoryTheory.Limits.pushoutPushoutLeftIsPushout

deleted def CategoryTheory.Limits.pushoutPushoutRightIsPushout

deleted def CategoryTheory.Limits.pushoutSymmetry

deleted def CategoryTheory.Limits.rightSquareIsPushout

deleted def CategoryTheory.Limits.span

deleted def CategoryTheory.Limits.spanCompIso

deleted theorem CategoryTheory.Limits.spanCompIso_app_left

deleted theorem CategoryTheory.Limits.spanCompIso_app_right

deleted theorem CategoryTheory.Limits.spanCompIso_app_zero

deleted theorem CategoryTheory.Limits.spanCompIso_hom_app_left

deleted theorem CategoryTheory.Limits.spanCompIso_hom_app_right

deleted theorem CategoryTheory.Limits.spanCompIso_hom_app_zero

deleted theorem CategoryTheory.Limits.spanCompIso_inv_app_left

deleted theorem CategoryTheory.Limits.spanCompIso_inv_app_right

deleted theorem CategoryTheory.Limits.spanCompIso_inv_app_zero

deleted def CategoryTheory.Limits.spanExt

deleted theorem CategoryTheory.Limits.spanExt_app_left

deleted theorem CategoryTheory.Limits.spanExt_app_one

deleted theorem CategoryTheory.Limits.spanExt_app_right

deleted theorem CategoryTheory.Limits.spanExt_hom_app_left

deleted theorem CategoryTheory.Limits.spanExt_hom_app_right

deleted theorem CategoryTheory.Limits.spanExt_hom_app_zero

deleted theorem CategoryTheory.Limits.spanExt_inv_app_left

deleted theorem CategoryTheory.Limits.spanExt_inv_app_right

deleted theorem CategoryTheory.Limits.spanExt_inv_app_zero

deleted theorem CategoryTheory.Limits.span_left

deleted theorem CategoryTheory.Limits.span_map_fst

deleted theorem CategoryTheory.Limits.span_map_id

deleted theorem CategoryTheory.Limits.span_map_snd

deleted theorem CategoryTheory.Limits.span_right

deleted theorem CategoryTheory.Limits.span_zero

deleted def CategoryTheory.Limits.walkingCospanOpEquiv

deleted def CategoryTheory.Limits.walkingSpanOpEquiv

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

Modified Mathlib/CategoryTheory/Limits/VanKampen.lean

Modified Mathlib/CategoryTheory/MorphismProperty/Limits.lean

Modified Mathlib/CategoryTheory/Sites/Grothendieck.lean

Modified Mathlib/CategoryTheory/Sites/IsSheafFor.lean

Modified Mathlib/CategoryTheory/Sites/Preserves.lean

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

Modified Mathlib/CategoryTheory/SmallObject/Construction.lean

Modified Mathlib/Topology/Category/CompHaus/Limits.lean

Modified Mathlib/Topology/Category/Profinite/Limits.lean

Modified scripts/noshake.json