awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
x : (↑(R.{v, u} F) : Type (max u v))
⊢ x * 0 = 0

Tactic:
Quot.inductionOn x ?_

Premises used: Quot.inductionOn
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
x : (↑(R.{v, u} F) : Type (max u v))
refine :
  ∀
    (a :
      (j : J) ×
        ((F ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                  (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                  (CD := MonCat.carrier)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).obj
          j),
    Quot.mk
          ((F ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                  (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                  (CD := MonCat.carrier)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).ColimitTypeRel
          a *
        0 =
      0
⊢ x * 0 = 0

Tactic:
refine Quot.inductionOn x ?_
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
x :
  (j : J) ×
    ((F ⋙
            forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
              carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
              MonCat.carrier)) ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            MonCat.carrier)).obj
      j
obtain :
  ∀ (j : J)
    (x :
      ((F ⋙
              forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                (CD := MonCat.carrier)) ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              MonCat.carrier)).obj
        j),
    Quot.mk
          ((F ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                  (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                  (CD := MonCat.carrier)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : J) ↦
            ((F ⋙
                    forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                      (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC := carrier) MonCat (FD :=
                      fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier)) ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    MonCat.carrier)).obj
              j)
            j x) *
        0 =
      0
⊢ Quot.mk
        ((F ⋙
              forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                (CD := MonCat.carrier)) ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              MonCat.carrier)).ColimitTypeRel
        x *
      0 =
    0

Tactic:
obtain ⟨j, x⟩ := x
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
x y z : (↑(R.{v, u} F) : Type (max u v))
⊢ x * (y + z) = x * y + x * z

Tactic:
Quot.induction_on₃ x y z ?_

Premises used: Quot.induction_on₃
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
j₁ : J
x :
  ((F ⋙
          forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
            carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
            MonCat.carrier)) ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          MonCat.carrier)).obj
    j₁
j₂ : J
y :
  ((F ⋙
          forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
            carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
            MonCat.carrier)) ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          MonCat.carrier)).obj
    j₂
j₃ : J
z :
  ((F ⋙
          forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
            carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
            MonCat.carrier)) ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          MonCat.carrier)).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₃
simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [CategoryTheory.Functor.map_id]

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
x y z : (↑(R.{v, u} F) : Type (max u v))
⊢ (x + y) * z = x * z + y * z

Tactic:
Quot.induction_on₃ x y z ?_

Premises used: Quot.induction_on₃
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
t : Cocone F
j : J
x : (↑(F.obj j) : Type (max u v))
⊢ Eq (α := (↑t.pt : Type (max u v)))
    ((descAddMonoidHom t : (a : (↑(R F) : Type (max v u))) → (↑t.pt : Type (max u v)))
        (Quot.mk
          ((F ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                  (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                  (CD := MonCat.carrier)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : J) ↦
            ((F ⋙
                    forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                      (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC := carrier) MonCat (FD :=
                      fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier)) ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    MonCat.carrier)).obj
              j)
            j x)) :
      (↑t.pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
            carrier) (t.ι.app j) :
          (a : (↑(F.obj j) : Type (max u v))) → (↑(((Functor.const J).obj t.pt).obj j) : Type (max u v)))
        x :
      (↑(Functor.obj (Functor.obj (Functor.const J) t.pt) j) : Type (max u v)))

Tactic:
ConcreteCategory.congr_hom ((forget AddCommMonCat).congr_map
    ((AddCommMonCat.FilteredColimits.colimitCoconeIsColimit.{v, u}
      (F ⋙ forget₂ SemiRingCat AddCommMonCat)).fac
        ((forget₂ SemiRingCat AddCommMonCat).mapCocone t) j)) x

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Functor.mapCocone, CategoryTheory.Functor.comp, AddCommMonCat, AddCommMonCat.FilteredColimits.colimitCoconeIsColimit, CategoryTheory.forget₂, CategoryTheory.forget, CategoryTheory.Functor.congr_map, SemiRingCat, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Functor.ιColimitType
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
t : Cocone F
j : J
x : (↑(F.obj j) : Type (max u v))
⊢ Eq (α := (↑t.pt : Type (max u v)))
    ((descMonoidHom t : (a : (↑(R F) : Type (max v u))) → (↑t.pt : Type (max u v)))
        (Quot.mk
          ((F ⋙
                forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v)))
                  (CC := carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                  (CD := MonCat.carrier)) ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                MonCat.carrier)).ColimitTypeRel
          (Sigma.mk (β := fun (j : J) ↦
            ((F ⋙
                    forget₂ SemiRingCat (FC := fun (R S : SemiRingCat) ↦
                      (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC := carrier) MonCat (FD :=
                      fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD := MonCat.carrier)) ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    MonCat.carrier)).obj
              j)
            j x)) :
      (↑t.pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC :=
            carrier) (t.ι.app j) :
          (a : (↑(F.obj j) : Type (max u v))) → (↑(((Functor.const J).obj t.pt).obj j) : Type (max u v)))
        x :
      (↑(Functor.obj (Functor.obj (Functor.const J) t.pt) j) : Type (max u v)))

