awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
hφ : ∀ (j : J), c₁.ι.app j ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } = f.app j ≫ c₂.ι.app j
⊢ colimitsOfShape.{v, u, v_1, u_1} W J (Y := c₂.pt)
    (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } : c₁.pt ⟶ { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt)

Tactic:
⟨_, _, _, _, _, h₂, _, hf⟩

Premises used: CategoryTheory.MorphismProperty.colimitsOfShape.mk
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
hφ : ∀ (j : J), c₁.ι.app j ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } = f.app j ≫ c₂.ι.app j
⊢ colimitsOfShape.{v, u, v_1, u_1} W J (Y := c₂.pt)
    (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } : c₁.pt ⟶ { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt)

Tactic:
exact ⟨_, _, _, _, _, h₂, _, hf⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W₁ W₂ : MorphismProperty.{v, u} C
h : W₁ ≤ W₂
J : Type u_2
inst_1 : Category.{v_2, u_2} J
X Y : C
X₁ X₂ : Functor.{v_2, v, u_2, u} J C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W₁.functorCategory J f
⊢ colimitsOfShape.{v, u, v_2, u_2} W₂ J (Y := { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt)
    (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Tactic:
⟨_, _, _, _, _, h₂, f, fun j ↦ h _ (hf j)⟩

Premises used: CategoryTheory.MorphismProperty.colimitsOfShape.mk, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W₁ W₂ : MorphismProperty.{v, u} C
h : W₁ ≤ W₂
J : Type u_2
inst_1 : Category.{v_2, u_2} J
X Y : C
X₁ X₂ : Functor.{v_2, v, u_2, u} J C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W₁.functorCategory J f
⊢ colimitsOfShape.{v, u, v_2, u_2} W₂ J (Y := { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt)
    (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Tactic:
exact ⟨_, _, _, _, _, h₂, f, fun j ↦ h _ (hf j)⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
J' : Type u_2
inst_2 : Category.{v_2, u_2} J'
F : Functor.{v_1, v_2, u_1, u_2} J J'
inst_3 : F.Final
X : C
_ : ∀ ⦃Y : C⦄ (f : X ⟶ Y), colimitsOfShape.{v, u, v_2, u_2} W J' f → colimitsOfShape.{v, u, v_1, u_1} W J f
⊢ ∀ ⦃Y : C⦄ (f : X ⟶ Y), colimitsOfShape.{v, u, v_2, u_2} W J' f → colimitsOfShape.{v, u, v_1, u_1} W J f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
J' : Type u_2
inst_2 : Category.{v_2, u_2} J'
F : Functor.{v_1, v_2, u_1, u_2} J J'
inst_3 : F.Final
X Y : C
_ : ∀ (f : X ⟶ Y), colimitsOfShape.{v, u, v_2, u_2} W J' f → colimitsOfShape.{v, u, v_1, u_1} W J f
⊢ ∀ (f : X ⟶ Y), colimitsOfShape.{v, u, v_2, u_2} W J' f → colimitsOfShape.{v, u, v_1, u_1} W J f

Tactic:
_
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
J' : Type u_2
inst_2 : Category.{v_2, u_2} J'
F : Functor.{v_1, v_2, u_1, u_2} J J'
inst_3 : F.Final
X Y : C
f : X ⟶ Y
this :
  ∀ (X₁ X₂ : Functor.{v_2, v, u_2, u} J' C) (c₁ : Cocone X₁) (c₂ : Cocone X₂) (h₁ : IsColimit c₁) (h₂ : IsColimit c₂)
    (f : X₁ ⟶ X₂) (hf : W.functorCategory J' f),
    colimitsOfShape.{v, u, v_1, u_1} W J (Y := { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt)
      (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })
⊢ colimitsOfShape.{v, u, v_2, u_2} W J' f → colimitsOfShape.{v, u, v_1, u_1} W J f

Tactic:
⟨X₁, X₂, c₁, c₂, h₁, h₂, f, hf⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
J' : Type u_2
inst_2 : Category.{v_2, u_2} J'
F : Functor.{v_1, v_2, u_1, u_2} J J'
inst_3 : F.Final
X Y : C
f_1 : X ⟶ Y
X₁ X₂ : Functor.{v_2, v, u_2, u} J' C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
have :
  ∀ (h₁' : IsColimit (Cocone.whisker F c₁)),
    colimitsOfShape.{v, u, v_1, u_1} W J (Y := { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt)
      (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })
⊢ colimitsOfShape.{v, u, v_1, u_1} W J (Y := { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt)
    (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Tactic:
have h₁' : IsColimit (c₁.whisker F) := (Functor.Final.isColimitWhiskerEquiv F c₁).symm h₁
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
J' : Type u_2
inst_2 : Category.{v_2, u_2} J'
F : Functor.{v_1, v_2, u_1, u_2} J J'
inst_3 : F.Final
X Y : C
f_1 : X ⟶ Y
X₁ X₂ : Functor.{v_2, v, u_2, u} J' C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
h₁' : IsColimit (Cocone.whisker F c₁)
have :
  ∀ (h₂' : IsColimit (Cocone.whisker F c₂)),
    colimitsOfShape.{v, u, v_1, u_1} W J (Y := { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt)
      (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })
⊢ colimitsOfShape.{v, u, v_1, u_1} W J (Y := { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt)
    (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Tactic:
have h₂' : IsColimit (c₂.whisker F) := (Functor.Final.isColimitWhiskerEquiv F c₂).symm h₂
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
J' : Type u_2
inst_2 : Category.{v_2, u_2} J'
F : Functor.{v_1, v_2, u_1, u_2} J J'
inst_3 : F.Final
X Y : C
f_1 : X ⟶ Y
X₁ X₂ : Functor.{v_2, v, u_2, u} J' C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
h₁' : IsColimit (Cocone.whisker F c₁)
h₂' : IsColimit (Cocone.whisker F c₂)
j : J
⊢ (Cocone.whisker F c₁).ι.app j ≫ h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ F.whiskerLeft c₂.ι } =
    { pt := c₂.pt, ι := F.whiskerLeft f ≫ F.whiskerLeft c₂.ι : Cocone (F ⋙ X₁) }.ι.app j

Tactic:
have := h₁'.fac (Cocone.mk c₂.pt (Functor.whiskerLeft F f ≫ Functor.whiskerLeft F c₂.ι)) j
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
J' : Type u_2
inst_2 : Category.{v_2, u_2} J'
F : Functor.{v_1, v_2, u_1, u_2} J J'
inst_3 : F.Final
X Y : C
f_1 : X ⟶ Y
X₁ X₂ : Functor.{v_2, v, u_2, u} J' C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
h₁' : IsColimit (Cocone.whisker F c₁)
h₂' : IsColimit (Cocone.whisker F c₂)
j : J
this :
  (Cocone.whisker F c₁).ι.app j ≫ h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ F.whiskerLeft c₂.ι } =
    { pt := c₂.pt, ι := F.whiskerLeft f ≫ F.whiskerLeft c₂.ι : Cocone (F ⋙ X₁) }.ι.app j
dsimp :
  Eq (α := X₁.obj (F.obj j) ⟶ c₂.pt)
    (c₁.ι.app (F.obj j) ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } : X₁.obj (F.obj j) ⟶ c₂.pt)
    (c₁.ι.app (F.obj j) ≫ h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ F.whiskerLeft c₂.ι } :
      X₁.obj (F.obj j) ⟶ c₂.pt)
⊢ Eq (α := (F ⋙ X₁).obj j ⟶ { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt)
    ((Cocone.whisker F c₁).ι.app j ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })
    ((Cocone.whisker F c₁).ι.app j ≫ h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι })

Tactic:
dsimp at this ⊢
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
J' : Type u_2
inst_2 : Category.{v_2, u_2} J'
F : Functor.{v_1, v_2, u_1, u_2} J J'
inst_3 : F.Final
X Y : C
f_1 : X ⟶ Y
X₁ X₂ : Functor.{v_2, v, u_2, u} J' C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
h₁' : IsColimit (Cocone.whisker F c₁)
h₂' : IsColimit (Cocone.whisker F c₂)
j : J
this :
  Eq (α := X₁.obj (F.obj j) ⟶ c₂.pt)
    (c₁.ι.app (F.obj j) ≫ h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ F.whiskerLeft c₂.ι } :
      X₁.obj (F.obj j) ⟶ c₂.pt)
    (f.app (F.obj j) ≫ c₂.ι.app (F.obj j) : X₁.obj (F.obj j) ⟶ c₂.pt)
⊢ Eq (α := X₁.obj (F.obj j) ⟶ c₂.pt)
    (c₁.ι.app (F.obj j) ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } : X₁.obj (F.obj j) ⟶ c₂.pt)
    (c₁.ι.app (F.obj j) ≫ h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ F.whiskerLeft c₂.ι } :
      X₁.obj (F.obj j) ⟶ c₂.pt)

Tactic:
simp [this]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
J' : Type u_2
inst_2 : Category.{v_2, u_2} J'
F : Functor.{v_1, v_2, u_1, u_2} J J'
inst_3 : F.Final
X Y : C
f_1 : X ⟶ Y
X₁ X₂ : Functor.{v_2, v, u_2, u} J' C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
h₁' : IsColimit (Cocone.whisker F c₁)
h₂' : IsColimit (Cocone.whisker F c₂)
⊢ Eq (α := c₁.pt ⟶ { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt) (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })
    (h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι })

Tactic:
have : h₁.desc (Cocone.mk c₂.pt (f ≫ c₂.ι)) =
      h₁'.desc (Cocone.mk c₂.pt (Functor.whiskerLeft _ f ≫ (c₂.whisker F).ι)) :=
    h₁'.hom_ext (fun j ↦ by
      have := h₁'.fac (Cocone.mk c₂.pt (Functor.whiskerLeft F f ≫ Functor.whiskerLeft F c₂.ι)) j
      dsimp at this ⊢
      simp [this])
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
J' : Type u_2
inst_2 : Category.{v_2, u_2} J'
F : Functor.{v_1, v_2, u_1, u_2} J J'
inst_3 : F.Final
X Y : C
f_1 : X ⟶ Y
X₁ X₂ : Functor.{v_2, v, u_2, u} J' C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
h₁' : IsColimit (Cocone.whisker F c₁)
h₂' : IsColimit (Cocone.whisker F c₂)
this :
  Eq (α := c₁.pt ⟶ { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt) (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })
    (h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι })
rw :
  colimitsOfShape.{v, u, v_1, u_1} W J (Y := { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt)
    (h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι } :
      (Cocone.whisker F c₁).pt ⟶ { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι : Cocone (F ⋙ X₁) }.pt)
⊢ colimitsOfShape.{v, u, v_1, u_1} W J (Y := { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt)
    (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
J' : Type u_2
inst_2 : Category.{v_2, u_2} J'
F : Functor.{v_1, v_2, u_1, u_2} J J'
inst_3 : F.Final
X Y : C
f_1 : X ⟶ Y
X₁ X₂ : Functor.{v_2, v, u_2, u} J' C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
h₁' : IsColimit (Cocone.whisker F c₁)
h₂' : IsColimit (Cocone.whisker F c₂)
this :
  Eq (α := c₁.pt ⟶ { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt) (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })
    (h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι })
⊢ colimitsOfShape.{v, u, v_1, u_1} W J (Y := { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt)
    (h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι } :
      (Cocone.whisker F c₁).pt ⟶ { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι : Cocone (F ⋙ X₁) }.pt)

Tactic:
⟨_, _, _, _, h₁', h₂', _, fun _ ↦ hf _⟩

Premises used: CategoryTheory.Functor.comp, CategoryTheory.MorphismProperty.colimitsOfShape.mk, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
J' : Type u_2
inst_2 : Category.{v_2, u_2} J'
F : Functor.{v_1, v_2, u_1, u_2} J J'
inst_3 : F.Final
X Y : C
f_1 : X ⟶ Y
X₁ X₂ : Functor.{v_2, v, u_2, u} J' C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
h₁' : IsColimit (Cocone.whisker F c₁)
h₂' : IsColimit (Cocone.whisker F c₂)
this :
  Eq (α := c₁.pt ⟶ { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt) (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })
    (h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι })
⊢ colimitsOfShape.{v, u, v_1, u_1} W J (Y := { pt := c₂.pt, ι := f ≫ c₂.ι : Cocone X₁ }.pt)
    (h₁'.desc { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι } :
      (Cocone.whisker F c₁).pt ⟶ { pt := c₂.pt, ι := F.whiskerLeft f ≫ (Cocone.whisker F c₂).ι : Cocone (F ⋙ X₁) }.pt)

Tactic:
exact ⟨_, _, _, _, h₁', h₂', _, fun _ ↦ hf _⟩
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
J' : Type u_2
inst_2 : Category.{v_2, u_2} J'
e : Equivalence.{v_1, v_2, u_1, u_2} J J'
⊢ colimitsOfShape.{v, u, v_1, u_1} W J = colimitsOfShape.{v, u, v_2, u_2} W J'

Tactic:
le_antisymm (W.colimitsOfShape_le_of_final e.inverse)
    (W.colimitsOfShape_le_of_final e.functor)

Premises used: CategoryTheory.Equivalence.functor, le_antisymm, CategoryTheory.MorphismProperty.colimitsOfShape_le_of_final, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : Functor.obj.{v, v, u, u} (𝟭 C) Y₁ ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y₂
X Y : C
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e :
  { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
    { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
e₁ : Functor.obj (C := Arrow.{v, u} C) Arrow.leftFunc
    { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Functor.obj Arrow.leftFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.leftFunc e
e₂ : Functor.obj (C := Arrow.{v, u} C) Arrow.rightFunc
    { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Functor.obj Arrow.rightFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.rightFunc e
⊢ e₁.hom ≫ g = h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ e₂.hom

Tactic:
have fac : e₁.hom ≫ g = h₁.desc (Cocone.mk _ (f ≫ c₂.ι)) ≫ e₂.hom := e.hom.w
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : Functor.obj.{v, v, u, u} (𝟭 C) Y₁ ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y₂
X Y : C
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e :
  { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
    { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
e₁ : Functor.obj (C := Arrow.{v, u} C) Arrow.leftFunc
    { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Functor.obj Arrow.leftFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.leftFunc e
e₂ : Functor.obj (C := Arrow.{v, u} C) Arrow.rightFunc
    { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Functor.obj Arrow.rightFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.rightFunc e
fac : e₁.hom ≫ g = h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ e₂.hom
c₁' : Cocone X₁ := { pt := Y₁, ι := c₁.ι ≫ Functor.map (Functor.const J) e₁.hom }
c₂' : Cocone X₂ := { pt := Y₂, ι := c₂.ι ≫ Functor.map (Functor.const J) e₂.hom }
have :
  ∀ (h₁' : IsColimit c₁'),
    colimitsOfShape.{v, u, v_1, u_1} W J
      (Arrow.hom { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) })
⊢ colimitsOfShape.{v, u, v_1, u_1} W J
    (Arrow.hom { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) })

Tactic:
have h₁' : IsColimit c₁' := IsColimit.ofIsoColimit h₁ (Cocone.ext e₁)
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : Functor.obj.{v, v, u, u} (𝟭 C) Y₁ ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y₂
X Y : C
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e :
  { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
    { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
e₁ : Functor.obj (C := Arrow.{v, u} C) Arrow.leftFunc
    { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Functor.obj Arrow.leftFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.leftFunc e
e₂ : Functor.obj (C := Arrow.{v, u} C) Arrow.rightFunc
    { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Functor.obj Arrow.rightFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.rightFunc e
fac : e₁.hom ≫ g = h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ e₂.hom
c₁' : Cocone X₁ := { pt := Y₁, ι := c₁.ι ≫ Functor.map (Functor.const J) e₁.hom }
c₂' : Cocone X₂ := { pt := Y₂, ι := c₂.ι ≫ Functor.map (Functor.const J) e₂.hom }
h₁' : IsColimit c₁'
have :
  ∀ (h₂' : IsColimit c₂'),
    colimitsOfShape.{v, u, v_1, u_1} W J
      (Arrow.hom { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) })
⊢ colimitsOfShape.{v, u, v_1, u_1} W J
    (Arrow.hom { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) })

Tactic:
have h₂' : IsColimit c₂' := IsColimit.ofIsoColimit h₂ (Cocone.ext e₂)
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : Functor.obj.{v, v, u, u} (𝟭 C) Y₁ ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y₂
X Y : C
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e :
  { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
    { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
e₁ : Functor.obj (C := Arrow.{v, u} C) Arrow.leftFunc
    { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Functor.obj Arrow.leftFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.leftFunc e
e₂ : Functor.obj (C := Arrow.{v, u} C) Arrow.rightFunc
    { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Functor.obj Arrow.rightFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.rightFunc e
fac : e₁.hom ≫ g = h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ e₂.hom
c₁' : Cocone X₁ := { pt := Y₁, ι := c₁.ι ≫ Functor.map (Functor.const J) e₁.hom }
c₂' : Cocone X₂ := { pt := Y₂, ι := c₂.ι ≫ Functor.map (Functor.const J) e₂.hom }
h₁' : IsColimit c₁'
h₂' : IsColimit c₂'
j : J
rw : { pt := c₂'.pt, ι := f ≫ c₂'.ι : Cocone X₁ }.ι.app j = c₁'.ι.app j ≫ g
⊢ c₁'.ι.app j ≫ h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } = c₁'.ι.app j ≫ g

Tactic:
rw [h₁'.fac]

Premises used: CategoryTheory.Limits.IsColimit.fac
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : Functor.obj.{v, v, u, u} (𝟭 C) Y₁ ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y₂
X Y : C
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e :
  { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
    { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
e₁ : Functor.obj (C := Arrow.{v, u} C) Arrow.leftFunc
    { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Functor.obj Arrow.leftFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.leftFunc e
e₂ : Functor.obj (C := Arrow.{v, u} C) Arrow.rightFunc
    { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Functor.obj Arrow.rightFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.rightFunc e
fac : e₁.hom ≫ g = h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ e₂.hom
c₁' : Cocone X₁ := { pt := Y₁, ι := c₁.ι ≫ Functor.map (Functor.const J) e₁.hom }
c₂' : Cocone X₂ := { pt := Y₂, ι := c₂.ι ≫ Functor.map (Functor.const J) e₂.hom }
h₁' : IsColimit c₁'
h₂' : IsColimit c₂'
j : J
⊢ { pt := c₂'.pt, ι := f ≫ c₂'.ι : Cocone X₁ }.ι.app j = c₁'.ι.app j ≫ g

Tactic:
simp [fac, c₁', c₂']
-- Module: Mathlib.CategoryTheory.MorphismProperty.Limits
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
J : Type u_1
inst_1 : Category.{v_1, u_1} J
Y₁ Y₂ : C
g : Functor.obj.{v, v, u, u} (𝟭 C) Y₁ ⟶ Functor.obj.{v, v, u, u} (𝟭 C) Y₂
X Y : C
X₁ X₂ : Functor.{v_1, v, u_1, u} J C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
e :
  { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
    { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) }
e₁ : Functor.obj (C := Arrow.{v, u} C) Arrow.leftFunc
    { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Functor.obj Arrow.leftFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.leftFunc e
e₂ : Functor.obj (C := Arrow.{v, u} C) Arrow.rightFunc
    { left := c₁.1, right := c₂.1, hom := h₁.1 { pt := c₂.pt, ι := f ≫ c₂.ι } } ≅
  Functor.obj Arrow.rightFunc { left := Y₁, right := Y₂, hom := g : Comma.{v, v, v, u, u, u} (𝟭 C) (𝟭 C) } :=
  Functor.mapIso Arrow.rightFunc e
fac : e₁.hom ≫ g = h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ e₂.hom
c₁' : Cocone X₁ := { pt := Y₁, ι := c₁.ι ≫ Functor.map (Functor.const J) e₁.hom }
c₂' : Cocone X₂ := { pt := Y₂, ι := c₂.ι ≫ Functor.map (Functor.const J) e₂.hom }
h₁' : IsColimit c₁'
h₂' : IsColimit c₂'
⊢ h₁'.desc { pt := c₂'.pt, ι := f ≫ c₂'.ι } = g

Tactic:
obtain hg : h₁'.desc (Cocone.mk _ (f ≫ c₂'.ι)) = g :=
      h₁'.hom_ext (fun j ↦ by
        rw [h₁'.fac]
        simp [fac, c₁', c₂'])

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Limits.Cocone.mk, CategoryTheory.Limits.Cocone.ι, CategoryTheory.Limits.IsColimit.desc, CategoryTheory.CategoryStruct.comp