-- 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)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          (IsLimit.lift
            (Types.Small.limitConeIsLimit
              (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)))
            (Functor.mapCone
              (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) s)) :
        (a : (fun (X : Type u) ↦ X) ((forget MonCat).mapCone s).pt) →
          (fun (X : Type u) ↦ X) (Types.Small.limitCone (F ⋙ forget MonCat)).pt)
      (x * y) =
    HMul.hMul (α :=
      (Types.Small.limitCone
          (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))).pt)
      (β :=
      (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)
              (IsLimit.lift
                (Types.Small.limitConeIsLimit
                  (F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)))
                (Functor.mapCone
                  (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
                  s)) :
            (a : (fun (X : Type u) ↦ X) ((forget MonCat).mapCone s).pt) →
              (fun (X : Type u) ↦ X) (Types.Small.limitCone (F ⋙ forget MonCat)).pt)
          x :
        (fun (X : Type u) ↦ X)
          (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)
              (IsLimit.lift
                (Types.Small.limitConeIsLimit
                  (F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)))
                (Functor.mapCone
                  (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
                  s)) :
            (a : (fun (X : Type u) ↦ X) ((forget MonCat).mapCone s).pt) →
              (fun (X : Type u) ↦ X) (Types.Small.limitCone (F ⋙ forget MonCat)).pt)
          y :
        (fun (X : Type u) ↦ X)
          (Types.Small.limitCone
              (F ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))).pt)
have h : (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) ↦
        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)))
      sorry) =
  HMul.hMul (α :=
    Shrink.{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)))
    (β :=
    Shrink.{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)))
    ((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)
          sorry) :
      Shrink.{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)))
    ((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)
          sorry) :
      Shrink.{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)))
Tactic: simp only [Types.Small.limitCone_pt, Functor.comp_obj, Functor.mapCone_pt,
        Types.Small.limitConeIsLimit_lift, Functor.const_obj_obj, Functor.mapCone_π_app,
        ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, map_mul]