Tactic:
ConcreteCategory.congr_hom ((forget MonCat).congr_map
    ((MonCat.FilteredColimits.colimitCoconeIsColimit.{v, u}
      (F ⋙ forget₂ _ _)).fac ((forget₂ _ _).mapCocone t) j)) x

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Functor.mapCocone, CategoryTheory.Functor.comp, MonCat, CategoryTheory.Functor.descColimitType, CategoryTheory.forget₂, CategoryTheory.forget, CategoryTheory.Functor.congr_map, MonCat.FilteredColimits.colimitCoconeIsColimit, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
t : Cocone F
⊢ Eq (α := (↑t.pt : Type (max u v))) ((descMonoidHom t : (a : (↑(R F) : Type (max v u))) → (↑t.pt : Type (max u v))) 1)
    1

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
t : Cocone F
x y : (↑(R.{v, u} F) : Type (max u v))
change :
  (descAddMonoidHom t : (a : (↑(R F) : Type (max v u))) → (↑t.pt : Type (max u v))) (x * y) =
    HMul.hMul (α := (↑t.pt : Type (max u v))) (β := (↑t.pt : Type (max u v)))
      ((descAddMonoidHom t : (a : (↑(R F) : Type (max v u))) → (↑t.pt : Type (max u v))) x : (↑t.pt : Type (max u v)))
      ((descAddMonoidHom t : (a : (↑(R F) : Type (max v u))) → (↑t.pt : Type (max u v))) y : (↑t.pt : Type (max u v)))
⊢ ZeroHom.toFun (↑(descAddMonoidHom t) : ZeroHom (↑(R F) : Type (max v u)) (↑t.pt : Type (max u v))) (x * y) =
    ZeroHom.toFun (↑(descAddMonoidHom t) : ZeroHom (↑(R F) : Type (max v u)) (↑t.pt : Type (max u v))) x *
      ZeroHom.toFun (↑(descAddMonoidHom t) : ZeroHom (↑(R F) : Type (max v u)) (↑t.pt : Type (max u v))) y

Tactic:
change descAddMonoidHom t (x * y) =
          descAddMonoidHom t x * descAddMonoidHom t y

Premises used: HMul.hMul, SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descAddMonoidHom, DFunLike.coe
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
t : Cocone F
x y : (↑(R.{v, u} F) : Type (max u v))
⊢ (descAddMonoidHom t : (a : (↑(R F) : Type (max v u))) → (↑t.pt : Type (max u v))) (x * y) =
    HMul.hMul (α := (↑t.pt : Type (max u v))) (β := (↑t.pt : Type (max u v)))
      ((descAddMonoidHom t : (a : (↑(R F) : Type (max v u))) → (↑t.pt : Type (max u v))) x : (↑t.pt : Type (max u v)))
      ((descAddMonoidHom t : (a : (↑(R F) : Type (max v u))) → (↑t.pt : Type (max u v))) y : (↑t.pt : Type (max u v)))

Tactic:
simp [← descMonoidHom_apply_eq]

Premises used: SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descMonoidHom_apply_eq
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
t : Cocone F
j : J
hf :
  ∀ (x : (↑(F.obj j) : Type (max u v))),
    Eq (α := (↑t.pt : Type (max u v)))
      ((Hom.hom
              ((colimitCocone.{v, u} F).ι.app j ≫
                ofHom
                  (let __src : (↑(R.{v, u} F) : Type (max v u)) →+ (↑t.pt : Type (max u v)) := descAddMonoidHom t;
                  { toFun := (↑__src : ZeroHom (↑(R F) : Type (max v u)) (↑t.pt : Type (max u v))).toFun, map_one' := ⋯,
                    map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })) :
            (a : (↑(F.obj j) : Type (max u v))) → (↑t.pt : Type (max u v)))
          x :
        (↑t.pt : Type (max u v)))
      ((Hom.hom (t.ι.app j) : (a : (↑(F.obj j) : Type (max u v))) → (↑t.pt : Type (max u v))) x :
        (↑t.pt : Type (max u v)))
