-- 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
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 (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 } } })
pt_1 : C
app_1 :
  (X : J) →
    Functor.obj.{w, v₁, w', u₁} (Functor.obj (Functor.const J) pt_1) X ⟶
      { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C }.obj X
naturality_1 :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    Functor.map (Functor.obj (Functor.const J) pt_1) f ≫ app_1 Y =
      app_1 X ≫ { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp }.map f
m :
  { pt := pt_1,
        π :=
          { app := app_1, naturality := naturality_1 :
            NatTrans (Functor.obj (Functor.const J) pt_1)
              { 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 := 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
w :
  ∀ (j : J),
    m ≫
        { 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 } }.π.app
          j =
      { pt := pt_1,
              π :=
                { app := app_1, naturality := naturality_1 :
                  NatTrans (Functor.obj (Functor.const J) pt_1)
                    { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                      Functor.{w, v₁, w', u₁} J C } } }.π.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 }) ↦
        (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 } ⋙ 𝟭 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 } ⋙
                        𝟭 C) } :
                Cone
                  ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } ⋙
                    𝟭 C) } ⟶
            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 } } })))
      { pt := pt_1,
        π :=
          { app := app_1, naturality := naturality_1 :
            NatTrans (Functor.obj (Functor.const J) pt_1)
              { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w, v₁, w', u₁} J C } } }

Tactic:
h.uniq _ m w

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Limits.IsLimit.uniq