-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma colimitsOfShape_le_of_final {J' : Type*} [Category J'] (F : J ⥤ J') [F.Final] :
    W.colimitsOfShape J' ≤ W.colimitsOfShape J

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{u_4, u_1} J
J' : Type u_2
inst✝¹ : Category.{u_3, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : 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 :
  c₁.ι.app (F.obj j) ≫ h₁'.desc { pt := c₂.pt, ι := whiskerLeft F f ≫ whiskerLeft F c₂.ι } =
    f.app (F.obj j) ≫ c₂.ι.app (F.obj j)
⊢ c₁.ι.app (F.obj j) ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } =
    c₁.ι.app (F.obj j) ≫ h₁'.desc { pt := c₂.pt, ι := whiskerLeft F f ≫ whiskerLeft F c₂.ι }

Tactic:
simp [this]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{u_4, u_1} J
J' : Type u_2
inst✝¹ : Category.{u_3, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : 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₂)
⊢ W.colimitsOfShape J (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Tactic:
have : h₁.desc (Cocone.mk c₂.pt (f ≫ c₂.ι)) =
    h₁'.desc (Cocone.mk c₂.pt (whiskerLeft _ f ≫ (c₂.whisker F).ι)) :=
  h₁'.hom_ext (fun j ↦ by
    have := h₁'.fac (Cocone.mk c₂.pt (whiskerLeft F f ≫ whiskerLeft F c₂.ι)) j
    dsimp at this ⊢
    simp [this])

Result:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{u_4, u_1} J
J' : Type u_2
inst✝¹ : Category.{u_3, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : 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 : h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } = h₁'.desc { pt := c₂.pt, ι := whiskerLeft F f ≫ (Cocone.whisker F c₂).ι }
⊢ W.colimitsOfShape J (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{u_4, u_1} J
J' : Type u_2
inst✝¹ : Category.{u_3, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : 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 ≫ c₂.ι } =
    (Cocone.whisker F c₁).ι.app j ≫ h₁'.desc { pt := c₂.pt, ι := whiskerLeft F f ≫ (Cocone.whisker F c₂).ι }

Tactic:
have := h₁'.fac (Cocone.mk c₂.pt (whiskerLeft F f ≫ whiskerLeft F c₂.ι)) j

Result:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{u_4, u_1} J
J' : Type u_2
inst✝¹ : Category.{u_3, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : 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, ι := whiskerLeft F f ≫ whiskerLeft F c₂.ι } =
    { pt := c₂.pt, ι := whiskerLeft F f ≫ whiskerLeft F c₂.ι }.ι.app j
⊢ (Cocone.whisker F c₁).ι.app j ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } =
    (Cocone.whisker F c₁).ι.app j ≫ h₁'.desc { pt := c₂.pt, ι := whiskerLeft F f ≫ (Cocone.whisker F c₂).ι }

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{u_4, u_1} J
J' : Type u_2
inst✝¹ : Category.{u_3, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
⊢ W.colimitsOfShape J' ≤ W.colimitsOfShape J

Tactic:
intro _ _ _ ⟨X₁, X₂, c₁, c₂, h₁, h₂, f, hf⟩

Result:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{u_4, u_1} J
J' : Type u_2
inst✝¹ : Category.{u_3, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : J' ⥤ C
c₁ : Cocone X₁
c₂ : Cocone X₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J' f
⊢ W.colimitsOfShape J (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{u_4, u_1} J
J' : Type u_2
inst✝¹ : Category.{u_3, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : 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₁)
⊢ W.colimitsOfShape J (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Tactic:
have h₂' : IsColimit (c₂.whisker F) := (Functor.Final.isColimitWhiskerEquiv F c₂).symm h₂

Result:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{u_4, u_1} J
J' : Type u_2
inst✝¹ : Category.{u_3, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : 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₂)
⊢ W.colimitsOfShape J (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{u_4, u_1} J
J' : Type u_2
inst✝¹ : Category.{u_3, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : 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, ι := whiskerLeft F f ≫ whiskerLeft F c₂.ι } =
    { pt := c₂.pt, ι := whiskerLeft F f ≫ whiskerLeft F c₂.ι }.ι.app j
⊢ (Cocone.whisker F c₁).ι.app j ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } =
    (Cocone.whisker F c₁).ι.app j ≫ h₁'.desc { pt := c₂.pt, ι := whiskerLeft F f ≫ (Cocone.whisker F c₂).ι }

Tactic:
dsimp at this ⊢

Result:
C : Type u
inst✝³ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝² : Category.{u_4, u_1} J
J' : Type u_2
inst✝¹ : Category.{u_3, u_2} J'
F : J ⥤ J'
inst✝ : F.Final
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X₁ X₂ : 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 :
  c₁.ι.app (F.obj j) ≫ h₁'.desc { pt := c₂.pt, ι := whiskerLeft F f ≫ whiskerLeft F c₂.ι } =
    f.app (F.obj j) ≫ c₂.ι.app (F.obj j)
⊢ c₁.ι.app (F.obj j) ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } =
    c₁.ι.app (F.obj j) ≫ h₁'.desc { pt := c₂.pt, ι := whiskerLeft F f ≫ whiskerLeft F c₂.ι }