-- 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
hf :
  ∀ (x : (↑(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)))
⊢ m =
    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' := ⋯ })

Tactic:
ext ⟨j, x⟩