-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
t : Cocone F
m : (colimitCocone.{v, u} F).pt ⟶ t.pt
hm : ∀ (j : J), (colimitCocone.{v, u} F).ι.app j ≫ m = t.ι.app j
x_1 : (↑(colimitCocone.{v, u} F).pt : Type (max u v))
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
⊢ Eq (α := (↑t.pt : Type (max u v)))
    ((Hom.hom m : (a : (↑(colimitCocone F).pt : Type (max u v))) → (↑t.pt : Type (max u v)))
        (Quot.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)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : J) ↦
            ((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)
            j x)) :
      (↑t.pt : Type (max u v)))
    ((Hom.hom
            (ofHom
              (let __src : (↑(R.{v, u} F) : Type (max v u)) →+ (↑t.pt : Type (max u v)) := descAddMonoidHom t;
              { toFun := (↑__src : ZeroHom (↑(R F) : Type (max v u)) (↑t.pt : Type (max u v))).toFun, map_one' := ⋯,
                map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })) :
          (a : (↑(colimitCocone F).pt : Type (max u v))) → (↑t.pt : Type (max u v)))
        (Quot.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)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : J) ↦
            ((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)
            j x)) :
      (↑t.pt : Type (max u v)))

Tactic:
(ConcreteCategory.congr_hom ((forget SemiRingCat).congr_map (hm j)) x).trans
      (descAddMonoidHom_quotMk t x).symm

Premises used: CategoryTheory.forget, CategoryTheory.Functor.congr_map, SemiRingCat, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Functor.ιColimitType, Eq.trans