4. Categorical tactics for kernels🔗

Two of the most powerful tactics for categories is Mathlib are monoidal and coherence. To facilitate the use of these tactics for kernel equalities, we provide the kernel_coherence and kernel_monoidal tactics, which first apply kernel_hom to the goal to translate the kernel equality into a categorical equality in the SFinKer category, then apply coherence or monoidal to solve or simplify the categorical equality.