Lean4
@[inherit_doc whisker_simps, tactic Mathlib.Tactic.BicategoryCoherence.whisker_simps]
public meta def
_aux_Mathlib_Tactic_CategoryTheory_BicategoryCoherence___elabRules_Mathlib_Tactic_BicategoryCoherence_whisker_simps_1 :
Lean.Elab.Tactic.Tactic✝ := fun
| `(tactic| whisker_simps$cfg) => do
evalTactic
(←
`(tactic|
simp$cfg only [Category.assoc, Bicategory.comp_whiskerLeft, Bicategory.id_whiskerLeft,
Bicategory.whiskerRight_comp, Bicategory.whiskerRight_id, Bicategory.whiskerLeft_comp,
Bicategory.whiskerLeft_id, Bicategory.comp_whiskerRight, Bicategory.id_whiskerRight,
Bicategory.whisker_assoc]))
-- We have unused typeclass arguments here.
-- They are intentional, to ensure that `simp only [assoc_liftHom₂]` only left associates
-- bicategorical structural morphisms.
| _ => no_error_if_unused% throwUnsupportedSyntax✝
