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)
L : Type u₃
inst✝¹ : Category L
D : L ⥤ K
inst✝ h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
⊢ pre F E ≫ pre (E ⋙ F) D = 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✝³ : HasLimit F
E : K ⥤ J
inst✝² : HasLimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category L
D : L ⥤ K
inst✝ h : HasLimit (D ⋙ E ⋙ F)
⊢ pre F E ≫ pre (E ⋙ F) D = pre F (D ⋙ E)
haveI : HasLimit ((D ⋙  E) ⋙  F) := h
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)
L : Type u₃
inst✝¹ : Category L
D : L ⥤ K
inst✝ h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
j : L
⊢ (pre F E ≫ pre (E ⋙ F) D) ≫ π (D ⋙ E ⋙ F) j = pre F (D ⋙ E) ≫ π (D ⋙ 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)
L : Type u₃
inst✝¹ : Category L
D : L ⥤ K
inst✝ h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
⊢ pre F E ≫ pre (E ⋙ F) D = 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✝³ : HasLimit F
E : K ⥤ J
inst✝² : HasLimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category L
D : L ⥤ K
inst✝ h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
j : L
⊢ π F (E.obj (D.obj j)) = π F ((D ⋙ E).obj 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✝³ : HasLimit F
E : K ⥤ J
inst✝² : HasLimit (E ⋙ F)
L : Type u₃
inst✝¹ : Category L
D : L ⥤ K
inst✝ h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
j : L
⊢ (pre F E ≫ pre (E ⋙ F) D) ≫ π (D ⋙ E ⋙ F) j = pre F (D ⋙ E) ≫ π (D ⋙ E ⋙ F) j
erw [assoc, limit.pre_π, limit.pre_π, limit.pre_π]
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)
L : Type u₃
inst✝¹ : Category L
D : L ⥤ K
inst✝ h : HasLimit (D ⋙ E ⋙ F)
this : HasLimit ((D ⋙ E) ⋙ F)
j : L
⊢ π F (E.obj (D.obj j)) = π F ((D ⋙ E).obj j)
rfl