{R₁ : Type u₁} →
  {R₂ : Type u₂} →
    {R₃ : Type u₃} →
      [inst : Ring R₁] →
        [inst_1 : Ring R₂] →
          [inst_2 : Ring R₃] →
            (f : R₁ →+* R₂) →
              (g : R₂ →+* R₃) →
                ModuleCat.restrictScalars (g.comp f) ≅ (ModuleCat.restrictScalars g).comp (ModuleCat.restrictScalars f)