awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
n : Type v
inst : Unique n
X Y : CommRingCat
f : X ⟶ Y
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)))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
R : CommRingCat
X Y Z : CommMonCat
f : X ⟶ Y
g : Y ⟶ Z
h :
  Hom.hom
      (Under.Hom.right
        (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom (f ≫ g)))) ⋯)) =
    Hom.hom
      (Under.Hom.right
        (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom f))) ⋯ ≫
          Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom g))) ⋯))
⊢ Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom (f ≫ g)))) ⋯ =
    Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom f))) ⋯ ≫
      Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom g))) ⋯

Tactic:
ext : 2
-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
R : CommRingCat
X Y Z : CommMonCat
f : X ⟶ Y
g : Y ⟶ Z
r : (↑R : Type (max u v))
⊢ Eq (α :=
    (↑(Under.right (X := R)
          (Under.mk (Y := of (MonoidAlgebra (↑R : Type (max u v)) (↑Z : Type v)))
            (ofHom MonoidAlgebra.singleOneRingHom))) :
      Type (max u v)))
    ((Hom.hom
            (Under.Hom.right
              (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom (f ≫ g))))
                ⋯)) :
          (a : MonoidAlgebra (↑R : Type (max u v)) (↑X : Type v)) →
            (↑(Under.mk (ofHom MonoidAlgebra.singleOneRingHom)).right : Type (max u v)))
        (MonoidAlgebra.single 1 r) :
      (↑(Under.right (X := R)
            (Under.mk (Y := of (MonoidAlgebra (↑R : Type (max u v)) (↑Z : Type v)))
              (ofHom MonoidAlgebra.singleOneRingHom))) :
        Type (max u v)))
    ((Hom.hom
            (Under.Hom.right
              (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom f))) ⋯ ≫
                Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom g))) ⋯)) :
          (a : MonoidAlgebra (↑R : Type (max u v)) (↑X : Type v)) →
            (↑(Under.mk (ofHom MonoidAlgebra.singleOneRingHom)).right : Type (max u v)))
        (MonoidAlgebra.single 1 r) :
      (↑(Under.right (X := R)
            (Under.mk (Y := of (MonoidAlgebra (↑R : Type (max u v)) (↑Z : Type v)))
              (ofHom MonoidAlgebra.singleOneRingHom))) :
        Type (max u v)))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
R : CommRingCat
X Y Z : CommMonCat
f : X ⟶ Y
g : Y ⟶ Z
m : (↑X : Type v)
⊢ Eq (α :=
    (↑(Under.right (X := R)
          (Under.mk (Y := of (MonoidAlgebra (↑R : Type (max u v)) (↑Z : Type v)))
            (ofHom MonoidAlgebra.singleOneRingHom))) :
      Type (max u v)))
    ((Hom.hom
            (Under.Hom.right
              (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom (f ≫ g))))
                ⋯)) :
          (a : MonoidAlgebra (↑R : Type (max u v)) (↑X : Type v)) →
            (↑(Under.mk (ofHom MonoidAlgebra.singleOneRingHom)).right : Type (max u v)))
        (MonoidAlgebra.single m 1) :
      (↑(Under.right (X := R)
            (Under.mk (Y := of (MonoidAlgebra (↑R : Type (max u v)) (↑Z : Type v)))
              (ofHom MonoidAlgebra.singleOneRingHom))) :
        Type (max u v)))
    ((Hom.hom
            (Under.Hom.right
              (Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom f))) ⋯ ≫
                Under.homMk (ofHom (MonoidAlgebra.mapDomainRingHom (↑R : Type (max u v)) (CommMonCat.Hom.hom g))) ⋯)) :
          (a : MonoidAlgebra (↑R : Type (max u v)) (↑X : Type v)) →
            (↑(Under.mk (ofHom MonoidAlgebra.singleOneRingHom)).right : Type (max u v)))
        (MonoidAlgebra.single m 1) :
      (↑(Under.right (X := R)
            (Under.mk (Y := of (MonoidAlgebra (↑R : Type (max u v)) (↑Z : Type v)))
              (ofHom MonoidAlgebra.singleOneRingHom))) :
        Type (max u v)))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
