-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
j : J
x :
  ((F ⋙
          forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
            carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
            MonCat.carrier)) ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          MonCat.carrier)).obj
    j
rw :
  MonCat.FilteredColimits.M.mk
      (F ⋙
        forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
          carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
          MonCat.carrier))
      (Sigma.mk (β := fun (j : J) ↦
        (↑(Functor.obj
              (forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                (CD := MonCat.carrier))
              (F.obj j)) :
          Type (max u v)))
        j 0) =
    AddMonCat.FilteredColimits.M.mk
      ((F ⋙
          forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
            carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat) ↦
            (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddCommMonCat.carrier)) ⋙
        forget₂ AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
          (CC := AddCommMonCat.carrier) AddMonCat (FD := fun (x1 x2 : AddMonCat) ↦
          (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddMonCat.carrier))
      (Sigma.mk (β := fun (j : J) ↦
        (↑(Functor.obj
              (forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat) ↦
                (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddCommMonCat.carrier))
              (F.obj j)) :
          Type (max u v)))
        j 0)
⊢ MonCat.FilteredColimits.M.mk
      (F ⋙
        forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
          carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
          MonCat.carrier))
      (Sigma.mk (β := fun (j : J) ↦
        (↑(Functor.obj
              (forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                (CD := MonCat.carrier))
              (F.obj j)) :
          Type (max u v)))
        j (0 * x)) =
    AddMonCat.FilteredColimits.M.mk
      ((F ⋙
          forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
            carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat) ↦
            (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddCommMonCat.carrier)) ⋙
        forget₂ AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat) ↦ (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v)))
          (CC := AddCommMonCat.carrier) AddMonCat (FD := fun (x1 x2 : AddMonCat) ↦
          (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddMonCat.carrier))
      (Sigma.mk (β := fun (j : J) ↦
        (↑(Functor.obj
              (forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                (CC := carrier) AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat) ↦
                (↑x1 : Type (max u v)) →+ (↑x2 : Type (max u v))) (CD := AddCommMonCat.carrier))
              (F.obj j)) :
          Type (max u v)))
        j 0)

Tactic:
rw [zero_mul x]

Premises used: MulZeroClass.zero_mul