∀ {R : CommRingCat} {A B C : Type u} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  [inst_3 : Algebra (↑R) A] [inst_4 : Algebra (↑R) B] [inst_5 : Algebra (↑R) C] (f : A →ₐ[↑R] B) (g : B →ₐ[↑R] C),
  (g.comp f).toUnder = CategoryTheory.CategoryStruct.comp f.toUnder g.toUnder