∀ {B : Type u_2} [inst : CategoryTheory.Bicategory B] (a b : B) {X Y : a ⟶ b} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Bicategory.precomposing a a b).obj (CategoryTheory.CategoryStruct.id a)).map f)
      ((fun x => CategoryTheory.Bicategory.leftUnitor x) Y).hom =
    CategoryTheory.CategoryStruct.comp ((fun x => CategoryTheory.Bicategory.leftUnitor x) X).hom
      ((CategoryTheory.Functor.id (a ⟶ b)).map f)