-- 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
x : s.pt.V
j : ι
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) f.hom).toFun x j =
    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 j
have h₁ : Eq (α := F j)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) f.hom : (a : s.pt.V) → (ofMulAction G ((i : ι) → F i)).V) x j : F j)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (Hom.hom (s.π.app { as := j : Discrete ι })) :
        (a : s.pt.V) → (ofMulAction G (F j)).V)
      x :
    V (ofMulAction G (F j)))
Tactic: dsimp at *