awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J SemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
s : Cone F
x y : (↑s.1 : Type u)
⊢ Subtype.mk (p :=
      fun
        (x :
          (j : J) →
            ToType (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (F.obj j)) ↦
      x ∈
        (F ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections)
      (fun (j : J) ↦
        HMul.hMul (α := (↑(F.obj j) : Type u)) (β := (↑(F.obj j) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                  (s.π.app j) :
                (a : (↑s.pt : Type u)) → (↑(F.obj j) : Type u))
              x :
            (↑(F.obj j) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                  (s.π.app j) :
                (a : (↑s.pt : Type u)) → (↑(F.obj j) : Type u))
              y :
            (↑(F.obj j) : Type u)))
      ⋯ =
    HMul.hMul (α :=
      (↑(F ⋙
              forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                carrier)).sections :
        Type (max u v)))
      (Subtype.mk (p :=
        fun
          (x :
            (j : J) →
              ToType (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (F.obj j)) ↦
        x ∈
          (F ⋙
              forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                carrier)).sections)
        (fun (j : J) ↦
          (ConcreteCategory.hom (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                (s.π.app j) :
              (a : (↑s.pt : Type u)) → (↑(F.obj j) : Type u))
            x)
        ⋯)
      (Subtype.mk (p :=
        fun
          (x :
            (j : J) →
              ToType (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (F.obj j)) ↦
        x ∈
          (F ⋙
              forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                carrier)).sections)
        (fun (j : J) ↦
          (ConcreteCategory.hom (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                (s.π.app j) :
              (a : (↑s.pt : Type u)) → (↑(F.obj j) : Type u))
            y)
        ⋯)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J SemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
s : Cone F
⊢ Eq.{u + 1} (α :=
    Shrink.{u, max u v}
      (↑(F ⋙
              forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                carrier)).sections :
        Type (max u v)))
    ((equivShrink
            (↑(F ⋙
                    forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      carrier)).sections :
              Type (max u v)) :
          (a : (↑(F ⋙ forget SemiRingCat).sections : Type (max u v))) →
            Shrink.{u, max u v} (↑(F ⋙ forget SemiRingCat).sections : Type (max u v)))
        (Subtype.mk (p :=
          fun
            (x :
              (j : J) →
                ToType (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                  (F.obj j)) ↦
          x ∈
            (F ⋙
                forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier)).sections)
          (fun (j : J) ↦ 0) ⋯) :
      Shrink.{u, max u v}
        (↑(F ⋙
                forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier)).sections :
          Type (max u v)))
    (0 :
      (Types.Small.limitCone
          (F ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier))).pt)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J SemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
s : Cone F
x y : (↑s.1 : Type u)
⊢ Subtype.mk (p :=
      fun
        (x :
          (j : J) →
            ToType (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (F.obj j)) ↦
      x ∈
        (F ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections)
      (fun (j : J) ↦
        HAdd.hAdd (α := (↑(F.obj j) : Type u)) (β := (↑(F.obj j) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                  (s.π.app j) :
                (a : (↑s.pt : Type u)) → (↑(F.obj j) : Type u))
              x :
            (↑(F.obj j) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                  (s.π.app j) :
                (a : (↑s.pt : Type u)) → (↑(F.obj j) : Type u))
              y :
            (↑(F.obj j) : Type u)))
      ⋯ =
    HAdd.hAdd (α :=
      (↑(F ⋙
              forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                carrier)).sections :
        Type (max u v)))
      (Subtype.mk (p :=
        fun
          (x :
            (j : J) →
              ToType (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (F.obj j)) ↦
        x ∈
          (F ⋙
              forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                carrier)).sections)
        (fun (j : J) ↦
          (ConcreteCategory.hom (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                (s.π.app j) :
              (a : (↑s.pt : Type u)) → (↑(F.obj j) : Type u))
            x)
        ⋯)
      (Subtype.mk (p :=
        fun
          (x :
            (j : J) →
              ToType (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) (F.obj j)) ↦
        x ∈
          (F ⋙
              forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                carrier)).sections)
        (fun (j : J) ↦
          (ConcreteCategory.hom (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                (s.π.app j) :
              (a : (↑s.pt : Type u)) → (↑(F.obj j) : Type u))
            y)
        ⋯)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J SemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
⊢ HasLimit F

Tactic:
⟨limitCone.{v, u} F, limitConeIsLimit.{v, u} F⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', SemiRingCat.HasLimits.limitCone, CategoryTheory.Limits.LimitCone.mk, SemiRingCat.HasLimits.limitConeIsLimit
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J SemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
⊢ HasLimits SemiRingCat

Tactic:
SemiRingCat.hasLimitsOfSize.{u, u}

Premises used: SemiRingCat.hasLimitsOfSize
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J SemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
h : Small.{u, max u v}
  (↑((F ⋙
            forget₂ SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
              AddCommMonCat.carrier)) ⋙
          forget AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
            AddCommMonCat.carrier)).sections :
    Type (max u v)) :=
  ⋯
