-- 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 (↑(R.obj i) : Type (max u_1 u_2)) (↑(M.obj i) : Type (max u_1 u_3))
H :
  ∀ {i j : C} (f : i ⟶ j) (r : (↑(R.obj i) : Type (max u_1 u_2))) (m : (↑(M.obj i) : Type (max u_1 u_3))),
    (ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦ (↑x1 : Type (max u_1 u_3)) →+ (↑x2 : Type (max u_1 u_3)))
            (CC := AddCommGrpCat.carrier) (M.map f) :
          (a : (↑(M.obj i) : Type (max u_1 u_3))) → (↑(M.obj j) : Type (max u_1 u_3)))
        (r • m) =
      HSMul.hSMul (α := (↑(R.obj j) : Type (max u_1 u_2))) (β := (↑(M.obj j) : Type (max u_1 u_3)))
        ((ConcreteCategory.hom (FC := fun (R S : RingCat) ↦ (↑R : Type (max u_1 u_2)) →+* (↑S : Type (max u_1 u_2)))
                (CC := RingCat.carrier) (R.map f) :
              (a : (↑(R.obj i) : Type (max u_1 u_2))) → (↑(R.obj j) : Type (max u_1 u_2)))
            r :
          (↑(R.obj j) : Type (max u_1 u_2)))
        ((ConcreteCategory.hom (FC := fun (x1 x2 : AddCommGrpCat) ↦
                (↑x1 : Type (max u_1 u_3)) →+ (↑x2 : Type (max u_1 u_3))) (CC := AddCommGrpCat.carrier) (M.map f) :
              (a : (↑(M.obj i) : Type (max u_1 u_3))) → (↑(M.obj j) : Type (max u_1 u_3)))
            m :
          (↑(M.obj j) : Type (max u_1 u_3)))
r : (↑(RingCat.FilteredColimits.colimit.{u_1, u_2} R) : Type (max u_1 u_2))
m n : (↑(AddCommGrpCat.FilteredColimits.colimit.{u_1, u_3} M) : Type (max u_1 u_3))
U : C
a :
  (((R ⋙
            forget₂ RingCat (FC := fun (R S : RingCat) ↦ (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC :=
              RingCat.carrier) SemiRingCat (FD := fun (R S : SemiRingCat) ↦
              (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CD := SemiRingCat.carrier)) ⋙
          forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1)))
            (CC := SemiRingCat.carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦
            (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1))) (CD := MonCat.carrier)) ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1))) (CC :=
          MonCat.carrier)).obj
    U
V₁ : C
b₁ :
  (((M ⋙
            forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
              (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddCommGrpCat.carrier) AddGrpCat (FD :=
              fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
              AddGrpCat.carrier)) ⋙
          forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1)))
            (CC := AddGrpCat.carrier) AddMonCat (FD := fun (x1 x2 : AddMonCat) ↦
            (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD := AddMonCat.carrier)) ⋙
        forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1)))
          (CC := AddMonCat.carrier)).obj
    V₁
V₂ : C
b₂ :
  (((M ⋙
            forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
              (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddCommGrpCat.carrier) AddGrpCat (FD :=
              fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
              AddGrpCat.carrier)) ⋙
          forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1)))
            (CC := AddGrpCat.carrier) AddMonCat (FD := fun (x1 x2 : AddMonCat) ↦
            (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD := AddMonCat.carrier)) ⋙
        forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1)))
          (CC := AddMonCat.carrier)).obj
    V₂