R : CommRingCat
S : Under R
hf :
  ∀ (x : (↑R : Type u)),
    Eq (α := (↑(Functor.obj (𝟭 (Under R)) S).right : Type u))
      ((Hom.hom
              ((Functor.obj
                    ((Under.forget R ⋙
                        forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          carrier) CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                          (CD := CommMonCat.carrier)) ⋙
                      R.monoidAlgebra)
                    S).hom ≫
                ofHom
                  (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                    (MonoidHom.id
                      (↑(Functor.obj
                            (Under.forget R ⋙
                              forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                                (CC := carrier) CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦
                                (↑x1 : Type u) →* (↑x2 : Type u)) (CD := CommMonCat.carrier))
                            S) :
                        Type u))
                    ⋯)) :
            (a : (↑R : Type u)) → (↑((𝟭 (Under R)).obj S).right : Type u))
          x :
        (↑(Functor.obj (𝟭 (Under R)) S).right : Type u))
      ((Hom.hom (Functor.obj (𝟭 (Under R)) S).hom : (a : (↑R : Type u)) → (↑((𝟭 (Under R)).obj S).right : Type u)) x :
        (↑(Functor.obj (𝟭 (Under R)) S).right : Type u))
⊢ (Functor.obj
          ((Under.forget R ⋙
              forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
                CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                CommMonCat.carrier)) ⋙
            R.monoidAlgebra)
          S).hom ≫
      ofHom
        (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
          (MonoidHom.id
            (↑(Functor.obj
                  (Under.forget R ⋙
                    forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      carrier) CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                      CommMonCat.carrier))
                  S) :
              Type u))
          ⋯) =
    (Functor.obj (𝟭 (Under R)) S).hom

Tactic:
ext
-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
R : CommRingCat
S : Under R
x : (↑R : Type u)
⊢ Eq (α := (↑(Functor.obj (𝟭 (Under R)) S).right : Type u))
    ((Hom.hom
            ((Functor.obj
                  ((Under.forget R ⋙
                      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        carrier) CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                        (CD := CommMonCat.carrier)) ⋙
                    R.monoidAlgebra)
                  S).hom ≫
              ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                  (MonoidHom.id
                    (↑(Functor.obj
                          (Under.forget R ⋙
                            forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                              (CC := carrier) CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦
                              (↑x1 : Type u) →* (↑x2 : Type u)) (CD := CommMonCat.carrier))
                          S) :
                      Type u))
                  ⋯)) :
          (a : (↑R : Type u)) → (↑((𝟭 (Under R)).obj S).right : Type u))
        x :
      (↑(Functor.obj (𝟭 (Under R)) S).right : Type u))
    ((Hom.hom (Functor.obj (𝟭 (Under R)) S).hom : (a : (↑R : Type u)) → (↑((𝟭 (Under R)).obj S).right : Type u)) x :
      (↑(Functor.obj (𝟭 (Under R)) S).right : Type u))

Tactic:
simp [MonoidAlgebra.liftNCRingHom]

Premises used: MonoidAlgebra.liftNCRingHom
-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
R : CommRingCat
S T : Under R
f : S ⟶ T
r : (↑R : Type u)
⊢ Eq (α := (↑(Functor.obj (𝟭 (Under R)) T).right : Type u))
    ((Hom.hom
            (Under.Hom.right
              (CategoryTheory.Functor.map
                  ((Under.forget R ⋙
                      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        carrier) CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                        (CD := CommMonCat.carrier)) ⋙
                    R.monoidAlgebra)
                  f ≫
                Under.homMk
                  (ofHom
                    (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
                      (MonoidHom.id
                        (↑(Functor.obj
                              (Under.forget R ⋙
                                forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦
                                  (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) CommMonCat (FD :=
                                  fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                                  CommMonCat.carrier))
                              T) :
                          Type u))
                      ⋯))
                  ⋯)) :
          (a : MonoidAlgebra (↑R : Type u) (↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S) : Type u)) →
            (↑((𝟭 (Under R)).obj T).right : Type u))
        (MonoidAlgebra.single 1 r) :
      (↑(Functor.obj (𝟭 (Under R)) T).right : Type u))
    ((Hom.hom
            (Under.Hom.right
              (Under.homMk
                  (ofHom
                    (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                      (MonoidHom.id
                        (↑(Functor.obj
                              (Under.forget R ⋙
                                forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦
                                  (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) CommMonCat (FD :=
                                  fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                                  CommMonCat.carrier))
                              S) :
                          Type u))
                      ⋯))
                  ⋯ ≫
                CategoryTheory.Functor.map (𝟭 (Under R)) f)) :
          (a : MonoidAlgebra (↑R : Type u) (↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S) : Type u)) →
            (↑((𝟭 (Under R)).obj T).right : Type u))
        (MonoidAlgebra.single 1 r) :
      (↑(Functor.obj (𝟭 (Under R)) T).right : Type u))

Tactic:
simp [MonoidAlgebra.liftNCRingHom, ← Under.w f, -Under.w]

Premises used: CategoryTheory.Under.w, MonoidAlgebra.liftNCRingHom
-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
R : CommRingCat
S T : Under R
f : S ⟶ T
m :
  (↑(Functor.obj
        (Under.forget R ⋙
          forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
            CommMonCat.carrier))
        S) :
    Type u)
