[GOAL]
J : Type v
inst✝ : SmallCategory J
F : J ⥤ SemiRingCatMax
j : J
⊢ Semiring ↑(F.obj j)
[PROOFSTEP]
infer_instance
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
x y z : ↑(R F)
⊢ x * (y + z) = x * y + x * z
[PROOFSTEP]
refine Quot.induction_on₃ x y z ?_
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
x y z : ↑(R F)
⊢ ∀ (a b c : (j : J) × ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j),
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) a *
        (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) b +
          Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) c) =
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) a *
          Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) b +
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) a *
          Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) c
[PROOFSTEP]
clear x y z
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
⊢ ∀ (a b c : (j : J) × ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j),
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) a *
        (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) b +
          Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) c) =
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) a *
          Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) b +
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) a *
          Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) c
[PROOFSTEP]
intro x y z
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
x y z : (j : J) × ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j
⊢ Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) x *
      (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) y +
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) z) =
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) x *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) y +
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) x *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) z
[PROOFSTEP]
cases' x with j₁ x
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
y z : (j : J) × ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j
j₁ : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₁
⊢ Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
      (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) y +
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) z) =
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) y +
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) z
[PROOFSTEP]
cases' y with j₂ y
[GOAL]
case mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
z : (j : J) × ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j
j₁ : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₂
⊢ Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
      (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y } +
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) z) =
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y } +
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) z
[PROOFSTEP]
cases' z with j₃ z
[GOAL]
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j₁ : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₃
⊢ Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
      (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y } +
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z }) =
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y } +
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z }
[PROOFSTEP]
let k := IsFiltered.max₃ j₁ j₂ j₃
[GOAL]
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j₁ : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₃
k : J := IsFiltered.max₃ j₁ j₂ j₃
⊢ Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
      (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y } +
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z }) =
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y } +
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z }
[PROOFSTEP]
let f := IsFiltered.firstToMax₃ j₁ j₂ j₃
[GOAL]
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j₁ : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₃
k : J := IsFiltered.max₃ j₁ j₂ j₃
f : j₁ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.firstToMax₃ j₁ j₂ j₃
⊢ Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
      (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y } +
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z }) =
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y } +
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z }
[PROOFSTEP]
let g := IsFiltered.secondToMax₃ j₁ j₂ j₃
[GOAL]
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j₁ : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCatMax 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₃
⊢ Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
      (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y } +
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z }) =
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y } +
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z }
[PROOFSTEP]
let h := IsFiltered.thirdToMax₃ j₁ j₂ j₃
[GOAL]
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j₁ : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCatMax 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₃
⊢ Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
      (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y } +
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z }) =
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y } +
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z }
[PROOFSTEP]
erw [colimit_add_mk_eq _ ⟨j₂, _⟩ ⟨j₃, _⟩ k g h, colimit_mul_mk_eq _ ⟨j₁, _⟩ ⟨k, _⟩ k f (𝟙 k),
  colimit_mul_mk_eq _ ⟨j₁, _⟩ ⟨j₂, _⟩ k f g, colimit_mul_mk_eq _ ⟨j₁, _⟩ ⟨j₃, _⟩ k f h,
  colimit_add_mk_eq _ ⟨k, _⟩ ⟨k, _⟩ k (𝟙 k) (𝟙 k)]
[GOAL]
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j₁ : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCatMax 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₂ SemiRingCatMax MonCat)
      { fst := k,
        snd :=
          ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map f) { fst := j₁, snd := x }.snd *
            ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (𝟙 k))
              { fst := k,
                  snd :=
                    ↑(((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map g)
                        { fst := j₂, snd := y }.snd +
                      ↑(((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map h)
                        { fst := j₃, snd := z }.snd }.snd } =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat)
      { fst := k,
        snd :=
          ↑(((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map (𝟙 k))
              { fst := k,
                  snd :=
                    ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map f) { fst := j₁, snd := x }.snd *
                      ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map g) { fst := j₂, snd := y }.snd }.snd +
            ↑(((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map (𝟙 k))
              { fst := k,
                  snd :=
                    ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map f) { fst := j₁, snd := x }.snd *
                      ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map h) { fst := j₃, snd := z }.snd }.snd }
[PROOFSTEP]
simp only [CategoryTheory.Functor.map_id, id_apply]
[GOAL]
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j₁ : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCatMax 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₂ SemiRingCatMax MonCat)
      { fst := IsFiltered.max₃ j₁ j₂ j₃,
        snd :=
          ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (IsFiltered.firstToMax₃ j₁ j₂ j₃)) x *
            ↑(𝟙 ((F ⋙ forget₂ SemiRingCatMax MonCat).obj (IsFiltered.max₃ j₁ j₂ j₃)))
              (↑(((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map
                      (IsFiltered.secondToMax₃ j₁ j₂ j₃))
                  y +
                ↑(((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map
                      (IsFiltered.thirdToMax₃ j₁ j₂ j₃))
                  z) } =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat)
      { fst := IsFiltered.max₃ j₁ j₂ j₃,
        snd :=
          ↑(𝟙
                  (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).obj
                    (IsFiltered.max₃ j₁ j₂ j₃)))
              (↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (IsFiltered.firstToMax₃ j₁ j₂ j₃)) x *
                ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (IsFiltered.secondToMax₃ j₁ j₂ j₃)) y) +
            ↑(𝟙
                  (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).obj
                    (IsFiltered.max₃ j₁ j₂ j₃)))
              (↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (IsFiltered.firstToMax₃ j₁ j₂ j₃)) x *
                ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (IsFiltered.thirdToMax₃ j₁ j₂ j₃)) z) }
