awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
j : J
x y : (↑(F.1 j) : Type (max u v))
⊢ HMul.hMul (α := M.{v, u} F) (β := M.{v, u} F)
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((Types.TypeMax.colimitCocone
                      (F ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                          (CC := carrier))).ι.app
                j) :
            (a : (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget MonCat).obj j)) →
              (fun (X : Type (max u v)) ↦ X)
                (((Functor.const J).obj (Types.TypeMax.colimitCocone (F ⋙ forget MonCat)).pt).obj j))
          x :
        (fun (X : Type (max u v)) ↦ X)
          (Functor.obj
            (Functor.obj (Functor.const J)
              (Types.TypeMax.colimitCocone
                  (F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier))).pt)
            j))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              ((Types.TypeMax.colimitCocone
                      (F ⋙
                        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v)))
                          (CC := carrier))).ι.app
                j) :
            (a : (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget MonCat).obj j)) →
              (fun (X : Type (max u v)) ↦ X)
                (((Functor.const J).obj (Types.TypeMax.colimitCocone (F ⋙ forget MonCat)).pt).obj j))
          y :
        (fun (X : Type (max u v)) ↦ X)
          (Functor.obj
            (Functor.obj (Functor.const J)
              (Types.TypeMax.colimitCocone
                  (F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier))).pt)
            j)) =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((Types.TypeMax.colimitCocone
                  (F ⋙
                    forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                      carrier))).ι.app
            j) :
        (a : (fun (X : Type (max u v)) ↦ X) ((F ⋙ forget MonCat).obj j)) →
          (fun (X : Type (max u v)) ↦ X)
            (((Functor.const J).obj (Types.TypeMax.colimitCocone (F ⋙ forget MonCat)).pt).obj j))
      (x * y)

Tactic:
apply colimit_mul_mk_eq'

Premises used: MonCat.FilteredColimits.colimit_mul_mk_eq'
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
j j' : J
f : j ⟶ j'
⊢ Eq (α := F.obj j ⟶ colimit.{v, u} F) (F.map f ≫ coconeMorphism F j') (coconeMorphism F j)

Tactic:
MonCat.ext fun x =>
    ConcreteCategory.congr_hom ((Types.TypeMax.colimitCocone (F ⋙ forget MonCat)).ι.naturality f) x

Premises used: MonCat.ext
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
t : Cocone F
⊢ Eq (α := (↑t.1 : Type (max u v)))
    ((F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier)).descColimitType
        (((F ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    carrier)).coconeTypesEquiv.symm :
            (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
          (Functor.mapCocone
            (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier))
            t))
        1 :
      Functor.CoconeTypes.pt (J := J) (F :=
        F ⋙
          forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC := carrier))
        (((F ⋙
                  forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                    carrier)).coconeTypesEquiv.symm :
            (a : Cocone (F ⋙ forget MonCat)) → (F ⋙ forget MonCat).CoconeTypes)
          (Functor.mapCocone
            (forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier))
            t)))
    1

Tactic:
simp [colimit_one_eq F IsFiltered.nonempty.some]

Premises used: Nonempty.some, CategoryTheory.IsFiltered.nonempty, MonCat.FilteredColimits.colimit_one_eq
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
t : Cocone F
m : (colimitCocone.{v, u} F).pt ⟶ t.pt
h : ∀ (j : J), (colimitCocone.{v, u} F).ι.app j ≫ m = t.ι.app j
y : (↑(colimitCocone.{v, u} F).pt : Type (max u v))
obtain :
  ∀ (j : J)
    (y :
      (F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier)).obj
        j),
    Eq (α := (↑t.pt : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier) m :
            (a : (↑(colimitCocone F).pt : Type (max u v))) → (↑t.pt : Type (max u v)))
          ((F ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  carrier)).ιColimitType
            j y) :
        (↑t.pt : Type (max u v)))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
              carrier) (X := (colimitCocone.{v, u} F).pt) (colimitDesc F t) :
            (a : (↑(colimitCocone F).pt : Type (max u v))) → (↑t.pt : Type (max u v)))
          ((F ⋙
                forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                  carrier)).ιColimitType
            j y) :
        (↑t.pt : Type (max u v)))
⊢ Eq (α := (↑t.pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) m :
          (a : (↑(colimitCocone F).pt : Type (max u v))) → (↑t.pt : Type (max u v)))
        y :
      (↑t.pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) (X := (colimitCocone.{v, u} F).pt) (colimitDesc F t) :
          (a : (↑(colimitCocone F).pt : Type (max u v))) → (↑t.pt : Type (max u v)))
        y :
      (↑t.pt : Type (max u v)))

