-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem coconeOfHom_homOfCocone (s : Cocone F) : coconeOfHom h (homOfCocone h s) = s

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
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_ι }

Tactic:
congr

Result:
case e_ι
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
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_ι

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
s : Cocone F
⊢ coconeOfHom h (homOfCocone h s) = s

Tactic:
dsimp [coconeOfHom, homOfCocone]

Result:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
s : Cocone F
⊢ { pt := s.pt, ι := h.hom.app s.pt { down := (h.inv.app s.pt s.ι).down } } = s

Proof state:
case e_ι
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
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_ι

Tactic:
dsimp

Result:
case e_ι
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
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_ι

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
s : Cocone F
⊢ { pt := s.pt, ι := h.hom.app s.pt { down := (h.inv.app s.pt s.ι).down } } = s

Tactic:
have ⟨s_pt,s_ι⟩ := s

Result:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
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_ι }

Proof state:
case e_ι
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
X : C
h : coyoneda.obj (op X) ⋙ uliftFunctor.{u₁, v₃} ≅ F.cocones
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_ι

Tactic:
convert congrFun (congrFun (congrArg NatTrans.app h.inv_hom_id) s_pt) s_ι using 1

Result:
no goals