[PROOFSTEP]
erw [left_distrib (F.map f x) (F.map g y) (F.map h z)]
[GOAL]
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j₁ : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCatMax 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₂ SemiRingCatMax MonCat)
      { fst := IsFiltered.max₃ j₁ j₂ j₃, snd := ↑(F.map f) x * ↑(F.map g) y + ↑(F.map f) x * ↑(F.map h) z } =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat)
      { fst := IsFiltered.max₃ j₁ j₂ j₃,
        snd :=
          ↑(𝟙
                  (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).obj
                    (IsFiltered.max₃ j₁ j₂ j₃)))
              (↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (IsFiltered.firstToMax₃ j₁ j₂ j₃)) x *
                ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (IsFiltered.secondToMax₃ j₁ j₂ j₃)) y) +
            ↑(𝟙
                  (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).obj
                    (IsFiltered.max₃ j₁ j₂ j₃)))
              (↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (IsFiltered.firstToMax₃ j₁ j₂ j₃)) x *
                ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (IsFiltered.thirdToMax₃ j₁ j₂ j₃)) z) }
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
x y z : ↑(R F)
⊢ (x + y) * z = x * z + y * z
[PROOFSTEP]
refine Quot.induction_on₃ x y z ?_
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
x y z : ↑(R F)
⊢ ∀ (a b c : (j : J) × ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j),
    (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) a +
          Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) b) *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) c =
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) a *
          Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) c +
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) b *
          Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) c
[PROOFSTEP]
clear x y z
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
⊢ ∀ (a b c : (j : J) × ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j),
    (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) a +
          Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) b) *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) c =
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) a *
          Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) c +
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) b *
          Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) c
[PROOFSTEP]
intro x y z
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
x y z : (j : J) × ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j
⊢ (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) x +
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) y) *
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) z =
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) x *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) z +
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) y *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) z
[PROOFSTEP]
cases' x with j₁ x
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
y z : (j : J) × ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j
j₁ : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₁
⊢ (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } +
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) y) *
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) z =
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) z +
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) y *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) z
[PROOFSTEP]
cases' y with j₂ y
[GOAL]
case mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
z : (j : J) × ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j
j₁ : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₂
⊢ (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } +
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y }) *
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) z =
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) z +
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) z
[PROOFSTEP]
cases' z with j₃ z
[GOAL]
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j₁ : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₃
⊢ (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } +
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y }) *
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z } =
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z } +
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z }
[PROOFSTEP]
let k := IsFiltered.max₃ j₁ j₂ j₃
[GOAL]
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j₁ : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₃
k : J := IsFiltered.max₃ j₁ j₂ j₃
⊢ (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } +
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y }) *
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z } =
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z } +
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z }
[PROOFSTEP]
let f := IsFiltered.firstToMax₃ j₁ j₂ j₃
[GOAL]
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j₁ : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₃
k : J := IsFiltered.max₃ j₁ j₂ j₃
f : j₁ ⟶ IsFiltered.max₃ j₁ j₂ j₃ := IsFiltered.firstToMax₃ j₁ j₂ j₃
⊢ (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } +
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y }) *
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z } =
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z } +
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z }
[PROOFSTEP]
let g := IsFiltered.secondToMax₃ j₁ j₂ j₃
[GOAL]
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j₁ : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCatMax 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₃
⊢ (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } +
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y }) *
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z } =
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z } +
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z }
[PROOFSTEP]
let h := IsFiltered.thirdToMax₃ j₁ j₂ j₃
[GOAL]
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j₁ : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCatMax 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₃
⊢ (Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } +
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y }) *
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z } =
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₁, snd := x } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z } +
      Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₂, snd := y } *
        Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j₃, snd := z }