⊢ Eq (α := (↑(Functor.obj (𝟭 (Under R)) T).right : Type u))
    ((Hom.hom
            (Under.Hom.right
              (CategoryTheory.Functor.map
                  ((Under.forget R ⋙
                      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        carrier) CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                        (CD := CommMonCat.carrier)) ⋙
                    R.monoidAlgebra)
                  f ≫
                Under.homMk
                  (ofHom
                    (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
                      (MonoidHom.id
                        (↑(Functor.obj
                              (Under.forget R ⋙
                                forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦
                                  (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) CommMonCat (FD :=
                                  fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                                  CommMonCat.carrier))
                              T) :
                          Type u))
                      ⋯))
                  ⋯)) :
          (a : MonoidAlgebra (↑R : Type u) (↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S) : Type u)) →
            (↑((𝟭 (Under R)).obj T).right : Type u))
        (MonoidAlgebra.single m 1) :
      (↑(Functor.obj (𝟭 (Under R)) T).right : Type u))
    ((Hom.hom
            (Under.Hom.right
              (Under.homMk
                  (ofHom
                    (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                      (MonoidHom.id
                        (↑(Functor.obj
                              (Under.forget R ⋙
                                forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦
                                  (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) CommMonCat (FD :=
                                  fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                                  CommMonCat.carrier))
                              S) :
                          Type u))
                      ⋯))
                  ⋯ ≫
                CategoryTheory.Functor.map (𝟭 (Under R)) f)) :
          (a : MonoidAlgebra (↑R : Type u) (↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S) : Type u)) →
            (↑((𝟭 (Under R)).obj T).right : Type u))
        (MonoidAlgebra.single m 1) :
      (↑(Functor.obj (𝟭 (Under R)) T).right : Type u))

Tactic:
simp [MonoidAlgebra.liftNCRingHom, ← Under.w f, -Under.w]

Premises used: CategoryTheory.Under.w, MonoidAlgebra.liftNCRingHom
-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
R : CommRingCat
G : CommMonCat
r : (↑R : Type u)
⊢ Eq (α := (↑(R.monoidAlgebra.obj G).right : Type u))
    (((Hom.hom
              (Under.Hom.right
                (CategoryStruct.comp (Y :=
                  R.monoidAlgebra.obj
                    (Functor.obj
                      (Under.forget R ⋙
                        forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          carrier) CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                          (CD := CommMonCat.carrier))
                      (R.monoidAlgebra.obj G)))
                  (R.monoidAlgebra.map
                    (NatTrans.app
                      {
                        app := fun (G : CommMonCat.{u}) ↦
                          CommMonCat.ofHom (MonoidAlgebra.of (↑R : Type u) (↑G : Type u)),
                        naturality := ⋯ }
                      G))
                  (NatTrans.app
                    {
                      app := fun (S : Under R) ↦
                        Under.homMk
                          (ofHom
                            (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                              (MonoidHom.id
                                (↑(Functor.obj
                                      (Under.forget R ⋙
                                        forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦
                                          (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) CommMonCat (FD :=
                                          fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                                          CommMonCat.carrier))
                                      S) :
                                  Type u))
                              ⋯))
                          ⋯,
                      naturality := ⋯ }
                    (R.monoidAlgebra.obj G)))) :
            (↑(R.monoidAlgebra.obj G).right : Type u) →+* (↑(R.monoidAlgebra.obj G).right : Type u)) :
          (a : MonoidAlgebra (↑R : Type u) (↑G : Type u)) → (↑(R.monoidAlgebra.obj G).right : Type u))
        (MonoidAlgebra.single 1 r) :
      (↑(R.monoidAlgebra.obj G).right : Type u))
    ((Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G))) :
          (a : MonoidAlgebra (↑R : Type u) (↑G : Type u)) → (↑(R.monoidAlgebra.obj G).right : Type u))
        (MonoidAlgebra.single 1 r) :
      (↑(R.monoidAlgebra.obj G).right : Type u))

Tactic:
simp [MonoidAlgebra.liftNCRingHom]

