Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j₁ : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₃
k : J := IsFiltered.max₃ j₁ j₂ j₃
f : j₁ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.firstToMax₃ j₁ j₂ j₃
g : j₂ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.secondToMax₃ j₁ j₂ j₃
h : j₃ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.thirdToMax₃ j₁ j₂ j₃
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat)
      ⟨k,
        (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map f)) ⟨j₁, x⟩.snd *
          (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map (𝟙 k)))
            ⟨k,
                (ConcreteCategory.hom
                      (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map g))
                    ⟨j₂, y⟩.snd +
                  (ConcreteCategory.hom
                      (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map h))
                    ⟨j₃, z⟩.snd⟩.snd⟩ =
    MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat)
        ⟨k,
          (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map f)) ⟨j₁, x⟩.snd *
            (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map g)) ⟨j₂, y⟩.snd⟩ +
      MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat)
        ⟨k,
          (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map f)) ⟨j₁, x⟩.snd *
            (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map h)) ⟨j₃, z⟩.snd⟩

Tactic:
colimit_add_mk_eq _ ⟨k, _⟩ ⟨k, _⟩ k (𝟙 k) (𝟙 k)

Goal state after:
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
j₁ : J
x : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCat MonCat) ⋙ forget MonCat).obj j₃
k : J := IsFiltered.max₃ j₁ j₂ j₃
f : j₁ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.firstToMax₃ j₁ j₂ j₃
g : j₂ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.secondToMax₃ j₁ j₂ j₃
h : j₃ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.thirdToMax₃ j₁ j₂ j₃
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCat MonCat)
      ⟨k,
        (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map f)) ⟨j₁, x⟩.snd *
          (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map (𝟙 k)))
            ⟨k,
                (ConcreteCategory.hom
                      (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map g))
                    ⟨j₂, y⟩.snd +
                  (ConcreteCategory.hom
                      (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map h))
                    ⟨j₃, z⟩.snd⟩.snd⟩ =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat)
      ⟨k,
        (ConcreteCategory.hom (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map (𝟙 k)))
            ⟨k,
                (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map f)) ⟨j₁, x⟩.snd *
                  (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map g)) ⟨j₂, y⟩.snd⟩.snd +
          (ConcreteCategory.hom (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map (𝟙 k)))
            ⟨k,
                (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map f)) ⟨j₁, x⟩.snd *
                  (ConcreteCategory.hom ((F ⋙ forget₂ SemiRingCat MonCat).map h)) ⟨j₃, z⟩.snd⟩.snd⟩