The kernel_monoidal 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, kernel_coherence, and the kernel_disch 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, coherence, or cat_disch 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.
def
The kernel_disch tactic applies the kernel_hom transformation to the goal and then
invokes the cat_disch 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.