-- Lean 4 proof step from Mathlib.CategoryTheory.Action.Concrete (goal)
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
⊢ 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 := ⋯ } }))
have 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 := sorry } }))
    (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 := sorry :
                      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 := sorry :
                          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 := sorry } }.pt.V)
            g)))
      x)
Tactic: ext x