-- 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 s_1 : (↑(RingCat.FilteredColimits.colimit.{u_1, u_2} R) : Type (max u_1 u_2))
m : (↑(AddCommGrpCat.FilteredColimits.colimit.{u_1, u_3} M) : Type (max u_1 u_3))
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₁
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₂
V : C
b :
  (((M ⋙
            forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
              (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddCommGrpCat.carrier) AddGrpCat (FD :=
              fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
              AddGrpCat.carrier)) ⋙
          forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1)))
            (CC := AddGrpCat.carrier) AddMonCat (FD := fun (x1 x2 : AddMonCat) ↦
            (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD := AddMonCat.carrier)) ⋙
        forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1)))
          (CC := AddMonCat.carrier)).obj
    V
s : C
α : IsFiltered.max (IsFiltered.max U₁ U₂) V ⟶ s
β : IsFiltered.max U₁ (IsFiltered.max U₂ V) ⟶ s
h₁ : (leftToMax U₁ U₂ ≫ leftToMax (IsFiltered.max U₁ U₂) V) ≫ α = leftToMax U₁ (IsFiltered.max U₂ V) ≫ β
h₂ :
  (rightToMax U₁ U₂ ≫ leftToMax (IsFiltered.max U₁ U₂) V) ≫ α =
    (leftToMax U₂ V ≫ rightToMax U₁ (IsFiltered.max U₂ V)) ≫ β
h₃ : rightToMax (IsFiltered.max U₁ U₂) V ≫ α = (rightToMax U₂ V ≫ rightToMax U₁ (IsFiltered.max U₂ V)) ≫ β
⊢ 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 s))
    ((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 α) :
          (a : (↑(M.obj (IsFiltered.max (IsFiltered.max U₁ U₂) V)) : Type (max u_1 u_3))) →
            (↑(M.obj s) : Type (max u_1 u_3)))
        (HSMul.hSMul (α := (↑(R.obj (IsFiltered.max (IsFiltered.max U₁ U₂) V)) : Type (max u_1 u_2))) (β :=
          (↑(M.obj (IsFiltered.max (IsFiltered.max U₁ U₂) V)) : 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 (IsFiltered.max U₁ U₂) V))
                  (R.map (leftToMax (IsFiltered.max U₁ U₂) V)) :
                (a : (↑(R.obj (IsFiltered.max U₁ U₂)) : Type (max u_1 u_2))) →
                  (↑(R.obj (IsFiltered.max (IsFiltered.max U₁ U₂) V)) : Type (max u_1 u_2)))
              (HMul.hMul (α :=
                (↑(Functor.obj
                      (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))
                      (Functor.obj
                        (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))
                        (R.obj (IsFiltered.max U₁ U₂)))) :
                  Type (max u_2 u_1)))
                (β :=
                (↑(Functor.obj
                      (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))
                      (Functor.obj
                        (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))
                        (R.obj (IsFiltered.max U₁ U₂)))) :
                  Type (max u_2 u_1)))
                ((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₁ U₂)) (R.map (leftToMax U₁ U₂)) :
                      (a : (↑(R.obj U₁) : Type (max u_1 u_2))) → (↑(R.obj (IsFiltered.max U₁ U₂)) : Type (max u_1 u_2)))
                    a₁ :
                  (↑(R.obj (IsFiltered.max U₁ U₂)) : Type (max u_1 u_2)))
                ((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₁ U₂)) (R.map (rightToMax U₁ U₂)) :
                      (a : (↑(R.obj U₂) : Type (max u_1 u_2))) → (↑(R.obj (IsFiltered.max U₁ U₂)) : Type (max u_1 u_2)))
                    a₂ :
                  (↑(R.obj (IsFiltered.max U₁ U₂)) : Type (max u_1 u_2)))) :
            (↑(R.obj (IsFiltered.max (IsFiltered.max U₁ U₂) V)) : 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) (Y :=
                  M.obj (IsFiltered.max (IsFiltered.max U₁ U₂) V)) (M.map (rightToMax (IsFiltered.max U₁ U₂) V)) :
                (a : (↑(M.obj V) : Type (max u_1 u_3))) →
                  (↑(M.obj (IsFiltered.max (IsFiltered.max U₁ U₂) V)) : Type (max u_1 u_3)))
              b :
            (↑(M.obj (IsFiltered.max (IsFiltered.max U₁ U₂) V)) : Type (max u_1 u_3)))) :
      (↑(M.obj s) : 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 β) :
          (a : (↑(M.obj (IsFiltered.max U₁ (IsFiltered.max U₂ V))) : Type (max u_1 u_3))) →
            (↑(M.obj s) : Type (max u_1 u_3)))
        (HSMul.hSMul (α := (↑(R.obj (IsFiltered.max U₁ (IsFiltered.max U₂ V))) : Type (max u_1 u_2))) (β :=
          (↑(M.obj (IsFiltered.max U₁ (IsFiltered.max U₂ V))) : 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₁ (IsFiltered.max U₂ V)))
                  (R.map (leftToMax U₁ (IsFiltered.max U₂ V))) :
                (a : (↑(R.obj U₁) : Type (max u_1 u_2))) →
                  (↑(R.obj (IsFiltered.max U₁ (IsFiltered.max U₂ V))) : Type (max u_1 u_2)))
              a₁ :
            (↑(R.obj (IsFiltered.max U₁ (IsFiltered.max U₂ V))) : 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 (IsFiltered.max U₂ V)) (Y := M.obj (IsFiltered.max U₁ (IsFiltered.max U₂ V)))
                  (M.map (rightToMax U₁ (IsFiltered.max U₂ V))) :
                (a : (↑(M.obj (IsFiltered.max U₂ V)) : Type (max u_1 u_3))) →
                  (↑(M.obj (IsFiltered.max U₁ (IsFiltered.max U₂ V))) : Type (max u_1 u_3)))
              (HSMul.hSMul (α := (↑(R.obj (IsFiltered.max U₂ V)) : Type (max u_1 u_2))) (β :=
                (↑(M.obj (IsFiltered.max U₂ V)) : 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₂ V)) (R.map (leftToMax U₂ V)) :
                      (a : (↑(R.obj U₂) : Type (max u_1 u_2))) → (↑(R.obj (IsFiltered.max U₂ V)) : Type (max u_1 u_2)))
                    a₂ :
                  (↑(R.obj (IsFiltered.max U₂ V)) : 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) (Y :=
                        M.obj (IsFiltered.max U₂ V)) (M.map (rightToMax U₂ V)) :
                      (a : (↑(M.obj V) : Type (max u_1 u_3))) → (↑(M.obj (IsFiltered.max U₂ V)) : Type (max u_1 u_3)))
                    b :
                  (↑(M.obj (IsFiltered.max U₂ V)) : Type (max u_1 u_3)))) :
            (↑(M.obj (IsFiltered.max U₁ (IsFiltered.max U₂ V))) : Type (max u_1 u_3)))) :
      (↑(M.obj s) : Type (max u_1 u_3)))

Tactic:
simp only [map_mul, ← ConcreteCategory.comp_apply, ← Functor.map_comp, mul_smul, *]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, map_mul, CategoryTheory.Functor.map_comp, SemigroupAction.mul_smul