Documentation Verification Report

Limits

📁 Source: Mathlib/Topology/Category/CompHausLike/Limits.lean

Statistics

Metric	Count
Definitions `HasExplicitFiniteCoproduct`, `HasExplicitFiniteCoproducts`, `HasExplicitPullback`, `HasExplicitPullbacks`, `HasExplicitPullbacksOfInclusions`, `finiteCoproduct`, `cofan`, `desc`, `isColimit`, `ι`, `instCreatesLimitTopCatWalkingCospanCospanCompHausLikeToTop`, `isTerminalPUnit`, `pullback`, `cone`, `fst`, `isLimit`, `snd`	17
Theorems `hasProp`, `hasProp`, `hasProp`, `isOpenEmbedding_ι`, `finitaryExtensive`, `hom_ext`, `isOpenEmbedding_ι`, `ι_desc`, `ι_desc_apply`, `ι_desc_assoc`, `ι_injective`, `ι_jointly_surjective`, `hasPullbacksOfInclusions`, `instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions`, `instHasColimitsOfShapeDiscreteOfHasExplicitFiniteCoproductsOfFinite`, `instHasCoproduct`, `instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks`, `instHasFiniteCoproductsOfHasExplicitFiniteCoproducts`, `instHasLimitWalkingCospanCospan`, `instHasPullbacksOfHasExplicitPullbacks`, `instHasPullbacksOfInclusionsOfHasExplicitPullbacksOfInclusions`, `instPreservesFiniteCoproductsToCompHausLike`, `instPreservesFiniteCoproductsTopCatCompHausLikeToTopOfHasExplicitFiniteCoproducts`, `instPreservesLimitTopCatWalkingCospanCospanCompHausLikeToTop`, `instPreservesLimitWalkingCospanCospanToCompHausLike`, `instPreservesPullbacksOfInclusionsTopCatCompHausLikeToTopOfHasExplicitPullbacksOfInclusions`, `condition`, `condition_assoc`, `cone_pt`, `cone_π`, `hom_ext`, `isLimit_lift`, `lift_fst`, `lift_fst_assoc`, `lift_snd`, `lift_snd_assoc`	36
Total	53

CompHausLike

Definitions

