-- Lean 4 proof step from Mathlib.Algebra.Category.Ring.FilteredColimits (goal)
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
⊢ 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' := ⋯ })
have 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' := sorry,
                map_mul' := sorry, map_zero' := sorry, map_add' := sorry })) :
          (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: ext ⟨j, x⟩