J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
s : Cocone F
⊢ { pt := s.pt, ι := h.hom.app s.pt { down := (h.inv.app s.pt s.ι).down } } = s
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
s : Cocone F
⊢ coconeOfHom h (homOfCocone h s) = s
dsimp [coconeOfHom, homOfCocone]
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
s : Cocone F
s_pt : C
s_ι : F ⟶ (const J).obj s_pt
⊢ { pt := { pt := s_pt, ι := s_ι }.pt,
      ι :=
        h.hom.app { pt := s_pt, ι := s_ι }.pt
          { down := (h.inv.app { pt := s_pt, ι := s_ι }.pt { pt := s_pt, ι := s_ι }.ι).down } } =
    { pt := s_pt, ι := s_ι }
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
s : Cocone F
⊢ { pt := s.pt, ι := h.hom.app s.pt { down := (h.inv.app s.pt s.ι).down } } = s
have ⟨s_pt,s_ι⟩ := s
case e_ι
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
s : Cocone F
s_pt : C
s_ι : F ⟶ (const J).obj s_pt
⊢ h.hom.app { pt := s_pt, ι := s_ι }.pt
      { down := (h.inv.app { pt := s_pt, ι := s_ι }.pt { pt := s_pt, ι := s_ι }.ι).down } =
    s_ι
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
s : Cocone F
s_pt : C
s_ι : F ⟶ (const J).obj s_pt
⊢ { pt := { pt := s_pt, ι := s_ι }.pt,
      ι :=
        h.hom.app { pt := s_pt, ι := s_ι }.pt
          { down := (h.inv.app { pt := s_pt, ι := s_ι }.pt { pt := s_pt, ι := s_ι }.ι).down } } =
    { pt := s_pt, ι := s_ι }
congr
case e_ι
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
s : Cocone F
s_pt : C
s_ι : F ⟶ (const J).obj s_pt
⊢ h.hom.app s_pt { down := (h.inv.app s_pt s_ι).down } = s_ι
case e_ι
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
s : Cocone F
s_pt : C
s_ι : F ⟶ (const J).obj s_pt
⊢ h.hom.app { pt := s_pt, ι := s_ι }.pt
      { down := (h.inv.app { pt := s_pt, ι := s_ι }.pt { pt := s_pt, ι := s_ι }.ι).down } =
    s_ι
dsimp
no goals
case e_ι
J : Type u₁
inst✝² : Category J
K : Type u₂
inst✝¹ : Category K
C : Type u₃
inst✝ : Category C
F : J ⥤ C
t : Cocone F
X : C
h : coyoneda.obj X.op ⋙ uliftFunctor ≅ Functor.cocones F
s : Cocone F
s_pt : C
s_ι : F ⟶ (const J).obj s_pt
⊢ h.hom.app s_pt { down := (h.inv.app s_pt s_ι).down } = s_ι
convert congrFun (congrFun (congrArg NatTrans.app h.inv_hom_id) s_pt) s_ι using 1