-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
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) →
    { 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
    { 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 } }
s : Cocone ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙ 𝟭 C)
m :
  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 } }) ⟶
    s.pt
w :
  ∀ (j : J),
    NatTrans.app
          (Cocone.ι
            (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) } }))
          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 } ⋙
                𝟭 C)) ↦
        (h.desc { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } } :
          { 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 ⟶
            Cocone.pt.{w', v₁, w, u₁} (J := J) (F :=
              { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp })
              { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := ⋯ } }))
      s
have mk : ∀ (pt_1 : C)
  (app_1 :
    (X : J) →
      ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙ 𝟭 C).obj X ⟶
        Functor.obj.{w', v₁, w, u₁} (Functor.obj (Functor.const J) pt_1) X)
  (naturality_1 :
    ∀ ⦃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 } ⋙ 𝟭 C).map f ≫
          app_1 Y =
        app_1 X ≫ Functor.map (Functor.obj (Functor.const J) pt_1) f)
  (m :
    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 } }) ⟶
      { pt := pt_1,
          ι :=
            { app := app_1, naturality := naturality_1 :
              NatTrans
                ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙
                  𝟭 C)
                (Functor.obj (Functor.const J) pt_1) } :
          Cocone
            ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙
              𝟭 C) }.pt)
  (w :
    ∀ (j : J),
      NatTrans.app
            (Cocone.ι
              (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) } }))
            j ≫
          m =
        { pt := pt_1,
                ι :=
                  { app := app_1, naturality := naturality_1 :
                    NatTrans
                      ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp :
                          Functor.{w', v₁, w, u₁} J C } ⋙
                        𝟭 C)
                      (Functor.obj (Functor.const J) pt_1) } :
                Cocone
                  ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙
                    𝟭 C) }.ι.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 } ⋙
                𝟭 C)) ↦
        (h.desc { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := sorry } } :
          { 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 ⟶
            Cocone.pt.{w', v₁, w, u₁} (J := J) (F :=
              { obj := obj, map := @map, map_id := map_id, map_comp := @map_comp })
              { pt := s.pt, ι := { app := fun (j : J) ↦ s.ι.app j, naturality := sorry } }))
      { pt := pt_1,
        ι :=
          { app := app_1, naturality := naturality_1 :
            NatTrans
              ({ obj := obj, map := @map, map_id := map_id, map_comp := @map_comp : Functor.{w', v₁, w, u₁} J C } ⋙ 𝟭 C)
              (Functor.obj (Functor.const J) pt_1) } }
Tactic: rcases s with ⟨_, _, _⟩
Cleared hypotheses: s, m, w