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
D : Type u'
inst✝¹ : Category D
inst✝ : HasLimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ (H.map (limMap α) ≫ post G H) ≫ π (G ⋙ H) j✝ = (post F H ≫ limMap (whiskerRight α H)) ≫ π (G ⋙ H) 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
D : Type u'
inst✝¹ : Category D
inst✝ : HasLimitsOfShape J D
H : C ⥤ D
⊢ H.map (limMap α) ≫ post G H = post F H ≫ limMap (whiskerRight α H)
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✝² : HasLimitsOfShape J C
G : J ⥤ C
α : F ⟶ G
D : Type u'
inst✝¹ : Category D
inst✝ : HasLimitsOfShape J D
H : C ⥤ D
j✝ : J
⊢ (H.map (limMap α) ≫ post G H) ≫ π (G ⋙ H) j✝ = (post F H ≫ limMap (whiskerRight α H)) ≫ π (G ⋙ H) j✝
simp only [whiskerRight_app, limMap_π, assoc, limit.post_π_assoc, limit.post_π, ← H.map_comp]