-- Lean 4 proof step from Mathlib.Algebra.Category.ModuleCat.Stalk (goal)
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)))
m : (↑(AddCommGrpCat.FilteredColimits.colimit.{u_1, u_3} M) : Type (max u_1 u_3))
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have dsimp : 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 (Nonempty.some sorry) V)))
  ((@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 (Nonempty.some sorry) V))) :
        (a : (↑(M.obj (IsFiltered.max sorry.some V)) : Type (max u_1 u_3))) →
          (↑(M.obj (IsFiltered.max sorry.some V)) : Type (max u_1 u_3)))
      (HSMul.hSMul (α := (↑(R.obj (IsFiltered.max (Nonempty.some sorry) V)) : Type (max u_1 u_2))) (β :=
        (↑(M.obj (IsFiltered.max (Nonempty.some sorry) 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) (X := R.obj (Nonempty.some sorry)) (Y := R.obj (IsFiltered.max (Nonempty.some sorry) V))
              (R.map (leftToMax (Nonempty.some sorry) V)) :
            (a : (↑(R.obj sorry.some) : Type (max u_1 u_2))) → (↑(R.obj (IsFiltered.max sorry.some V)) : Type (max u_1 u_2)))
          1)
        ((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 (Nonempty.some sorry) V)) (M.map (rightToMax (Nonempty.some sorry) V)) :
              (a : (↑(M.obj V) : Type (max u_1 u_3))) → (↑(M.obj (IsFiltered.max sorry.some V)) : Type (max u_1 u_3)))
            b :
          (↑(M.obj (IsFiltered.max (Nonempty.some sorry) V)) : Type (max u_1 u_3)))) :
    (↑(M.obj (IsFiltered.max (Nonempty.some sorry) V)) : 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) (Y := M.obj (IsFiltered.max (Nonempty.some sorry) V))
          (M.map (rightToMax (Nonempty.some sorry) V)) :
        (a : (↑(M.obj V) : Type (max u_1 u_3))) → (↑(M.obj (IsFiltered.max sorry.some V)) : Type (max u_1 u_3)))
      b :
    (↑(M.obj (IsFiltered.max (Nonempty.some sorry) V)) : Type (max u_1 u_3)))
Tactic: dsimp