Commit 2025-07-02 09:20 c5c25a18
View on Github →chore(CategoryTheory): rename whiskerLeft to Functor.whiskerLeft (#26611)
In Mathlib, we have many MonoidalCategory.whiskerLeft_comp in simp or rw arguments even when we are in the MonoidalCategory namespace. This is because we have whiskerLeft and related lemmas directly in the CategoryTheory namespace. This PR renames these names to Functor.* so that we can access MonoidalCategory.whiskerLeft_comp just by whiskerLeft_comp in the MonoidalCategory namespace.