Premises used: MonoidAlgebra.liftNCRingHom
-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
R : CommRingCat
G : CommMonCat
m : (↑G : Type u)
⊢ Eq (α := (↑(R.monoidAlgebra.obj G).right : Type u))
    (((Hom.hom
              (Under.Hom.right
                (CategoryStruct.comp (Y :=
                  R.monoidAlgebra.obj
                    (Functor.obj
                      (Under.forget R ⋙
                        forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          carrier) CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u))
                          (CD := CommMonCat.carrier))
                      (R.monoidAlgebra.obj G)))
                  (R.monoidAlgebra.map
                    (NatTrans.app
                      {
                        app := fun (G : CommMonCat.{u}) ↦
                          CommMonCat.ofHom (MonoidAlgebra.of (↑R : Type u) (↑G : Type u)),
                        naturality := ⋯ }
                      G))
                  (NatTrans.app
                    {
                      app := fun (S : Under R) ↦
                        Under.homMk
                          (ofHom
                            (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                              (MonoidHom.id
                                (↑(Functor.obj
                                      (Under.forget R ⋙
                                        forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦
                                          (↑R : Type u) →+* (↑S : Type u)) (CC := carrier) CommMonCat (FD :=
                                          fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                                          CommMonCat.carrier))
                                      S) :
                                  Type u))
                              ⋯))
                          ⋯,
                      naturality := ⋯ }
                    (R.monoidAlgebra.obj G)))) :
            (↑(R.monoidAlgebra.obj G).right : Type u) →+* (↑(R.monoidAlgebra.obj G).right : Type u)) :
          (a : MonoidAlgebra (↑R : Type u) (↑G : Type u)) → (↑(R.monoidAlgebra.obj G).right : Type u))
        (MonoidAlgebra.single m 1) :
      (↑(R.monoidAlgebra.obj G).right : Type u))
    ((Hom.hom (Under.Hom.right (𝟙 (R.monoidAlgebra.obj G))) :
          (a : MonoidAlgebra (↑R : Type u) (↑G : Type u)) → (↑(R.monoidAlgebra.obj G).right : Type u))
        (MonoidAlgebra.single m 1) :
      (↑(R.monoidAlgebra.obj G).right : Type u))

Tactic:
simp [MonoidAlgebra.liftNCRingHom]

Premises used: MonoidAlgebra.liftNCRingHom
-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
R : CommRingCat
S : Under R
x :
  (↑(Functor.obj
        (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
          CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD := CommMonCat.carrier))
        S.right) :
    Type u)
⊢ Eq (α :=
    (↑(Functor.obj
          (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
            CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
            CommMonCat.carrier))
          S.right) :
      Type u))
    ((CommMonCat.Hom.hom
            (CategoryStruct.comp (Y :=
              Functor.obj
                (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier) CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                  CommMonCat.carrier))
                (of (MonoidAlgebra (↑R : Type u) (↑S.right : Type u))))
              (CommMonCat.ofHom (MonoidAlgebra.of (↑R : Type u) (↑S.right : Type u)))
              (CommMonCat.ofHom
                (↑(MonoidAlgebra.liftNCRingHom (Hom.hom S.hom) (MonoidHom.id (↑S.right : Type u)) ⋯) :
                  MonoidAlgebra (↑R : Type u) (↑S.right : Type u) →* (↑S.right : Type u)))) :
          (a : (↑((forget₂ CommRingCat CommMonCat).obj S.right) : Type u)) →
            (↑((forget₂ CommRingCat CommMonCat).obj S.right) : Type u))
        x :
      (↑(Functor.obj
            (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
              CommMonCat.carrier))
            S.right) :
        Type u))
    ((CommMonCat.Hom.hom
            (𝟙
              (Functor.obj
                (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  carrier) CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
                  CommMonCat.carrier))
                S.right)) :
          (a : (↑((forget₂ CommRingCat CommMonCat).obj S.right) : Type u)) →
            (↑((forget₂ CommRingCat CommMonCat).obj S.right) : Type u))
        x :
      (↑(Functor.obj
            (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := carrier)
              CommMonCat (FD := fun (x1 x2 : CommMonCat.{u}) ↦ (↑x1 : Type u) →* (↑x2 : Type u)) (CD :=
              CommMonCat.carrier))
            S.right) :
        Type u))

Tactic:
simp [MonoidAlgebra.liftNCRingHom]

Premises used: MonoidAlgebra.liftNCRingHom
-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
R : CommRingCat
⊢ R.monoidAlgebra.IsLeftAdjoint

Tactic:
⟨_, ⟨CommRingCat.monoidAlgebraAdj R⟩⟩

Premises used: Nonempty.intro, CommRingCat.monoidAlgebraAdj, Exists.intro, CategoryTheory.Functor.IsLeftAdjoint.mk
-- Module: Mathlib.Algebra.Category.Ring.Adjunctions
Goal:
⊢ Functor.IsRightAdjoint
    (forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := carrier)
      CommMonCat (FD := fun (x1 x2 : CommMonCat.{u_1}) ↦ (↑x1 : Type u_1) →* (↑x2 : Type u_1)) (CD :=
      CommMonCat.carrier))

Tactic:
⟨_, ⟨CommRingCat.forget₂Adj Limits.initialIsInitial⟩⟩

Premises used: CommRingCat.forget₂Adj, CategoryTheory.Limits.initialIsInitial, Nonempty.intro, Exists.intro, CategoryTheory.Functor.IsRightAdjoint.mk