Name	Category	Theorems
`HasExplicitFiniteCoproduct` 📖	MathDef	1 math math: `HasExplicitFiniteCoproducts.hasProp`
`HasExplicitFiniteCoproducts` 📖	CompData	4 math math: `Stonean.instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier`, `LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology`, `Profinite.instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceCarrier`, `CompHaus.instHasExplicitFiniteCoproductsTrue`
`HasExplicitPullback` 📖	MathDef	2 math math: `HasExplicitPullbacksOfInclusions.hasProp`, `HasExplicitPullbacks.hasProp`
`HasExplicitPullbacks` 📖	CompData	3 math math: `LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology`, `CompHaus.instHasExplicitPullbacksTrue`, `Profinite.instHasExplicitPullbacksTotallyDisconnectedSpaceCarrier`
`HasExplicitPullbacksOfInclusions` 📖	CompData	3 math math: `hasPullbacksOfInclusions`, `Stonean.instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedCarrier`, `instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks`
`finiteCoproduct` 📖	CompOp	7 math math: `finiteCoproduct.ι_desc`, `finiteCoproduct.isOpenEmbedding_ι`, `finiteCoproduct.ι_desc_assoc`, `finiteCoproduct.ι_injective`, `LocallyConstant.sigmaComparison_comp_sigmaIso`, `finiteCoproduct.ι_jointly_surjective`, `finiteCoproduct.ι_desc_apply`
`instCreatesLimitTopCatWalkingCospanCospanCompHausLikeToTop` 📖	CompOp	—
`isTerminalPUnit` 📖	CompOp	—
`pullback` 📖	CompOp	8 math math: `pullback.lift_fst_assoc`, `pullback.condition`, `pullback.condition_assoc`, `pullback.cone_π`, `pullback.lift_fst`, `pullback.lift_snd_assoc`, `pullback.cone_pt`, `pullback.lift_snd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finitaryExtensive` 📖	mathematical	`HasExplicitPullback`	`CategoryTheory.FinitaryExtensive` `CompHausLike` `category`	—	`hasPullbacksOfInclusions` `CategoryTheory.finitaryExtensive_of_preserves_and_reflects` `CategoryTheory.finitaryExtensive_TopCat` `instHasFiniteCoproductsOfHasExplicitFiniteCoproducts` `instHasPullbacksOfInclusionsOfHasExplicitPullbacksOfInclusions` `instPreservesPullbacksOfInclusionsTopCatCompHausLikeToTopOfHasExplicitPullbacksOfInclusions` `CategoryTheory.Limits.ReflectsFiniteLimits.reflects` `CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimits` `CategoryTheory.Limits.fullyFaithful_reflectsLimits` `instFullTopCatCompHausLikeToTop` `instFaithfulTopCatCompHausLikeToTop` `CategoryTheory.Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts` `Finite.of_fintype` `instPreservesFiniteCoproductsTopCatCompHausLikeToTopOfHasExplicitFiniteCoproducts` `CategoryTheory.Limits.ReflectsFiniteColimits.reflects` `CategoryTheory.Limits.instReflectsFiniteColimitsOfReflectsColimits` `CategoryTheory.Limits.fullyFaithful_reflectsColimits`
`hasPullbacksOfInclusions` 📖	mathematical	`HasExplicitPullback`	`HasExplicitPullbacksOfInclusions`	—	`CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `instHasColimitsOfShapeDiscreteOfHasExplicitFiniteCoproductsOfFinite` `Finite.of_fintype` `Sigma.isOpenEmbedding_ι` `HasExplicitFiniteCoproducts.hasProp`
`instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` 📖	mathematical	—	`CategoryTheory.FinitaryExtensive` `CompHausLike` `category`	—	`CategoryTheory.finitaryExtensive_of_preserves_and_reflects` `CategoryTheory.finitaryExtensive_TopCat` `instHasFiniteCoproductsOfHasExplicitFiniteCoproducts` `instHasPullbacksOfInclusionsOfHasExplicitPullbacksOfInclusions` `instPreservesPullbacksOfInclusionsTopCatCompHausLikeToTopOfHasExplicitPullbacksOfInclusions` `CategoryTheory.Limits.ReflectsFiniteLimits.reflects` `CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimits` `CategoryTheory.Limits.fullyFaithful_reflectsLimits` `instFullTopCatCompHausLikeToTop` `instFaithfulTopCatCompHausLikeToTop` `CategoryTheory.Limits.instPreservesColimitsOfShapeDiscreteOfFiniteOfPreservesFiniteCoproducts` `Finite.of_fintype` `instPreservesFiniteCoproductsTopCatCompHausLikeToTopOfHasExplicitFiniteCoproducts` `CategoryTheory.Limits.ReflectsFiniteColimits.reflects` `CategoryTheory.Limits.instReflectsFiniteColimitsOfReflectsColimits` `CategoryTheory.Limits.fullyFaithful_reflectsColimits`
`instHasColimitsOfShapeDiscreteOfHasExplicitFiniteCoproductsOfFinite` 📖	mathematical	—	`CategoryTheory.Limits.HasColimitsOfShape` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CompHausLike` `category`	—	`CategoryTheory.Limits.hasColimit_of_iso` `instHasCoproduct` `HasExplicitFiniteCoproducts.hasProp`
`instHasCoproduct` 📖	mathematical	—	`CategoryTheory.Limits.HasCoproduct` `CompHausLike` `category`	—	—
`instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` 📖	mathematical	—	`HasExplicitPullbacksOfInclusions`	—	`CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `instHasColimitsOfShapeDiscreteOfHasExplicitFiniteCoproductsOfFinite` `Finite.of_fintype` `HasExplicitPullbacks.hasProp`
`instHasFiniteCoproductsOfHasExplicitFiniteCoproducts` 📖	mathematical	—	`CategoryTheory.Limits.HasFiniteCoproducts` `CompHausLike` `category`	—	`CategoryTheory.Limits.hasColimitsOfShape_of_equivalence` `instHasColimitsOfShapeDiscreteOfHasExplicitFiniteCoproductsOfFinite` `instFiniteULift` `Finite.of_fintype`
`instHasLimitWalkingCospanCospan` 📖	mathematical	—	`CategoryTheory.Limits.HasLimit` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CompHausLike` `category` `CategoryTheory.Limits.cospan`	—	—
`instHasPullbacksOfHasExplicitPullbacks` 📖	mathematical	—	`CategoryTheory.Limits.HasPullbacks` `CompHausLike` `category`	—	`CategoryTheory.Limits.hasLimit_of_iso` `instHasLimitWalkingCospanCospan` `HasExplicitPullbacks.hasProp`
`instHasPullbacksOfInclusionsOfHasExplicitPullbacksOfInclusions` 📖	mathematical	—	`CategoryTheory.HasPullbacksOfInclusions` `CompHausLike` `category` `instHasColimitsOfShapeDiscreteOfHasExplicitFiniteCoproductsOfFinite` `CategoryTheory.Limits.WalkingPair` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair`	—	`instHasColimitsOfShapeDiscreteOfHasExplicitFiniteCoproductsOfFinite` `Finite.of_fintype` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `instHasLimitWalkingCospanCospan` `HasExplicitPullbacksOfInclusions.hasProp`
`instPreservesFiniteCoproductsToCompHausLike` 📖	mathematical	`toTop`	`CategoryTheory.Limits.PreservesFiniteCoproducts` `CompHausLike` `category` `toCompHausLike`	—	`instPreservesFiniteCoproductsTopCatCompHausLikeToTopOfHasExplicitFiniteCoproducts` `CategoryTheory.Limits.preservesFiniteCoproducts_of_reflects_of_preserves` `CategoryTheory.Limits.instReflectsFiniteCoproductsOfReflectsFiniteColimits` `CategoryTheory.Limits.instReflectsFiniteColimitsOfReflectsColimits` `CategoryTheory.Limits.fullyFaithful_reflectsColimits` `instFullTopCatCompHausLikeToTop` `instFaithfulTopCatCompHausLikeToTop`
`instPreservesFiniteCoproductsTopCatCompHausLikeToTopOfHasExplicitFiniteCoproducts` 📖	mathematical	—	`CategoryTheory.Limits.PreservesFiniteCoproducts` `CompHausLike` `category` `TopCat` `TopCat.instCategory` `compHausLikeToTop`	—	`CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone` `Finite.of_fintype` `HasExplicitFiniteCoproducts.hasProp` `CategoryTheory.Limits.preservesColimit_of_iso_diagram`
`instPreservesLimitTopCatWalkingCospanCospanCompHausLikeToTop` 📖	mathematical	—	`CategoryTheory.Limits.PreservesLimit` `CompHausLike` `category` `TopCat` `TopCat.instCategory` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan` `compHausLikeToTop`	—	`CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Limits.hasFiniteLimits_of_hasLimits` `TopCat.topCat_hasLimits`
`instPreservesLimitWalkingCospanCospanToCompHausLike` 📖	mathematical	`toTop`	`CategoryTheory.Limits.PreservesLimit` `CompHausLike` `category` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.cospan` `toCompHausLike`	—	`instPreservesLimitTopCatWalkingCospanCospanCompHausLikeToTop` `CategoryTheory.Limits.preservesLimit_of_reflects_of_preserves` `CategoryTheory.Limits.reflectsLimit_of_reflectsLimitsOfShape` `CategoryTheory.Limits.ReflectsFiniteLimits.reflects` `CategoryTheory.Limits.instReflectsFiniteLimitsOfReflectsLimits` `CategoryTheory.Limits.fullyFaithful_reflectsLimits` `instFullTopCatCompHausLikeToTop` `instFaithfulTopCatCompHausLikeToTop`
`instPreservesPullbacksOfInclusionsTopCatCompHausLikeToTopOfHasExplicitPullbacksOfInclusions` 📖	mathematical	—	`CategoryTheory.PreservesPullbacksOfInclusions` `CompHausLike` `category` `TopCat` `TopCat.instCategory` `compHausLikeToTop` `instHasColimitsOfShapeDiscreteOfHasExplicitFiniteCoproductsOfFinite` `CategoryTheory.Limits.WalkingPair` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair`	—	`instHasColimitsOfShapeDiscreteOfHasExplicitFiniteCoproductsOfFinite` `Finite.of_fintype` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `instPreservesLimitTopCatWalkingCospanCospanCompHausLikeToTop` `HasExplicitPullbacksOfInclusions.hasProp`