⊢ (colimitCocone.{v, u} F).ι.app j ≫
      ofHom
        (let __src : (↑(R.{v, u} F) : Type (max v u)) →+ (↑t.pt : Type (max u v)) := descAddMonoidHom t;
        { toFun := (↑__src : ZeroHom (↑(R F) : Type (max v u)) (↑t.pt : Type (max u v))).toFun, map_one' := ⋯,
          map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }) =
    t.ι.app j

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
t : Cocone F
j : J
x : (↑(F.obj j) : Type (max u v))
⊢ Eq (α := (↑t.pt : Type (max u v)))
    ((Hom.hom
            ((colimitCocone.{v, u} F).ι.app j ≫
              ofHom
                (let __src : (↑(R.{v, u} F) : Type (max v u)) →+ (↑t.pt : Type (max u v)) := descAddMonoidHom t;
                { toFun := (↑__src : ZeroHom (↑(R F) : Type (max v u)) (↑t.pt : Type (max u v))).toFun, map_one' := ⋯,
                  map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })) :
          (a : (↑(F.obj j) : Type (max u v))) → (↑t.pt : Type (max u v)))
        x :
      (↑t.pt : Type (max u v)))
    ((Hom.hom (t.ι.app j) : (a : (↑(F.obj j) : Type (max u v))) → (↑t.pt : Type (max u v))) x :
      (↑t.pt : Type (max u v)))

Tactic:
descAddMonoidHom_quotMk t x

Premises used: SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descAddMonoidHom_quotMk, CategoryTheory.Functor.ιColimitType
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
t : Cocone F
j : J
x : (↑(F.obj j) : Type (max u v))
⊢ Eq (α := (↑t.pt : Type (max u v)))
    ((Hom.hom
            ((colimitCocone.{v, u} F).ι.app j ≫
              ofHom
                (let __src : (↑(R.{v, u} F) : Type (max v u)) →+ (↑t.pt : Type (max u v)) := descAddMonoidHom t;
                { toFun := (↑__src : ZeroHom (↑(R F) : Type (max v u)) (↑t.pt : Type (max u v))).toFun, map_one' := ⋯,
                  map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })) :
          (a : (↑(F.obj j) : Type (max u v))) → (↑t.pt : Type (max u v)))
        x :
      (↑t.pt : Type (max u v)))
    ((Hom.hom (t.ι.app j) : (a : (↑(F.obj j) : Type (max u v))) → (↑t.pt : Type (max u v))) x :
      (↑t.pt : Type (max u v)))

Tactic:
exact descAddMonoidHom_quotMk t x

Premises used: SemiRingCat.FilteredColimits.colimitCoconeIsColimit.descAddMonoidHom_quotMk
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ SemiRingCat
inst_1 : IsFiltered J
⊢ PreservesFilteredColimits
    (forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier))

Tactic:
Limits.comp_preservesFilteredColimits (forget₂ SemiRingCat MonCat) (forget MonCat.{u})

