-- 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))
s : Cone F
x y : (↑s.1 : Type u)
⊢ EquivLike.coe (E :=
      (↑(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)))
      (Subtype.mk (p :=
        fun
          (x :
            (j : J) →
              (F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                      carrier)).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 := TypeCat.Fun)
                (NatTrans.app
                  (Cone.π
                    (Functor.mapCone
                      (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        carrier))
                      s))
                  j) :
              (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj ((forget MonCat).mapCone s).pt).obj j)) →
                (fun (X : Type u) ↦ X) ((F ⋙ forget MonCat).obj j))
            (x * y))
        ⋯) =
    EquivLike.coe (E :=
        (↑(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)))
        (Subtype.mk (p :=
          fun
            (x :
              (j : J) →
                (F ⋙
                      forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        carrier)).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 := TypeCat.Fun)
                  (NatTrans.app
                    (Cone.π
                      (Functor.mapCone
                        (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                          carrier))
                        s))
                    j) :
                (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj ((forget MonCat).mapCone s).pt).obj j)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ forget MonCat).obj j))
              x)
          ⋯) *
      EquivLike.coe (E :=
        (↑(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)))
        (Subtype.mk (p :=
          fun
            (x :
              (j : J) →
                (F ⋙
                      forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        carrier)).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 := TypeCat.Fun)
                  (NatTrans.app
                    (Cone.π
                      (Functor.mapCone
                        (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                          carrier))
                        s))
                    j) :
                (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj ((forget MonCat).mapCone s).pt).obj j)) →
                  (fun (X : Type u) ↦ X) ((F ⋙ forget MonCat).obj j))
              y)
          ⋯)
have refine_2 : 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 (α :=
    (↑(F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).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)
    (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)
Tactic: simp [← equivShrink_mul]