Lean4
@[inherit_doc monoidal_simps, tactic Mathlib.Tactic.Coherence.monoidal_simps]
public meta def _aux_Mathlib_Tactic_CategoryTheory_Coherence___elabRules_Mathlib_Tactic_Coherence_monoidal_simps_1 :
Lean.Elab.Tactic.Tactic✝ := fun
| `(tactic| monoidal_simps$cfg:optConfig) => do
evalTactic
(←
`(tactic|
simp$cfg only [Category.assoc, MonoidalCategory.tensor_whiskerLeft, MonoidalCategory.id_whiskerLeft,
MonoidalCategory.whiskerRight_tensor, MonoidalCategory.whiskerRight_id, MonoidalCategory.whiskerLeft_comp,
MonoidalCategory.whiskerLeft_id, MonoidalCategory.comp_whiskerRight, MonoidalCategory.id_whiskerRight,
MonoidalCategory.whisker_assoc, MonoidalCategory.id_tensorHom, MonoidalCategory.tensorHom_id];
-- I'm not sure if `tensorHom` should be expanded.
try simp only [MonoidalCategory.tensorHom_def]))
| _ => no_error_if_unused% throwUnsupportedSyntax✝