[PROOFSTEP]
erw [colimit_add_mk_eq _ ⟨j₁, _⟩ ⟨j₂, _⟩ k f g, colimit_mul_mk_eq _ ⟨k, _⟩ ⟨j₃, _⟩ k (𝟙 k) h,
  colimit_mul_mk_eq _ ⟨j₁, _⟩ ⟨j₃, _⟩ k f h, colimit_mul_mk_eq _ ⟨j₂, _⟩ ⟨j₃, _⟩ k g h,
  colimit_add_mk_eq _ ⟨k, _⟩ ⟨k, _⟩ k (𝟙 k) (𝟙 k)]
[GOAL]
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j₁ : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCatMax 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₂ SemiRingCatMax MonCat)
      { fst := k,
        snd :=
          ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (𝟙 k))
              { fst := k,
                  snd :=
                    ↑(((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map f)
                        { fst := j₁, snd := x }.snd +
                      ↑(((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map g)
                        { fst := j₂, snd := y }.snd }.snd *
            ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map h) { fst := j₃, snd := z }.snd } =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat)
      { fst := k,
        snd :=
          ↑(((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map (𝟙 k))
              { fst := k,
                  snd :=
                    ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map f) { fst := j₁, snd := x }.snd *
                      ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map h) { fst := j₃, snd := z }.snd }.snd +
            ↑(((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map (𝟙 k))
              { fst := k,
                  snd :=
                    ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map g) { fst := j₂, snd := y }.snd *
                      ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map h) { fst := j₃, snd := z }.snd }.snd }
[PROOFSTEP]
simp only [CategoryTheory.Functor.map_id, id_apply]
[GOAL]
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j₁ : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCatMax 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₂ SemiRingCatMax MonCat)
      { fst := IsFiltered.max₃ j₁ j₂ j₃,
        snd :=
          ↑(𝟙 ((F ⋙ forget₂ SemiRingCatMax MonCat).obj (IsFiltered.max₃ j₁ j₂ j₃)))
              (↑(((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map
                      (IsFiltered.firstToMax₃ j₁ j₂ j₃))
                  x +
                ↑(((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).map
                      (IsFiltered.secondToMax₃ j₁ j₂ j₃))
                  y) *
            ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (IsFiltered.thirdToMax₃ j₁ j₂ j₃)) z } =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat)
      { fst := IsFiltered.max₃ j₁ j₂ j₃,
        snd :=
          ↑(𝟙
                  (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).obj
                    (IsFiltered.max₃ j₁ j₂ j₃)))
              (↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (IsFiltered.firstToMax₃ j₁ j₂ j₃)) x *
                ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (IsFiltered.thirdToMax₃ j₁ j₂ j₃)) z) +
            ↑(𝟙
                  (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).obj
                    (IsFiltered.max₃ j₁ j₂ j₃)))
              (↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (IsFiltered.secondToMax₃ j₁ j₂ j₃)) y *
                ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (IsFiltered.thirdToMax₃ j₁ j₂ j₃)) z) }
[PROOFSTEP]
erw [right_distrib (F.map f x) (F.map g y) (F.map h z)]
[GOAL]
case mk.mk.mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j₁ : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₁
j₂ : J
y : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j₂
j₃ : J
z : ((F ⋙ forget₂ SemiRingCatMax 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₂ SemiRingCatMax MonCat)
      { fst := IsFiltered.max₃ j₁ j₂ j₃, snd := ↑(F.map f) x * ↑(F.map h) z + ↑(F.map g) y * ↑(F.map h) z } =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat)
      { fst := IsFiltered.max₃ j₁ j₂ j₃,
        snd :=
          ↑(𝟙
                  (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).obj
                    (IsFiltered.max₃ j₁ j₂ j₃)))
              (↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (IsFiltered.firstToMax₃ j₁ j₂ j₃)) x *
                ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (IsFiltered.thirdToMax₃ j₁ j₂ j₃)) z) +
            ↑(𝟙
                  (((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat).obj
                    (IsFiltered.max₃ j₁ j₂ j₃)))
              (↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (IsFiltered.secondToMax₃ j₁ j₂ j₃)) y *
                ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (IsFiltered.thirdToMax₃ j₁ j₂ j₃)) z) }
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
x : ↑(R F)
⊢ 0 * x = 0
[PROOFSTEP]
refine Quot.inductionOn x ?_
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
x : ↑(R F)
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j),
    0 * Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) a = 0
