-- 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
    { 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)
j : J
mk :
  ∀ (pt_1 : C)
    (π :
      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 } ⋙ 𝟭 C),
    CategoryStruct.comp (Y :=
        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 } } }))
        ((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))
            { pt := pt_1, π := π } :
          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 :=
                  { pt := pt_1, π := π :
                      Cone
                        ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                            Functor.{w', v₁, w, u₁} J C } ⋙
                          𝟭 C) }.pt,
                π :=
                  {
                    app := fun (j : J) ↦
                      { pt := pt_1, π := π :
                              Cone
                                ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                                    Functor.{w', v₁, w, u₁} J C } ⋙
                                  𝟭 C) }.π.app
                        j,
                    naturality := ⋯ :
                    NatTrans
                      (Functor.obj (Functor.const J)
                        { pt := pt_1, π := π :
                            Cone
                              ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                                  Functor.{w', v₁, w, u₁} J C } ⋙
                                𝟭 C) }.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)
        (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 :
          Functor.obj.{w', v₁, w, u₁}
              (Functor.obj (Functor.const J)
                (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 } } :
                      Cone
                        { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                          Functor.{w', v₁, w, u₁} J C } })))
              j ⟶
            ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙
                  𝟭 C).obj
              j) =
      { pt := pt_1, π := π :
              Cone
                ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙
                  𝟭 C) }.π.app
        j
⊢ CategoryStruct.comp (Y :=
      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 } } }))
      ((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 :
        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)
      (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 :
        Functor.obj.{w', v₁, w, u₁}
            (Functor.obj (Functor.const J)
              (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 } } :
                    Cone
                      { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                        Functor.{w', v₁, w, u₁} J C } })))
            j ⟶
          ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙ 𝟭 C).obj
            j) =
    s.π.app j

Tactic:
cases s