∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d e f : B} {g : c ⟶ e} {h : d ⟶ f} {l₁ : c ⟶ d} {r₁ : d ⟶ c}
  {l₂ : e ⟶ f} {r₂ : f ⟶ e} (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁)
  (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂)
  (α : CategoryTheory.CategoryStruct.comp g l₂ ⟶ CategoryTheory.CategoryStruct.comp l₁ h),
  (CategoryTheory.Bicategory.mateEquiv adj₁ adj₂) α =
    CategoryTheory.bicategoricalComp (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp r₁ g))
      (CategoryTheory.bicategoricalComp
        (CategoryTheory.Bicategory.whiskerLeft r₁ (CategoryTheory.Bicategory.whiskerLeft g adj₂.unit))
        (CategoryTheory.bicategoricalComp
          (CategoryTheory.Bicategory.whiskerLeft r₁ (CategoryTheory.Bicategory.whiskerRight α r₂))
          (CategoryTheory.bicategoricalComp
            (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight adj₁.counit h) r₂)
            (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp h r₂)))))