[PROOFSTEP]
clear x
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j),
    0 * Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) a = 0
[PROOFSTEP]
intro x
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
x : (j : J) × ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j
⊢ 0 * Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) x = 0
[PROOFSTEP]
cases' x with j x
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j
⊢ 0 * Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j, snd := x } = 0
[PROOFSTEP]
erw [colimit_zero_eq _ j, colimit_mul_mk_eq _ ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j)]
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCatMax MonCat)
      { fst := j,
        snd :=
          ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (𝟙 j)) { fst := j, snd := 0 }.snd *
            ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (𝟙 j)) { fst := j, snd := x }.snd } =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat)
      { fst := j, snd := 0 }
[PROOFSTEP]
rw [CategoryTheory.Functor.map_id]
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCatMax MonCat)
      { fst := j,
        snd :=
          ↑(𝟙 ((F ⋙ forget₂ SemiRingCatMax MonCat).obj { fst := j, snd := 0 }.fst)) { fst := j, snd := 0 }.snd *
            ↑(𝟙 ((F ⋙ forget₂ SemiRingCatMax MonCat).obj { fst := j, snd := 0 }.fst)) { fst := j, snd := x }.snd } =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat)
      { fst := j, snd := 0 }
[PROOFSTEP]
dsimp
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCatMax MonCat) { fst := j, snd := 0 * x } =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat)
      { fst := j, snd := 0 }
[PROOFSTEP]
rw [zero_mul x]
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCatMax MonCat) { fst := j, snd := 0 } =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat)
      { fst := j, snd := 0 }
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
x : ↑(R F)
⊢ x * 0 = 0
[PROOFSTEP]
refine Quot.inductionOn x ?_
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
x : ↑(R F)
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j),
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) a * 0 = 0
[PROOFSTEP]
clear x
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
⊢ ∀ (a : (j : J) × ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j),
    Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) a * 0 = 0
[PROOFSTEP]
intro x
[GOAL]
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
x : (j : J) × ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j
⊢ Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) x * 0 = 0
[PROOFSTEP]
cases' x with j x
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j
⊢ Quot.mk (Types.Quot.Rel ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat)) { fst := j, snd := x } * 0 = 0
[PROOFSTEP]
erw [colimit_zero_eq _ j, colimit_mul_mk_eq _ ⟨j, _⟩ ⟨j, _⟩ j (𝟙 j) (𝟙 j)]
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCatMax MonCat)
      { fst := j,
        snd :=
          ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (𝟙 j)) { fst := j, snd := x }.snd *
            ↑((F ⋙ forget₂ SemiRingCatMax MonCat).map (𝟙 j)) { fst := j, snd := 0 }.snd } =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat)
      { fst := j, snd := 0 }
[PROOFSTEP]
rw [CategoryTheory.Functor.map_id]
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCatMax MonCat)
      { fst := j,
        snd :=
          ↑(𝟙 ((F ⋙ forget₂ SemiRingCatMax MonCat).obj { fst := j, snd := x }.fst)) { fst := j, snd := x }.snd *
            ↑(𝟙 ((F ⋙ forget₂ SemiRingCatMax MonCat).obj { fst := j, snd := x }.fst)) { fst := j, snd := 0 }.snd } =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat)
      { fst := j, snd := 0 }
[PROOFSTEP]
dsimp
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCatMax MonCat) { fst := j, snd := x * 0 } =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat)
      { fst := j, snd := 0 }
[PROOFSTEP]
rw [mul_zero x]
[GOAL]
case mk
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCatMax
inst✝ : IsFiltered J
src✝¹ : Monoid ↑(R F) := (R F).str
src✝ : AddCommMonoid ↑(AddCommMonCat.FilteredColimits.M (F ⋙ forget₂ SemiRingCat AddCommMonCat)) :=
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid (F ⋙ forget₂ SemiRingCat AddCommMonCat)
j : J
x : ((F ⋙ forget₂ SemiRingCatMax MonCat) ⋙ forget MonCat).obj j
⊢ MonCat.FilteredColimits.M.mk (F ⋙ forget₂ SemiRingCatMax MonCat) { fst := j, snd := 0 } =
    AddMonCat.FilteredColimits.M.mk ((F ⋙ forget₂ SemiRingCat AddCommMonCat) ⋙ forget₂ AddCommMonCat AddMonCat)
      { fst := j, snd := 0 }
[PROOFSTEP]
rfl
