-- 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))
rw :
  HMul.hMul (α := (↑t.pt : Type (max u v))) (β := (↑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) (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)))
          ((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) :
        (↑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) (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)))
          ((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) :
        (↑t.pt : 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)))
rw₁ :
  HMul.hMul (α := (↑t.pt : Type (max u v))) (β := (↑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 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) (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)))
          ((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) :
        (↑t.pt : 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)))
⊢ (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)))
have rw₂ : HMul.hMul (α := (↑t.pt : Type (max u v))) (β := (↑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 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))) =
  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: rw [map_mul, t.w_apply, t.w_apply]