awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.AlgCat.Limits
Goal:
R : Type u
inst : CommRing R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ AlgCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).sections :
      Type (max v w))
s : Cone F
refine_1 :
  Eq (α :=
    (j : J) →
      (F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).obj
        j)
    (fun (j : J) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (Cone.π
                (Functor.mapCone
                  (forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                    (CC := carrier))
                  s))
              j) :
          (a : (fun (X : Type w) ↦ X) (((Functor.const J).obj ((forget (AlgCat R)).mapCone s).pt).obj j)) →
            (fun (X : Type w) ↦ X) ((F ⋙ forget (AlgCat R)).obj j))
        1)
    1
⊢ EquivLike.coe (E :=
      (↑(F ⋙
                forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                  (CC := carrier)).sections :
          Type (max w v)) ≃
        Shrink.{w, max w v}
          (↑(F ⋙
                  forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                    (CC := carrier)).sections :
            Type (max w v)))
      (equivShrink
        (↑(F ⋙
                forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                  (CC := carrier)).sections :
          Type (max w v)))
      (Subtype.mk (p :=
        fun
          (x :
            (j : J) →
              (F ⋙
                    forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                      (CC := carrier)).obj
                j) ↦
        x ∈
          (F ⋙
              forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                (CC := carrier)).sections)
        (fun (j : J) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app
                  (Cone.π
                    (Functor.mapCone
                      (forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                        (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier))
                      s))
                  j) :
              (a : (fun (X : Type w) ↦ X) (((Functor.const J).obj ((forget (AlgCat R)).mapCone s).pt).obj j)) →
                (fun (X : Type w) ↦ X) ((F ⋙ forget (AlgCat R)).obj j))
            1)
        ⋯) =
    1

Tactic:
congr
-- Module: Mathlib.Algebra.Category.AlgCat.Limits
Goal:
R : Type u
inst : CommRing R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ AlgCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).sections :
      Type (max v w))
s : Cone F
refine_1 :
  ∀ (j : J),
    Eq (α :=
      (fun (X : Type w) ↦ X)
        ((F ⋙
              forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                (CC := carrier)).obj
          j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app
                (Cone.π
                  (Functor.mapCone
                    (forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                      (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier))
                    s))
                j) :
            (a : (fun (X : Type w) ↦ X) (((Functor.const J).obj ((forget (AlgCat R)).mapCone s).pt).obj j)) →
              (fun (X : Type w) ↦ X) ((F ⋙ forget (AlgCat R)).obj j))
          1 :
        (fun (X : Type w) ↦ X)
          ((F ⋙
                forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                  (CC := carrier)).obj
            j))
      (1 j : (↑(F.obj j) : Type w))
⊢ Eq (α :=
    (j : J) →
      (F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).obj
        j)
    (fun (j : J) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (Cone.π
                (Functor.mapCone
                  (forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                    (CC := carrier))
                  s))
              j) :
          (a : (fun (X : Type w) ↦ X) (((Functor.const J).obj ((forget (AlgCat R)).mapCone s).pt).obj j)) →
            (fun (X : Type w) ↦ X) ((F ⋙ forget (AlgCat R)).obj j))
        1)
    1

Tactic:
ext j
-- Module: Mathlib.Algebra.Category.AlgCat.Limits
Goal:
R : Type u
inst : CommRing R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ AlgCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).sections :
      Type (max v w))
s : Cone F
j : J
⊢ Eq (α :=
    (fun (X : Type w) ↦ X)
      ((F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).obj
        j))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (Cone.π
                (Functor.mapCone
                  (forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                    (CC := carrier))
                  s))
              j) :
          (a : (fun (X : Type w) ↦ X) (((Functor.const J).obj ((forget (AlgCat R)).mapCone s).pt).obj j)) →
            (fun (X : Type w) ↦ X) ((F ⋙ forget (AlgCat R)).obj j))
        1 :
      (fun (X : Type w) ↦ X)
        ((F ⋙
              forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                (CC := carrier)).obj
          j))
    (1 j : (↑(F.obj j) : Type w))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.AlgCat.Limits
