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)