-- 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)
⊢ (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)))
        ⋯) =
    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)
            ⋯) :
        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)
            ⋯) :
        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)))
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))
    (↑((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)
              sorry))) :
      (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)
              sorry))) :
      (j : J) → (↑(F.obj j) : Type u))
Tactic: congr