-- 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
⊢ s.pt ⟶
    (LiftableCone.liftedCone (D := Type u) (F :=
        forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) (c := c)
        {
          liftedCone :=
            {
              pt :=
                of
                  (Types.Small.limitCone
                      (F ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                          carrier))).pt,
              π :=
                { app := fun (j : J) ↦ ofHom (limitπMonoidHom F j), naturality := ⋯ :
                  NatTrans
                    (Functor.obj (Functor.const J)
                      (of
                        (Types.Small.limitCone
                            (F ⋙
                              forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                                carrier))).pt))
                    F } :
              Cone F },
          validLift :=
            Cone.ext
              (Equiv.toIso
                (Equiv.symm
                  ((Types.isLimitEquivSections t).trans
                    (equivShrink
                      (↑(F ⋙
                              forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                                carrier)).sections :
                        Type (max u v))))))
              ⋯ :
          LiftableCone F
            (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)) c }).pt
have h : ∀ (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)
Tactic: refine ofHom
      { toFun := (Types.Small.limitConeIsLimit.{v, u} _).lift ((forget MonCat).mapCone _),
        map_one' := by simp; rfl, map_mul' := ?_ }