-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K : Functor.{w', v₁, w, u₁} J_1 C
J : Type w'
𝒥 : Category.{w, w'} J
obj : J → C
map : {X Y : J} → (X ⟶ Y) → (obj X ⟶ obj Y)
map_id : ∀ (X : J), map (𝟙 X) = 𝟙 (obj X)
map_comp : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = map f ≫ map g
c : Cocone { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C }
h :
  IsColimit (F :=
    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } ⋙ 𝟭 C)
    (Functor.mapCocone (𝟭 C) c)
mk :
  ∀ (pt : C)
    (app :
      (X : J) →
        { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C }.obj X ⟶
          Functor.obj.{w, v₁, w', u₁} (Functor.obj (Functor.const J) pt) X)
    (naturality :
      ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
        { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C }.map f ≫
            app Y =
          app X ≫ Functor.map (Functor.obj (Functor.const J) pt) f)
    (h :
      IsColimit (F :=
        { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } ⋙ 𝟭 C)
        (Functor.mapCocone (𝟭 C)
          { pt := pt,
            ι :=
              { app := app, naturality := naturality :
                NatTrans
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C }
                  (Functor.obj (Functor.const J) pt) } }))
    (s : Cocone { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C })
    (m :
      { pt := pt,
            ι :=
              { app := app, naturality := naturality :
                NatTrans
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C }
                  (Functor.obj (Functor.const J) pt) } :
            Cocone
              { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } }.pt ⟶
        s.pt),
    (∀ (j : J),
        { pt := pt,
                    ι :=
                      { app := app, naturality := naturality :
                        NatTrans
                          { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                            Functor.{w, v₁, w', u₁} J C }
                          (Functor.obj (Functor.const J) pt) } :
                    Cocone
                      { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                        Functor.{w, v₁, w', u₁} J C } }.ι.app
              j ≫
            m =
          s.ι.app j) →
      m =
        (fun
              (s :
                Cocone
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C }) ↦
            (h.desc { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } } :
              Cocone.pt (F :=
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } ⋙
                    𝟭 C)
                  (Functor.mapCocone (𝟭 C)
                    { pt := pt,
                      ι :=
                        { app := app, naturality := naturality :
                          NatTrans
                            { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                              Functor.{w, v₁, w', u₁} J C }
                            (Functor.obj (Functor.const J) pt) } :
                      Cocone
                        { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                          Functor.{w, v₁, w', u₁} J C } }) ⟶
                Cocone.pt.{w, v₁, w', u₁} (J := J) (F :=
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } ⋙
                    𝟭 C)
                  { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } }))
          s
⊢ ∀ (s : Cocone { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C })
    (m : c.pt ⟶ s.pt),
    (∀ (j : J), c.ι.app j ≫ m = s.ι.app j) →
      m =
        (fun
              (s :
                Cocone
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C }) ↦
            (h.desc { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } } :
              Cocone.pt (F :=
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } ⋙
                    𝟭 C)
                  (Functor.mapCocone (𝟭 C) c) ⟶
                Cocone.pt.{w, v₁, w', u₁} (J := J) (F :=
                  { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } ⋙
                    𝟭 C)
                  { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } }))
          s

Tactic:
rcases c with ⟨_, _, _⟩