case w
C : Type u₁
inst✝³ : Category C
J : Type u
inst✝² : Category J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
j✝ : J
⊢ (limit.π F j ≫ limit.lift F (coneOfDiagramTerminal I F)) ≫ limit.π F j✝ = 𝟙 (limit F) ≫ limit.π F j✝
C : Type u₁
inst✝³ : Category C
J : Type u
inst✝² : Category J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ limit.π F j ≫ limit.lift F (coneOfDiagramTerminal I F) = 𝟙 (limit F)
ext
no goals
case w
C : Type u₁
inst✝³ : Category C
J : Type u
inst✝² : Category J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
j✝ : J
⊢ (limit.π F j ≫ limit.lift F (coneOfDiagramTerminal I F)) ≫ limit.π F j✝ = 𝟙 (limit F) ≫ limit.π F j✝
simp
no goals
C : Type u₁
inst✝³ : Category C
J : Type u
inst✝² : Category J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ limit.lift F (coneOfDiagramTerminal I F) ≫ limit.π F j = 𝟙 (F.obj j)
simp