awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
c : Cone (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
t : IsLimit c
⊢ 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))

Tactic:
have : Small.{u} (Functor.sections (F ⋙ forget MonCat)) :=
    (Types.hasLimit_iff_small_sections _).mp (HasLimit.mk { cone := c, isLimit := t })
-- 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))
c : Cone (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
t : IsLimit c
this :
  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
simp :
  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)
⊢ Eq (α :=
    (Types.Small.limitCone
        (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))).pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (IsLimit.lift
              (Types.Small.limitConeIsLimit
                (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier)))
              (Functor.mapCone
                (forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
                s)) :
          (a : (fun (X : Type u) ↦ X) ((forget MonCat).mapCone s).pt) →
            (fun (X : Type u) ↦ X) (Types.Small.limitCone (F ⋙ forget MonCat)).pt)
        1 :
      (fun (X : Type u) ↦ X)
        (Types.Small.limitCone
            (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))).pt)
    (1 :
      (Types.Small.limitCone
          (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))).pt)

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))
c : Cone (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
t : IsLimit c
this :
  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))
c : Cone (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
t : IsLimit c
this :
  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)
⊢ (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 (α := (j : J) → (↑(F.obj j) : Type u))
      (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)
      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 CommMonCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
⊢ Small.{u, max u v}
    (↑((F ⋙
              forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : 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))

Tactic:
inferInstanceAs <| Small.{u} (Functor.sections (F ⋙ forget CommMonCat))

Premises used: _private.0.CommMonCat.instSmallElemForallObjCompMonCatForget₂MonoidHomCarrierCarrierForgetSections._proof_1
-- Module: Mathlib.Algebra.Category.MonCat.Limits
Goal:
J : Type v
inst : Category.{w, v} J
F : CategoryTheory.Functor.{w, u, v, u + 1} J CommMonCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
c' :
  Cone
    (F ⋙
      forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) MonCat
        (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier))
t : IsLimit c'
⊢ Functor.mapCone
      (forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) MonCat
        (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier))
      {
        pt :=
          of
            (Types.Small.limitCone
                (F ⋙
                  forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                    carrier))).pt,
        π :=
          {
            app := fun (j : J) ↦
              ofHom
                (limitπMonoidHom
                  (F ⋙
                    forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
                      carrier) MonCat (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                      MonCat.carrier))
                  j),
            naturality := ⋯ } } ≅
    c'

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

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

Tactic:
CommMonCat.hasLimitsOfSize.{u, u}

Premises used: CommMonCat.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 CommMonCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
⊢ PreservesLimits
    (forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier) MonCat
      (FD := fun (x1 x2 : MonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := MonCat.carrier))

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

Premises used: CommMonCat.forget₂Mon_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 CommMonCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
⊢ PreservesLimits
    (forget AddCommMonCat (FC := fun (x1 x2 : AddCommMonCat.{u}) ↦ (↑x1 : Type u) →+ (↑x2 : Type u)) (CC :=
      AddCommMonCat.carrier))

Tactic:
AddCommMonCat.forget_preservesLimitsOfSize.{u, u}

Premises used: AddCommMonCat.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 CommMonCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
⊢ PreservesLimits
    (forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))

Tactic:
CommMonCat.forget_preservesLimitsOfSize.{u, u}

Premises used: CommMonCat.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 CommMonCat
inst_1 :
  Small.{u, max u v}
    (↑(F ⋙
            forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC :=
              carrier)).sections :
      Type (max u v))
e : Iso (C := CommMonCat ⥤ Type u)
  (forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
  (forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : 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)) :=
  NatIso.ofComponents
    (fun (x : CommMonCat.{u}) ↦
      Iso.refl
        (Functor.obj
          (forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))
          x))
    ⋯
⊢ CreatesLimit F
    (forget CommMonCat (FC := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CC := carrier))

Tactic:
exact createsLimitOfNatIso e.symm

