-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.Limits (goal)
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J MonCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections :
      Type (max u v))
c : Cone (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
t : IsLimit c
this :
  Small.{u, max u v}
    (↑(F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections :
      Type (max u v))
s : Cone F
x y : (↑s.1 : Type u)
⊢ (fun (j : J) ↦
      HMul.hMul (α := (↑(F.obj j) : Type u)) (β := (↑(F.obj j) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                (s.π.app j) :
              (a : (↑s.pt : Type u)) → (↑(F.obj j) : Type u))
            x :
          (↑(F.obj j) : Type u))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                (s.π.app j) :
              (a : (↑s.pt : Type u)) → (↑(F.obj j) : Type u))
            y :
          (↑(F.obj j) : Type u))) =
    HMul.hMul (α := (j : J) → (↑(F.obj j) : Type u))
      (↑((Equiv.symm
                (equivShrink
                  (↑(F ⋙
                          forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                            carrier)).sections :
                    Type (max u v))) :
              (a : Shrink.{u, max u v} (↑(F ⋙ forget MonCat).sections : Type (max u v))) →
                (↑(F ⋙ forget MonCat).sections : Type (max u v)))
            ((equivShrink
                  (↑(F ⋙
                          forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                            carrier)).sections :
                    Type (max u v)) :
                (a : (↑(F ⋙ forget MonCat).sections : Type (max u v))) →
                  Shrink.{u, max u v} (↑(F ⋙ forget MonCat).sections : Type (max u v)))
              (Subtype.mk (p :=
                fun
                  (x :
                    (j : J) →
                      ToType (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                        (F.obj j)) ↦
                x ∈
                  (F ⋙
                      forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        carrier)).sections)
                (fun (j : J) ↦
                  (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        carrier) (s.π.app j) :
                      (a : (↑s.pt : Type u)) → (↑(F.obj j) : Type u))
                    x)
                ⋯))) :
        (j : J) → (↑(F.obj j) : Type u))
      (↑((Equiv.symm
                (equivShrink
                  (↑(F ⋙
                          forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                            carrier)).sections :
                    Type (max u v))) :
              (a : Shrink.{u, max u v} (↑(F ⋙ forget MonCat).sections : Type (max u v))) →
                (↑(F ⋙ forget MonCat).sections : Type (max u v)))
            ((equivShrink
                  (↑(F ⋙
                          forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                            carrier)).sections :
                    Type (max u v)) :
                (a : (↑(F ⋙ forget MonCat).sections : Type (max u v))) →
                  Shrink.{u, max u v} (↑(F ⋙ forget MonCat).sections : Type (max u v)))
              (Subtype.mk (p :=
                fun
                  (x :
                    (j : J) →
                      ToType (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                        (F.obj j)) ↦
                x ∈
                  (F ⋙
                      forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        carrier)).sections)
                (fun (j : J) ↦
                  (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        carrier) (s.π.app j) :
                      (a : (↑s.pt : Type u)) → (↑(F.obj j) : Type u))
                    y)
                ⋯))) :
        (j : J) → (↑(F.obj j) : Type u))
have h : (fun (j : J) ↦
    HMul.hMul (α := (↑(F.obj j) : Type u)) (β := (↑(F.obj j) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
              (s.π.app j) :
            (a : (↑s.pt : Type u)) → (↑(F.obj j) : Type u))
          x :
        (↑(F.obj j) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
              (s.π.app j) :
            (a : (↑s.pt : Type u)) → (↑(F.obj j) : Type u))
          y :
        (↑(F.obj j) : Type u))) =
  HMul.hMul (α := (j : J) → (↑(F.obj j) : Type u))
    (fun (j : J) ↦
      (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
            (s.π.app j) :
          (a : (↑s.pt : Type u)) → (↑(F.obj j) : Type u))
        x)
    fun (j : J) ↦
    (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
          (s.π.app j) :
        (a : (↑s.pt : Type u)) → (↑(F.obj j) : Type u))
      y
Tactic: simp only [Functor.comp_obj, Equiv.symm_apply_apply]