∀ {B : Type u_3} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {u : b ⟶ a}
  (adj : CategoryTheory.Bicategory.Adjunction f u) {x : B} (h : x ⟶ a)
  (s :
    CategoryTheory.Bicategory.LeftLift u (CategoryTheory.CategoryStruct.comp h (CategoryTheory.CategoryStruct.id a))),
  CategoryTheory.bicategoricalComp
      (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp h (CategoryTheory.CategoryStruct.id a)))
      (CategoryTheory.bicategoricalComp
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft
            (CategoryTheory.CategoryStruct.comp h (CategoryTheory.CategoryStruct.id a)) adj.unit)
          (CategoryTheory.Bicategory.whiskerRight s.unit (CategoryTheory.CategoryStruct.comp f u)))
        (CategoryTheory.bicategoricalComp
          (CategoryTheory.Bicategory.whiskerLeft s.lift (CategoryTheory.Bicategory.whiskerRight adj.counit u))
          (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp s.lift u)))) =
    CategoryTheory.bicategoricalComp s.unit
      (CategoryTheory.bicategoricalComp
        (CategoryTheory.Bicategory.whiskerLeft s.lift (CategoryTheory.Bicategory.rightZigzag adj.unit adj.counit))
        (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp s.lift u)))