⊢ IsLimit (F :=
    F ⋙
      forget₂ SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
        AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommMonCat.carrier))
    (Functor.mapCone
      (forget₂ SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
        AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
        AddCommMonCat.carrier))
      (limitCone F))

Tactic:
apply AddCommMonCat.limitConeIsLimit.{v, u}
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J SemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
⊢ PreservesLimits
    (forget₂ SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
      AddCommMonCat (FD := fun (x1 x2 : AddCommMonCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CD :=
      AddCommMonCat.carrier))

Tactic:
SemiRingCat.forget₂AddCommMon_preservesLimitsOfSize.{u, u}

Premises used: SemiRingCat.forget₂AddCommMon_preservesLimitsOfSize
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J SemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
h : Small.{u, max u v}
  (↑((F ⋙
            forget₂ SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              MonCat (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier)) ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
            MonCat.carrier)).sections :
    Type (max u v)) :=
  ⋯
⊢ IsLimit (F :=
    F ⋙
      forget₂ SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) MonCat
        (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier))
    (Functor.mapCone
      (forget₂ SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) MonCat
        (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier))
      (limitCone F))

Tactic:
apply MonCat.HasLimits.limitConeIsLimit (F ⋙ forget₂ SemiRingCat MonCat.{u})
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J SemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
⊢ PreservesLimits
    (forget₂ SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) MonCat
      (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier))

Tactic:
SemiRingCat.forget₂Mon_preservesLimitsOfSize.{u, u}

Premises used: SemiRingCat.forget₂Mon_preservesLimitsOfSize
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J SemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
⊢ PreservesLimits
    (forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier))

Tactic:
SemiRingCat.forget_preservesLimitsOfSize.{u, u}

Premises used: SemiRingCat.forget_preservesLimitsOfSize
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J CommSemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
h : Functor.ReflectsIsomorphisms
  (forget₂ CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
    SemiRingCat (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := SemiRingCat.carrier)) :=
  ⋯
h_1 : Small.{u, max u v}
  (↑((F ⋙
            forget₂ CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier) SemiRingCat (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
              SemiRingCat.carrier)) ⋙
          forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            SemiRingCat.carrier)).sections :
    Type (max u v)) :=
  ⋯
c : Cone F :=
  {
    pt :=
      of
        (Types.Small.limitCone
            (F ⋙
              forget CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                carrier))).pt,
    π :=
      {
        app := fun (j : J) ↦
          ofHom
            (SemiRingCat.limitπRingHom
              (F ⋙
                forget₂ CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier) SemiRingCat (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
                  SemiRingCat.carrier))
              j),
        naturality := ⋯ } }
c' :
  Cone
    (F ⋙
      forget₂ CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
        SemiRingCat (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := SemiRingCat.carrier))
t : IsLimit c'
⊢ IsLimit c

Tactic:
refine IsLimit.ofFaithful (forget₂ CommSemiRingCat.{u} SemiRingCat.{u})
          (SemiRingCat.HasLimits.limitConeIsLimit.{v, u} _) (fun s => _) fun s => rfl
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J CommSemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
⊢ HasLimit F

Tactic:
⟨limitCone.{v, u} F, limitConeIsLimit.{v, u} F⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.HasLimit.mk', CommSemiRingCat.limitConeIsLimit, CategoryTheory.Limits.LimitCone.mk, CommSemiRingCat.limitCone
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J CommSemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
⊢ HasLimits CommSemiRingCat

Tactic:
CommSemiRingCat.hasLimitsOfSize.{u, u}

