Pasting

📁 Source: Mathlib/CategoryTheory/Limits/Shapes/Pullback/Pasting.lean

Statistics

Metric	Count
Definitions `pasteHoriz`, `pasteVert`, `pasteVertFlip`, `pasteHoriz`, `pasteVert`, `pasteVertFlip`, `botSquareIsPushout`, `leftSquareIsPullback`, `pasteHorizIsPullback`, `pasteHorizIsPullbackEquiv`, `pasteHorizIsPushout`, `pasteHorizIsPushoutEquiv`, `pasteVertIsPullback`, `pasteVertIsPullbackEquiv`, `pasteVertIsPushout`, `pasteVertIsPushoutEquiv`, `pullbackLeftPullbackSndIso`, `pullbackRightPullbackFstIso`, `pushoutLeftPushoutInrIso`, `pushoutRightPushoutInlIso`, `rightSquareIsPushout`, `topSquareIsPullback`	22
Theorems `hasPullbackHorizPaste`, `hasPullbackVertPaste`, `hasPushoutVertPaste`, `inl_inl_pushoutLeftPushoutInrIso_hom`, `inl_inl_pushoutLeftPushoutInrIso_hom_assoc`, `inl_pushoutLeftPushoutInrIso_inv`, `inl_pushoutLeftPushoutInrIso_inv_assoc`, `inl_pushoutRightPushoutInlIso_hom`, `inl_pushoutRightPushoutInlIso_hom_assoc`, `inl_pushoutRightPushoutInlIso_inv`, `inl_pushoutRightPushoutInlIso_inv_assoc`, `inr_inl_pushoutLeftPushoutInrIso_hom`, `inr_inl_pushoutLeftPushoutInrIso_hom_assoc`, `inr_inl_pushoutRightPushoutInlIso_hom`, `inr_inl_pushoutRightPushoutInlIso_hom_assoc`, `inr_inr_pushoutRightPushoutInlIso_hom`, `inr_inr_pushoutRightPushoutInlIso_hom_assoc`, `inr_pushoutLeftPushoutInrIso_hom`, `inr_pushoutLeftPushoutInrIso_hom_assoc`, `inr_pushoutLeftPushoutInrIso_inv`, `inr_pushoutLeftPushoutInrIso_inv_assoc`, `inr_pushoutRightPushoutInlIso_inv`, `inr_pushoutRightPushoutInlIso_inv_assoc`, `instHasPushoutComp`, `pullbackLeftPullbackSndIso_hom_fst`, `pullbackLeftPullbackSndIso_hom_fst_assoc`, `pullbackLeftPullbackSndIso_hom_snd`, `pullbackLeftPullbackSndIso_hom_snd_assoc`, `pullbackLeftPullbackSndIso_inv_fst`, `pullbackLeftPullbackSndIso_inv_fst_assoc`, `pullbackLeftPullbackSndIso_inv_fst_snd`, `pullbackLeftPullbackSndIso_inv_fst_snd_assoc`, `pullbackLeftPullbackSndIso_inv_snd_snd`, `pullbackLeftPullbackSndIso_inv_snd_snd_assoc`, `pullbackRightPullbackFstIso_hom_fst`, `pullbackRightPullbackFstIso_hom_fst_assoc`, `pullbackRightPullbackFstIso_hom_snd`, `pullbackRightPullbackFstIso_hom_snd_assoc`, `pullbackRightPullbackFstIso_inv_fst`, `pullbackRightPullbackFstIso_inv_fst_assoc`, `pullbackRightPullbackFstIso_inv_snd_fst`, `pullbackRightPullbackFstIso_inv_snd_fst_assoc`, `pullbackRightPullbackFstIso_inv_snd_snd`, `pullbackRightPullbackFstIso_inv_snd_snd_assoc`	44
Total	66

CategoryTheory.Limits

Definitions

