-- 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))
f :
  s.pt ⟶
    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 := ⋯ } }
h :
  ∀ (j : Discrete ι),
    f ≫
        NatTrans.app
          (Cone.π
            { 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 := ⋯ } })
          j =
      s.π.app j
h₁ :
  ∀ (x : s.pt.V),
    (ConcreteCategory.hom (FC := TypeCat.Fun) f.hom).toFun x =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Hom.hom
            {
              hom :=
                ↾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,
              comm := ⋯ :
              s.pt.Hom
                (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)) }) }))
        x
⊢ f =
    {
      hom :=
        ↾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,
      comm := ⋯ }

Tactic:
ext x