Goal:
R : Type u
inst : CommRing R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ AlgCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).sections :
      Type (max v w))
s : Cone F
x y : (↑s.1 : Type w)
j : J
⊢ HMul.hMul (α := (↑(F.obj j) : Type w)) (β := (↑(F.obj j) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)
              (s.π.app j) :
            (a : (↑s.pt : Type w)) → (↑(F.obj j) : Type w))
          x :
        (↑(F.obj j) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)
              (s.π.app j) :
            (a : (↑s.pt : Type w)) → (↑(F.obj j) : Type w))
          y :
        (↑(F.obj j) : Type w)) =
    (↑(HMul.hMul (α :=
            (↑(F ⋙
                    forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                      (CC := carrier)).sections :
              Type (max w v)))
            (Subtype.mk (p :=
              fun
                (x :
                  (j : J) →
                    ToType (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)
                      (F.obj j)) ↦
              x ∈
                (F ⋙
                    forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                      (CC := carrier)).sections)
              (fun (j : J) ↦
                (ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
                      carrier) (s.π.app j) :
                    (a : (↑s.pt : Type w)) → (↑(F.obj j) : Type w))
                  x)
              ⋯)
            (Subtype.mk (p :=
              fun
                (x :
                  (j : J) →
                    ToType (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)
                      (F.obj j)) ↦
              x ∈
                (F ⋙
                    forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                      (CC := carrier)).sections)
              (fun (j : J) ↦
                (ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
                      carrier) (s.π.app j) :
                    (a : (↑s.pt : Type w)) → (↑(F.obj j) : Type w))
                  y)
              ⋯)) :
        (j : J) → ToType (F.obj j))
      j

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Limits
Goal:
R : Type u
inst : CommRing R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ AlgCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).sections :
      Type (max v w))
s : Cone F
j : J
⊢ Eq.{w + 1} (α :=
    ToType (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier) (F.obj j)) 0
    ((↑0 : (j : J) → ToType (F.obj j)) j)

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Limits
Goal:
R : Type u
inst : CommRing R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ AlgCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).sections :
      Type (max v w))
s : Cone F
x y : (↑s.1 : Type w)
j : J
⊢ HAdd.hAdd (α := (↑(F.obj j) : Type w)) (β := (↑(F.obj j) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)
              (s.π.app j) :
            (a : (↑s.pt : Type w)) → (↑(F.obj j) : Type w))
          x :
        (↑(F.obj j) : Type w))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)
              (s.π.app j) :
            (a : (↑s.pt : Type w)) → (↑(F.obj j) : Type w))
          y :
        (↑(F.obj j) : Type w)) =
    (↑(HAdd.hAdd (α :=
            (↑(F ⋙
                    forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                      (CC := carrier)).sections :
              Type (max w v)))
            (Subtype.mk (p :=
              fun
                (x :
                  (j : J) →
                    ToType (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)
                      (F.obj j)) ↦
              x ∈
                (F ⋙
                    forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                      (CC := carrier)).sections)
              (fun (j : J) ↦
                (ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
                      carrier) (s.π.app j) :
                    (a : (↑s.pt : Type w)) → (↑(F.obj j) : Type w))
                  x)
              ⋯)
            (Subtype.mk (p :=
              fun
                (x :
                  (j : J) →
                    ToType (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)
                      (F.obj j)) ↦
              x ∈
                (F ⋙
                    forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                      (CC := carrier)).sections)
              (fun (j : J) ↦
                (ConcreteCategory.hom (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
                      carrier) (s.π.app j) :
                    (a : (↑s.pt : Type w)) → (↑(F.obj j) : Type w))
                  y)
              ⋯)) :
        (j : J) → ToType (F.obj j))
      j

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Limits
Goal:
R : Type u
inst : CommRing R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ AlgCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).sections :
      Type (max v w))
