∀ {R S T : RingCat} (f : R ⟶ S) (g : S ⟶ T) (r : ↑R),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) r =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) r)