∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (c : B) (f : a ⟶ b) {X Y : b ⟶ c} (x : X ⟶ Y),
  (CategoryTheory.Bicategory.precomp c f).map x = CategoryTheory.Bicategory.whiskerLeft f x