J : Type u₁
inst✝⁶ : Category J
K : Type u₂
inst✝⁵ : Category K
C : Type u
inst✝⁴ : Category C
F✝ : J ⥤ C
D : Type u'
inst✝³ : Category D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
⊢ G.map (pre F E) ≫ post (E ⋙ F) G = post F G ≫ pre (F ⋙ G) E
J : Type u₁
inst✝⁶ : Category J
K : Type u₂
inst✝⁵ : Category K
C : Type u
inst✝⁴ : Category C
F✝ : J ⥤ C
D : Type u'
inst✝³ : Category D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
⊢ G.map (pre F E) ≫ post (E ⋙ F) G = post F G ≫ pre (F ⋙ G) E
haveI : HasLimit (E ⋙  F ⋙  G) := h
case w
J : Type u₁
inst✝⁶ : Category J
K : Type u₂
inst✝⁵ : Category K
C : Type u
inst✝⁴ : Category C
F✝ : J ⥤ C
D : Type u'
inst✝³ : Category D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
j✝ : K
⊢ (G.map (pre F E) ≫ post (E ⋙ F) G) ≫ π ((E ⋙ F) ⋙ G) j✝ = (post F G ≫ pre (F ⋙ G) E) ≫ π ((E ⋙ F) ⋙ G) j✝
J : Type u₁
inst✝⁶ : Category J
K : Type u₂
inst✝⁵ : Category K
C : Type u
inst✝⁴ : Category C
F✝ : J ⥤ C
D : Type u'
inst✝³ : Category D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
⊢ G.map (pre F E) ≫ post (E ⋙ F) G = post F G ≫ pre (F ⋙ G) E
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
D : Type u'
inst✝³ : Category D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
j✝ : K
⊢ (G.map (pre F E) ≫ post (E ⋙ F) G) ≫ π ((E ⋙ F) ⋙ G) j✝ = (post F G ≫ pre (F ⋙ G) E) ≫ π ((E ⋙ F) ⋙ G) j✝
erw [assoc, limit.post_π, ← G.map_comp, limit.pre_π, assoc, limit.pre_π, limit.post_π]