CompHausLike.HasExplicitFiniteCoproducts

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasProp` 📖	mathematical	—	`CompHausLike.HasExplicitFiniteCoproduct`	—	—

CompHausLike.HasExplicitPullbacks

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasProp` 📖	mathematical	—	`CompHausLike.HasExplicitPullback`	—	—

CompHausLike.HasExplicitPullbacksOfInclusions

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasProp` 📖	mathematical	—	`CompHausLike.HasExplicitPullback` `CategoryTheory.Limits.coprod` `CompHausLike` `CompHausLike.category` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CompHausLike.instHasColimitsOfShapeDiscreteOfHasExplicitFiniteCoproductsOfFinite` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.pair` `CategoryTheory.Limits.coprod.inl`	—	—

CompHausLike.Sigma

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpenEmbedding_ι` 📖	mathematical	—	`Topology.IsOpenEmbedding` `CategoryTheory.Limits.sigmaObj` `CompHausLike` `CompHausLike.category` `CompHausLike.instHasCoproduct` `TopCat.str` `CompHausLike.toTop` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `TopCat.carrier` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory` `CategoryTheory.Limits.Sigma.ι`	—	`Topology.IsOpenEmbedding.of_comp` `CompHausLike.instHasCoproduct` `Homeomorph.isOpenEmbedding` `CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom` `CompHausLike.finiteCoproduct.isOpenEmbedding_ι`

CompHausLike.finiteCoproduct

Definitions

Name	Category	Theorems
`cofan` 📖	CompOp	1 math math: `CompHausLike.sigmaComparison_eq_comp_isos`
`desc` 📖	CompOp	3 math math: `ι_desc`, `ι_desc_assoc`, `ι_desc_apply`
`isColimit` 📖	CompOp	1 math math: `CompHausLike.sigmaComparison_eq_comp_isos`
`ι` 📖	CompOp	6 math math: `ι_desc`, `isOpenEmbedding_ι`, `ι_desc_assoc`, `ι_injective`, `ι_jointly_surjective`, `ι_desc_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_ext` 📖	—	`CategoryTheory.CategoryStruct.comp` `CompHausLike` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.category` `CompHausLike.finiteCoproduct` `ι`	—	—	`CategoryTheory.ConcreteCategory.ext` `ContinuousMap.ext`
`isOpenEmbedding_ι` 📖	mathematical	—	`Topology.IsOpenEmbedding` `CompHausLike.finiteCoproduct` `TopCat.str` `CompHausLike.toTop` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `CompHausLike` `CompHausLike.category` `ContinuousMap` `TopCat.carrier` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory` `ι`	—	`Topology.IsOpenEmbedding.sigmaMk`
`ι_desc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CompHausLike` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.category` `CompHausLike.finiteCoproduct` `ι` `desc`	—	—
`ι_desc_apply` 📖	mathematical	—	`DFunLike.coe` `CompHausLike.finiteCoproduct` `CategoryTheory.ConcreteCategory.hom` `CompHausLike` `CompHausLike.category` `ContinuousMap` `TopCat.carrier` `CompHausLike.toTop` `TopCat.str` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory` `desc` `ι`	—	—
`ι_desc_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CompHausLike` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.category` `CompHausLike.finiteCoproduct` `ι` `desc`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `ι_desc`
`ι_injective` 📖	mathematical	—	`CompHausLike.finiteCoproduct` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `CompHausLike` `CompHausLike.category` `ContinuousMap` `TopCat.carrier` `CompHausLike.toTop` `TopCat.str` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory` `ι`	—	—
`ι_jointly_surjective` 📖	mathematical	—	`DFunLike.coe` `CompHausLike.finiteCoproduct` `CategoryTheory.ConcreteCategory.hom` `CompHausLike` `CompHausLike.category` `ContinuousMap` `TopCat.carrier` `CompHausLike.toTop` `TopCat.str` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory` `ι`	—	—

