case w
J : Type u₁
inst✝⁴ : Category J
K : Type u₂
inst✝³ : Category K
C : Type u
inst✝² : Category C
F✝ F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
j✝ : J
⊢ (lift F c ≫ limMap α) ≫ π G j✝ = lift G ((Cones.postcompose α).obj c) ≫ π G j✝
J : Type u₁
inst✝⁴ : Category J
K : Type u₂
inst✝³ : Category K
C : Type u
inst✝² : Category C
F✝ F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
⊢ lift F c ≫ limMap α = lift G ((Cones.postcompose α).obj c)
ext
case w
J : Type u₁
inst✝⁴ : Category J
K : Type u₂
inst✝³ : Category K
C : Type u
inst✝² : Category C
F✝ F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
j✝ : J
⊢ c.π.app j✝ ≫ α.app j✝ = ((Cones.postcompose α).obj c).π.app j✝
case w
J : Type u₁
inst✝⁴ : Category J
K : Type u₂
inst✝³ : Category K
C : Type u
inst✝² : Category C
F✝ F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
j✝ : J
⊢ (lift F c ≫ limMap α) ≫ π G j✝ = lift G ((Cones.postcompose α).obj c) ≫ π G j✝
rw [assoc, limMap_π, limit.lift_π_assoc, limit.lift_π]
no goals
case w
J : Type u₁
inst✝⁴ : Category J
K : Type u₂
inst✝³ : Category K
C : Type u
inst✝² : Category C
F✝ F G : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasLimit G
c : Cone F
α : F ⟶ G
j✝ : J
⊢ c.π.app j✝ ≫ α.app j✝ = ((Cones.postcompose α).obj c).π.app j✝
rfl