-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
J : Type v
F : J → Type u
inst : Small.{u, v} J
this : Small.{u, max u v} ((j : J) → F j)
s : Cone (Discrete.functor F)
m :
  s.pt ⟶
    Cone.pt.{v, u, v, u + 1} (J := Discrete J) (F := Discrete.functor F)
      { pt := Shrink.{u, max u v} ((j : J) → F j),
        π :=
          Discrete.natTrans fun (x : Discrete J) ↦
            match (motive :=
              (x : Discrete J) →
                Functor.obj (Functor.obj (Functor.const (Discrete J)) (Shrink.{u, max u v} ((j : J) → F j))) x ⟶
                  Functor.obj (Discrete.functor F) x)
              x with
            | { as := j } =>
              ↾fun
                  (f :
                    Functor.obj (Functor.obj (Functor.const (Discrete J)) (Shrink.{u, max u v} ((j : J) → F j)))
                      { as := j : Discrete J }) ↦
                (Equiv.symm (equivShrink ((j : J) → F j)) : (a : Shrink.{u, max u v} ((j : J) → F j)) → (j : J) → F j) f
                  j }
w :
  ∀ (j : Discrete J),
    m ≫
        NatTrans.app
          (Cone.π
            { pt := Shrink.{u, max u v} ((j : J) → F j),
              π :=
                Discrete.natTrans fun (x : Discrete J) ↦
                  match (motive :=
                    (x : Discrete J) →
                      Functor.obj (Functor.obj (Functor.const (Discrete J)) (Shrink.{u, max u v} ((j : J) → F j))) x ⟶
                        Functor.obj (Discrete.functor F) x)
                    x with
                  | { as := j } =>
                    ↾fun
                        (f :
                          Functor.obj (Functor.obj (Functor.const (Discrete J)) (Shrink.{u, max u v} ((j : J) → F j)))
                            { as := j : Discrete J }) ↦
                      (Equiv.symm (equivShrink ((j : J) → F j)) :
                          (a : Shrink.{u, max u v} ((j : J) → F j)) → (j : J) → F j)
                        f j })
          j =
      s.π.app j
x : s.pt
j : J
⊢ Eq.{u + 1} (α := F j)
    ((Equiv.symm (equivShrink ((x : J) → F x)) : (a : Shrink.{u, max u v} ((x : J) → F x)) → (x : J) → F x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) m :
              (a : s.pt) →
                { pt := Shrink.{u, max u v} ((j : J) → F j),
                    π :=
                      Discrete.natTrans fun (x : Discrete J) ↦
                        match (motive :=
                          (x : Discrete J) →
                            ((Functor.const (Discrete J)).obj (Shrink.{u, max u v} ((j : J) → F j))).obj x ⟶
                              (Discrete.functor F).obj x)
                          x with
                        | { as := j } =>
                          ↾fun
                              (f :
                                ((Functor.const (Discrete J)).obj (Shrink.{u, max u v} ((j : J) → F j))).obj
                                  { as := j }) ↦
                            ((equivShrink ((j : J) → F j)).symm :
                                (a : Shrink.{u, max u v} ((j : J) → F j)) → (j : J) → F j)
                              f j }.pt)
            x :
          Cone.pt.{v, u, v, u + 1} (J := Discrete J) (F := Discrete.functor F)
            { pt := Shrink.{u, max u v} ((j : J) → F j),
              π :=
                Discrete.natTrans fun (x : Discrete J) ↦
                  match (motive :=
                    (x : Discrete J) →
                      Functor.obj (Functor.obj (Functor.const (Discrete J)) (Shrink.{u, max u v} ((j : J) → F j))) x ⟶
                        Functor.obj (Discrete.functor F) x)
                    x with
                  | { as := j } =>
                    ↾fun
                        (f :
                          Functor.obj (Functor.obj (Functor.const (Discrete J)) (Shrink.{u, max u v} ((j : J) → F j)))
                            { as := j : Discrete J }) ↦
                      (Equiv.symm (equivShrink ((j : J) → F j)) :
                          (a : Shrink.{u, max u v} ((j : J) → F j)) → (j : J) → F j)
                        f j })
        j :
      F j)
    ((Equiv.symm (equivShrink ((x : J) → F x)) : (a : Shrink.{u, max u v} ((x : J) → F x)) → (x : J) → F x)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (↾fun (x : s.pt) ↦
                  (equivShrink ((j : J) → F j) : (a : (j : J) → F j) → Shrink.{u, max u v} ((j : J) → F j))
                    fun (j : J) ↦
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (s.π.app { as := j : Discrete J }) :
                        (a : (fun (X : Type u) ↦ X) (((Functor.const (Discrete J)).obj s.pt).obj { as := j })) →
                          (fun (X : Type u) ↦ X) ((Discrete.functor F).obj { as := j }))
                      x) :
              (a : s.pt) →
                { pt := Shrink.{u, max u v} ((j : J) → F j),
                    π :=
                      Discrete.natTrans fun (x : Discrete J) ↦
                        match (motive :=
                          (x : Discrete J) →
                            ((Functor.const (Discrete J)).obj (Shrink.{u, max u v} ((j : J) → F j))).obj x ⟶
                              (Discrete.functor F).obj x)
                          x with
                        | { as := j } =>
                          ↾fun
                              (f :
                                ((Functor.const (Discrete J)).obj (Shrink.{u, max u v} ((j : J) → F j))).obj
                                  { as := j }) ↦
                            ((equivShrink ((j : J) → F j)).symm :
                                (a : Shrink.{u, max u v} ((j : J) → F j)) → (j : J) → F j)
                              f j }.pt)
            x :
          Cone.pt.{v, u, v, u + 1} (J := Discrete J) (F := Discrete.functor F)
            { pt := Shrink.{u, max u v} ((j : J) → F j),
              π :=
                Discrete.natTrans fun (x : Discrete J) ↦
                  match (motive :=
                    (x : Discrete J) →
                      Functor.obj (Functor.obj (Functor.const (Discrete J)) (Shrink.{u, max u v} ((j : J) → F j))) x ⟶
                        Functor.obj (Discrete.functor F) x)
                    x with
                  | { as := j } =>
                    ↾fun
                        (f :
                          Functor.obj (Functor.obj (Functor.const (Discrete J)) (Shrink.{u, max u v} ((j : J) → F j)))
                            { as := j : Discrete J }) ↦
                      (Equiv.symm (equivShrink ((j : J) → F j)) :
                          (a : Shrink.{u, max u v} ((j : J) → F j)) → (j : J) → F j)
                        f j })
        j :
      F j)

Tactic:
simpa using ConcreteCategory.congr_hom (w ⟨j⟩) x

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.ConcreteCategory.congr_hom