s : Cone F
r : R
j : J
⊢ Eq.{w + 1} (α :=
    (F ⋙
          forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
            carrier)).obj
      j)
    ((↑(Subtype.mk (p :=
            fun
              (x :
                (j : J) →
                  (F ⋙
                        forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                          (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)).obj
                    j) ↦
            x ∈
              (F ⋙
                  forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                    (CC := carrier)).sections)
            (fun (j : J) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun)
                    (NatTrans.app
                      (Cone.π
                        (Functor.mapCone
                          (forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                            (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier))
                          s))
                      j) :
                  (a : ((Functor.const J).obj ((forget (AlgCat R)).mapCone s).pt).obj j) →
                    (F ⋙ forget (AlgCat R)).obj j)
                ((algebraMap R (↑s.1 : Type w) : (a : R) → (↑s.1 : Type w)) r : (↑s.1 : Type w)))
            ⋯) :
        (j : J) → (F ⋙ forget (AlgCat R)).obj j)
      j)
    ((↑((algebraMap R ↥(sectionsSubalgebra F) : (a : R) → ↥(sectionsSubalgebra F)) r) :
        (j : J) → (F ⋙ forget (AlgCat R)).obj j)
      j)

Tactic:
(s.π.app j).hom.commutes r

Premises used: CategoryTheory.Limits.Cone.π, AlgHom.commutes, CategoryTheory.NatTrans.app, AlgCat.Hom.hom
-- Module: Mathlib.Algebra.Category.AlgCat.Limits
Goal:
R : Type u
inst : CommRing R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ AlgCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).sections :
      Type (max v w))
s : Cone F
r : R
j : J
⊢ Eq.{w + 1} (α :=
    (F ⋙
          forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
            carrier)).obj
      j)
    ((↑(Subtype.mk (p :=
            fun
              (x :
                (j : J) →
                  (F ⋙
                        forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                          (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier)).obj
                    j) ↦
            x ∈
              (F ⋙
                  forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w))
                    (CC := carrier)).sections)
            (fun (j : J) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun)
                    (NatTrans.app
                      (Cone.π
                        (Functor.mapCone
                          (forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦
                            (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC := carrier))
                          s))
                      j) :
                  (a : ((Functor.const J).obj ((forget (AlgCat R)).mapCone s).pt).obj j) →
                    (F ⋙ forget (AlgCat R)).obj j)
                ((algebraMap R (↑s.1 : Type w) : (a : R) → (↑s.1 : Type w)) r : (↑s.1 : Type w)))
            ⋯) :
        (j : J) → (F ⋙ forget (AlgCat R)).obj j)
      j)
    ((↑((algebraMap R ↥(sectionsSubalgebra F) : (a : R) → ↥(sectionsSubalgebra F)) r) :
        (j : J) → (F ⋙ forget (AlgCat R)).obj j)
      j)

Tactic:
exact (s.π.app j).hom.commutes r

Premises used: CategoryTheory.Limits.Cone.π, AlgHom.commutes, CategoryTheory.NatTrans.app, AlgCat.Hom.hom
-- Module: Mathlib.Algebra.Category.AlgCat.Limits
Goal:
R : Type u
inst : CommRing R
inst_1 : UnivLE.{v, w}
⊢ HasLimitsOfSize.{t, v, w, max (w + 1) u} (AlgCat.{w, u} R)

Tactic:
{ has_limits_of_shape := fun _ _ =>
    { has_limit := fun F => HasLimit.mk
        { cone := limitCone F
          isLimit := limitConeIsLimit F } } }

Premises used: AlgCat.HasLimits.limitCone, CategoryTheory.Limits.HasLimitsOfShape.mk, CategoryTheory.Limits.HasLimitsOfSize.mk, CategoryTheory.Limits.HasLimit.mk, AlgCat.HasLimits.limitConeIsLimit, CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.Algebra.Category.AlgCat.Limits
Goal:
R : Type u
inst : CommRing R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ AlgCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).sections :
      Type (max v w))