obtain :
  ∀ (s : C) (α : IsFiltered.max (IsFiltered.max U V₁) (IsFiltered.max U V₂) ⟶ s)
    (β : IsFiltered.max U (IsFiltered.max V₁ V₂) ⟶ s)
    (h₁ :
      (leftToMax U V₁ ≫ leftToMax (IsFiltered.max U V₁) (IsFiltered.max U V₂)) ≫ α =
        leftToMax U (IsFiltered.max V₁ V₂) ≫ β)
    (h₂ :
      (leftToMax U V₂ ≫ rightToMax (IsFiltered.max U V₁) (IsFiltered.max U V₂)) ≫ α =
        leftToMax U (IsFiltered.max V₁ V₂) ≫ β)
    (h₃ :
      (rightToMax U V₁ ≫ leftToMax (IsFiltered.max U V₁) (IsFiltered.max U V₂)) ≫ α =
        (leftToMax V₁ V₂ ≫ rightToMax U (IsFiltered.max V₁ V₂)) ≫ β)
    (h₄ :
      (rightToMax U V₂ ≫ rightToMax (IsFiltered.max U V₁) (IsFiltered.max U V₂)) ≫ α =
        (rightToMax V₁ V₂ ≫ rightToMax U (IsFiltered.max V₁ V₂)) ≫ β),
    Quot.mk
          (((R ⋙
                  forget₂ RingCat (FC := fun (R S : RingCat) ↦ (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1)))
                    (CC := RingCat.carrier) SemiRingCat (FD := fun (R S : SemiRingCat) ↦
                    (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CD := SemiRingCat.carrier)) ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                  (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC := SemiRingCat.carrier) MonCat (FD :=
                  fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1))) (CD :=
                  MonCat.carrier)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1)))
                (CC := MonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : C) ↦
            (((R ⋙
                      forget₂ RingCat (FC := fun (R S : RingCat) ↦
                        (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC := RingCat.carrier) SemiRingCat
                        (FD := fun (R S : SemiRingCat) ↦ (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CD :=
                        SemiRingCat.carrier)) ⋙
                    forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                      (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC := SemiRingCat.carrier) MonCat (FD :=
                      fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1))) (CD :=
                      MonCat.carrier)) ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1)))
                    (CC := MonCat.carrier)).obj
              j)
            U a) •
        (Quot.mk
            (((M ⋙
                    forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                      (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddCommGrpCat.carrier) AddGrpCat
                      (FD := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
                      AddGrpCat.carrier)) ⋙
                  forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦
                    (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddGrpCat.carrier) AddMonCat (FD :=
                    fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
                    AddMonCat.carrier)) ⋙
                forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦
                  (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddMonCat.carrier)).ColimitTypeRel
            (Sigma.mk (β := fun (j : C) ↦
              (((M ⋙
                        forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                          (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddCommGrpCat.carrier)
                          AddGrpCat (FD := fun (x1 x2 : AddGrpCat) ↦
                          (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD := AddGrpCat.carrier)) ⋙
                      forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦
                        (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddGrpCat.carrier) AddMonCat
                        (FD := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1)))
                        (CD := AddMonCat.carrier)) ⋙
                    forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦
                      (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddMonCat.carrier)).obj
                j)
              V₁ b₁) +
          Quot.mk
            (((M ⋙
                    forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                      (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddCommGrpCat.carrier) AddGrpCat
                      (FD := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
                      AddGrpCat.carrier)) ⋙
                  forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦
                    (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddGrpCat.carrier) AddMonCat (FD :=
                    fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
                    AddMonCat.carrier)) ⋙
                forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦
                  (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddMonCat.carrier)).ColimitTypeRel
            (Sigma.mk (β := fun (j : C) ↦
              (((M ⋙
                        forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                          (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddCommGrpCat.carrier)
                          AddGrpCat (FD := fun (x1 x2 : AddGrpCat) ↦
                          (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD := AddGrpCat.carrier)) ⋙
                      forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦
                        (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddGrpCat.carrier) AddMonCat
                        (FD := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1)))
                        (CD := AddMonCat.carrier)) ⋙
                    forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦
                      (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddMonCat.carrier)).obj
                j)
              V₂ b₂)) =
      Quot.mk
            (((R ⋙
                    forget₂ RingCat (FC := fun (R S : RingCat) ↦
                      (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC := RingCat.carrier) SemiRingCat
                      (FD := fun (R S : SemiRingCat) ↦ (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CD :=
                      SemiRingCat.carrier)) ⋙
                  forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                    (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC := SemiRingCat.carrier) MonCat (FD :=
                    fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1))) (CD :=
                    MonCat.carrier)) ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1)))
                  (CC := MonCat.carrier)).ColimitTypeRel
            (Sigma.mk (β := fun (j : C) ↦
              (((R ⋙
                        forget₂ RingCat (FC := fun (R S : RingCat) ↦
                          (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC := RingCat.carrier) SemiRingCat
                          (FD := fun (R S : SemiRingCat) ↦ (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1)))
                          (CD := SemiRingCat.carrier)) ⋙
                      forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                        (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC := SemiRingCat.carrier) MonCat
                        (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1))) (CD :=
                        MonCat.carrier)) ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦
                      (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1))) (CC := MonCat.carrier)).obj
                j)
              U a) •
          Quot.mk
            (((M ⋙
                    forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                      (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddCommGrpCat.carrier) AddGrpCat
                      (FD := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
                      AddGrpCat.carrier)) ⋙
                  forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦
                    (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddGrpCat.carrier) AddMonCat (FD :=
                    fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
                    AddMonCat.carrier)) ⋙
                forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦
                  (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddMonCat.carrier)).ColimitTypeRel
            (Sigma.mk (β := fun (j : C) ↦
              (((M ⋙
                        forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                          (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddCommGrpCat.carrier)
                          AddGrpCat (FD := fun (x1 x2 : AddGrpCat) ↦
                          (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD := AddGrpCat.carrier)) ⋙
                      forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦
                        (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddGrpCat.carrier) AddMonCat
                        (FD := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1)))
                        (CD := AddMonCat.carrier)) ⋙
                    forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦
                      (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddMonCat.carrier)).obj
                j)
              V₁ b₁) +
        Quot.mk
            (((R ⋙
                    forget₂ RingCat (FC := fun (R S : RingCat) ↦
                      (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC := RingCat.carrier) SemiRingCat
                      (FD := fun (R S : SemiRingCat) ↦ (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CD :=
                      SemiRingCat.carrier)) ⋙
                  forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                    (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC := SemiRingCat.carrier) MonCat (FD :=
                    fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1))) (CD :=
                    MonCat.carrier)) ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1)))
                  (CC := MonCat.carrier)).ColimitTypeRel
            (Sigma.mk (β := fun (j : C) ↦
              (((R ⋙
                        forget₂ RingCat (FC := fun (R S : RingCat) ↦
                          (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC := RingCat.carrier) SemiRingCat
                          (FD := fun (R S : SemiRingCat) ↦ (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1)))
                          (CD := SemiRingCat.carrier)) ⋙
                      forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                        (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC := SemiRingCat.carrier) MonCat
                        (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1))) (CD :=
                        MonCat.carrier)) ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦
                      (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1))) (CC := MonCat.carrier)).obj
                j)
              U a) •
          Quot.mk
            (((M ⋙
                    forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                      (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddCommGrpCat.carrier) AddGrpCat
                      (FD := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
                      AddGrpCat.carrier)) ⋙
                  forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦
                    (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddGrpCat.carrier) AddMonCat (FD :=
                    fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
                    AddMonCat.carrier)) ⋙
                forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦
                  (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddMonCat.carrier)).ColimitTypeRel
            (Sigma.mk (β := fun (j : C) ↦
              (((M ⋙
                        forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                          (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddCommGrpCat.carrier)
                          AddGrpCat (FD := fun (x1 x2 : AddGrpCat) ↦
                          (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD := AddGrpCat.carrier)) ⋙
                      forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦
                        (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddGrpCat.carrier) AddMonCat
                        (FD := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1)))
                        (CD := AddMonCat.carrier)) ⋙
                    forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦
                      (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddMonCat.carrier)).obj
                j)
              V₂ b₂)
