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
s : Cone F
⊢ { pt := s.pt, π := h.hom.app s.pt.op { down := (h.inv.app s.pt.op 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 : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
s : Cone F
⊢ coneOfHom h (homOfCone h s) = s
dsimp [coneOfHom, homOfCone]
no goals
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
s : Cone F
⊢ { pt := s.pt, π := h.hom.app s.pt.op { down := (h.inv.app s.pt.op s.π).down } } = s
match s with
| .mk s_pt s_π =>
  congr; dsimp
  convert congrFun (congrFun (congrArg NatTrans.app h.inv_hom_id) (op s_pt)) s_π using 1
case e_π
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
s : Cone F
s_pt : C
s_π : (const J).obj s_pt ⟶ F
⊢ h.hom.app { pt := s_pt, π := s_π }.pt.op
      { down := (h.inv.app { pt := s_pt, π := s_π }.pt.op { 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 : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
s : Cone F
s_pt : C
s_π : (const J).obj s_pt ⟶ F
⊢ { pt := { pt := s_pt, π := s_π }.pt,
      π :=
        h.hom.app { pt := s_pt, π := s_π }.pt.op
          { down := (h.inv.app { pt := s_pt, π := s_π }.pt.op { 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 : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
s : Cone F
s_pt : C
s_π : (const J).obj s_pt ⟶ F
⊢ h.hom.app s_pt.op { down := (h.inv.app s_pt.op 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 : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
s : Cone F
s_pt : C
s_π : (const J).obj s_pt ⟶ F
⊢ h.hom.app { pt := s_pt, π := s_π }.pt.op
      { down := (h.inv.app { pt := s_pt, π := s_π }.pt.op { 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 : Cone F
X : C
h : yoneda.obj X ⋙ uliftFunctor ≅ Functor.cones F
s : Cone F
s_pt : C
s_π : (const J).obj s_pt ⟶ F
⊢ h.hom.app s_pt.op { down := (h.inv.app s_pt.op s_π).down } = s_π
convert congrFun (congrFun (congrArg NatTrans.app h.inv_hom_id) (op s_pt)) s_π using 1