-- Module: Mathlib.Algebra.Category.ModuleCat.Stalk
Goal:
C : Type u_1
inst : SmallCategory C
inst_1 : IsFiltered C
R : C ⥤ RingCat
M : C ⥤ Ab
inst_2 : (i : C) → Module (↑(R.obj i) : Type (max u_1 u_2)) (↑(M.obj i) : Type (max u_1 u_3))
H :
  ∀ {i j : C} (f : i ⟶ j) (r : (↑(R.obj i) : Type (max u_1 u_2))) (m : (↑(M.obj i) : Type (max u_1 u_3))),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u_1 u_3)) →+ (↑x2 : Type (max u_1 u_3)))
            (CC := AddCommGrpCat.carrier) (M.map f) :
          (a : (↑(M.obj i) : Type (max u_1 u_3))) → (↑(M.obj j) : Type (max u_1 u_3)))
        (r • m) =
      HSMul.hSMul (α := (↑(R.obj j) : Type (max u_1 u_2))) (β := (↑(M.obj j) : Type (max u_1 u_3)))
        ((ConcreteCategory.hom (FC := fun (R S : RingCat) ↦ (↑R : Type (max u_1 u_2)) →+* (↑S : Type (max u_1 u_2)))
                (CC := RingCat.carrier) (R.map f) :
              (a : (↑(R.obj i) : Type (max u_1 u_2))) → (↑(R.obj j) : Type (max u_1 u_2)))
            r :
          (↑(R.obj j) : Type (max u_1 u_2)))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦
                (↑x1 : Type (max u_1 u_3)) →+ (↑x2 : Type (max u_1 u_3))) (CC := AddCommGrpCat.carrier) (M.map f) :
              (a : (↑(M.obj i) : Type (max u_1 u_3))) → (↑(M.obj j) : Type (max u_1 u_3)))
            m :
          (↑(M.obj j) : Type (max u_1 u_3)))
r : (↑(RingCat.FilteredColimits.colimit.{u_1, u_2} R) : Type (max u_1 u_2))
U : C
a :
  (((R ⋙
            forget₂ RingCat (FC := fun (R S : RingCat) ↦ (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC :=
              RingCat.carrier) SemiRingCat (FD := fun (R S : SemiRingCat) ↦
              (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CD := SemiRingCat.carrier)) ⋙
          forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1)))
            (CC := SemiRingCat.carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦
            (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1))) (CD := MonCat.carrier)) ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1))) (CC :=
          MonCat.carrier)).obj
    U
⊢ Eq (α :=
    ToType (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u_1 u_3)) →+ (↑x2 : Type (max u_1 u_3))) (CC :=
      AddCommGrpCat.carrier) (M.obj (IsFiltered.max U (Nonempty.some ⋯))))
    ((@ConcreteCategory.hom _ AddCommGrpCat.instCategory
            (fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u_1 u_3)) →+ (↑x2 : Type (max u_1 u_3)))
            AddCommGrpCat.carrier
            (fun (X Y : AddCommGrpCat) ↦
              (AddMonoidHom.instFunLike :
                FunLike ((↑X : Type (max u_1 u_3)) →+ (↑Y : Type (max u_1 u_3))) (↑X : Type (max u_1 u_3))
                  (↑Y : Type (max u_1 u_3))))
            _ _ _ (M.map (𝟙 (IsFiltered.max U (Nonempty.some ⋯)))) :
          (a : (↑(M.obj (IsFiltered.max U ⋯.some)) : Type (max u_1 u_3))) →
            (↑(M.obj (IsFiltered.max U ⋯.some)) : Type (max u_1 u_3)))
        (HSMul.hSMul (α := (↑(R.obj (IsFiltered.max U (Nonempty.some ⋯))) : Type (max u_1 u_2))) (β :=
          (↑(M.obj (IsFiltered.max U (Nonempty.some ⋯))) : Type (max u_1 u_3)))
          ((ConcreteCategory.hom (FC := fun (R S : RingCat) ↦ (↑R : Type (max u_1 u_2)) →+* (↑S : Type (max u_1 u_2)))
                  (CC := RingCat.carrier) (Y := R.obj (IsFiltered.max U (Nonempty.some ⋯)))
                  (R.map (leftToMax U (Nonempty.some ⋯))) :
                (a : (↑(R.obj U) : Type (max u_1 u_2))) → (↑(R.obj (IsFiltered.max U ⋯.some)) : Type (max u_1 u_2)))
              a :
            (↑(R.obj (IsFiltered.max U (Nonempty.some ⋯))) : Type (max u_1 u_2)))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦
                (↑x1 : Type (max u_1 u_3)) →+ (↑x2 : Type (max u_1 u_3))) (CC := AddCommGrpCat.carrier) (X :=
                M.obj (Nonempty.some ⋯)) (Y := M.obj (IsFiltered.max U (Nonempty.some ⋯)))
                (M.map (rightToMax U (Nonempty.some ⋯))) :
              (a : (↑(M.obj ⋯.some) : Type (max u_1 u_3))) → (↑(M.obj (IsFiltered.max U ⋯.some)) : Type (max u_1 u_3)))
            0)) :
      (↑(M.obj (IsFiltered.max U (Nonempty.some ⋯))) : Type (max u_1 u_3)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦
            (↑x1 : Type (max u_1 u_3)) →+ (↑x2 : Type (max u_1 u_3))) (CC := AddCommGrpCat.carrier) (X :=
            M.obj (Nonempty.some ⋯)) (Y := M.obj (IsFiltered.max U (Nonempty.some ⋯)))
            (M.map (rightToMax U (Nonempty.some ⋯))) :
          (a : (↑(M.obj ⋯.some) : Type (max u_1 u_3))) → (↑(M.obj (IsFiltered.max U ⋯.some)) : Type (max u_1 u_3)))
        0 :
      (↑(M.obj (IsFiltered.max U (Nonempty.some ⋯))) : Type (max u_1 u_3)))

Tactic:
simp only [map_zero, smul_zero]

Premises used: smul_zero, map_zero