-- 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.{u_2, u_3} (↑(R.obj i) : Type u_2) (↑(M.obj i) : Type u_3)
H :
  ∀ {i j : C} (f : i ⟶ j) (r : (↑(R.obj i) : Type u_2)) (m : (↑(M.obj i) : Type u_3)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC :=
            AddCommGrpCat.carrier) (M.map f) :
          (a : (↑(M.obj i) : Type u_3)) → (↑(M.obj j) : Type u_3))
        (r • m) =
      HSMul.hSMul (α := (↑(R.obj j) : Type u_2)) (β := (↑(M.obj j) : Type u_3))
        ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2)) (CC :=
                RingCat.carrier) (R.map f) :
              (a : (↑(R.obj i) : Type u_2)) → (↑(R.obj j) : Type u_2))
            r :
          (↑(R.obj j) : Type u_2))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC :=
                AddCommGrpCat.carrier) (M.map f) :
              (a : (↑(M.obj i) : Type u_3)) → (↑(M.obj j) : Type u_3))
            m :
          (↑(M.obj j) : Type u_3))
r :
  (R ⋙
      forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2)) (CC :=
        RingCat.carrier)).ColimitType
m :
  (M ⋙
      forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC :=
        AddCommGrpCat.carrier)).ColimitType
refine_1 :
  ∀
    (a :
      (j : C) ×
        (R ⋙
              forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2)) (CC :=
                RingCat.carrier)).obj
          j)
    (b₁ b₂ :
      (j : C) ×
        (M ⋙
              forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC :=
                AddCommGrpCat.carrier)).obj
          j),
    (M ⋙
            forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC :=
              AddCommGrpCat.carrier)).ColimitTypeRel
        b₁ b₂ →
      Eq (α :=
        (M ⋙
            forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC :=
              AddCommGrpCat.carrier)).ColimitType)
        ((fun
              (Ua :
                (j : C) ×
                  (R ⋙
                        forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2)) (CC :=
                          RingCat.carrier)).obj
                    j)
              (Vb :
                (j : C) ×
                  (M ⋙
                        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3))
                          (CC := AddCommGrpCat.carrier)).obj
                    j) ↦
            (M ⋙
                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC :=
                    AddCommGrpCat.carrier)).ιColimitType
              (IsFiltered.max
                (Ua.fst (β := fun (j : C) ↦
                  (R ⋙
                        forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2)) (CC :=
                          RingCat.carrier)).obj
                    j))
                (Vb.fst (β := fun (j : C) ↦
                  (M ⋙
                        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3))
                          (CC := AddCommGrpCat.carrier)).obj
                    j)))
              (HSMul.hSMul (α :=
                (↑(R.obj
                      (IsFiltered.max
                        (Ua.fst (β := fun (j : C) ↦
                          (R ⋙
                                forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2))
                                  (CC := RingCat.carrier)).obj
                            j))
                        (Vb.fst (β := fun (j : C) ↦
                          (M ⋙
                                forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                  (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                            j)))) :
                  Type u_2))
                (β :=
                (↑(M.obj
                      (IsFiltered.max
                        (Ua.fst (β := fun (j : C) ↦
                          (R ⋙
                                forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2))
                                  (CC := RingCat.carrier)).obj
                            j))
                        (Vb.fst (β := fun (j : C) ↦
                          (M ⋙
                                forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                  (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                            j)))) :
                  Type u_3))
                ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2)) (CC :=
                        RingCat.carrier) (Y :=
                        R.obj
                          (IsFiltered.max
                            (Ua.fst (β := fun (j : C) ↦
                              (R ⋙
                                    forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦
                                      (↑R : Type u_2) →+* (↑S : Type u_2)) (CC := RingCat.carrier)).obj
                                j))
                            (Vb.fst (β := fun (j : C) ↦
                              (M ⋙
                                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                      (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                                j))))
                        (R.map
                          (leftToMax
                            (Ua.fst (β := fun (j : C) ↦
                              (R ⋙
                                    forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦
                                      (↑R : Type u_2) →+* (↑S : Type u_2)) (CC := RingCat.carrier)).obj
                                j))
                            (Vb.fst (β := fun (j : C) ↦
                              (M ⋙
                                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                      (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                                j)))) :
                      (a : (↑(R.obj Ua.fst) : Type u_2)) → (↑(R.obj (IsFiltered.max Ua.fst Vb.fst)) : Type u_2))
                    (Ua.snd (β := fun (j : C) ↦
                      (R ⋙
                            forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2))
                              (CC := RingCat.carrier)).obj
                        j)) :
                  (↑(R.obj
                        (IsFiltered.max
                          (Ua.fst (β := fun (j : C) ↦
                            (R ⋙
                                  forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2))
                                    (CC := RingCat.carrier)).obj
                              j))
                          (Vb.fst (β := fun (j : C) ↦
                            (M ⋙
                                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                    (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                              j)))) :
                    Type u_2))
                ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3))
                        (CC := AddCommGrpCat.carrier) (X :=
                        M.obj
                          (Vb.fst (β := fun (j : C) ↦
                            (M ⋙
                                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                    (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                              j)))
                        (Y :=
                        M.obj
                          (IsFiltered.max
                            (Ua.fst (β := fun (j : C) ↦
                              (R ⋙
                                    forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦
                                      (↑R : Type u_2) →+* (↑S : Type u_2)) (CC := RingCat.carrier)).obj
                                j))
                            (Vb.fst (β := fun (j : C) ↦
                              (M ⋙
                                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                      (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                                j))))
                        (M.map
                          (rightToMax
                            (Ua.fst (β := fun (j : C) ↦
                              (R ⋙
                                    forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦
                                      (↑R : Type u_2) →+* (↑S : Type u_2)) (CC := RingCat.carrier)).obj
                                j))
                            (Vb.fst (β := fun (j : C) ↦
                              (M ⋙
                                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                      (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                                j)))) :
                      (a : (↑(M.obj Vb.fst) : Type u_3)) → (↑(M.obj (IsFiltered.max Ua.fst Vb.fst)) : Type u_3))
                    (Vb.snd (β := fun (j : C) ↦
                      (M ⋙
                            forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3))
                              (CC := AddCommGrpCat.carrier)).obj
                        j)) :
                  (↑(M.obj
                        (IsFiltered.max
                          (Ua.fst (β := fun (j : C) ↦
                            (R ⋙
                                  forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2))
                                    (CC := RingCat.carrier)).obj
                              j))
                          (Vb.fst (β := fun (j : C) ↦
                            (M ⋙
                                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                    (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                              j)))) :
                    Type u_3))))
          a b₁)
        ((fun
              (Ua :
                (j : C) ×
                  (R ⋙
                        forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2)) (CC :=
                          RingCat.carrier)).obj
                    j)
              (Vb :
                (j : C) ×
                  (M ⋙
                        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3))
                          (CC := AddCommGrpCat.carrier)).obj
                    j) ↦
            (M ⋙
                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC :=
                    AddCommGrpCat.carrier)).ιColimitType
              (IsFiltered.max
                (Ua.fst (β := fun (j : C) ↦
                  (R ⋙
                        forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2)) (CC :=
                          RingCat.carrier)).obj
                    j))
                (Vb.fst (β := fun (j : C) ↦
                  (M ⋙
                        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3))
                          (CC := AddCommGrpCat.carrier)).obj
                    j)))
              (HSMul.hSMul (α :=
                (↑(R.obj
                      (IsFiltered.max
                        (Ua.fst (β := fun (j : C) ↦
                          (R ⋙
                                forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2))
                                  (CC := RingCat.carrier)).obj
                            j))
                        (Vb.fst (β := fun (j : C) ↦
                          (M ⋙
                                forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                  (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                            j)))) :
                  Type u_2))
                (β :=
                (↑(M.obj
                      (IsFiltered.max
                        (Ua.fst (β := fun (j : C) ↦
                          (R ⋙
                                forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2))
                                  (CC := RingCat.carrier)).obj
                            j))
                        (Vb.fst (β := fun (j : C) ↦
                          (M ⋙
                                forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                  (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                            j)))) :
                  Type u_3))
                ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2)) (CC :=
                        RingCat.carrier) (Y :=
                        R.obj
                          (IsFiltered.max
                            (Ua.fst (β := fun (j : C) ↦
                              (R ⋙
                                    forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦
                                      (↑R : Type u_2) →+* (↑S : Type u_2)) (CC := RingCat.carrier)).obj
                                j))
                            (Vb.fst (β := fun (j : C) ↦
                              (M ⋙
                                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                      (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                                j))))
                        (R.map
                          (leftToMax
                            (Ua.fst (β := fun (j : C) ↦
                              (R ⋙
                                    forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦
                                      (↑R : Type u_2) →+* (↑S : Type u_2)) (CC := RingCat.carrier)).obj
                                j))
                            (Vb.fst (β := fun (j : C) ↦
                              (M ⋙
                                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                      (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                                j)))) :
                      (a : (↑(R.obj Ua.fst) : Type u_2)) → (↑(R.obj (IsFiltered.max Ua.fst Vb.fst)) : Type u_2))
                    (Ua.snd (β := fun (j : C) ↦
                      (R ⋙
                            forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2))
                              (CC := RingCat.carrier)).obj
                        j)) :
                  (↑(R.obj
                        (IsFiltered.max
                          (Ua.fst (β := fun (j : C) ↦
                            (R ⋙
                                  forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2))
                                    (CC := RingCat.carrier)).obj
                              j))
                          (Vb.fst (β := fun (j : C) ↦
                            (M ⋙
                                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                    (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                              j)))) :
                    Type u_2))
                ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3))
                        (CC := AddCommGrpCat.carrier) (X :=
                        M.obj
                          (Vb.fst (β := fun (j : C) ↦
                            (M ⋙
                                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                    (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                              j)))
                        (Y :=
                        M.obj
                          (IsFiltered.max
                            (Ua.fst (β := fun (j : C) ↦
                              (R ⋙
                                    forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦
                                      (↑R : Type u_2) →+* (↑S : Type u_2)) (CC := RingCat.carrier)).obj
                                j))
                            (Vb.fst (β := fun (j : C) ↦
                              (M ⋙
                                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                      (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                                j))))
                        (M.map
                          (rightToMax
                            (Ua.fst (β := fun (j : C) ↦
                              (R ⋙
                                    forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦
                                      (↑R : Type u_2) →+* (↑S : Type u_2)) (CC := RingCat.carrier)).obj
                                j))
                            (Vb.fst (β := fun (j : C) ↦
                              (M ⋙
                                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                      (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                                j)))) :
                      (a : (↑(M.obj Vb.fst) : Type u_3)) → (↑(M.obj (IsFiltered.max Ua.fst Vb.fst)) : Type u_3))
                    (Vb.snd (β := fun (j : C) ↦
                      (M ⋙
                            forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3))
                              (CC := AddCommGrpCat.carrier)).obj
                        j)) :
                  (↑(M.obj
                        (IsFiltered.max
                          (Ua.fst (β := fun (j : C) ↦
                            (R ⋙
                                  forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2))
                                    (CC := RingCat.carrier)).obj
                              j))
                          (Vb.fst (β := fun (j : C) ↦
                            (M ⋙
                                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                    (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                              j)))) :
                    Type u_3))))
          a b₂)
