case w
J : Type u₁
inst✝⁶ : Category J
K : Type u₂
inst✝⁵ : Category K
C : Type u
inst✝⁴ : Category C
F : J ⥤ C
inst✝³ : HasColimit F
E : K ⥤ J
inst✝² : HasColimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category L
D : L ⥤ K
inst✝ h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ ι (D ⋙ E ⋙ F) j ≫ pre (E ⋙ F) D ≫ pre F E = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)
J : Type u₁
inst✝⁶ : Category J
K : Type u₂
inst✝⁵ : Category K
C : Type u
inst✝⁴ : Category C
F : J ⥤ C
inst✝³ : HasColimit F
E : K ⥤ J
inst✝² : HasColimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category L
D : L ⥤ K
inst✝ h : HasColimit (D ⋙ E ⋙ F)
⊢ pre (E ⋙ F) D ≫ pre F E = pre F (D ⋙ E)
ext j
case w
J : Type u₁
inst✝⁶ : Category J
K : Type u₂
inst✝⁵ : Category K
C : Type u
inst✝⁴ : Category C
F : J ⥤ C
inst✝³ : HasColimit F
E : K ⥤ J
inst✝² : HasColimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category L
D : L ⥤ K
inst✝ h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ ι F (E.obj (D.obj j)) = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)
case w
J : Type u₁
inst✝⁶ : Category J
K : Type u₂
inst✝⁵ : Category K
C : Type u
inst✝⁴ : Category C
F : J ⥤ C
inst✝³ : HasColimit F
E : K ⥤ J
inst✝² : HasColimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category L
D : L ⥤ K
inst✝ h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ ι (D ⋙ E ⋙ F) j ≫ pre (E ⋙ F) D ≫ pre F E = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)
rw [← assoc, colimit.ι_pre, colimit.ι_pre]
case w
J : Type u₁
inst✝⁶ : Category J
K : Type u₂
inst✝⁵ : Category K
C : Type u
inst✝⁴ : Category C
F : J ⥤ C
inst✝³ : HasColimit F
E : K ⥤ J
inst✝² : HasColimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category L
D : L ⥤ K
inst✝ h : HasColimit (D ⋙ E ⋙ F)
j : L
this : HasColimit ((D ⋙ E) ⋙ F)
⊢ ι F (E.obj (D.obj j)) = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)
case w
J : Type u₁
inst✝⁶ : Category J
K : Type u₂
inst✝⁵ : Category K
C : Type u
inst✝⁴ : Category C
F : J ⥤ C
inst✝³ : HasColimit F
E : K ⥤ J
inst✝² : HasColimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category L
D : L ⥤ K
inst✝ h : HasColimit (D ⋙ E ⋙ F)
j : L
⊢ ι F (E.obj (D.obj j)) = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)
haveI : HasColimit ((D ⋙ E) ⋙ F) := h
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✝³ : HasColimit F
E : K ⥤ J
inst✝² : HasColimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category L
D : L ⥤ K
inst✝ h : HasColimit (D ⋙ E ⋙ F)
j : L
this : HasColimit ((D ⋙ E) ⋙ F)
⊢ ι F (E.obj (D.obj j)) = ι (D ⋙ E ⋙ F) j ≫ pre F (D ⋙ E)
exact (colimit.ι_pre F (D ⋙ E) j).symm