CompHausLike.pullback

Definitions

Name	Category	Theorems
`cone` 📖	CompOp	3 math math: `isLimit_lift`, `cone_π`, `cone_pt`
`fst` 📖	CompOp	5 math math: `lift_fst_assoc`, `condition`, `condition_assoc`, `cone_π`, `lift_fst`
`isLimit` 📖	CompOp	1 math math: `isLimit_lift`
`snd` 📖	CompOp	5 math math: `condition`, `condition_assoc`, `cone_π`, `lift_snd_assoc`, `lift_snd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`condition` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CompHausLike` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.category` `CompHausLike.pullback` `fst` `snd`	—	`CategoryTheory.ConcreteCategory.ext` `ContinuousMap.ext`
`condition_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CompHausLike` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.category` `CompHausLike.pullback` `fst` `snd`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `condition`
`cone_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CompHausLike` `CompHausLike.category` `CategoryTheory.Limits.cospan` `cone` `CompHausLike.pullback`	—	—
`cone_π` 📖	mathematical	—	`CategoryTheory.Limits.Cone.π` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CompHausLike` `CompHausLike.category` `CategoryTheory.Limits.cospan` `cone` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.const` `CompHausLike.pullback` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CategoryStruct.comp` `fst` `snd` `condition`	—	—
`hom_ext` 📖	—	`CategoryTheory.CategoryStruct.comp` `CompHausLike` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.category` `CompHausLike.pullback` `fst` `snd`	—	—	`CategoryTheory.ConcreteCategory.ext` `ContinuousMap.ext`
`isLimit_lift` 📖	mathematical	—	`CategoryTheory.Limits.IsLimit.lift` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CompHausLike` `CompHausLike.category` `CategoryTheory.Limits.cospan` `cone` `isLimit` `lift` `CategoryTheory.Limits.Cone.pt` `CategoryTheory.Limits.PullbackCone.fst` `CategoryTheory.Limits.PullbackCone.snd`	—	—
`lift_fst` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CompHausLike` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.category`	`CompHausLike.pullback` `lift` `fst`	—	—
`lift_fst_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CompHausLike` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.category`	`CompHausLike.pullback` `lift` `fst`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `lift_fst`
`lift_snd` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CompHausLike` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.category`	`CompHausLike.pullback` `lift` `snd`	—	—
`lift_snd_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CompHausLike` `CategoryTheory.Category.toCategoryStruct` `CompHausLike.category`	`CompHausLike.pullback` `lift` `snd`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `lift_snd`

---

← Back to Index