-- Module: Mathlib.CategoryTheory.Limits.Types.Coproducts
Goal:
C : Type u
F_1 : C → Type v
J : Type v
F : J → Type (max v u)
s : Cocone (Discrete.functor F)
m :
  Cocone.pt (J := Discrete J) (F := Discrete.functor F)
      { pt := (j : J) × F j,
        ι :=
          Discrete.natTrans fun (x : Discrete J) ↦
            match (motive :=
              (x : Discrete J) →
                Functor.obj (Discrete.functor F) x ⟶
                  Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) × F j)) x)
              x with
            | { as := j } =>
              ↾fun (x : Functor.obj (Discrete.functor F) { as := j : Discrete J }) ↦
                Sigma.mk (β := fun (j : J) ↦ F j) j x :
        Cocone (Discrete.functor F) } ⟶
    s.pt
w :
  ∀ (j : Discrete J),
    NatTrans.app
          (Cocone.ι
            { pt := (j : J) × F j,
              ι :=
                Discrete.natTrans fun (x : Discrete J) ↦
                  match (motive :=
                    (x : Discrete J) →
                      Functor.obj (Discrete.functor F) x ⟶
                        Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) × F j)) x)
                    x with
                  | { as := j } =>
                    ↾fun (x : Functor.obj (Discrete.functor F) { as := j : Discrete J }) ↦
                      Sigma.mk (β := fun (j : J) ↦ F j) j x })
          j ≫
        m =
      s.ι.app j
h :
  ∀ (j : J) (x : F j),
    (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun (Sigma.mk (β := fun (j : J) ↦ F j) j x) =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾fun
              (x :
                Cocone.pt (J := Discrete J) (F := Discrete.functor F)
                  { pt := (j : J) × F j,
                    ι :=
                      Discrete.natTrans fun (x : Discrete J) ↦
                        match (motive :=
                          (x : Discrete J) →
                            Functor.obj (Discrete.functor F) x ⟶
                              Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) × F j)) x)
                          x with
                        | { as := j } =>
                          ↾fun (x : Functor.obj (Discrete.functor F) { as := j : Discrete J }) ↦
                            Sigma.mk (β := fun (j : J) ↦ F j) j x :
                    Cocone (Discrete.functor F) }) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app { as := x.fst (β := fun (j : J) ↦ F j) : Discrete J }) :
                (a : (fun (X : Type (max u v)) ↦ X) ((Discrete.functor F).obj { as := x.fst })) →
                  (fun (X : Type (max u v)) ↦ X) (((Functor.const (Discrete J)).obj s.pt).obj { as := x.fst }))
              (x.snd (β := fun (j : J) ↦ F j))))
        (Sigma.mk (β := fun (j : J) ↦ F j) j x)
⊢ m =
    ↾fun
        (x :
          Cocone.pt (J := Discrete J) (F := Discrete.functor F)
            { pt := (j : J) × F j,
              ι :=
                Discrete.natTrans fun (x : Discrete J) ↦
                  match (motive :=
                    (x : Discrete J) →
                      Functor.obj (Discrete.functor F) x ⟶
                        Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) × F j)) x)
                    x with
                  | { as := j } =>
                    ↾fun (x : Functor.obj (Discrete.functor F) { as := j : Discrete J }) ↦
                      Sigma.mk (β := fun (j : J) ↦ F j) j x }) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (s.ι.app { as := x.fst (β := fun (j : J) ↦ F j) : Discrete J }) :
          (a : (fun (X : Type (max u v)) ↦ X) ((Discrete.functor F).obj { as := x.fst })) →
            (fun (X : Type (max u v)) ↦ X) (((Functor.const (Discrete J)).obj s.pt).obj { as := x.fst }))
        (x.snd (β := fun (j : J) ↦ F j))

Tactic:
ext ⟨j, x⟩