-- 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)))
r : (↑(RingCat.FilteredColimits.colimit.{u_1, u_2} R) : Type (max u_1 u_2))
m n : (↑(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
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₁
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 V₁) (IsFiltered.max U V₂) ⟶ s
β : IsFiltered.max U (IsFiltered.max V₁ V₂) ⟶ s
h₁ :
  (leftToMax U V₁ ≫ leftToMax (IsFiltered.max U V₁) (IsFiltered.max U V₂)) ≫ α = leftToMax U (IsFiltered.max V₁ V₂) ≫ β
h₂ :
  (leftToMax U V₂ ≫ rightToMax (IsFiltered.max U V₁) (IsFiltered.max U V₂)) ≫ α = leftToMax U (IsFiltered.max V₁ V₂) ≫ β
h₃ :
  (rightToMax U V₁ ≫ leftToMax (IsFiltered.max U V₁) (IsFiltered.max U V₂)) ≫ α =
    (leftToMax V₁ V₂ ≫ rightToMax U (IsFiltered.max V₁ V₂)) ≫ β
h₄ :
  (rightToMax U V₂ ≫ rightToMax (IsFiltered.max U V₁) (IsFiltered.max U V₂)) ≫ α =
    (rightToMax V₁ V₂ ≫ rightToMax U (IsFiltered.max V₁ 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 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 U (IsFiltered.max V₁ 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 V₁ V₂))) : Type (max u_1 u_2))) (β :=
        (↑(M.obj (IsFiltered.max U (IsFiltered.max V₁ 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 V₁ V₂)))
                (R.map (leftToMax U (IsFiltered.max V₁ V₂))) :
              (a : (↑(R.obj U) : Type (max u_1 u_2))) →
                (↑(R.obj (IsFiltered.max U (IsFiltered.max V₁ V₂))) : Type (max u_1 u_2)))
            a :
          (↑(R.obj (IsFiltered.max U (IsFiltered.max V₁ 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 V₁ V₂)) (Y := M.obj (IsFiltered.max U (IsFiltered.max V₁ V₂)))
                (M.map (rightToMax U (IsFiltered.max V₁ V₂))) :
              (a : (↑(M.obj (IsFiltered.max V₁ V₂)) : Type (max u_1 u_3))) →
                (↑(M.obj (IsFiltered.max U (IsFiltered.max V₁ V₂))) : Type (max u_1 u_3)))
            (HAdd.hAdd (α :=
              (↑(Functor.obj
                    (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))
                    (Functor.obj
                      (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))
                      (M.obj (IsFiltered.max V₁ V₂)))) :
                Type (max u_3 u_1)))
              (β :=
              (↑(Functor.obj
                    (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))
                    (Functor.obj
                      (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))
                      (M.obj (IsFiltered.max V₁ V₂)))) :
                Type (max u_3 u_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 V₁ V₂)) (M.map (leftToMax V₁ V₂)) :
                    (a : (↑(M.obj V₁) : Type (max u_1 u_3))) → (↑(M.obj (IsFiltered.max V₁ V₂)) : Type (max u_1 u_3)))
                  b₁ :
                (↑(M.obj (IsFiltered.max V₁ 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 V₁ V₂)) (M.map (rightToMax V₁ V₂)) :
                    (a : (↑(M.obj V₂) : Type (max u_1 u_3))) → (↑(M.obj (IsFiltered.max V₁ V₂)) : Type (max u_1 u_3)))
                  b₂ :
                (↑(M.obj (IsFiltered.max V₁ V₂)) : Type (max u_1 u_3)))) :
          (↑(M.obj (IsFiltered.max U (IsFiltered.max V₁ 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 (IsFiltered.max U V₁) (IsFiltered.max U V₂))) : Type (max u_1 u_3))) →
          (↑(M.obj s) : Type (max u_1 u_3)))
      (HAdd.hAdd (α :=
        (↑(Functor.obj
              (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))
              (Functor.obj
                (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))
                (M.obj (IsFiltered.max (IsFiltered.max U V₁) (IsFiltered.max U V₂))))) :
          Type (max u_3 u_1)))
        (β :=
        (↑(Functor.obj
              (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))
              (Functor.obj
                (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))
                (M.obj (IsFiltered.max (IsFiltered.max U V₁) (IsFiltered.max U V₂))))) :
          Type (max u_3 u_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 (IsFiltered.max U V₁) (IsFiltered.max U V₂)))
                (M.map (leftToMax (IsFiltered.max U V₁) (IsFiltered.max U V₂))) :
              (a : (↑(M.obj (IsFiltered.max U V₁)) : Type (max u_1 u_3))) →
                (↑(M.obj (IsFiltered.max (IsFiltered.max U V₁) (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 (IsFiltered.max U V₁) (IsFiltered.max U 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) (X :=
                M.obj (IsFiltered.max U V₂)) (Y := M.obj (IsFiltered.max (IsFiltered.max U V₁) (IsFiltered.max U V₂)))
                (M.map (rightToMax (IsFiltered.max U V₁) (IsFiltered.max U V₂))) :
              (a : (↑(M.obj (IsFiltered.max U V₂)) : Type (max u_1 u_3))) →
                (↑(M.obj (IsFiltered.max (IsFiltered.max U V₁) (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 (IsFiltered.max U V₁) (IsFiltered.max U V₂))) : Type (max u_1 u_3)))) :
    (↑(M.obj s) : Type (max u_1 u_3)))
Tactic: dsimp