Premises used: CategoryTheory.createsLimitOfNatIso, CategoryTheory.Iso.symm
-- Module: Mathlib.Algebra.Category.MonCat.Shrink
Goal:
C : Type u
inst : Category.{v, u} C
F : CategoryTheory.Functor.{v, w', u, w' + 1} C MonCat
inst_1 : ∀ (X : C), Small.{w, w'} (↑(F.obj X) : Type w')
⊢ FunctorToTypes.Small.{w, w', v, u}
    (F ⋙ forget MonCat (FC := fun (x1 x2 : MonCat.{w'}) ↦ (↑x1 : Type w') →* (↑x2 : Type w')) (CC := MonCat.carrier))

Tactic:
fun X ↦ inferInstanceAs <| Small.{w} (F.obj X)

Premises used: _private.0.instSmallCompMonCatForgetMonoidHomCarrierOfSmallObj._proof_1
-- Module: Mathlib.Algebra.Category.MonCat.Shrink
Goal:
C : Type u
inst : Category.{v, u} C
F G : CategoryTheory.Functor.{v, w', u, w' + 1} C MonCat
τ : F ⟶ G
inst_1 : ∀ (X : C), Small.{w, w'} (↑(F.obj X) : Type w')
inst_2 : ∀ (X : C), Small.{w, w'} (↑(G.obj X) : Type w')
X Y : C
f : X ⟶ Y
hf :
  ∀ (x : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)),
    Eq (α := (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
      ((Hom.hom
              ((shrinkFunctor.{w, w', v, u} F).map f ≫
                ofHom
                  (MonoidHom.comp
                    (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm Shrink.mulEquiv)) (Hom.hom (τ.app Y)))
                    (MulEquiv.toMonoidHom Shrink.mulEquiv))) :
            (a : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)) →
              (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
          x :
        (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
      ((Hom.hom
              (ofHom
                  (MonoidHom.comp
                    (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm Shrink.mulEquiv)) (Hom.hom (τ.app X)))
                    (MulEquiv.toMonoidHom Shrink.mulEquiv)) ≫
                (shrinkFunctor.{w, w', v, u} G).map f) :
            (a : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)) →
              (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
          x :
        (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
⊢ (shrinkFunctor.{w, w', v, u} F).map f ≫
      ofHom
        (MonoidHom.comp (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm Shrink.mulEquiv)) (Hom.hom (τ.app Y)))
          (MulEquiv.toMonoidHom Shrink.mulEquiv)) =
    ofHom
        (MonoidHom.comp (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm Shrink.mulEquiv)) (Hom.hom (τ.app X)))
          (MulEquiv.toMonoidHom Shrink.mulEquiv)) ≫
      (shrinkFunctor.{w, w', v, u} G).map f

Tactic:
ext x
-- Module: Mathlib.Algebra.Category.MonCat.Shrink
Goal:
C : Type u
inst : Category.{v, u} C
F G : CategoryTheory.Functor.{v, w', u, w' + 1} C MonCat
τ : F ⟶ G
inst_1 : ∀ (X : C), Small.{w, w'} (↑(F.obj X) : Type w')
inst_2 : ∀ (X : C), Small.{w, w'} (↑(G.obj X) : Type w')
X Y : C
f : X ⟶ Y
x : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)
⊢ Eq (α := (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
    ((Hom.hom
            ((shrinkFunctor.{w, w', v, u} F).map f ≫
              ofHom
                (MonoidHom.comp
                  (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm Shrink.mulEquiv)) (Hom.hom (τ.app Y)))
                  (MulEquiv.toMonoidHom Shrink.mulEquiv))) :
          (a : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)) →
            (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
        x :
      (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
    ((Hom.hom
            (ofHom
                (MonoidHom.comp
                  (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm Shrink.mulEquiv)) (Hom.hom (τ.app X)))
                  (MulEquiv.toMonoidHom Shrink.mulEquiv)) ≫
              (shrinkFunctor.{w, w', v, u} G).map f) :
          (a : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)) →
            (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
        x :
      (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))

Tactic:
congr($((FunctorToTypes.shrinkMap.{w} (Functor.whiskerRight τ (forget _))).naturality f) x)

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, id, MonCat, CategoryTheory.Functor.whiskerRight, CategoryTheory.NatTrans.naturality, CategoryTheory.forget, DFunLike.coe, CategoryTheory.FunctorToTypes.shrinkMap
-- Module: Mathlib.Algebra.Category.MonCat.Shrink
Goal:
C : Type u
inst : Category.{v, u} C
F G : CategoryTheory.Functor.{v, w', u, w' + 1} C MonCat
τ : F ⟶ G
inst_1 : ∀ (X : C), Small.{w, w'} (↑(F.obj X) : Type w')
inst_2 : ∀ (X : C), Small.{w, w'} (↑(G.obj X) : Type w')
X Y : C
f : X ⟶ Y
x : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)
⊢ Eq (α := (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
    ((Hom.hom
            ((shrinkFunctor.{w, w', v, u} F).map f ≫
              ofHom
                (MonoidHom.comp
                  (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm Shrink.mulEquiv)) (Hom.hom (τ.app Y)))
                  (MulEquiv.toMonoidHom Shrink.mulEquiv))) :
          (a : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)) →
            (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
        x :
      (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
    ((Hom.hom
            (ofHom
                (MonoidHom.comp
                  (MonoidHom.comp (MulEquiv.toMonoidHom (MulEquiv.symm Shrink.mulEquiv)) (Hom.hom (τ.app X)))
                  (MulEquiv.toMonoidHom Shrink.mulEquiv)) ≫
              (shrinkFunctor.{w, w', v, u} G).map f) :
          (a : (↑((shrinkFunctor.{w, w', v, u} F).obj X) : Type w)) →
            (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))
        x :
      (↑((shrinkFunctor.{w, w', v, u} G).obj Y) : Type w))

Tactic:
exact
      congr($((FunctorToTypes.shrinkMap.{w} (Functor.whiskerRight τ (forget _))).naturality f) x)
-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
α : Type u
⊢ (↑(free.obj α) : Type u) = MvPolynomial α ℤ

Tactic:
rfl

Premises used: AddMonoidAlgebra, rfl
-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
α β : Type u
f : α ⟶ β
⊢ Eq (α := (a : (↑(free.obj α) : Type u)) → (↑(free.obj β) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
          (free.map f)) :
      (a : (↑(free.obj α) : Type u)) → (↑(free.obj β) : Type u))
    (⇑(rename
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) α) → (fun (X : Type u) ↦ X) β)) :
      (a : MvPolynomial ((fun (X : Type u) ↦ X) α) ℤ) → MvPolynomial ((fun (X : Type u) ↦ X) β) ℤ)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.eval₂, Finset.sum, rfl
-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
⊢ Functor.IsRightAdjoint
    (forget CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier))

Tactic:
⟨_, ⟨adj⟩⟩

Premises used: Nonempty.intro, CommRingCat.adj, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.mk
-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
R : CommRingCat
⊢ Functor.IsRightAdjoint (Functor.obj yoneda R)

Tactic:
⟨_, ⟨coyonedaAdj R⟩⟩

Premises used: CommRingCat.coyonedaAdj, Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.mk
-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
n : Type v
inst : Unique n
X Y : CommRingCat
f : X ⟶ Y
hf :
  ∀ (x : (↑((coyoneda.obj (op n)).obj X) : Type (max u v))),
    Eq (α := (↑(Functor.obj (𝟭 CommRingCat) Y) : Type (max u v)))
      ((Hom.hom
              ((coyoneda.obj (op n)).map f ≫
                Iso.hom
                  ((fun (X : CommRingCat) ↦
                      (RingEquiv.toCommRingCatIso (RingEquiv.piUnique fun (i : unop (op n)) ↦ (↑X : Type (max u v))) :
                        of (unop (op n) → (↑X : Type (max u v))) ≅ of (↑X : Type (max u v))))
                    Y)) :
            (a : (↑((coyoneda.obj (op n)).obj X) : Type (max u v))) → (↑((𝟭 CommRingCat).obj Y) : Type (max u v)))
          x :
        (↑(Functor.obj (𝟭 CommRingCat) Y) : Type (max u v)))
      ((Hom.hom
              (Iso.hom
                  ((fun (X : CommRingCat) ↦
                      (RingEquiv.toCommRingCatIso (RingEquiv.piUnique fun (i : unop (op n)) ↦ (↑X : Type (max u v))) :
                        of (unop (op n) → (↑X : Type (max u v))) ≅ of (↑X : Type (max u v))))
                    X) ≫
                CategoryTheory.Functor.map (𝟭 CommRingCat) f) :
            (a : (↑((coyoneda.obj (op n)).obj X) : Type (max u v))) → (↑((𝟭 CommRingCat).obj Y) : Type (max u v)))
          x :
        (↑(Functor.obj (𝟭 CommRingCat) Y) : Type (max u v)))
⊢ Eq (α := (coyoneda.obj (op n)).obj X ⟶ Functor.obj (𝟭 CommRingCat) Y)
    ((coyoneda.obj (op n)).map f ≫
      Iso.hom
        ((fun (X : CommRingCat) ↦
            (RingEquiv.toCommRingCatIso (RingEquiv.piUnique fun (i : unop (op n)) ↦ (↑X : Type (max u v))) :
              of (unop (op n) → (↑X : Type (max u v))) ≅ of (↑X : Type (max u v))))
          Y))
    (Iso.hom
        ((fun (X : CommRingCat) ↦
            (RingEquiv.toCommRingCatIso (RingEquiv.piUnique fun (i : unop (op n)) ↦ (↑X : Type (max u v))) :
              of (unop (op n) → (↑X : Type (max u v))) ≅ of (↑X : Type (max u v))))
          X) ≫
      CategoryTheory.Functor.map (𝟭 CommRingCat) f)

Tactic:
ext