case w
J : Type u₁
inst✝⁴ : Category J
K : Type u₂
inst✝³ : Category K
C : Type u
inst✝² : Category C
F : J ⥤ C
inst✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
c : Cone F
j✝ : K
⊢ (lift F c ≫ pre F E) ≫ π (E ⋙ F) j✝ = lift (E ⋙ F) (Cone.whisker E c) ≫ π (E ⋙ F) j✝
J : Type u₁
inst✝⁴ : Category J
K : Type u₂
inst✝³ : Category K
C : Type u
inst✝² : Category C
F : J ⥤ C
inst✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
c : Cone F
⊢ lift F c ≫ pre F E = lift (E ⋙ F) (Cone.whisker E c)
ext
no goals
case w
J : Type u₁
inst✝⁴ : Category J
K : Type u₂
inst✝³ : Category K
C : Type u
inst✝² : Category C
F : J ⥤ C
inst✝¹ : HasLimit F
E : K ⥤ J
inst✝ : HasLimit (E ⋙ F)
c : Cone F
j✝ : K
⊢ (lift F c ≫ pre F E) ≫ π (E ⋙ F) j✝ = lift (E ⋙ F) (Cone.whisker E c) ≫ π (E ⋙ F) j✝
simp