Tactic:
obtain ⟨j, y, rfl⟩ := Functor.ιColimitType_jointly_surjective _ y

Premises used: CategoryTheory.Functor.ιColimitType_jointly_surjective, rfl
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
t : Cocone F
m : (colimitCocone.{v, u} F).pt ⟶ t.pt
h : ∀ (j : J), (colimitCocone.{v, u} F).ι.app j ≫ m = t.ι.app j
j : J
y :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          carrier)).obj
    j
⊢ Eq (α := (↑t.pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) m :
          (a : (↑(colimitCocone F).pt : Type (max u v))) → (↑t.pt : Type (max u v)))
        ((F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier)).ιColimitType
          j y) :
      (↑t.pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) (X := (colimitCocone.{v, u} F).pt) (colimitDesc F t) :
          (a : (↑(colimitCocone F).pt : Type (max u v))) → (↑t.pt : Type (max u v)))
        ((F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier)).ιColimitType
          j y) :
      (↑t.pt : Type (max u v)))

Tactic:
ConcreteCategory.congr_hom (h j) y

Premises used: CategoryTheory.Functor.descColimitType, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.Functor.ιColimitType
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ MonCat
inst_1 : IsFiltered J
t : Cocone F
m : (colimitCocone.{v, u} F).pt ⟶ t.pt
h : ∀ (j : J), (colimitCocone.{v, u} F).ι.app j ≫ m = t.ι.app j
j : J
y :
  (F ⋙
        forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          carrier)).obj
    j
⊢ Eq (α := (↑t.pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) m :
          (a : (↑(colimitCocone F).pt : Type (max u v))) → (↑t.pt : Type (max u v)))
        ((F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier)).ιColimitType
          j y) :
      (↑t.pt : Type (max u v)))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) (X := (colimitCocone.{v, u} F).pt) (colimitDesc F t) :
          (a : (↑(colimitCocone F).pt : Type (max u v))) → (↑t.pt : Type (max u v)))
        ((F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
                carrier)).ιColimitType
          j y) :
      (↑t.pt : Type (max u v)))

Tactic:
exact ConcreteCategory.congr_hom (h j) y

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ CommMonCat
x y : (↑(M.{v, u} F) : Type (max u v))
obtain :
  ∀ (i : J)
    (x :
      (↑(Functor.obj
            (F ⋙
              forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : 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))
            i) :
        Type (max u v))),
    MonCat.FilteredColimits.M.mk
          (F ⋙
            forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : 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))
          (Sigma.mk (β := fun (j : J) ↦
            (↑(Functor.obj
                  (F ⋙
                    forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                      (↑x1 : Type (max u v)) →* (↑x2 : 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))
                  j) :
              Type (max u v)))
            i x) *
        y =
      y *
        MonCat.FilteredColimits.M.mk
          (F ⋙
            forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : 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))
          (Sigma.mk (β := fun (j : J) ↦
            (↑(Functor.obj
                  (F ⋙
                    forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦
                      (↑x1 : Type (max u v)) →* (↑x2 : 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))
                  j) :
              Type (max u v)))
            i x)
⊢ x * y = y * x

Tactic:
obtain ⟨i, x, rfl⟩ := x.mk_surjective

Premises used: rfl, MonCat.FilteredColimits.M.mk_surjective
-- Module: Mathlib.Algebra.Category.MonCat.FilteredColimits
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ CommMonCat
⊢ PreservesFilteredColimits
    (forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))

Tactic:
Limits.comp_preservesFilteredColimits (forget₂ CommMonCat MonCat) (forget MonCat)

Premises used: CategoryTheory.Functor.comp, MonCat, CategoryTheory.forget₂, CommMonCat, CategoryTheory.Limits.comp_preservesFilteredColimits, CategoryTheory.forget
-- Module: Mathlib.Algebra.Category.MonCat.ForgetCorepresentable
Goal:
⊢ Functor.IsCorepresentable
    (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))

Tactic:
Functor.IsCorepresentable.mk' MonCat.coyonedaObjIsoForget

Premises used: CategoryTheory.Functor.IsCorepresentable.mk', MonCat.coyonedaObjIsoForget
-- Module: Mathlib.Algebra.Category.MonCat.ForgetCorepresentable
Goal:
⊢ Functor.IsCorepresentable
    (forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))

Tactic:
Functor.IsCorepresentable.mk' CommMonCat.coyonedaObjIsoForget

