-- 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))
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
⊢ 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 := ⋯ }
have 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 := sorry :
            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 := 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)) }) }))
      x
Tactic: ext x