-- 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
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)
have 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 := 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 j)
Tactic: funext j