⊢ HasLimits (AlgCat.{w, u} R)

Tactic:
AlgCat.hasLimitsOfSize.{w, w, u}

Premises used: AlgCat.hasLimitsOfSize
-- Module: Mathlib.Algebra.Category.AlgCat.Limits
Goal:
R : Type u
inst : CommRing R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ AlgCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).sections :
      Type (max v w))
⊢ PreservesLimits
    (forget₂ (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
      carrier) RingCat (FD := fun (R S : RingCat.{w}) ↦ (↑R : Type w) →+* (↑S : Type w)) (CD := RingCat.carrier))

Tactic:
AlgCat.forget₂Ring_preservesLimitsOfSize.{w, w}

Premises used: AlgCat.forget₂Ring_preservesLimitsOfSize
-- Module: Mathlib.Algebra.Category.AlgCat.Limits
Goal:
R : Type u
inst : CommRing R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ AlgCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).sections :
      Type (max v w))
⊢ PreservesLimits
    (forget₂ (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
      carrier) (ModuleCat.{w, u} R) (FD := fun (x1 x2 : ModuleCat.{w, u} R) ↦ (↑x1 : Type w) →ₗ[R] (↑x2 : Type w))
      (CD := ModuleCat.carrier))

Tactic:
AlgCat.forget₂Module_preservesLimitsOfSize.{w, w}

Premises used: AlgCat.forget₂Module_preservesLimitsOfSize
-- Module: Mathlib.Algebra.Category.AlgCat.Limits
Goal:
R : Type u
inst : CommRing R
J : Type v
inst_1 : Category.{t, v} J
F : J ⥤ AlgCat.{w, u} R
inst_2 :
  Small.{w, max v w}
    (↑(F ⋙
            forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
              carrier)).sections :
      Type (max v w))
⊢ PreservesLimits
    (forget (AlgCat.{w, u} R) (FC := fun (x1 x2 : AlgCat.{w, u} R) ↦ (↑x1 : Type w) →ₐ[R] (↑x2 : Type w)) (CC :=
      carrier))

Tactic:
AlgCat.forget_preservesLimitsOfSize.{w, w}

Premises used: AlgCat.forget_preservesLimitsOfSize
-- Module: Mathlib.Algebra.Category.AlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
K L M N : AlgCat R
f : K ⟶ L
g : M ⟶ N
⊢ Hom.hom (f ⊗ₘ g) = Algebra.TensorProduct.map (Hom.hom f) (Hom.hom g)

Tactic:
rfl

Premises used: Algebra.TensorProduct.algHomOfLinearMapTensorProduct, Algebra.TensorProduct.map, AlgHom.ofLinearMap, rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
L M N : AlgCat R
f : M ⟶ N
⊢ Hom.hom (L ◁ f) = Algebra.TensorProduct.map (AlgHom.id R (↑L : Type u)) (Hom.hom f)

Tactic:
rfl

Premises used: Algebra.TensorProduct.algHomOfLinearMapTensorProduct, Algebra.TensorProduct.map, AlgHom.ofLinearMap, rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
L M : AlgCat R
f : L ⟶ M
N : AlgCat R
⊢ Hom.hom (f ▷ N) = Algebra.TensorProduct.map (Hom.hom f) (AlgHom.id R (↑N : Type u))

Tactic:
rfl