Premises used: CategoryTheory.Functor.IsCorepresentable.mk', CommMonCat.coyonedaObjIsoForget
-- Module: Mathlib.Algebra.Category.MonCat.ForgetCorepresentable
Goal:
⊢ Functor.IsCorepresentable
    (forget AddMonCat (FC := fun (x1 x2 : AddMonCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))

Tactic:
Functor.IsCorepresentable.mk' AddMonCat.coyonedaObjIsoForget

Premises used: AddMonCat.coyonedaObjIsoForget, CategoryTheory.Functor.IsCorepresentable.mk'
-- Module: Mathlib.Algebra.Category.MonCat.ForgetCorepresentable
Goal:
⊢ Functor.IsCorepresentable
    (forget AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC := carrier))

Tactic:
Functor.IsCorepresentable.mk' AddCommMonCat.coyonedaObjIsoForget

Premises used: CategoryTheory.Functor.IsCorepresentable.mk', AddCommMonCat.coyonedaObjIsoForget
-- Module: Mathlib.Algebra.Category.MonCat.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J MonCat
a b : (j : J) → (↑(F.obj j) : Type u)
ah :
  a ∈ (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections
bh :
  b ∈ (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections
j j' : J
f : j ⟶ j'
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).map
            f) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget MonCat).obj j)) → (fun (X : Type u) ↦ X) ((F ⋙ forget MonCat).obj j'))
      ((a * b) j) =
    (a * b) j'

Tactic:
simp [← ah f, ← bh f]
-- Module: Mathlib.Algebra.Category.MonCat.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J MonCat
j j' : J
f : j ⟶ j'
⊢ Eq (α :=
    (fun (X : Type u) ↦ X)
      ((F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).obj j'))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).map
              f) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget MonCat).obj j)) →
            (fun (X : Type u) ↦ X) ((F ⋙ forget MonCat).obj j'))
        (1 j) :
      (fun (X : Type u) ↦ X)
        ((F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).obj
          j'))
    (1 j' : (↑(F.obj j') : Type u))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.MonCat.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J MonCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections :
      Type (max u v))
j : J
simp : Eq.{u + 1} (α := (↑(F.obj j) : Type u)) ((↑1 : (j : J) → ToType (F.obj j)) j) 1
⊢ Eq (α := (↑(F.obj j) : Type u))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((Types.Small.limitCone
                    (F ⋙
                      forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                        carrier))).π.app
              j) :
          (a : (fun (X : Type u) ↦ X) (((Functor.const J).obj (Types.Small.limitCone (F ⋙ forget MonCat)).pt).obj j)) →
            (fun (X : Type u) ↦ X) ((F ⋙ forget MonCat).obj j))
        1 :
      (fun (X : Type u) ↦ X)
        ((F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).obj j))
    (1 : (↑(F.obj j) : Type u))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.MonCat.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J MonCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections :
      Type (max u v))
j : J
⊢ Eq.{u + 1} (α := (↑(F.obj j) : Type u)) ((↑1 : (j : J) → ToType (F.obj j)) j) 1

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

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.MonCat.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J MonCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : 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 (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) (F.obj j)) ↦
      x ∈
        (F ⋙
            forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections)
      (fun (j : J) ↦
        HMul.hMul (α := (↑(F.obj j) : Type u)) (β := (↑(F.obj j) : Type u))
          ((ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : 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 (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : 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 MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier)).sections :
        Type (max u v)))
      (Subtype.mk (p :=
        fun
          (x :
            (j : J) →
              ToType (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) (F.obj j)) ↦
        x ∈
          (F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier)).sections)
        (fun (j : J) ↦
          (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : 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 (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) (F.obj j)) ↦
        x ∈
          (F ⋙
              forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                carrier)).sections)
        (fun (j : J) ↦
          (ConcreteCategory.hom (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)
                (s.π.app j) :
              (a : (↑s.pt : Type u)) → (↑(F.obj j) : Type u))
            y)
        ⋯)

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

Tactic:
HasLimit.mk {
    cone := limitCone F
    isLimit := limitConeIsLimit F
  }

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

Tactic:
MonCat.hasLimitsOfSize.{u, u}

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

Tactic:
MonCat.forget_preservesLimitsOfSize.{u, u}

Premises used: MonCat.forget_preservesLimitsOfSize
-- Module: Mathlib.Algebra.Category.MonCat.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J MonCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)).sections :
      Type (max u v))
h :
  (c : Cone (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))) →
    (t : IsLimit c) →
      LiftsToLimit F (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
        c t
⊢ CreatesLimit F (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))

Tactic:
apply createsLimitOfReflectsIso

Premises used: CategoryTheory.createsLimitOfReflectsIso