-- 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.{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
U₁ : C
a₁ :
  (R ⋙
        forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2)) (CC :=
          RingCat.carrier)).obj
    U₁
U₂ V : C
b :
  (M ⋙
        forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC :=
          AddCommGrpCat.carrier)).obj
    V
f : U₁ ⟶ U₂
s : C
α : IsFiltered.max U₁ V ⟶ s
β : IsFiltered.max U₂ V ⟶ s
h₁ : leftToMax U₁ V ≫ α = (f ≫ leftToMax U₂ V) ≫ β
h₂ : rightToMax U₁ V ≫ α = rightToMax U₂ V ≫ β
⊢ 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))))
      (Sigma.mk (β := 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)
        U₁ a₁)
      (Sigma.mk (β := 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)
        V 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))))
      (Sigma.mk (β := 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)
        U₂
        ((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 U₁) : Type u_2)) → (↑(R.obj U₂) : Type u_2))
          a₁))
      (Sigma.mk (β := 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)
        V b))
have refine_2 : Eq (α :=
  (fun (X : Type u_3) ↦ X)
    ((M ⋙
          forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC :=
            AddCommGrpCat.carrier)).obj
      s))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          ((M ⋙
                forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC :=
                  AddCommGrpCat.carrier)).map
            α) :
        (a : (fun (X : Type u_3) ↦ X) ((M ⋙ forget Ab).obj (IsFiltered.max ⟨U₁, a₁⟩.fst ⟨V, b⟩.fst))) →
          (fun (X : Type u_3) ↦ X) ((M ⋙ forget Ab).obj s))
      (HSMul.hSMul (α :=
        (↑(R.obj
              (IsFiltered.max
                ((Sigma.mk (β := 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)
                      U₁ a₁).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))
                ((Sigma.mk (β := 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)
                      V b).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
                ((Sigma.mk (β := 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)
                      U₁ a₁).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))
                ((Sigma.mk (β := 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)
                      V b).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
                    ((Sigma.mk (β := 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)
                          U₁ a₁).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))
                    ((Sigma.mk (β := 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)
                          V b).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
                    ((Sigma.mk (β := 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)
                          U₁ a₁).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))
                    ((Sigma.mk (β := 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)
                          V b).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 ⟨U₁, a₁⟩.fst) : Type u_2)) → (↑(R.obj (IsFiltered.max ⟨U₁, a₁⟩.fst ⟨V, b⟩.fst)) : Type u_2))
            ((Sigma.mk (β := 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)
                  U₁ a₁).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
                  ((Sigma.mk (β := 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)
                        U₁ a₁).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))
                  ((Sigma.mk (β := 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)
                        V b).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
                  ((Sigma.mk (β := 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)
                        V b).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
                    ((Sigma.mk (β := 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)
                          U₁ a₁).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))
                    ((Sigma.mk (β := 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)
                          V b).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
                    ((Sigma.mk (β := 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)
                          U₁ a₁).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))
                    ((Sigma.mk (β := 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)
                          V b).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 ⟨V, b⟩.fst) : Type u_3)) → (↑(M.obj (IsFiltered.max ⟨U₁, a₁⟩.fst ⟨V, b⟩.fst)) : Type u_3))
            ((Sigma.mk (β := 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)
                  V b).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
                  ((Sigma.mk (β := 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)
                        U₁ a₁).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))
                  ((Sigma.mk (β := 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)
                        V b).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))) :
    (fun (X : Type u_3) ↦ X)
      ((M ⋙
            forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC :=
              AddCommGrpCat.carrier)).obj
        s))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          ((M ⋙
                forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC :=
                  AddCommGrpCat.carrier)).map
            β) :
        (a :
            (fun (X : Type u_3) ↦ X)
              ((M ⋙ forget Ab).obj
                (IsFiltered.max
                  ⟨U₂,
                      (ConcreteCategory.hom (R.map f) : (a : (↑(R.obj U₁) : Type u_2)) → (↑(R.obj U₂) : Type u_2))
                        a₁⟩.fst
                  ⟨V, b⟩.fst))) →
          (fun (X : Type u_3) ↦ X) ((M ⋙ forget Ab).obj s))
      (HSMul.hSMul (α :=
        (↑(R.obj
              (IsFiltered.max
                (Sigma.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)
                  (Sigma.mk (β := 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)
                    U₂
                    ((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 U₁) : Type u_2)) → (↑(R.obj U₂) : Type u_2))
                      a₁)))
                ((Sigma.mk (β := 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)
                      V b).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
                (Sigma.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)
                  (Sigma.mk (β := 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)
                    U₂
                    ((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 U₁) : Type u_2)) → (↑(R.obj U₂) : Type u_2))
                      a₁)))
                ((Sigma.mk (β := 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)
                      V b).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
                    (Sigma.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)
                      (Sigma.mk (β := 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)
                        U₂
                        ((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 U₁) : Type u_2)) → (↑(R.obj U₂) : Type u_2))
                          a₁)))
                    ((Sigma.mk (β := 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)
                          V b).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
                    (Sigma.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)
                      (Sigma.mk (β := 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)
                        U₂
                        ((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 U₁) : Type u_2)) → (↑(R.obj U₂) : Type u_2))
                          a₁)))
                    ((Sigma.mk (β := 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)
                          V b).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
                        ⟨U₂,
                            (ConcreteCategory.hom (R.map f) : (a : (↑(R.obj U₁) : Type u_2)) → (↑(R.obj U₂) : Type u_2))
                              a₁⟩.fst) :
                    Type u_2)) →
                (↑(R.obj
                      (IsFiltered.max
                        ⟨U₂,
                            (ConcreteCategory.hom (R.map f) : (a : (↑(R.obj U₁) : Type u_2)) → (↑(R.obj U₂) : Type u_2))
                              a₁⟩.fst
                        ⟨V, b⟩.fst)) :
                  Type u_2))
            (Sigma.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)
                (Sigma.mk (β := 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)
                  U₂
                  ((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 U₁) : Type u_2)) → (↑(R.obj U₂) : Type u_2))
                    a₁)) :
              (R ⋙
                    forget RingCat (FC := fun (R S : RingCat.{u_2}) ↦ (↑R : Type u_2) →+* (↑S : Type u_2)) (CC :=
                      RingCat.carrier)).obj
                (Sigma.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)
                  (Sigma.mk (β := 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)
                    U₂
                    ((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 U₁) : Type u_2)) → (↑(R.obj U₂) : Type u_2))
                      a₁)))) :
          (↑(R.obj
                (IsFiltered.max
                  (Sigma.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)
                    (Sigma.mk (β := 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)
                      U₂
                      ((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 U₁) : Type u_2)) → (↑(R.obj U₂) : Type u_2))
                        a₁)))
                  ((Sigma.mk (β := 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)
                        V b).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
                  ((Sigma.mk (β := 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)
                        V b).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
                    (Sigma.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)
                      (Sigma.mk (β := 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)
                        U₂
                        ((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 U₁) : Type u_2)) → (↑(R.obj U₂) : Type u_2))
                          a₁)))
                    ((Sigma.mk (β := 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)
                          V b).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
                    (Sigma.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)
                      (Sigma.mk (β := 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)
                        U₂
                        ((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 U₁) : Type u_2)) → (↑(R.obj U₂) : Type u_2))
                          a₁)))
                    ((Sigma.mk (β := 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)
                          V b).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 ⟨V, b⟩.fst) : Type u_3)) →
                (↑(M.obj
                      (IsFiltered.max
                        ⟨U₂,
                            (ConcreteCategory.hom (R.map f) : (a : (↑(R.obj U₁) : Type u_2)) → (↑(R.obj U₂) : Type u_2))
                              a₁⟩.fst
                        ⟨V, b⟩.fst)) :
                  Type u_3))
            ((Sigma.mk (β := 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)
                  V b).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
                  (Sigma.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)
                    (Sigma.mk (β := 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)
                      U₂
                      ((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 U₁) : Type u_2)) → (↑(R.obj U₂) : Type u_2))
                        a₁)))
                  ((Sigma.mk (β := 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)
                        V b).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))) :
    (fun (X : Type u_3) ↦ X)
      ((M ⋙
            forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC :=
              AddCommGrpCat.carrier)).obj
        s))
Tactic: refine Functor.ιColimitType_eq_of_map_eq_map _ _ _ α β ?_