Name	Category	Theorems
`botSquareIsPushout` 📖	CompOp	—
`leftSquareIsPullback` 📖	CompOp	—
`pasteHorizIsPullback` 📖	CompOp	—
`pasteHorizIsPullbackEquiv` 📖	CompOp	—
`pasteHorizIsPushout` 📖	CompOp	—
`pasteHorizIsPushoutEquiv` 📖	CompOp	—
`pasteVertIsPullback` 📖	CompOp	—
`pasteVertIsPullbackEquiv` 📖	CompOp	—
`pasteVertIsPushout` 📖	CompOp	—
`pasteVertIsPushoutEquiv` 📖	CompOp	—
`pullbackLeftPullbackSndIso` 📖	CompOp	12 math math: `CategoryTheory.MorphismProperty.Over.pullbackComp_hom_app_left`, `pullbackLeftPullbackSndIso_inv_fst_snd_assoc`, `pullbackLeftPullbackSndIso_inv_fst`, `CategoryTheory.MorphismProperty.Over.pullbackComp_inv_app_left`, `pullbackLeftPullbackSndIso_inv_fst_snd`, `pullbackLeftPullbackSndIso_hom_snd_assoc`, `pullbackLeftPullbackSndIso_hom_snd`, `pullbackLeftPullbackSndIso_hom_fst_assoc`, `pullbackLeftPullbackSndIso_hom_fst`, `pullbackLeftPullbackSndIso_inv_snd_snd`, `pullbackLeftPullbackSndIso_inv_snd_snd_assoc`, `pullbackLeftPullbackSndIso_inv_fst_assoc`
`pullbackRightPullbackFstIso` 📖	CompOp	10 math math: `pullbackRightPullbackFstIso_hom_fst`, `pullbackRightPullbackFstIso_hom_snd`, `pullbackRightPullbackFstIso_hom_fst_assoc`, `pullbackRightPullbackFstIso_inv_fst`, `pullbackRightPullbackFstIso_inv_snd_snd_assoc`, `pullbackRightPullbackFstIso_inv_fst_assoc`, `pullbackRightPullbackFstIso_inv_snd_fst_assoc`, `pullbackRightPullbackFstIso_inv_snd_fst`, `pullbackRightPullbackFstIso_hom_snd_assoc`, `pullbackRightPullbackFstIso_inv_snd_snd`
`pushoutLeftPushoutInrIso` 📖	CompOp	10 math math: `inr_inl_pushoutLeftPushoutInrIso_hom`, `inr_pushoutLeftPushoutInrIso_inv`, `inl_inl_pushoutLeftPushoutInrIso_hom_assoc`, `inr_pushoutLeftPushoutInrIso_inv_assoc`, `inl_inl_pushoutLeftPushoutInrIso_hom`, `inl_pushoutLeftPushoutInrIso_inv`, `inl_pushoutLeftPushoutInrIso_inv_assoc`, `inr_inl_pushoutLeftPushoutInrIso_hom_assoc`, `inr_pushoutLeftPushoutInrIso_hom_assoc`, `inr_pushoutLeftPushoutInrIso_hom`
`pushoutRightPushoutInlIso` 📖	CompOp	10 math math: `inr_inl_pushoutRightPushoutInlIso_hom_assoc`, `inr_inr_pushoutRightPushoutInlIso_hom`, `inr_inl_pushoutRightPushoutInlIso_hom`, `inl_pushoutRightPushoutInlIso_inv`, `inr_pushoutRightPushoutInlIso_inv`, `inr_inr_pushoutRightPushoutInlIso_hom_assoc`, `inr_pushoutRightPushoutInlIso_inv_assoc`, `inl_pushoutRightPushoutInlIso_hom`, `inl_pushoutRightPushoutInlIso_hom_assoc`, `inl_pushoutRightPushoutInlIso_inv_assoc`
`rightSquareIsPushout` 📖	CompOp	—
`topSquareIsPullback` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasPullbackHorizPaste` 📖	mathematical	—	`HasPullback` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—
`hasPullbackVertPaste` 📖	mathematical	—	`HasPullback` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—
`hasPushoutVertPaste` 📖	mathematical	—	`HasPushout` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—
`inl_inl_pushoutLeftPushoutInrIso_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `instHasPushoutComp` `pushout.inl` `pushout.inr` `CategoryTheory.Iso.hom` `pushoutLeftPushoutInrIso`	—	`instHasPushoutComp` `CategoryTheory.Category.assoc` `IsColimit.comp_coconePointUniqueUpToIso_hom`
`inl_inl_pushoutLeftPushoutInrIso_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `pushout.inl` `pushout.inr` `instHasPushoutComp` `CategoryTheory.Iso.hom` `pushoutLeftPushoutInrIso`	—	`instHasPushoutComp` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inl_inl_pushoutLeftPushoutInrIso_hom`
`inl_pushoutLeftPushoutInrIso_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `instHasPushoutComp` `pushout.inr` `pushout.inl` `CategoryTheory.Iso.inv` `pushoutLeftPushoutInrIso`	—	`IsColimit.comp_coconePointUniqueUpToIso_inv` `instHasPushoutComp`
`inl_pushoutLeftPushoutInrIso_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `instHasPushoutComp` `pushout.inl` `pushout.inr` `CategoryTheory.Iso.inv` `pushoutLeftPushoutInrIso`	—	`instHasPushoutComp` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inl_pushoutLeftPushoutInrIso_inv`
`inl_pushoutRightPushoutInlIso_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `pushout.inl` `hasPushoutVertPaste` `CategoryTheory.Iso.hom` `pushoutRightPushoutInlIso`	—	`IsColimit.comp_coconePointUniqueUpToIso_hom` `hasPushoutVertPaste`
`inl_pushoutRightPushoutInlIso_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `pushout.inl` `hasPushoutVertPaste` `CategoryTheory.Iso.hom` `pushoutRightPushoutInlIso`	—	`hasPushoutVertPaste` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inl_pushoutRightPushoutInlIso_hom`
`inl_pushoutRightPushoutInlIso_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `hasPushoutVertPaste` `pushout.inl` `CategoryTheory.Iso.inv` `pushoutRightPushoutInlIso`	—	`IsColimit.comp_coconePointUniqueUpToIso_inv` `hasPushoutVertPaste`
`inl_pushoutRightPushoutInlIso_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `hasPushoutVertPaste` `pushout.inl` `CategoryTheory.Iso.inv` `pushoutRightPushoutInlIso`	—	`hasPushoutVertPaste` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inl_pushoutRightPushoutInlIso_inv`
`inr_inl_pushoutLeftPushoutInrIso_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `instHasPushoutComp` `pushout.inr` `pushout.inl` `CategoryTheory.Iso.hom` `pushoutLeftPushoutInrIso`	—	`instHasPushoutComp` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.eq_comp_inv` `inr_pushoutLeftPushoutInrIso_inv` `pushout.condition`
`inr_inl_pushoutLeftPushoutInrIso_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `pushout.inr` `pushout.inl` `instHasPushoutComp` `CategoryTheory.Iso.hom` `pushoutLeftPushoutInrIso`	—	`instHasPushoutComp` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inr_inl_pushoutLeftPushoutInrIso_hom`
`inr_inl_pushoutRightPushoutInlIso_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `hasPushoutVertPaste` `pushout.inl` `pushout.inr` `CategoryTheory.Iso.hom` `pushoutRightPushoutInlIso`	—	`hasPushoutVertPaste` `CategoryTheory.Category.assoc` `pushout.condition` `inl_pushoutRightPushoutInlIso_hom`
`inr_inl_pushoutRightPushoutInlIso_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `pushout.inl` `pushout.inr` `hasPushoutVertPaste` `CategoryTheory.Iso.hom` `pushoutRightPushoutInlIso`	—	`hasPushoutVertPaste` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inr_inl_pushoutRightPushoutInlIso_hom`
`inr_inr_pushoutRightPushoutInlIso_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `hasPushoutVertPaste` `pushout.inr` `pushout.inl` `CategoryTheory.Iso.hom` `pushoutRightPushoutInlIso`	—	`hasPushoutVertPaste` `CategoryTheory.Category.assoc` `IsColimit.comp_coconePointUniqueUpToIso_hom`
`inr_inr_pushoutRightPushoutInlIso_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `pushout.inr` `pushout.inl` `hasPushoutVertPaste` `CategoryTheory.Iso.hom` `pushoutRightPushoutInlIso`	—	`hasPushoutVertPaste` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inr_inr_pushoutRightPushoutInlIso_hom`
`inr_pushoutLeftPushoutInrIso_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `pushout.inr` `instHasPushoutComp` `CategoryTheory.Iso.hom` `pushoutLeftPushoutInrIso`	—	`IsColimit.comp_coconePointUniqueUpToIso_hom` `instHasPushoutComp`
`inr_pushoutLeftPushoutInrIso_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `pushout.inr` `instHasPushoutComp` `CategoryTheory.Iso.hom` `pushoutLeftPushoutInrIso`	—	`instHasPushoutComp` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inr_pushoutLeftPushoutInrIso_hom`
`inr_pushoutLeftPushoutInrIso_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `instHasPushoutComp` `pushout.inr` `CategoryTheory.Iso.inv` `pushoutLeftPushoutInrIso`	—	`IsColimit.comp_coconePointUniqueUpToIso_inv` `instHasPushoutComp`
`inr_pushoutLeftPushoutInrIso_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `instHasPushoutComp` `pushout.inr` `CategoryTheory.Iso.inv` `pushoutLeftPushoutInrIso`	—	`instHasPushoutComp` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inr_pushoutLeftPushoutInrIso_inv`
`inr_pushoutRightPushoutInlIso_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `hasPushoutVertPaste` `pushout.inl` `pushout.inr` `CategoryTheory.Iso.inv` `pushoutRightPushoutInlIso`	—	`IsColimit.comp_coconePointUniqueUpToIso_inv` `hasPushoutVertPaste`
`inr_pushoutRightPushoutInlIso_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pushout` `hasPushoutVertPaste` `pushout.inr` `pushout.inl` `CategoryTheory.Iso.inv` `pushoutRightPushoutInlIso`	—	`hasPushoutVertPaste` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `inr_pushoutRightPushoutInlIso_inv`
`instHasPushoutComp` 📖	mathematical	—	`HasPushout` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct`	—	—
`pullbackLeftPullbackSndIso_hom_fst` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `pullback.snd` `hasPullbackVertPaste` `CategoryTheory.Iso.hom` `pullbackLeftPullbackSndIso` `pullback.fst`	—	`IsLimit.conePointUniqueUpToIso_hom_comp` `hasPullbackVertPaste`
`pullbackLeftPullbackSndIso_hom_fst_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `pullback.snd` `hasPullbackVertPaste` `CategoryTheory.Iso.hom` `pullbackLeftPullbackSndIso` `pullback.fst`	—	`hasPullbackVertPaste` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `pullbackLeftPullbackSndIso_hom_fst`
`pullbackLeftPullbackSndIso_hom_snd` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `pullback.snd` `hasPullbackVertPaste` `CategoryTheory.Iso.hom` `pullbackLeftPullbackSndIso`	—	`IsLimit.conePointUniqueUpToIso_hom_comp` `hasPullbackVertPaste`
`pullbackLeftPullbackSndIso_hom_snd_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `pullback.snd` `hasPullbackVertPaste` `CategoryTheory.Iso.hom` `pullbackLeftPullbackSndIso`	—	`hasPullbackVertPaste` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `pullbackLeftPullbackSndIso_hom_snd`
`pullbackLeftPullbackSndIso_inv_fst` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `hasPullbackVertPaste` `pullback.snd` `CategoryTheory.Iso.inv` `pullbackLeftPullbackSndIso` `pullback.fst`	—	`IsLimit.conePointUniqueUpToIso_inv_comp` `hasPullbackVertPaste`
`pullbackLeftPullbackSndIso_inv_fst_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `hasPullbackVertPaste` `pullback.snd` `CategoryTheory.Iso.inv` `pullbackLeftPullbackSndIso` `pullback.fst`	—	`hasPullbackVertPaste` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `pullbackLeftPullbackSndIso_inv_fst`
`pullbackLeftPullbackSndIso_inv_fst_snd` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `hasPullbackVertPaste` `pullback.snd` `CategoryTheory.Iso.inv` `pullbackLeftPullbackSndIso` `pullback.fst`	—	`hasPullbackVertPaste` `pullback.condition` `pullbackLeftPullbackSndIso_inv_snd_snd_assoc`
`pullbackLeftPullbackSndIso_inv_fst_snd_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `hasPullbackVertPaste` `pullback.snd` `CategoryTheory.Iso.inv` `pullbackLeftPullbackSndIso` `pullback.fst`	—	`hasPullbackVertPaste` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `pullbackLeftPullbackSndIso_inv_fst_snd`
`pullbackLeftPullbackSndIso_inv_snd_snd` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `hasPullbackVertPaste` `pullback.snd` `CategoryTheory.Iso.inv` `pullbackLeftPullbackSndIso`	—	`IsLimit.conePointUniqueUpToIso_inv_comp` `hasPullbackVertPaste`
`pullbackLeftPullbackSndIso_inv_snd_snd_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `hasPullbackVertPaste` `pullback.snd` `CategoryTheory.Iso.inv` `pullbackLeftPullbackSndIso`	—	`hasPullbackVertPaste` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `pullbackLeftPullbackSndIso_inv_snd_snd`
`pullbackRightPullbackFstIso_hom_fst` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `pullback.fst` `hasPullbackHorizPaste` `CategoryTheory.Iso.hom` `pullbackRightPullbackFstIso`	—	`IsLimit.conePointUniqueUpToIso_hom_comp` `hasPullbackHorizPaste`
`pullbackRightPullbackFstIso_hom_fst_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `pullback.fst` `hasPullbackHorizPaste` `CategoryTheory.Iso.hom` `pullbackRightPullbackFstIso`	—	`hasPullbackHorizPaste` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `pullbackRightPullbackFstIso_hom_fst`
`pullbackRightPullbackFstIso_hom_snd` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `pullback.fst` `hasPullbackHorizPaste` `CategoryTheory.Iso.hom` `pullbackRightPullbackFstIso` `pullback.snd`	—	`IsLimit.conePointUniqueUpToIso_hom_comp` `hasPullbackHorizPaste`
`pullbackRightPullbackFstIso_hom_snd_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `pullback.fst` `hasPullbackHorizPaste` `CategoryTheory.Iso.hom` `pullbackRightPullbackFstIso` `pullback.snd`	—	`hasPullbackHorizPaste` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `pullbackRightPullbackFstIso_hom_snd`
`pullbackRightPullbackFstIso_inv_fst` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `hasPullbackHorizPaste` `pullback.fst` `CategoryTheory.Iso.inv` `pullbackRightPullbackFstIso`	—	`IsLimit.conePointUniqueUpToIso_inv_comp` `hasPullbackHorizPaste`
`pullbackRightPullbackFstIso_inv_fst_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `hasPullbackHorizPaste` `pullback.fst` `CategoryTheory.Iso.inv` `pullbackRightPullbackFstIso`	—	`hasPullbackHorizPaste` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `pullbackRightPullbackFstIso_inv_fst`
`pullbackRightPullbackFstIso_inv_snd_fst` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `hasPullbackHorizPaste` `pullback.fst` `CategoryTheory.Iso.inv` `pullbackRightPullbackFstIso` `pullback.snd`	—	`hasPullbackHorizPaste` `pullback.condition` `pullbackRightPullbackFstIso_inv_fst_assoc`
`pullbackRightPullbackFstIso_inv_snd_fst_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `hasPullbackHorizPaste` `pullback.fst` `CategoryTheory.Iso.inv` `pullbackRightPullbackFstIso` `pullback.snd`	—	`hasPullbackHorizPaste` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `pullbackRightPullbackFstIso_inv_snd_fst`
`pullbackRightPullbackFstIso_inv_snd_snd` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `hasPullbackHorizPaste` `pullback.fst` `CategoryTheory.Iso.inv` `pullbackRightPullbackFstIso` `pullback.snd`	—	`IsLimit.conePointUniqueUpToIso_inv_comp` `hasPullbackHorizPaste`
`pullbackRightPullbackFstIso_inv_snd_snd_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `pullback` `hasPullbackHorizPaste` `pullback.fst` `CategoryTheory.Iso.inv` `pullbackRightPullbackFstIso` `pullback.snd`	—	`hasPullbackHorizPaste` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `pullbackRightPullbackFstIso_inv_snd_snd`

CategoryTheory.Limits.PullbackCone

Definitions

Name	Category	Theorems
`pasteHoriz` 📖	CompOp	—
`pasteVert` 📖	CompOp	—
`pasteVertFlip` 📖	CompOp	—

CategoryTheory.Limits.PushoutCocone

Definitions

Name	Category	Theorems
`pasteHoriz` 📖	CompOp	—
`pasteVert` 📖	CompOp	—
`pasteVertFlip` 📖	CompOp	—

---

← Back to Index