-- 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 : Cone { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C }
h : IsLimit c
mk :
  ∀ (pt : C)
    (app :
      (X : J) →
        Functor.obj.{w', v₁, w, u₁} (Functor.obj (Functor.const J) pt) X ⟶
          { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C }.obj X)
    (naturality :
      ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
        Functor.map (Functor.obj (Functor.const J) pt) f ≫ app Y =
          app X ≫ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp }.map f)
    (h :
      IsLimit
        { pt := pt,
          π :=
            { app := app, naturality := naturality :
              NatTrans (Functor.obj (Functor.const J) pt)
                { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } } :
          Cone { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } })
    (s :
      Cone ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙ 𝟭 C))
    (m :
      s.pt ⟶
        Cone.pt (F :=
          { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙ 𝟭 C)
          (Functor.mapCone (𝟭 C)
            { pt := pt,
              π :=
                { app := app, naturality := naturality :
                  NatTrans (Functor.obj (Functor.const J) pt)
                    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                      Functor.{w', v₁, w, u₁} J C } } })),
    (∀ (j : J),
        m ≫
            NatTrans.app
              (Cone.π
                (Functor.mapCone (𝟭 C)
                  { pt := pt,
                    π :=
                      { app := app, naturality := naturality :
                        NatTrans (Functor.obj (Functor.const J) pt)
                          { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                            Functor.{w', v₁, w, u₁} J C } } }))
              j =
          s.π.app j) →
      m =
        (fun
              (s :
                Cone
                  ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙
                    𝟭 C)) ↦
            (h.lift { pt := s.pt, π := { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ } } :
              Cone.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 })
                  { pt := s.pt,
                    π :=
                      { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ :
                        NatTrans (Functor.obj (Functor.const J) s.pt)
                          { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                            Functor.{w', v₁, w, u₁} J C } } :
                    Cone
                      { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                        Functor.{w', v₁, w, u₁} J C } } ⟶
                { pt := pt,
                    π :=
                      { app := app, naturality := naturality :
                        NatTrans (Functor.obj (Functor.const J) pt)
                          { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                            Functor.{w', v₁, w, u₁} J C } } :
                    Cone
                      { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                        Functor.{w', v₁, w, u₁} J C } }.pt))
          s
⊢ ∀
    (s :
      Cone ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙ 𝟭 C))
    (m :
      s.pt ⟶
        Cone.pt (F :=
          { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙ 𝟭 C)
          (Functor.mapCone (𝟭 C) c)),
    (∀ (j : J), m ≫ NatTrans.app (Cone.π (Functor.mapCone (𝟭 C) c)) j = s.π.app j) →
      m =
        (fun
              (s :
                Cone
                  ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙
                    𝟭 C)) ↦
            (h.lift { pt := s.pt, π := { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ } } :
              Cone.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 })
                  { pt := s.pt,
                    π :=
                      { app := fun (j : J) ↦ s.π.app j, naturality := ⋯ :
                        NatTrans (Functor.obj (Functor.const J) s.pt)
                          { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                            Functor.{w', v₁, w, u₁} J C } } :
                    Cone
                      { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                        Functor.{w', v₁, w, u₁} J C } } ⟶
                c.pt))
          s

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