Premises used: CategoryTheory.Functor.comp, MonCat, CategoryTheory.forget₂, CategoryTheory.Limits.comp_preservesFilteredColimits, CategoryTheory.forget, SemiRingCat
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ CommSemiRingCat
x x_1 : J
f : x ⟶ x_1
x_2 : (↑(F.obj x) : Type (max u v))
⊢ Eq (α := (↑(Functor.obj (Functor.obj (Functor.const J) (colimit.{v, u} F)) x_1) : Type (max u v)))
    ((Hom.hom
            (F.map f ≫
              ofHom
                (SemiRingCat.Hom.hom
                  ((SemiRingCat.FilteredColimits.colimitCocone.{v, u}
                          (F ⋙
                            forget₂ CommSemiRingCat (FC := fun (R S : CommSemiRingCat) ↦
                              (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC := carrier) SemiRingCat (FD :=
                              fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CD :=
                              SemiRingCat.carrier))).ι.app
                    x_1))) :
          (a : (↑(F.obj x) : Type (max u v))) → (↑(((Functor.const J).obj (colimit F)).obj x_1) : Type (max u v)))
        x_2 :
      (↑(Functor.obj (Functor.obj (Functor.const J) (colimit.{v, u} F)) x_1) : Type (max u v)))
    ((Hom.hom
            (ofHom
                (SemiRingCat.Hom.hom
                  ((SemiRingCat.FilteredColimits.colimitCocone.{v, u}
                          (F ⋙
                            forget₂ CommSemiRingCat (FC := fun (R S : CommSemiRingCat) ↦
                              (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC := carrier) SemiRingCat (FD :=
                              fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CD :=
                              SemiRingCat.carrier))).ι.app
                    x)) ≫
              CategoryTheory.Functor.map (Functor.obj (Functor.const J) (colimit.{v, u} F)) f) :
          (a : (↑(F.obj x) : Type (max u v))) → (↑(((Functor.const J).obj (colimit F)).obj x_1) : Type (max u v)))
        x_2 :
      (↑(Functor.obj (Functor.obj (Functor.const J) (colimit.{v, u} F)) x_1) : Type (max u v)))

Tactic:
simpa using (Types.TypeMax.colimitCocone
          (F ⋙ forget CommSemiRingCat)).ι.naturality_apply f _

Premises used: CategoryTheory.NatTrans.naturality_apply, CategoryTheory.Limits.Types.TypeMax.colimitCocone, CategoryTheory.Functor.comp, CategoryTheory.Limits.Cocone.ι, CommSemiRingCat, CategoryTheory.forget
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ CommSemiRingCat
⊢ PreservesFilteredColimits
    (forget CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier))

Tactic:
Limits.comp_preservesFilteredColimits (forget₂ CommSemiRingCat SemiRingCat)
    (forget SemiRingCat.{u})

Premises used: CategoryTheory.Functor.comp, CategoryTheory.forget₂, CategoryTheory.Limits.comp_preservesFilteredColimits, CommSemiRingCat, CategoryTheory.forget, SemiRingCat
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ RingCat
x x_1 : J
f : x ⟶ x_1
x_2 : (↑(F.obj x) : Type (max u v))
⊢ Eq (α := (↑(Functor.obj (Functor.obj (Functor.const J) (colimit.{v, u} F)) x_1) : Type (max u v)))
    ((Hom.hom
            (F.map f ≫
              ofHom
                (SemiRingCat.Hom.hom
                  ((SemiRingCat.FilteredColimits.colimitCocone.{v, u}
                          (F ⋙
                            forget₂ RingCat (FC := fun (R S : RingCat) ↦
                              (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC := carrier) SemiRingCat (FD :=
                              fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CD :=
                              SemiRingCat.carrier))).ι.app
                    x_1))) :
          (a : (↑(F.obj x) : Type (max u v))) → (↑(((Functor.const J).obj (colimit F)).obj x_1) : Type (max u v)))
        x_2 :
      (↑(Functor.obj (Functor.obj (Functor.const J) (colimit.{v, u} F)) x_1) : Type (max u v)))
    ((Hom.hom
            (ofHom
                (SemiRingCat.Hom.hom
                  ((SemiRingCat.FilteredColimits.colimitCocone.{v, u}
                          (F ⋙
                            forget₂ RingCat (FC := fun (R S : RingCat) ↦
                              (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CC := carrier) SemiRingCat (FD :=
                              fun (R S : SemiRingCat) ↦ (↑R : Type (max u v)) →+* (↑S : Type (max u v))) (CD :=
                              SemiRingCat.carrier))).ι.app
                    x)) ≫
              CategoryTheory.Functor.map (Functor.obj (Functor.const J) (colimit.{v, u} F)) f) :
          (a : (↑(F.obj x) : Type (max u v))) → (↑(((Functor.const J).obj (colimit F)).obj x_1) : Type (max u v)))
        x_2 :
      (↑(Functor.obj (Functor.obj (Functor.const J) (colimit.{v, u} F)) x_1) : Type (max u v)))

Tactic:
simpa using (Types.TypeMax.colimitCocone (F ⋙ forget RingCat)).ι.naturality_apply f _

Premises used: CategoryTheory.NatTrans.naturality_apply, CategoryTheory.Limits.Types.TypeMax.colimitCocone, CategoryTheory.Functor.comp, RingCat, CategoryTheory.Limits.Cocone.ι, CategoryTheory.forget
-- Module: Mathlib.Algebra.Category.Ring.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ RingCat
⊢ PreservesFilteredColimits
    (forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier))

Tactic:
Limits.comp_preservesFilteredColimits (forget₂ RingCat SemiRingCat) (forget SemiRingCat.{u})

Premises used: CategoryTheory.Functor.comp, RingCat, CategoryTheory.forget₂, CategoryTheory.Limits.comp_preservesFilteredColimits, CategoryTheory.forget, SemiRingCat