The kernel_coherence tactic applies the kernel_hom transformation to the goal and then
invokes the monoidal tactic to solve or simplify the resulting goal.
5. 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, Kernel-Hom provide the kernel_monoidal and kernel_coherence tactics, which first apply kernel_hom to the goal to translate the kernel equality into a categorical equality in the SFinKer category, then apply monoidal or coherence to solve or simplify the categorical equality.
def
def
The kernel_coherence tactic applies the kernel_hom transformation to the goal and then
invokes the coherence tactic to solve the resulting goal.
For more details on the implementation of the monoidal and coherence tactics, see the documentation made by @Yuma Mizuno.