⊢ Quot.mk
        (((R ⋙
                forget₂ RingCat (FC := fun (R S : RingCat) ↦ (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1)))
                  (CC := RingCat.carrier) SemiRingCat (FD := fun (R S : SemiRingCat) ↦
                  (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CD := SemiRingCat.carrier)) ⋙
              forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC := SemiRingCat.carrier) MonCat (FD :=
                fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1))) (CD :=
                MonCat.carrier)) ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1))) (CC :=
              MonCat.carrier)).ColimitTypeRel
        (Sigma.mk (β := fun (j : C) ↦
          (((R ⋙
                    forget₂ RingCat (FC := fun (R S : RingCat) ↦
                      (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC := RingCat.carrier) SemiRingCat
                      (FD := fun (R S : SemiRingCat) ↦ (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CD :=
                      SemiRingCat.carrier)) ⋙
                  forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                    (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC := SemiRingCat.carrier) MonCat (FD :=
                    fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1))) (CD :=
                    MonCat.carrier)) ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1)))
                  (CC := MonCat.carrier)).obj
            j)
          U a) •
      (Quot.mk
          (((M ⋙
                  forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                    (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddCommGrpCat.carrier) AddGrpCat
                    (FD := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
                    AddGrpCat.carrier)) ⋙
                forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦
                  (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddGrpCat.carrier) AddMonCat (FD :=
                  fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
                  AddMonCat.carrier)) ⋙
              forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦
                (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddMonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : C) ↦
            (((M ⋙
                      forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                        (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddCommGrpCat.carrier)
                        AddGrpCat (FD := fun (x1 x2 : AddGrpCat) ↦
                        (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD := AddGrpCat.carrier)) ⋙
                    forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦
                      (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddGrpCat.carrier) AddMonCat
                      (FD := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
                      AddMonCat.carrier)) ⋙
                  forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦
                    (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddMonCat.carrier)).obj
              j)
            V₁ b₁) +
        Quot.mk
          (((M ⋙
                  forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                    (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddCommGrpCat.carrier) AddGrpCat
                    (FD := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
                    AddGrpCat.carrier)) ⋙
                forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦
                  (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddGrpCat.carrier) AddMonCat (FD :=
                  fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
                  AddMonCat.carrier)) ⋙
              forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦
                (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddMonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : C) ↦
            (((M ⋙
                      forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                        (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddCommGrpCat.carrier)
                        AddGrpCat (FD := fun (x1 x2 : AddGrpCat) ↦
                        (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD := AddGrpCat.carrier)) ⋙
                    forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦
                      (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddGrpCat.carrier) AddMonCat
                      (FD := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
                      AddMonCat.carrier)) ⋙
                  forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦
                    (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddMonCat.carrier)).obj
              j)
            V₂ b₂)) =
    Quot.mk
          (((R ⋙
                  forget₂ RingCat (FC := fun (R S : RingCat) ↦ (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1)))
                    (CC := RingCat.carrier) SemiRingCat (FD := fun (R S : SemiRingCat) ↦
                    (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CD := SemiRingCat.carrier)) ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                  (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC := SemiRingCat.carrier) MonCat (FD :=
                  fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1))) (CD :=
                  MonCat.carrier)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1)))
                (CC := MonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : C) ↦
            (((R ⋙
                      forget₂ RingCat (FC := fun (R S : RingCat) ↦
                        (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC := RingCat.carrier) SemiRingCat
                        (FD := fun (R S : SemiRingCat) ↦ (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CD :=
                        SemiRingCat.carrier)) ⋙
                    forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                      (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC := SemiRingCat.carrier) MonCat (FD :=
                      fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1))) (CD :=
                      MonCat.carrier)) ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1)))
                    (CC := MonCat.carrier)).obj
              j)
            U a) •
        Quot.mk
          (((M ⋙
                  forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                    (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddCommGrpCat.carrier) AddGrpCat
                    (FD := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
                    AddGrpCat.carrier)) ⋙
                forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦
                  (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddGrpCat.carrier) AddMonCat (FD :=
                  fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
                  AddMonCat.carrier)) ⋙
              forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦
                (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddMonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : C) ↦
            (((M ⋙
                      forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                        (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddCommGrpCat.carrier)
                        AddGrpCat (FD := fun (x1 x2 : AddGrpCat) ↦
                        (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD := AddGrpCat.carrier)) ⋙
                    forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦
                      (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddGrpCat.carrier) AddMonCat
                      (FD := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
                      AddMonCat.carrier)) ⋙
                  forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦
                    (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddMonCat.carrier)).obj
              j)
            V₁ b₁) +
      Quot.mk
          (((R ⋙
                  forget₂ RingCat (FC := fun (R S : RingCat) ↦ (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1)))
                    (CC := RingCat.carrier) SemiRingCat (FD := fun (R S : SemiRingCat) ↦
                    (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CD := SemiRingCat.carrier)) ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                  (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC := SemiRingCat.carrier) MonCat (FD :=
                  fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1))) (CD :=
                  MonCat.carrier)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1)))
                (CC := MonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : C) ↦
            (((R ⋙
                      forget₂ RingCat (FC := fun (R S : RingCat) ↦
                        (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC := RingCat.carrier) SemiRingCat
                        (FD := fun (R S : SemiRingCat) ↦ (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CD :=
                        SemiRingCat.carrier)) ⋙
                    forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                      (↑R : Type (max u_2 u_1)) →+* (↑S : Type (max u_2 u_1))) (CC := SemiRingCat.carrier) MonCat (FD :=
                      fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1))) (CD :=
                      MonCat.carrier)) ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u_2 u_1)) →* (↑x2 : Type (max u_2 u_1)))
                    (CC := MonCat.carrier)).obj
              j)
            U a) •
        Quot.mk
          (((M ⋙
                  forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                    (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddCommGrpCat.carrier) AddGrpCat
                    (FD := fun (x1 x2 : AddGrpCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
                    AddGrpCat.carrier)) ⋙
                forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦
                  (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddGrpCat.carrier) AddMonCat (FD :=
                  fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
                  AddMonCat.carrier)) ⋙
              forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦
                (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddMonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : C) ↦
            (((M ⋙
                      forget₂ AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat) ↦
                        (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddCommGrpCat.carrier)
                        AddGrpCat (FD := fun (x1 x2 : AddGrpCat) ↦
                        (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD := AddGrpCat.carrier)) ⋙
                    forget₂ AddGrpCat (FC := fun (x1 x2 : AddGrpCat) ↦
                      (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddGrpCat.carrier) AddMonCat
                      (FD := fun (x1 x2 : AddMonCat) ↦ (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CD :=
                      AddMonCat.carrier)) ⋙
                  forget AddMonCat (FC := fun (x1 x2 : AddMonCat) ↦
                    (↑x1 : Type (max u_3 u_1)) →+ (↑x2 : Type (max u_3 u_1))) (CC := AddMonCat.carrier)).obj
              j)
            V₂ b₂)

Tactic:
obtain ⟨s, α, β, h₁, h₂, h₃, h₄⟩ := crown₄
      (leftToMax U V₁ ≫ leftToMax (max U V₁) (max U V₂)) (leftToMax U (max V₁ V₂))
      (leftToMax U V₂ ≫ rightToMax (max U V₁) (max U V₂)) (leftToMax U (max V₁ V₂))
      (rightToMax U V₁ ≫ leftToMax (max U V₁) (max U V₂))
      (leftToMax V₁ V₂ ≫ rightToMax U (max V₁ V₂))
      (rightToMax U V₂ ≫ rightToMax (max U V₁) (max U V₂))
      (rightToMax V₁ V₂ ≫ rightToMax U (max V₁ V₂))

Premises used: CategoryTheory.IsFiltered.rightToMax, CategoryTheory.IsFiltered.crown₄, CategoryTheory.IsFiltered.max, CategoryTheory.CategoryStruct.comp, CategoryTheory.IsFiltered.leftToMax