-- 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))
j : J
x x_1 :
  (Types.Small.limitCone
      (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))).pt
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((Types.Small.limitCone
                  (F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                      carrier))).π.app
            j) :
        (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj (Types.Small.limitCone (F ⋙ forget MonCat)).pt).obj j)) →
          (fun (X : Type u) ↦ X) ((F ⋙ forget MonCat).obj j))
      (x * x_1) =
    HMul.hMul (α := (↑(F.obj j) : Type u)) (β := (↑(F.obj j) : Type u))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((Types.Small.limitCone
                      (F ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                          carrier))).π.app
                j) :
            (a :
                (fun (X : Type u) ↦ X) (((Functor.const J).obj (Types.Small.limitCone (F ⋙ forget MonCat)).pt).obj j)) →
              (fun (X : Type u) ↦ X) ((F ⋙ forget MonCat).obj j))
          x :
        (fun (X : Type u) ↦ X)
          ((F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).obj
            j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((Types.Small.limitCone
                      (F ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                          carrier))).π.app
                j) :
            (a :
                (fun (X : Type u) ↦ X) (((Functor.const J).obj (Types.Small.limitCone (F ⋙ forget MonCat)).pt).obj j)) →
              (fun (X : Type u) ↦ X) ((F ⋙ forget MonCat).obj j))
          x_1 :
        (fun (X : Type u) ↦ X)
          ((F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).obj
            j))
have simp : (↑(HMul.hMul (α :=
          (↑(F ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                    carrier)).sections :
            Type (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)))
          ((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)))
              x :
            (↑(F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                      carrier)).sections :
              Type (max u v)))
          ((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)))
              x_1 :
            (↑(F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                      carrier)).sections :
              Type (max u v)))) :
      (j : J) → ToType (F.obj j))
    j =
  HMul.hMul (α := (↑(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)))
            x) :
        (j : J) → ToType (F.obj j))
      j)
    ((↑((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)))
            x_1) :
        (j : J) → ToType (F.obj j))
      j)
Tactic: simp