This file contains declarations missing from mathlib, to be upstreamed.
theorem
CategoryTheory.Limits.PullbackCone.IsLimit.comp_lift
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{W' : C}
{W : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
{t : CategoryTheory.Limits.PullbackCone f g}
(σ : W' ⟶ W)
(ht : CategoryTheory.Limits.IsLimit t)
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
:
CategoryTheory.CategoryStruct.comp σ (ht.lift (CategoryTheory.Limits.PullbackCone.mk h k w)) = ht.lift
(CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.CategoryStruct.comp σ h)
(CategoryTheory.CategoryStruct.comp σ k) ⋯)
theorem
CategoryTheory.Limits.PullbackCone.IsLimit.comp_lift_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{X : C}
{Y : C}
{Z : C}
{W' : C}
{W : C}
{f : X ⟶ Z✝}
{g : Y ⟶ Z✝}
{t : CategoryTheory.Limits.PullbackCone f g}
(σ : W' ⟶ W)
(ht : CategoryTheory.Limits.IsLimit t)
(h : W ⟶ X)
(k : W ⟶ Y)
(w : CategoryTheory.CategoryStruct.comp h✝ f = CategoryTheory.CategoryStruct.comp k g)
{Z : C}
(h : t.pt ⟶ Z)
:
CategoryTheory.CategoryStruct.comp σ
(CategoryTheory.CategoryStruct.comp (ht.lift (CategoryTheory.Limits.PullbackCone.mk h✝ k w)) h) = CategoryTheory.CategoryStruct.comp
(ht.lift
(CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.CategoryStruct.comp σ h✝)
(CategoryTheory.CategoryStruct.comp σ k) ⋯))
h