C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
t : Cocone G
P : IsColimit t
⊢ IsColimit.desc (↑(IsColimit.ofCoconeEquiv (Equivalence.symm (coconesEquiv F G))).symm P) (Cocone.whisker F t) = 𝟙 t.pt
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
t : Cocone G
P : IsColimit t
⊢ IsColimit.desc (↑(isColimitWhiskerEquiv F t).symm P) (Cocone.whisker F t) = 𝟙 t.pt
dsimp [isColimitWhiskerEquiv]
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
t : Cocone G
P : IsColimit t
⊢ ∀ (j : D),
    t.ι.app j ≫
        IsColimit.desc (↑(IsColimit.ofCoconeEquiv (Equivalence.symm (coconesEquiv F G))).symm P) (Cocone.whisker F t) =
      t.ι.app j ≫ 𝟙 t.pt
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
t : Cocone G
P : IsColimit t
⊢ IsColimit.desc (↑(IsColimit.ofCoconeEquiv (Equivalence.symm (coconesEquiv F G))).symm P) (Cocone.whisker F t) = 𝟙 t.pt
apply P.hom_ext
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
t : Cocone G
P : IsColimit t
j : D
⊢ t.ι.app j ≫
      IsColimit.desc (↑(IsColimit.ofCoconeEquiv (Equivalence.symm (coconesEquiv F G))).symm P) (Cocone.whisker F t) =
    t.ι.app j ≫ 𝟙 t.pt
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
t : Cocone G
P : IsColimit t
⊢ ∀ (j : D),
    t.ι.app j ≫
        IsColimit.desc (↑(IsColimit.ofCoconeEquiv (Equivalence.symm (coconesEquiv F G))).symm P) (Cocone.whisker F t) =
      t.ι.app j ≫ 𝟙 t.pt
intro j
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
t : Cocone G
P : IsColimit t
j : D
⊢ t.ι.app j ≫
      IsColimit.desc (↑(IsColimit.ofCoconeEquiv (Equivalence.symm (coconesEquiv F G))).symm P) (Cocone.whisker F t) =
    t.ι.app j ≫ 𝟙 t.pt
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
t : Cocone G
P : IsColimit t
j : D
⊢ t.ι.app j ≫
      IsColimit.desc (↑(IsColimit.ofCoconeEquiv (Equivalence.symm (coconesEquiv F G))).symm P) (Cocone.whisker F t) =
    t.ι.app j ≫ 𝟙 t.pt
dsimp
no goals
C : Type u₁
inst✝³ : Category C
D : Type u₂
inst✝² : Category D
F : C ⥤ D
inst✝¹ : Final F
E : Type u₃
inst✝ : Category E
G : D ⥤ E
t : Cocone G
P : IsColimit t
j : D
⊢ t.ι.app j ≫
      IsColimit.desc (↑(IsColimit.ofCoconeEquiv (Equivalence.symm (coconesEquiv F G))).symm P) (Cocone.whisker F t) =
    t.ι.app j ≫ 𝟙 t.pt
simp