case w
J : Type u₁
inst✝⁴ : Category J
K : Type u₂
inst✝³ : Category K
C : Type u
inst✝² : Category C
F✝ : J ⥤ C
inst✝¹ : HasLimitsOfShape J C
G : J ⥤ C
α✝ : F✝ ⟶ G
inst✝ : HasLimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
j✝ : K
⊢ pre F E₂ ≫ π (E₂ ⋙ F) j✝ = (pre F E₁ ≫ lim.map (whiskerRight α F)) ≫ π (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✝¹ : HasLimitsOfShape J C
G : J ⥤ C
α✝ : F✝ ⟶ G
inst✝ : HasLimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
⊢ pre F E₂ = pre F E₁ ≫ lim.map (whiskerRight α F)
ext1
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✝¹ : HasLimitsOfShape J C
G : J ⥤ C
α✝ : F✝ ⟶ G
inst✝ : HasLimitsOfShape K C
F : J ⥤ C
E₁ E₂ : K ⥤ J
α : E₁ ⟶ E₂
j✝ : K
⊢ pre F E₂ ≫ π (E₂ ⋙ F) j✝ = (pre F E₁ ≫ lim.map (whiskerRight α F)) ≫ π (E₂ ⋙ F) j✝
simp [← category.assoc]