-- 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
h :
  ∀ (x : s.pt.V),
    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)
⊢ Eq (α :=
    s.pt.V ⟶
      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 := ⋯ } }))
    (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) :
      s.pt.V ⟶
        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 := ⋯ } }))
    (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 := ⋯ } }))
        (↾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 := ⋯ } }) :
            (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) :
      s.pt.V ⟶
        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 := ⋯ } }))

Tactic:
ext x