Premises used: CommSemiRingCat.hasLimitsOfSize
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J CommSemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
⊢ PreservesLimits
    (forget₂ CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
      SemiRingCat (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := SemiRingCat.carrier))

Tactic:
CommSemiRingCat.forget₂SemiRing_preservesLimitsOfSize.{u, u}

Premises used: CommSemiRingCat.forget₂SemiRing_preservesLimitsOfSize
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J CommSemiRingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
⊢ PreservesLimits
    (forget CommSemiRingCat (FC := fun (R S : CommSemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier))

Tactic:
CommSemiRingCat.forget_preservesLimitsOfSize.{u, u}

Premises used: CommSemiRingCat.forget_preservesLimitsOfSize
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J RingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)).sections :
      Type (max u v))
this_1 :
  Functor.ReflectsIsomorphisms
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) SemiRingCat
      (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := SemiRingCat.carrier))
this :
  Small.{u, max u v}
    (↑((F ⋙
              forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                SemiRingCat (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
                SemiRingCat.carrier)) ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              SemiRingCat.carrier)).sections :
      Type (max u v))
c : Cone F :=
  {
    pt :=
      of
        (Types.Small.limitCone
            (F ⋙ forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier))).pt,
    π :=
      {
        app := fun (x : J) ↦
          ofHom
            (SemiRingCat.limitπRingHom
              (F ⋙
                forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                  SemiRingCat (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
                  SemiRingCat.carrier))
              x),
        naturality := ⋯ } }
c' :
  Cone
    (F ⋙
      forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) SemiRingCat
        (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := SemiRingCat.carrier))
t : IsLimit c'
⊢ Functor.mapCone
      (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) SemiRingCat
        (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := SemiRingCat.carrier))
      c ≅
    c'

Tactic:
apply IsLimit.uniqueUpToIso (SemiRingCat.HasLimits.limitConeIsLimit _) t

Premises used: CategoryTheory.Limits.IsLimit.uniqueUpToIso, SemiRingCat.HasLimits.limitConeIsLimit
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J RingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)).sections :
      Type (max u v))
this_1 :
  Functor.ReflectsIsomorphisms
    (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) SemiRingCat
      (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := SemiRingCat.carrier))
this :
  Small.{u, max u v}
    (↑((F ⋙
              forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                SemiRingCat (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
                SemiRingCat.carrier)) ⋙
            forget SemiRingCat (FC := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              SemiRingCat.carrier)).sections :
      Type (max u v))
c : Cone F :=
  {
    pt :=
      of
        (Types.Small.limitCone
            (F ⋙ forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier))).pt,
    π :=
      {
        app := fun (x : J) ↦
          ofHom
            (SemiRingCat.limitπRingHom
              (F ⋙
                forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                  SemiRingCat (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
                  SemiRingCat.carrier))
              x),
        naturality := ⋯ } }
c' :
  Cone
    (F ⋙
      forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) SemiRingCat
        (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := SemiRingCat.carrier))
t : IsLimit c'
⊢ IsLimit (F :=
    F ⋙
      forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) SemiRingCat
        (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := SemiRingCat.carrier))
    (Functor.mapCone
      (forget₂ RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) SemiRingCat
        (FD := fun (R S : SemiRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD := SemiRingCat.carrier))
      c)

Tactic:
apply SemiRingCat.HasLimits.limitConeIsLimit _

Premises used: SemiRingCat.HasLimits.limitConeIsLimit
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J RingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)).sections :
      Type (max u v))
⊢ HasLimit F

Tactic:
let _ : Small.{u} (Functor.sections ((F ⋙ forget₂ _ SemiRingCat) ⋙ forget _)) :=
    inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget _))
  hasLimit_of_created F (forget₂ RingCat.{u} SemiRingCat.{u})

Premises used: CategoryTheory.hasLimit_of_created, RingCat.instCreatesLimitSemiRingCatForget₂RingHomCarrierCarrier._proof_1, RingCat, CategoryTheory.forget₂, SemiRingCat
-- Module: Mathlib.Algebra.Category.Ring.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J RingCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget RingCat (FC := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)).sections :
      Type (max u v))
⊢ HasLimits RingCat

Tactic:
RingCat.hasLimitsOfSize.{u, u}

Premises used: RingCat.hasLimitsOfSize