refine_2 :
  ∀
    (a₁ a₂ :
      (j : C) ×
        (R ⋙
              forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2)) (CC :=
                RingCat.carrier)).obj
          j)
    (b :
      (j : C) ×
        (M ⋙
              forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC :=
                AddCommGrpCat.carrier)).obj
          j),
    (R ⋙
            forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2)) (CC :=
              RingCat.carrier)).ColimitTypeRel
        a₁ a₂ →
      Eq (α :=
        (M ⋙
            forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC :=
              AddCommGrpCat.carrier)).ColimitType)
        ((fun
              (Ua :
                (j : C) ×
                  (R ⋙
                        forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2)) (CC :=
                          RingCat.carrier)).obj
                    j)
              (Vb :
                (j : C) ×
                  (M ⋙
                        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3))
                          (CC := AddCommGrpCat.carrier)).obj
                    j) ↦
            (M ⋙
                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC :=
                    AddCommGrpCat.carrier)).ιColimitType
              (IsFiltered.max
                (Ua.fst (β := fun (j : C) ↦
                  (R ⋙
                        forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2)) (CC :=
                          RingCat.carrier)).obj
                    j))
                (Vb.fst (β := fun (j : C) ↦
                  (M ⋙
                        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3))
                          (CC := AddCommGrpCat.carrier)).obj
                    j)))
              (HSMul.hSMul (α :=
                (↑(R.obj
                      (IsFiltered.max
                        (Ua.fst (β := fun (j : C) ↦
                          (R ⋙
                                forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2))
                                  (CC := RingCat.carrier)).obj
                            j))
                        (Vb.fst (β := fun (j : C) ↦
                          (M ⋙
                                forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                  (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                            j)))) :
                  Type u_2))
                (β :=
                (↑(M.obj
                      (IsFiltered.max
                        (Ua.fst (β := fun (j : C) ↦
                          (R ⋙
                                forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2))
                                  (CC := RingCat.carrier)).obj
                            j))
                        (Vb.fst (β := fun (j : C) ↦
                          (M ⋙
                                forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                  (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                            j)))) :
                  Type u_3))
                ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2)) (CC :=
                        RingCat.carrier) (Y :=
                        R.obj
                          (IsFiltered.max
                            (Ua.fst (β := fun (j : C) ↦
                              (R ⋙
                                    forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦
                                      (↑R : Type u_2) →+* (↑S : Type u_2)) (CC := RingCat.carrier)).obj
                                j))
                            (Vb.fst (β := fun (j : C) ↦
                              (M ⋙
                                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                      (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                                j))))
                        (R.map
                          (leftToMax
                            (Ua.fst (β := fun (j : C) ↦
                              (R ⋙
                                    forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦
                                      (↑R : Type u_2) →+* (↑S : Type u_2)) (CC := RingCat.carrier)).obj
                                j))
                            (Vb.fst (β := fun (j : C) ↦
                              (M ⋙
                                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                      (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                                j)))) :
                      (a : (↑(R.obj Ua.fst) : Type u_2)) → (↑(R.obj (IsFiltered.max Ua.fst Vb.fst)) : Type u_2))
                    (Ua.snd (β := fun (j : C) ↦
                      (R ⋙
                            forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2))
                              (CC := RingCat.carrier)).obj
                        j)) :
                  (↑(R.obj
                        (IsFiltered.max
                          (Ua.fst (β := fun (j : C) ↦
                            (R ⋙
                                  forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2))
                                    (CC := RingCat.carrier)).obj
                              j))
                          (Vb.fst (β := fun (j : C) ↦
                            (M ⋙
                                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                    (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                              j)))) :
                    Type u_2))
                ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3))
                        (CC := AddCommGrpCat.carrier) (X :=
                        M.obj
                          (Vb.fst (β := fun (j : C) ↦
                            (M ⋙
                                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                    (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                              j)))
                        (Y :=
                        M.obj
                          (IsFiltered.max
                            (Ua.fst (β := fun (j : C) ↦
                              (R ⋙
                                    forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦
                                      (↑R : Type u_2) →+* (↑S : Type u_2)) (CC := RingCat.carrier)).obj
                                j))
                            (Vb.fst (β := fun (j : C) ↦
                              (M ⋙
                                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                      (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                                j))))
                        (M.map
                          (rightToMax
                            (Ua.fst (β := fun (j : C) ↦
                              (R ⋙
                                    forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦
                                      (↑R : Type u_2) →+* (↑S : Type u_2)) (CC := RingCat.carrier)).obj
                                j))
                            (Vb.fst (β := fun (j : C) ↦
                              (M ⋙
                                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                      (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                                j)))) :
                      (a : (↑(M.obj Vb.fst) : Type u_3)) → (↑(M.obj (IsFiltered.max Ua.fst Vb.fst)) : Type u_3))
                    (Vb.snd (β := fun (j : C) ↦
                      (M ⋙
                            forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3))
                              (CC := AddCommGrpCat.carrier)).obj
                        j)) :
                  (↑(M.obj
                        (IsFiltered.max
                          (Ua.fst (β := fun (j : C) ↦
                            (R ⋙
                                  forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2))
                                    (CC := RingCat.carrier)).obj
                              j))
                          (Vb.fst (β := fun (j : C) ↦
                            (M ⋙
                                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                    (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                              j)))) :
                    Type u_3))))
          a₁ b)
        ((fun
              (Ua :
                (j : C) ×
                  (R ⋙
                        forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2)) (CC :=
                          RingCat.carrier)).obj
                    j)
              (Vb :
                (j : C) ×
                  (M ⋙
                        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3))
                          (CC := AddCommGrpCat.carrier)).obj
                    j) ↦
            (M ⋙
                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC :=
                    AddCommGrpCat.carrier)).ιColimitType
              (IsFiltered.max
                (Ua.fst (β := fun (j : C) ↦
                  (R ⋙
                        forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2)) (CC :=
                          RingCat.carrier)).obj
                    j))
                (Vb.fst (β := fun (j : C) ↦
                  (M ⋙
                        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3))
                          (CC := AddCommGrpCat.carrier)).obj
                    j)))
              (HSMul.hSMul (α :=
                (↑(R.obj
                      (IsFiltered.max
                        (Ua.fst (β := fun (j : C) ↦
                          (R ⋙
                                forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2))
                                  (CC := RingCat.carrier)).obj
                            j))
                        (Vb.fst (β := fun (j : C) ↦
                          (M ⋙
                                forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                  (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                            j)))) :
                  Type u_2))
                (β :=
                (↑(M.obj
                      (IsFiltered.max
                        (Ua.fst (β := fun (j : C) ↦
                          (R ⋙
                                forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2))
                                  (CC := RingCat.carrier)).obj
                            j))
                        (Vb.fst (β := fun (j : C) ↦
                          (M ⋙
                                forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                  (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                            j)))) :
                  Type u_3))
                ((ConcreteCategory.hom (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2)) (CC :=
                        RingCat.carrier) (Y :=
                        R.obj
                          (IsFiltered.max
                            (Ua.fst (β := fun (j : C) ↦
                              (R ⋙
                                    forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦
                                      (↑R : Type u_2) →+* (↑S : Type u_2)) (CC := RingCat.carrier)).obj
                                j))
                            (Vb.fst (β := fun (j : C) ↦
                              (M ⋙
                                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                      (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                                j))))
                        (R.map
                          (leftToMax
                            (Ua.fst (β := fun (j : C) ↦
                              (R ⋙
                                    forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦
                                      (↑R : Type u_2) →+* (↑S : Type u_2)) (CC := RingCat.carrier)).obj
                                j))
                            (Vb.fst (β := fun (j : C) ↦
                              (M ⋙
                                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                      (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                                j)))) :
                      (a : (↑(R.obj Ua.fst) : Type u_2)) → (↑(R.obj (IsFiltered.max Ua.fst Vb.fst)) : Type u_2))
                    (Ua.snd (β := fun (j : C) ↦
                      (R ⋙
                            forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2))
                              (CC := RingCat.carrier)).obj
                        j)) :
                  (↑(R.obj
                        (IsFiltered.max
                          (Ua.fst (β := fun (j : C) ↦
                            (R ⋙
                                  forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2))
                                    (CC := RingCat.carrier)).obj
                              j))
                          (Vb.fst (β := fun (j : C) ↦
                            (M ⋙
                                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                    (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                              j)))) :
                    Type u_2))
                ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3))
                        (CC := AddCommGrpCat.carrier) (X :=
                        M.obj
                          (Vb.fst (β := fun (j : C) ↦
                            (M ⋙
                                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                    (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                              j)))
                        (Y :=
                        M.obj
                          (IsFiltered.max
                            (Ua.fst (β := fun (j : C) ↦
                              (R ⋙
                                    forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦
                                      (↑R : Type u_2) →+* (↑S : Type u_2)) (CC := RingCat.carrier)).obj
                                j))
                            (Vb.fst (β := fun (j : C) ↦
                              (M ⋙
                                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                      (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                                j))))
                        (M.map
                          (rightToMax
                            (Ua.fst (β := fun (j : C) ↦
                              (R ⋙
                                    forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦
                                      (↑R : Type u_2) →+* (↑S : Type u_2)) (CC := RingCat.carrier)).obj
                                j))
                            (Vb.fst (β := fun (j : C) ↦
                              (M ⋙
                                    forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                      (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                                j)))) :
                      (a : (↑(M.obj Vb.fst) : Type u_3)) → (↑(M.obj (IsFiltered.max Ua.fst Vb.fst)) : Type u_3))
                    (Vb.snd (β := fun (j : C) ↦
                      (M ⋙
                            forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3))
                              (CC := AddCommGrpCat.carrier)).obj
                        j)) :
                  (↑(M.obj
                        (IsFiltered.max
                          (Ua.fst (β := fun (j : C) ↦
                            (R ⋙
                                  forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2))
                                    (CC := RingCat.carrier)).obj
                              j))
                          (Vb.fst (β := fun (j : C) ↦
                            (M ⋙
                                  forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦
                                    (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC := AddCommGrpCat.carrier)).obj
                              j)))) :
                    Type u_3))))
          a₂ b)
⊢ (M ⋙
      forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC :=
        AddCommGrpCat.carrier)).ColimitType

Tactic:
refine Quot.liftOn₂ r m (fun Ua Vb ↦ Functor.ιColimitType _ (max Ua.1 Vb.1) <|
    letI a : R.obj (max Ua.1 Vb.1) := R.map (leftToMax Ua.1 Vb.1) Ua.2
    letI b : M.obj (max Ua.1 Vb.1) := M.map (rightToMax Ua.1 Vb.1) Vb.2
    a • b) ?_ ?_

Premises used: CategoryTheory.IsFiltered.rightToMax, CategoryTheory.ConcreteCategory.hom, Quot.liftOn₂, CategoryTheory.IsFiltered.max, Sigma.fst, CategoryTheory.Functor.map, CategoryTheory.IsFiltered.leftToMax, Sigma.snd, DFunLike.coe, CategoryTheory.Functor.ιColimitType