J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
Y : C
f : Y ⟶ X
⊢ { pt := Y, π := h.hom.app Y.op { down := f } } = { pt := Y, π := (const J).map f ≫ h.hom.app X.op { down := 𝟙 X } }
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
Y : C
f : Y ⟶ X
⊢ coneOfHom h f = Cone.extend (limitCone h) f
dsimp [coneOfHom, limitCone, Cone.extend]
case e_π.w.h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
Y : C
f : Y ⟶ X
j : J
⊢ (h.hom.app Y.op { down := f }).app j = ((const J).map f ≫ h.hom.app X.op { down := 𝟙 X }).app j
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
Y : C
f : Y ⟶ X
⊢ { pt := Y, π := h.hom.app Y.op { down := f } } = { pt := Y, π := (const J).map f ≫ h.hom.app X.op { down := 𝟙 X } }
congr with j
case e_π.w.h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t✝ : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
Y : C
f : Y ⟶ X
j : J
t :
  ((yoneda.obj X ⋙ uliftFunctor).map f.op ≫ h.hom.app Y.op) { down := 𝟙 X } =
    (h.hom.app X.op ≫ (Functor.cones F).map f.op) { down := 𝟙 X }
⊢ (h.hom.app Y.op { down := f }).app j = ((const J).map f ≫ h.hom.app X.op { down := 𝟙 X }).app j
case e_π.w.h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
Y : C
f : Y ⟶ X
j : J
⊢ (h.hom.app Y.op { down := f }).app j = ((const J).map f ≫ h.hom.app X.op { down := 𝟙 X }).app j
have t := congrFun (h.hom.naturality f.op) ⟨𝟙 X⟩
case e_π.w.h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t✝ : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
Y : C
f : Y ⟶ X
j : J
t : h.hom.app Y.op { down := f ≫ 𝟙 X } = (Functor.cones F).map f.op (h.hom.app X.op { down := 𝟙 X })
⊢ (h.hom.app Y.op { down := f }).app j = ((const J).map f ≫ h.hom.app X.op { down := 𝟙 X }).app j
case e_π.w.h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t✝ : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
Y : C
f : Y ⟶ X
j : J
t :
  ((yoneda.obj X ⋙ uliftFunctor).map f.op ≫ h.hom.app Y.op) { down := 𝟙 X } =
    (h.hom.app X.op ≫ (Functor.cones F).map f.op) { down := 𝟙 X }
⊢ (h.hom.app Y.op { down := f }).app j = ((const J).map f ≫ h.hom.app X.op { down := 𝟙 X }).app j
dsimp at t
case e_π.w.h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t✝ : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
Y : C
f : Y ⟶ X
j : J
t : h.hom.app Y.op { down := f } = (Functor.cones F).map f.op (h.hom.app X.op { down := 𝟙 X })
⊢ (h.hom.app Y.op { down := f }).app j = ((const J).map f ≫ h.hom.app X.op { down := 𝟙 X }).app j
case e_π.w.h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t✝ : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
Y : C
f : Y ⟶ X
j : J
t : h.hom.app Y.op { down := f ≫ 𝟙 X } = (Functor.cones F).map f.op (h.hom.app X.op { down := 𝟙 X })
⊢ (h.hom.app Y.op { down := f }).app j = ((const J).map f ≫ h.hom.app X.op { down := 𝟙 X }).app j
simp only [comp_id] at t
case e_π.w.h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t✝ : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
Y : C
f : Y ⟶ X
j : J
t : h.hom.app Y.op { down := f } = (Functor.cones F).map f.op (h.hom.app X.op { down := 𝟙 X })
⊢ ((Functor.cones F).map f.op (h.hom.app X.op { down := 𝟙 X })).app j =
    ((const J).map f ≫ h.hom.app X.op { down := 𝟙 X }).app j
case e_π.w.h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t✝ : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
Y : C
f : Y ⟶ X
j : J
t : h.hom.app Y.op { down := f } = (Functor.cones F).map f.op (h.hom.app X.op { down := 𝟙 X })
⊢ (h.hom.app Y.op { down := f }).app j = ((const J).map f ≫ h.hom.app X.op { down := 𝟙 X }).app j
rw [congrFun (congrArg NatTrans.app t) j]
no goals
case e_π.w.h
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t✝ : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
Y : C
f : Y ⟶ X
j : J
t : h.hom.app Y.op { down := f } = (Functor.cones F).map f.op (h.hom.app X.op { down := 𝟙 X })
⊢ ((Functor.cones F).map f.op (h.hom.app X.op { down := 𝟙 X })).app j =
    ((const J).map f ≫ h.hom.app X.op { down := 𝟙 X }).app j
rfl