[GOAL]
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (ε : α), 1 < ε → a / ε ≤ b
ε : α
ε1 : ε < 1
⊢ a * ε ≤ b
[PROOFSTEP]
simpa only [div_eq_mul_inv, inv_inv] using h ε⁻¹ (Left.one_lt_inv_iff.2 ε1)


[GOAL]
⊢ ConcreteCategory SemiRingCat
[PROOFSTEP]
dsimp [SemiRingCat]
[GOAL]
⊢ ConcreteCategory (Bundled Semiring)
[PROOFSTEP]
infer_instance
[GOAL]
X Y : SemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget SemiRingCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget SemiRingCat).map f)
[GOAL]
X Y : SemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget SemiRingCat).map f)
i : (forget SemiRingCat).obj X ≅ (forget SemiRingCat).obj Y := asIso ((forget SemiRingCat).map f)
⊢ IsIso f
[PROOFSTEP]
let ff : X →+* Y := f
[GOAL]
X Y : SemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget SemiRingCat).map f)
i : (forget SemiRingCat).obj X ≅ (forget SemiRingCat).obj Y := asIso ((forget SemiRingCat).map f)
ff : ↑X →+* ↑Y := f
⊢ IsIso f
[PROOFSTEP]
let e : X ≃+* Y := { ff, i.toEquiv with }
[GOAL]
X Y : SemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget SemiRingCat).map f)
i : (forget SemiRingCat).obj X ≅ (forget SemiRingCat).obj Y := asIso ((forget SemiRingCat).map f)
ff : ↑X →+* ↑Y := f
e : ↑X ≃+* ↑Y :=
  let src := i.toEquiv;
  {
    toEquiv :=
      { toFun := ff.toFun, invFun := src.invFun, left_inv := (_ : Function.LeftInverse src.invFun src.toFun),
        right_inv := (_ : Function.RightInverse src.invFun src.toFun) },
    map_mul' := (_ : ∀ (x y : ↑X), OneHom.toFun (↑↑ff) (x * y) = OneHom.toFun (↑↑ff) x * OneHom.toFun (↑↑ff) y),
    map_add' := (_ : ∀ (x y : ↑X), OneHom.toFun (↑↑ff) (x + y) = OneHom.toFun (↑↑ff) x + OneHom.toFun (↑↑ff) y) }
⊢ IsIso f
[PROOFSTEP]
exact ⟨(IsIso.of_iso e.toSemiRingCatIso).1⟩
[GOAL]
⊢ ConcreteCategory RingCat
[PROOFSTEP]
dsimp [RingCat]
[GOAL]
⊢ ConcreteCategory (Bundled Ring)
[PROOFSTEP]
infer_instance
[GOAL]
⊢ ConcreteCategory CommSemiRingCat
[PROOFSTEP]
dsimp [CommSemiRingCat]
[GOAL]
⊢ ConcreteCategory (Bundled CommSemiring)
[PROOFSTEP]
infer_instance
[GOAL]
⊢ ∀ {X Y : CommSemiRingCat} {f : X ⟶ Y},
    HEq ((forget CommMonCat).map ((fun {R₁ R₂} f => ↑f) f)) ((forget CommSemiRingCat).map f)
[PROOFSTEP]
rfl
[GOAL]
X Y : CommSemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommSemiRingCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget CommSemiRingCat).map f)
[GOAL]
X Y : CommSemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommSemiRingCat).map f)
i : (forget CommSemiRingCat).obj X ≅ (forget CommSemiRingCat).obj Y := asIso ((forget CommSemiRingCat).map f)
⊢ IsIso f
[PROOFSTEP]
let ff : X →+* Y := f
[GOAL]
X Y : CommSemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommSemiRingCat).map f)
i : (forget CommSemiRingCat).obj X ≅ (forget CommSemiRingCat).obj Y := asIso ((forget CommSemiRingCat).map f)
ff : ↑X →+* ↑Y := f
⊢ IsIso f
[PROOFSTEP]
let e : X ≃+* Y := { ff, i.toEquiv with }
[GOAL]
X Y : CommSemiRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommSemiRingCat).map f)
i : (forget CommSemiRingCat).obj X ≅ (forget CommSemiRingCat).obj Y := asIso ((forget CommSemiRingCat).map f)
ff : ↑X →+* ↑Y := f
e : ↑X ≃+* ↑Y :=
  let src := i.toEquiv;
  {
    toEquiv :=
      { toFun := ff.toFun, invFun := src.invFun, left_inv := (_ : Function.LeftInverse src.invFun src.toFun),
        right_inv := (_ : Function.RightInverse src.invFun src.toFun) },
    map_mul' := (_ : ∀ (x y : ↑X), OneHom.toFun (↑↑ff) (x * y) = OneHom.toFun (↑↑ff) x * OneHom.toFun (↑↑ff) y),
    map_add' := (_ : ∀ (x y : ↑X), OneHom.toFun (↑↑ff) (x + y) = OneHom.toFun (↑↑ff) x + OneHom.toFun (↑↑ff) y) }
⊢ IsIso f
[PROOFSTEP]
exact ⟨(IsIso.of_iso e.toSemiRingCatIso).1⟩
[GOAL]
⊢ ConcreteCategory CommRingCat
[PROOFSTEP]
dsimp [CommRingCat]
[GOAL]
⊢ ConcreteCategory (Bundled CommRing)
[PROOFSTEP]
infer_instance
[GOAL]
⊢ ∀ {X Y : CommRingCat} {f : X ⟶ Y},
    HEq ((forget CommSemiRingCat).map ((fun {R₁ R₂} f => f) f)) ((forget CommRingCat).map f)
[PROOFSTEP]
rfl
[GOAL]
R S : CommRingCat
i : R ⟶ S
r : ↑R
h : r = 0
⊢ ↑i r = 0
[PROOFSTEP]
simp [h]
[GOAL]
X Y : RingCat
i : X ≅ Y
x : ↑X
⊢ ↑(i.hom ≫ i.inv) x = x
[PROOFSTEP]
rw [i.hom_inv_id]
[GOAL]
X Y : RingCat
i : X ≅ Y
x : ↑X
⊢ ↑(𝟙 X) x = x
[PROOFSTEP]
rfl
[GOAL]
X Y : RingCat
i : X ≅ Y
x : ↑Y
⊢ ↑(i.inv ≫ i.hom) x = x
[PROOFSTEP]
rw [i.inv_hom_id]
[GOAL]
X Y : RingCat
i : X ≅ Y
x : ↑Y
⊢ ↑(𝟙 Y) x = x
[PROOFSTEP]
rfl
[GOAL]
X Y : CommRingCat
i : X ≅ Y
x : ↑X
⊢ ↑(i.hom ≫ i.inv) x = x
[PROOFSTEP]
rw [i.hom_inv_id]
[GOAL]
X Y : CommRingCat
i : X ≅ Y
x : ↑X
⊢ ↑(𝟙 X) x = x
[PROOFSTEP]
rfl
[GOAL]
X Y : CommRingCat
i : X ≅ Y
x : ↑Y
⊢ ↑(i.inv ≫ i.hom) x = x
[PROOFSTEP]
rw [i.inv_hom_id]
[GOAL]
X Y : CommRingCat
i : X ≅ Y
x : ↑Y
⊢ ↑(𝟙 Y) x = x
[PROOFSTEP]
rfl
[GOAL]
X Y : CommRingCat
i : X ≅ Y
⊢ RingEquiv.toRingHom (commRingCatIsoToRingEquiv i) = i.hom
[PROOFSTEP]
ext
[GOAL]
case a
X Y : CommRingCat
i : X ≅ Y
x✝ : ↑X
⊢ ↑(RingEquiv.toRingHom (commRingCatIsoToRingEquiv i)) x✝ = ↑i.hom x✝
[PROOFSTEP]
rfl
[GOAL]
X Y : CommRingCat
i : X ≅ Y
⊢ RingEquiv.toRingHom (RingEquiv.symm (commRingCatIsoToRingEquiv i)) = i.inv
[PROOFSTEP]
ext
[GOAL]
case a
X Y : CommRingCat
i : X ≅ Y
x✝ : ↑Y
⊢ ↑(RingEquiv.toRingHom (RingEquiv.symm (commRingCatIsoToRingEquiv i))) x✝ = ↑i.inv x✝
[PROOFSTEP]
rfl
[GOAL]
X Y : RingCat
f : X ⟶ Y
x✝ : IsIso ((forget RingCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget RingCat).map f)
[GOAL]
X Y : RingCat
f : X ⟶ Y
x✝ : IsIso ((forget RingCat).map f)
i : (forget RingCat).obj X ≅ (forget RingCat).obj Y := asIso ((forget RingCat).map f)
⊢ IsIso f
[PROOFSTEP]
let ff : X →+* Y := f
[GOAL]
X Y : RingCat
f : X ⟶ Y
x✝ : IsIso ((forget RingCat).map f)
i : (forget RingCat).obj X ≅ (forget RingCat).obj Y := asIso ((forget RingCat).map f)
ff : ↑X →+* ↑Y := f
⊢ IsIso f
[PROOFSTEP]
let e : X ≃+* Y := { ff, i.toEquiv with }
[GOAL]
X Y : RingCat
f : X ⟶ Y
x✝ : IsIso ((forget RingCat).map f)
i : (forget RingCat).obj X ≅ (forget RingCat).obj Y := asIso ((forget RingCat).map f)
ff : ↑X →+* ↑Y := f
e : ↑X ≃+* ↑Y :=
  let src := i.toEquiv;
  {
    toEquiv :=
      { toFun := ff.toFun, invFun := src.invFun, left_inv := (_ : Function.LeftInverse src.invFun src.toFun),
        right_inv := (_ : Function.RightInverse src.invFun src.toFun) },
    map_mul' := (_ : ∀ (x y : ↑X), OneHom.toFun (↑↑ff) (x * y) = OneHom.toFun (↑↑ff) x * OneHom.toFun (↑↑ff) y),
    map_add' := (_ : ∀ (x y : ↑X), OneHom.toFun (↑↑ff) (x + y) = OneHom.toFun (↑↑ff) x + OneHom.toFun (↑↑ff) y) }
⊢ IsIso f
[PROOFSTEP]
exact ⟨(IsIso.of_iso e.toRingCatIso).1⟩
[GOAL]
X Y : CommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommRingCat).map f)
⊢ IsIso f
[PROOFSTEP]
let i := asIso ((forget CommRingCat).map f)
[GOAL]
X Y : CommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommRingCat).map f)
i : (forget CommRingCat).obj X ≅ (forget CommRingCat).obj Y := asIso ((forget CommRingCat).map f)
⊢ IsIso f
[PROOFSTEP]
let ff : X →+* Y := f
[GOAL]
X Y : CommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommRingCat).map f)
i : (forget CommRingCat).obj X ≅ (forget CommRingCat).obj Y := asIso ((forget CommRingCat).map f)
ff : ↑X →+* ↑Y := f
⊢ IsIso f
[PROOFSTEP]
let e : X ≃+* Y := { ff, i.toEquiv with }
[GOAL]
X Y : CommRingCat
f : X ⟶ Y
x✝ : IsIso ((forget CommRingCat).map f)
i : (forget CommRingCat).obj X ≅ (forget CommRingCat).obj Y := asIso ((forget CommRingCat).map f)
ff : ↑X →+* ↑Y := f
e : ↑X ≃+* ↑Y :=
  let src := i.toEquiv;
  {
    toEquiv :=
      { toFun := ff.toFun, invFun := src.invFun, left_inv := (_ : Function.LeftInverse src.invFun src.toFun),
        right_inv := (_ : Function.RightInverse src.invFun src.toFun) },
    map_mul' := (_ : ∀ (x y : ↑X), OneHom.toFun (↑↑ff) (x * y) = OneHom.toFun (↑↑ff) x * OneHom.toFun (↑↑ff) y),
    map_add' := (_ : ∀ (x y : ↑X), OneHom.toFun (↑↑ff) (x + y) = OneHom.toFun (↑↑ff) x + OneHom.toFun (↑↑ff) y) }
⊢ IsIso f
[PROOFSTEP]
exact ⟨(IsIso.of_iso e.toCommRingCatIso).1⟩
[GOAL]
⊢ ReflectsIsomorphisms (forget₂ RingCat AddCommGroupCat)
[PROOFSTEP]
infer_instance


[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


[GOAL]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
⊢ IsPrimePow ‖α‖
[PROOFSTEP]
cases' CharP.exists α with p _
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
⊢ IsPrimePow ‖α‖
[PROOFSTEP]
haveI hp := Fact.mk (CharP.char_is_prime α p)
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
⊢ IsPrimePow ‖α‖
[PROOFSTEP]
letI : Algebra (ZMod p) α := ZMod.algebra _ _
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
this : Algebra (ZMod p) α := ZMod.algebra α p
⊢ IsPrimePow ‖α‖
[PROOFSTEP]
let b := IsNoetherian.finsetBasis (ZMod p) α
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
this : Algebra (ZMod p) α := ZMod.algebra α p
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α } (ZMod p) α := IsNoetherian.finsetBasis (ZMod p) α
⊢ IsPrimePow ‖α‖
[PROOFSTEP]
rw [Module.card_fintype b, ZMod.card, isPrimePow_pow_iff]
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
this : Algebra (ZMod p) α := ZMod.algebra α p
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α } (ZMod p) α := IsNoetherian.finsetBasis (ZMod p) α
⊢ IsPrimePow p
[PROOFSTEP]
exact hp.1.isPrimePow
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
this : Algebra (ZMod p) α := ZMod.algebra α p
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α } (ZMod p) α := IsNoetherian.finsetBasis (ZMod p) α
⊢ ‖{ x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α }‖ ≠ 0
[PROOFSTEP]
rw [← FiniteDimensional.finrank_eq_card_basis b]
[GOAL]
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Field α
p : ℕ
h✝ : CharP α p
hp : Fact (Nat.Prime p)
this : Algebra (ZMod p) α := ZMod.algebra α p
b : Basis { x // x ∈ IsNoetherian.finsetBasisIndex (ZMod p) α } (ZMod p) α := IsNoetherian.finsetBasis (ZMod p) α
⊢ FiniteDimensional.finrank (ZMod p) α ≠ 0
[PROOFSTEP]
exact FiniteDimensional.finrank_pos.ne'
[GOAL]
α : Type u_1
inst✝ : Fintype α
⊢ Nonempty (Field α) ↔ IsPrimePow ‖α‖
[PROOFSTEP]
refine' ⟨fun ⟨h⟩ => Fintype.isPrimePow_card_of_field, _⟩
[GOAL]
α : Type u_1
inst✝ : Fintype α
⊢ IsPrimePow ‖α‖ → Nonempty (Field α)
[PROOFSTEP]
rintro ⟨p, n, hp, hn, hα⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Prime p
hn : 0 < n
hα : p ^ n = ‖α‖
⊢ Nonempty (Field α)
[PROOFSTEP]
haveI := Fact.mk hp.nat_prime
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Prime p
hn : 0 < n
hα : p ^ n = ‖α‖
this : Fact (Nat.Prime p)
⊢ Nonempty (Field α)
[PROOFSTEP]
exact ⟨(Fintype.equivOfCardEq ((GaloisField.card p n hn.ne').trans hα)).symm.field⟩
[GOAL]
α : Type u
inst✝ : Infinite α
⊢ Nonempty (Field α)
[PROOFSTEP]
letI K := FractionRing (MvPolynomial α <| ULift.{u} ℚ)
[GOAL]
α : Type u
inst✝ : Infinite α
K : Type u := FractionRing (MvPolynomial α (ULift ℚ))
⊢ Nonempty (Field α)
[PROOFSTEP]
suffices #α = #K by
  obtain ⟨e⟩ := Cardinal.eq.1 this
  exact ⟨e.field⟩
[GOAL]
α : Type u
inst✝ : Infinite α
K : Type u := FractionRing (MvPolynomial α (ULift ℚ))
this : #α = #K
⊢ Nonempty (Field α)
[PROOFSTEP]
obtain ⟨e⟩ := Cardinal.eq.1 this
[GOAL]
case intro
α : Type u
inst✝ : Infinite α
K : Type u := FractionRing (MvPolynomial α (ULift ℚ))
this : #α = #K
e : α ≃ K
⊢ Nonempty (Field α)
[PROOFSTEP]
exact ⟨e.field⟩
[GOAL]
α : Type u
inst✝ : Infinite α
K : Type u := FractionRing (MvPolynomial α (ULift ℚ))
⊢ #α = #K
[PROOFSTEP]
rw [← IsLocalization.card (MvPolynomial α <| ULift.{u} ℚ)⁰ K le_rfl]
[GOAL]
α : Type u
inst✝ : Infinite α
K : Type u := FractionRing (MvPolynomial α (ULift ℚ))
⊢ #α = #(MvPolynomial α (ULift ℚ))
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u
inst✝ : Infinite α
K : Type u := FractionRing (MvPolynomial α (ULift ℚ))
⊢ #α ≤ #(MvPolynomial α (ULift ℚ))
[PROOFSTEP]
refine' ⟨⟨fun a => MvPolynomial.monomial (Finsupp.single a 1) (1 : ULift.{u} ℚ), fun x y h => _⟩⟩
[GOAL]
case a
α : Type u
inst✝ : Infinite α
K : Type u := FractionRing (MvPolynomial α (ULift ℚ))
x y : α
h :
  (fun a => ↑(MvPolynomial.monomial (Finsupp.single a 1)) 1) x =
    (fun a => ↑(MvPolynomial.monomial (Finsupp.single a 1)) 1) y
⊢ x = y
[PROOFSTEP]
simpa [MvPolynomial.monomial_eq_monomial_iff, Finsupp.single_eq_single_iff] using h
[GOAL]
case a
α : Type u
inst✝ : Infinite α
K : Type u := FractionRing (MvPolynomial α (ULift ℚ))
⊢ #(MvPolynomial α (ULift ℚ)) ≤ #α
[PROOFSTEP]
simp
[GOAL]
α : Type u
⊢ Nonempty (Field α) ↔ IsPrimePow #α
[PROOFSTEP]
rw [Cardinal.isPrimePow_iff]
[GOAL]
α : Type u
⊢ Nonempty (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ n, #α = ↑n ∧ IsPrimePow n
[PROOFSTEP]
cases' fintypeOrInfinite α with h h
[GOAL]
case inl
α : Type u
h : Fintype α
⊢ Nonempty (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ n, #α = ↑n ∧ IsPrimePow n
[PROOFSTEP]
simpa only [Cardinal.mk_fintype, Nat.cast_inj, exists_eq_left', (Cardinal.nat_lt_aleph0 _).not_le, false_or_iff] using
  Fintype.nonempty_field_iff
[GOAL]
case inr
α : Type u
h : Infinite α
⊢ Nonempty (Field α) ↔ ℵ₀ ≤ #α ∨ ∃ n, #α = ↑n ∧ IsPrimePow n
[PROOFSTEP]
simpa only [← Cardinal.infinite_iff, h, true_or_iff, iff_true_iff] using Infinite.nonempty_field


[GOAL]
α : Sort u
x✝¹ x✝ : αᵒᵖ
unop✝¹ unop✝ : α
⊢ { unop := unop✝¹ }.unop = { unop := unop✝ }.unop → { unop := unop✝¹ } = { unop := unop✝ }
[PROOFSTEP]
simp


[GOAL]
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s₁ s₂ : Multiset α
⊢ sup (s₁ + s₂) = fold (fun x x_1 => x ⊔ x_1) (⊥ ⊔ ⊥) (s₁ + s₂)
[PROOFSTEP]
simp [sup]
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Multiset α
a : α
⊢ sup 0 ≤ a ↔ ∀ (b : α), b ∈ 0 → b ≤ a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Multiset α
a : α
⊢ ∀ ⦃a_1 : α⦄ {s : Multiset α},
    (sup s ≤ a ↔ ∀ (b : α), b ∈ s → b ≤ a) → (sup (a_1 ::ₘ s) ≤ a ↔ ∀ (b : α), b ∈ a_1 ::ₘ s → b ≤ a)
[PROOFSTEP]
simp (config := { contextual := true }) [or_imp, forall_and]
[GOAL]
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ sup (ndunion s₁ s₂) = sup s₁ ⊔ sup s₂
[PROOFSTEP]
rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_add]
[GOAL]
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ ndunion s₁ s₂ ↔ a ∈ s₁ + s₂
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ sup (s₁ ∪ s₂) = sup s₁ ⊔ sup s₂
[PROOFSTEP]
rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_add]
[GOAL]
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ sup (ndinsert a s) = a ⊔ sup s
[PROOFSTEP]
rw [← sup_dedup, dedup_ext.2, sup_dedup, sup_cons]
[GOAL]
α : Type u_1
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
inst✝¹ : DecidableEq α✝
α : Type u_2
inst✝ : DecidableEq α
m : Multiset (Multiset α)
⊢ Nodup (sup m) ↔ ∀ (a : Multiset α), a ∈ m → Nodup a
[PROOFSTEP]
induction' m using Multiset.induction_on with _ _ h
[GOAL]
case empty
α✝ : Type u_1
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
inst✝¹ : DecidableEq α✝
α : Type u_2
inst✝ : DecidableEq α
⊢ Nodup (sup 0) ↔ ∀ (a : Multiset α), a ∈ 0 → Nodup a
[PROOFSTEP]
simp
[GOAL]
case cons
α✝ : Type u_1
inst✝³ : SemilatticeSup α✝
inst✝² : OrderBot α✝
inst✝¹ : DecidableEq α✝
α : Type u_2
inst✝ : DecidableEq α
a✝ : Multiset α
s✝ : Multiset (Multiset α)
h : Nodup (sup s✝) ↔ ∀ (a : Multiset α), a ∈ s✝ → Nodup a
⊢ Nodup (sup (a✝ ::ₘ s✝)) ↔ ∀ (a : Multiset α), a ∈ a✝ ::ₘ s✝ → Nodup a
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
s₁ s₂ : Multiset α
⊢ inf (s₁ + s₂) = fold (fun x x_1 => x ⊓ x_1) (⊤ ⊓ ⊤) (s₁ + s₂)
[PROOFSTEP]
simp [inf]
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
s : Multiset α
a : α
⊢ a ≤ inf 0 ↔ ∀ (b : α), b ∈ 0 → a ≤ b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderTop α
s : Multiset α
a : α
⊢ ∀ ⦃a_1 : α⦄ {s : Multiset α},
    (a ≤ inf s ↔ ∀ (b : α), b ∈ s → a ≤ b) → (a ≤ inf (a_1 ::ₘ s) ↔ ∀ (b : α), b ∈ a_1 ::ₘ s → a ≤ b)
[PROOFSTEP]
simp (config := { contextual := true }) [or_imp, forall_and]
[GOAL]
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ inf (ndunion s₁ s₂) = inf s₁ ⊓ inf s₂
[PROOFSTEP]
rw [← inf_dedup, dedup_ext.2, inf_dedup, inf_add]
[GOAL]
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ ndunion s₁ s₂ ↔ a ∈ s₁ + s₂
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ inf (s₁ ∪ s₂) = inf s₁ ⊓ inf s₂
[PROOFSTEP]
rw [← inf_dedup, dedup_ext.2, inf_dedup, inf_add]
[GOAL]
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ + s₂
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ inf (ndinsert a s) = a ⊓ inf s
[PROOFSTEP]
rw [← inf_dedup, dedup_ext.2, inf_dedup, inf_cons]
[GOAL]
α : Type u_1
inst✝² : SemilatticeInf α
inst✝¹ : OrderTop α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ a ::ₘ s
[PROOFSTEP]
simp


[GOAL]
⊢ #ℂ = 𝔠
[PROOFSTEP]
rw [mk_congr Complex.equivRealProd, mk_prod, lift_id, mk_real, continuum_mul_self]
[GOAL]
⊢ #↑Set.univ = 𝔠
[PROOFSTEP]
rw [mk_univ, mk_complex]
[GOAL]
⊢ ¬Set.Countable Set.univ
[PROOFSTEP]
rw [← le_aleph0_iff_set_countable, not_le, mk_univ_complex]
[GOAL]
⊢ ℵ₀ < 𝔠
[PROOFSTEP]
apply cantor