-- 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
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
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₁
V₂ : C
f : V₁ ⟶ V₂
s : C
α : IsFiltered.max U V₁ ⟶ s
β : IsFiltered.max U V₂ ⟶ s
h₁ : leftToMax U V₁ ≫ α = leftToMax U V₂ ≫ β
h₂ : rightToMax U V₁ ≫ α = (f ≫ rightToMax U V₂) ≫ β
⊢ 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_1 : (↑(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_1 : (↑(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, a⟩.fst
                    ⟨V₂,
                        (ConcreteCategory.hom (M.map f) : (a : (↑(M.obj V₁) : Type u_3)) → (↑(M.obj V₂) : Type u_3))
                          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.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)
                    (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₂
                      ((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 V₁) : Type u_3)) → (↑(M.obj V₂) : Type u_3))
                        b₁))))) :
            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.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)
                    (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₂
                      ((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 V₁) : Type u_3)) → (↑(M.obj V₂) : Type u_3))
                        b₁))))) :
            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.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)
                        (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₂
                          ((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 V₁) : Type u_3)) → (↑(M.obj V₂) : Type u_3))
                            b₁)))))
                  (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.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)
                        (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₂
                          ((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 V₁) : Type u_3)) → (↑(M.obj V₂) : Type u_3))
                            b₁))))) :
                (a_1 : (↑(R.obj ⟨U, a⟩.fst) : Type u_2)) →
                  (↑(R.obj
                        (IsFiltered.max ⟨U, a⟩.fst
                          ⟨V₂,
                              (ConcreteCategory.hom (M.map f) :
                                  (a : (↑(M.obj V₁) : Type u_3)) → (↑(M.obj V₂) : Type u_3))
                                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.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)
                      (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₂
                        ((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 V₁) : Type u_3)) → (↑(M.obj V₂) : Type u_3))
                          b₁))))) :
              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.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)
                      (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₂
                        ((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 V₁) : Type u_3)) → (↑(M.obj V₂) : Type u_3))
                          b₁))))
                  (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.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)
                        (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₂
                          ((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 V₁) : Type u_3)) → (↑(M.obj V₂) : Type u_3))
                            b₁)))))
                  (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.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)
                        (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₂
                          ((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 V₁) : Type u_3)) → (↑(M.obj V₂) : Type u_3))
                            b₁))))) :
                (a_1 :
                    (↑(M.obj
                          ⟨V₂,
                              (ConcreteCategory.hom (M.map f) :
                                  (a : (↑(M.obj V₁) : Type u_3)) → (↑(M.obj V₂) : Type u_3))
                                b₁⟩.fst) :
                      Type u_3)) →
                  (↑(M.obj
                        (IsFiltered.max ⟨U, a⟩.fst
                          ⟨V₂,
                              (ConcreteCategory.hom (M.map f) :
                                  (a : (↑(M.obj V₁) : Type u_3)) → (↑(M.obj V₂) : Type u_3))
                                b₁⟩.fst)) :
                    Type u_3))
              (Sigma.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)
                  (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₂
                    ((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 V₁) : Type u_3)) → (↑(M.obj V₂) : Type u_3))
                      b₁)) :
                (M ⋙
                      forget Ab (FC := fun (x1 x2 : AddCommGrpCat.{u_3}) ↦ (↑x1 : Type u_3) →+ (↑x2 : Type u_3)) (CC :=
                        AddCommGrpCat.carrier)).obj
                  (Sigma.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)
                    (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₂
                      ((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 V₁) : Type u_3)) → (↑(M.obj V₂) : Type u_3))
                        b₁)))) :
            (↑(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.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)
                      (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₂
                        ((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 V₁) : Type u_3)) → (↑(M.obj V₂) : Type u_3))
                          b₁))))) :
              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:
simp [*, ← R.map_comp_apply, ← M.map_comp_apply, -Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp_apply, CategoryTheory.Functor.map_comp