-- Module: Mathlib.CategoryTheory.Action.Concrete
Goal:
ι : Type v
G : Type (max v u)
inst : Monoid G
F : ι → Type (max v u)
inst_1 : (i : ι) → MulAction G (F i)
s : Cone (J := Discrete ι) (C := Action (Type (max u v)) G) (Discrete.functor fun (i : ι) ↦ ofMulAction G (F i))
g : G
x : s.pt.V
h :
  ∀ (j : ι),
    Eq (α := F j)
      (TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          (CategoryStruct.comp (Y := s.pt.V) ((s.pt.ρ : (a : G) → End s.pt.V) g)
            (↾fun (x : s.pt.V) (i : ι) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (s.π.app { as := i : Discrete ι })) :
                  (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const (Discrete ι)).obj s.pt).obj { as := i }).V) →
                    (fun (X : Type (max u v)) ↦ X)
                      ((Discrete.functor fun (i : ι) ↦ ofMulAction G (F i)).obj { as := i }).V)
                x)))
        x j)
      (TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (CategoryStruct.comp (Y :=
            V
              (Cone.pt (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ ofMulAction G (F i))
                { pt := ofMulAction G ((i : ι) → F i),
                  π :=
                    Discrete.natTrans fun (i : Discrete ι) ↦
                      {
                        hom :=
                          ↾fun
                              (x :
                                V
                                  (Functor.obj
                                    (Functor.obj (Functor.const (Discrete ι)) (ofMulAction G ((i : ι) → F i))) i)) ↦
                            x i.as,
                        comm := ⋯ :
                        Hom (Functor.obj (Functor.obj (Functor.const (Discrete ι)) (ofMulAction G ((i : ι) → F i))) i)
                          (Functor.obj (Discrete.functor fun (i : ι) ↦ ofMulAction G (F i)) i) } :
                  Cone (J := Discrete ι) (C := Action (Type (max u v)) G)
                    (Discrete.functor fun (i : ι) ↦ ofMulAction G (F i)) }))
            (↾fun (x : s.pt.V) (i : ι) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (s.π.app { as := i : Discrete ι })) :
                  (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const (Discrete ι)).obj s.pt).obj { as := i }).V) →
                    (fun (X : Type (max u v)) ↦ X)
                      ((Discrete.functor fun (i : ι) ↦ ofMulAction G (F i)).obj { as := i }).V)
                x)
            ((ρ
                  (Cone.pt (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ ofMulAction G (F i))
                    { pt := ofMulAction G ((i : ι) → F i),
                      π :=
                        Discrete.natTrans fun (i : Discrete ι) ↦
                          {
                            hom :=
                              ↾fun
                                  (x :
                                    V
                                      (Functor.obj
                                        (Functor.obj (Functor.const (Discrete ι)) (ofMulAction G ((i : ι) → F i))) i)) ↦
                                x i.as,
                            comm := ⋯ :
                            Hom
                              (Functor.obj (Functor.obj (Functor.const (Discrete ι)) (ofMulAction G ((i : ι) → F i))) i)
                              (Functor.obj (Discrete.functor fun (i : ι) ↦ ofMulAction G (F i)) i) } :
                      Cone (J := Discrete ι) (C := Action (Type (max u v)) G)
                        (Discrete.functor fun (i : ι) ↦ ofMulAction G (F i)) }) :
                (a : G) →
                  End
                    { pt := ofMulAction G ((i : ι) → F i),
                          π :=
                            Discrete.natTrans fun (i : Discrete ι) ↦
                              {
                                hom :=
                                  ↾fun
                                      (x :
                                        (((Functor.const (Discrete ι)).obj (ofMulAction G ((i : ι) → F i))).obj i).V) ↦
                                    x i.as,
                                comm := ⋯ } }.pt.V)
              g)))
        x j)
⊢ Eq (α :=
    V
      (Cone.pt (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ ofMulAction G (F i))
        { pt := ofMulAction G ((i : ι) → F i),
          π :=
            Discrete.natTrans fun (i : Discrete ι) ↦
              {
                hom :=
                  ↾fun
                      (x :
                        V (Functor.obj (Functor.obj (Functor.const (Discrete ι)) (ofMulAction G ((i : ι) → F i))) i)) ↦
                    x i.as,
                comm := ⋯ } }))
    (TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        (CategoryStruct.comp (Y := s.pt.V) ((s.pt.ρ : (a : G) → End s.pt.V) g)
          (↾fun (x : s.pt.V) (i : ι) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (s.π.app { as := i : Discrete ι })) :
                (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const (Discrete ι)).obj s.pt).obj { as := i }).V) →
                  (fun (X : Type (max u v)) ↦ X)
                    ((Discrete.functor fun (i : ι) ↦ ofMulAction G (F i)).obj { as := i }).V)
              x)))
      x)
    (TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (CategoryStruct.comp (Y :=
          V
            (Cone.pt (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ ofMulAction G (F i))
              { pt := ofMulAction G ((i : ι) → F i),
                π :=
                  Discrete.natTrans fun (i : Discrete ι) ↦
                    {
                      hom :=
                        ↾fun
                            (x :
                              V
                                (Functor.obj (Functor.obj (Functor.const (Discrete ι)) (ofMulAction G ((i : ι) → F i)))
                                  i)) ↦
                          x i.as,
                      comm := ⋯ :
                      Hom (Functor.obj (Functor.obj (Functor.const (Discrete ι)) (ofMulAction G ((i : ι) → F i))) i)
                        (Functor.obj (Discrete.functor fun (i : ι) ↦ ofMulAction G (F i)) i) } :
                Cone (J := Discrete ι) (C := Action (Type (max u v)) G)
                  (Discrete.functor fun (i : ι) ↦ ofMulAction G (F i)) }))
          (↾fun (x : s.pt.V) (i : ι) ↦
            (ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (s.π.app { as := i : Discrete ι })) :
                (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const (Discrete ι)).obj s.pt).obj { as := i }).V) →
                  (fun (X : Type (max u v)) ↦ X)
                    ((Discrete.functor fun (i : ι) ↦ ofMulAction G (F i)).obj { as := i }).V)
              x)
          ((ρ
                (Cone.pt (J := Discrete ι) (F := Discrete.functor fun (i : ι) ↦ ofMulAction G (F i))
                  { pt := ofMulAction G ((i : ι) → F i),
                    π :=
                      Discrete.natTrans fun (i : Discrete ι) ↦
                        {
                          hom :=
                            ↾fun
                                (x :
                                  V
                                    (Functor.obj
                                      (Functor.obj (Functor.const (Discrete ι)) (ofMulAction G ((i : ι) → F i))) i)) ↦
                              x i.as,
                          comm := ⋯ :
                          Hom (Functor.obj (Functor.obj (Functor.const (Discrete ι)) (ofMulAction G ((i : ι) → F i))) i)
                            (Functor.obj (Discrete.functor fun (i : ι) ↦ ofMulAction G (F i)) i) } :
                    Cone (J := Discrete ι) (C := Action (Type (max u v)) G)
                      (Discrete.functor fun (i : ι) ↦ ofMulAction G (F i)) }) :
              (a : G) →
                End
                  { pt := ofMulAction G ((i : ι) → F i),
                        π :=
                          Discrete.natTrans fun (i : Discrete ι) ↦
                            {
                              hom :=
                                ↾fun
                                    (x : (((Functor.const (Discrete ι)).obj (ofMulAction G ((i : ι) → F i))).obj i).V) ↦
                                  x i.as,
                              comm := ⋯ } }.pt.V)
            g)))
      x)

Tactic:
funext j