Module: Mathlib.Algebra.Category.Ring.Adjunctions

Goal state before:
pp: case h₁
R : CommRingCat
S T : Under R
f : S ⟶ T
r✝ : ↑R
⊢ (Hom.hom
        (Under.Hom.right
          (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
            Under.homMk
              (ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
                  (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
              ⋯)))
      (MonoidAlgebra.single 1 r✝) =
    (Hom.hom
        (Under.Hom.right
          (Under.homMk
              (ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                  (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
              ⋯ ≫
            (𝟭 (Under R)).map f)))
      (MonoidAlgebra.single 1 r✝)

pp: case h_of
R : CommRingCat
S T : Under R
f : S ⟶ T
m✝ : ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)
⊢ (Hom.hom
        (Under.Hom.right
          (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
            Under.homMk
              (ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
                  (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
              ⋯)))
      (MonoidAlgebra.single m✝ 1) =
    (Hom.hom
        (Under.Hom.right
          (Under.homMk
              (ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                  (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
              ⋯ ≫
            (𝟭 (Under R)).map f)))
      (MonoidAlgebra.single m✝ 1)

Tactic:
<;>

Goal state after:
case h₁
R : CommRingCat
S T : Under R
f : S ⟶ T
r✝ : ↑R
⊢ (Hom.hom
        (Under.Hom.right
          (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
            Under.homMk
              (ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
                  (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
              ⋯)))
      (MonoidAlgebra.single 1 r✝) =
    (Hom.hom
        (Under.Hom.right
          (Under.homMk
              (ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                  (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
              ⋯ ≫
            (𝟭 (Under R)).map f)))
      (MonoidAlgebra.single 1 r✝)

case h_of
R : CommRingCat
S T : Under R
f : S ⟶ T
m✝ : ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)
⊢ (Hom.hom
        (Under.Hom.right
          (((Under.forget R ⋙ forget₂ CommRingCat CommMonCat) ⋙ R.monoidAlgebra).map f ≫
            Under.homMk
              (ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom T.hom)
                  (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj T)) ⋯))
              ⋯)))
      (MonoidAlgebra.single m✝ 1) =
    (Hom.hom
        (Under.Hom.right
          (Under.homMk
              (ofHom
                (MonoidAlgebra.liftNCRingHom (Hom.hom S.hom)
                  (MonoidHom.id ↑((Under.forget R ⋙ forget₂ CommRingCat CommMonCat).obj S)) ⋯))
              ⋯ ≫
            (𝟭 (Under R)).map f)))
      (MonoidAlgebra.single m✝ 1)