Premises used: Algebra.TensorProduct.algHomOfLinearMapTensorProduct, Algebra.TensorProduct.map, AlgHom.ofLinearMap, rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
M : AlgCat R
⊢ Hom.hom (Iso.hom (λ_ M)) =
    (↑(Algebra.TensorProduct.lid R (↑M : Type u)) : TensorProduct R R (↑M : Type u) →ₐ[R] (↑M : Type u))

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
M : AlgCat R
⊢ Hom.hom (Iso.inv (λ_ M)) =
    (↑(AlgEquiv.symm (Algebra.TensorProduct.lid R (↑M : Type u))) : (↑M : Type u) →ₐ[R] TensorProduct R R (↑M : Type u))

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
M : AlgCat R
⊢ Hom.hom (Iso.hom (ρ_ M)) =
    (↑(Algebra.TensorProduct.rid (↑((𝟙_ (AlgCat R)) (𝒞 := instCategory R)) : Type u) R (↑M : Type u)) :
      TensorProduct (↑(𝟙_ (AlgCat R)) : Type u) (↑M : Type u) (↑(𝟙_ (AlgCat R)) : Type u) →ₐ[R] (↑M : Type u))

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
M : AlgCat R
⊢ Hom.hom (Iso.inv (ρ_ M)) =
    (↑(AlgEquiv.symm (Algebra.TensorProduct.rid (↑((𝟙_ (AlgCat R)) (𝒞 := instCategory R)) : Type u) R (↑M : Type u))) :
      (↑M : Type u) →ₐ[R] TensorProduct (↑(𝟙_ (AlgCat R)) : Type u) (↑M : Type u) (↑(𝟙_ (AlgCat R)) : Type u))

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
M N K : AlgCat R
⊢ Hom.hom (Iso.hom (α_ M N K)) =
    (↑(Algebra.TensorProduct.assoc R R R (↑M : Type u) (↑N : Type u) (↑K : Type u)) :
      TensorProduct R (TensorProduct R (↑M : Type u) (↑N : Type u)) (↑K : Type u) →ₐ[R]
        TensorProduct R (↑M : Type u) (TensorProduct R (↑N : Type u) (↑K : Type u)))

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, rfl
-- Module: Mathlib.Algebra.Category.AlgCat.Monoidal
Goal:
R : Type u
inst : CommRing R
M N K : AlgCat R
⊢ Hom.hom (Iso.inv (α_ M N K)) =
    (↑(AlgEquiv.symm (Algebra.TensorProduct.assoc R R R (↑M : Type u) (↑N : Type u) (↑K : Type u))) :
      TensorProduct R (↑M : Type u) (TensorProduct R (↑N : Type u) (↑K : Type u)) →ₐ[R]
        TensorProduct R (TensorProduct R (↑M : Type u) (↑N : Type u)) (↑K : Type u))

Tactic:
rfl

Premises used: AlgEquiv.toAlgHom, rfl
-- Module: Mathlib.Algebra.Category.BialgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : Type v
inst_1 : Ring X
inst_2 : Bialgebra R X
⊢ Eq.{v + 1} (α := carrier (of R X) →ₗ[R] TensorProduct R (carrier (of R X)) (carrier (of R X))) CoalgebraStruct.comul
    CoalgebraStruct.comul

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.BialgCat.Basic
Goal:
R : Type u
inst : CommRing R
X : Type v
inst_1 : Ring X
inst_2 : Bialgebra R X
⊢ Eq (α := LinearMap.{u, u, v, u} (RingHom.id R) (carrier (of R X)) R) CoalgebraStruct.counit CoalgebraStruct.counit

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.BialgCat.Basic
Goal:
R : Type u
inst : CommRing R
V W : BialgCat.{v, u} R
x x_1 : V.Hom W
f g : V.carrier →ₐc[R] W.carrier
h : { toBialgHom' := f : V.Hom W }.toBialgHom = { toBialgHom' := g }.toBialgHom
⊢ { toBialgHom' := f : V.Hom W } = { toBialgHom' := g }

Tactic:
congr
-- Module: Mathlib.Algebra.Category.BialgCat.Basic
Goal:
R : Type u
inst : CommRing R
X Y : BialgCat.{v, u} R
f g : X ⟶ Y
h : Hom.toBialgHom f = Hom.toBialgHom g
⊢ f = g

Tactic:
Hom.ext h

Premises used: BialgCat.Hom.ext