-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
t : Cocone F
i : J
x : (↑(F.obj i) : Type (max u v))
j : J
y : (↑(F.obj j) : Type (max u v))
⊢ (F ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier)).descColimitType
      (((F ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  carrier)).coconeTypesEquiv.symm :
          (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
        (Functor.mapCocone
          (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier))
          t))
      (M.mk F
        (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) (IsFiltered.max i j)
          (HMul.hMul (α := (↑(F.obj (IsFiltered.max i j)) : Type (max u v))) (β :=
            (↑(F.obj (IsFiltered.max i j)) : Type (max u v)))
            ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                    (CC := carrier) (Y := F.obj (IsFiltered.max i j)) (F.map (IsFiltered.leftToMax i j)) :
                  (a : (↑(F.obj ⟨i, x⟩.fst) : Type (max u v))) → (↑(F.obj (IsFiltered.max i j)) : Type (max u v)))
                (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                  (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x)) :
              (↑(F.obj (IsFiltered.max i j)) : Type (max u v)))
            ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                    (CC := carrier) (Y := F.obj (IsFiltered.max i j)) (F.map (IsFiltered.rightToMax i j)) :
                  (a : (↑(F.obj ⟨j, y⟩.fst) : Type (max u v))) → (↑(F.obj (IsFiltered.max i j)) : Type (max u v)))
                (Sigma.snd (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v)))
                  (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j y)) :
              (↑(F.obj (IsFiltered.max i j)) : Type (max u v)))))) =
    HMul.hMul (α := (↑t.1 : Type (max u v))) (β := (↑t.1 : Type (max u v)))
      ((F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier)).descColimitType
          (((F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier)).coconeTypesEquiv.symm :
              (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
            (Functor.mapCocone
              (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier))
              t))
          (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) i x)) :
        Functor.CoconeTypes.pt (J := J) (F :=
          F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier))
          (((F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier)).coconeTypesEquiv.symm :
              (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
            (Functor.mapCocone
              (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier))
              t)))
      ((F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier)).descColimitType
        (((F ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    carrier)).coconeTypesEquiv.symm :
            (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
          (Functor.mapCocone
            (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier))
            t))
        (M.mk F (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) j y)))
have dsimp : (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier)
        (X := F.obj (IsFiltered.max i j)) (t.ι.app (IsFiltered.max i j)) :
      (a : (↑(F.obj (IsFiltered.max i j)) : Type (max u v))) → (↑t.pt : Type (max u v)))
    (HMul.hMul (α := (↑(F.obj (IsFiltered.max i j)) : Type (max u v))) (β :=
      (↑(F.obj (IsFiltered.max i j)) : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier) (Y := F.obj (IsFiltered.max i j)) (F.map (IsFiltered.leftToMax i j)) :
            (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj (IsFiltered.max i j)) : Type (max u v)))
          x :
        (↑(F.obj (IsFiltered.max i j)) : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier) (Y := F.obj (IsFiltered.max i j)) (F.map (IsFiltered.rightToMax i j)) :
            (a : (↑(F.obj j) : Type (max u v))) → (↑(F.obj (IsFiltered.max i j)) : Type (max u v)))
          y :
        (↑(F.obj (IsFiltered.max i j)) : Type (max u v)))) =
  HMul.hMul (α := (↑t.1 : Type (max u v))) (β := (↑t.1 : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) (t.ι.app i) :
          (a : (↑(F.obj i) : Type (max u v))) → (↑t.pt : Type (max u v)))
        x :
      (↑t.pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) (t.ι.app j) :
          (a : (↑(F.obj j) : Type (max u v))) → (↑t.pt : Type (max u v)))
        y :
      (↑t.pt : Type (max u v)))
Tactic: dsimp