-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coproducts (goal)
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
⊢ 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))
have 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)
Tactic: ext ⟨j, x⟩