awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
l : a ⟶ b
r : b ⟶ a
adj : l ⊣ r
l' : a ⟶ b
r' : b ⟶ a
adj' : l' ⊣ r'
φ : l' ⟶ l
simp :
  Eq (α := r ⟶ r' ≫ 𝟙 a)
    ((ρ_ r).inv ≫
      (mateEquiv adj adj' : (a_1 : 𝟙 a ≫ l' ⟶ l ≫ 𝟙 b) → r ≫ 𝟙 a ⟶ 𝟙 b ≫ r') ((λ_ l').hom ≫ φ ≫ (ρ_ l).inv) ≫
        (ρ_ (𝟙 b ≫ r')).inv ≫ Iso.hom (α_ (𝟙 b) r' (𝟙 a)) ≫ (λ_ (r' ≫ 𝟙 a)).hom)
    ((ρ_ r).inv ≫
      (mateEquiv adj adj' : (a_1 : 𝟙 a ≫ l' ⟶ l ≫ 𝟙 b) → r ≫ 𝟙 a ⟶ 𝟙 b ≫ r') ((λ_ l').hom ≫ φ ≫ (ρ_ l).inv) ≫
        (λ_ r').hom ≫ (ρ_ r').inv)
⊢ Eq (α := r ⟶ r' ≫ 𝟙 a)
    ((conjugateEquiv adj (Adjunction.comp (Adjunction.id a) adj') : (a_1 : 𝟙 a ≫ l' ⟶ l) → r ⟶ r' ≫ 𝟙 a)
        ((λ_ l').hom ≫ φ) :
      r ⟶ r' ≫ 𝟙 a)
    ((conjugateEquiv adj adj' : (a_1 : l' ⟶ l) → r ⟶ r') φ ≫ (ρ_ r').inv : r ⟶ r' ≫ 𝟙 a)

Tactic:
simp only [conjugateEquiv_apply, mateEquiv_id_comp_right,
    id_whiskerLeft, Category.assoc, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Bicategory.conjugateEquiv_apply, CategoryTheory.Bicategory.mateEquiv_id_comp_right, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Bicategory.id_whiskerLeft
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
l : a ⟶ b
r : b ⟶ a
adj : l ⊣ r
l' : a ⟶ b
r' : b ⟶ a
adj' : l' ⊣ r'
φ : l' ⟶ l
⊢ Eq (α := r ⟶ r' ≫ 𝟙 a)
    ((ρ_ r).inv ≫
      (mateEquiv adj adj' : (a_1 : 𝟙 a ≫ l' ⟶ l ≫ 𝟙 b) → r ≫ 𝟙 a ⟶ 𝟙 b ≫ r') ((λ_ l').hom ≫ φ ≫ (ρ_ l).inv) ≫
        (ρ_ (𝟙 b ≫ r')).inv ≫ Iso.hom (α_ (𝟙 b) r' (𝟙 a)) ≫ (λ_ (r' ≫ 𝟙 a)).hom)
    ((ρ_ r).inv ≫
      (mateEquiv adj adj' : (a_1 : 𝟙 a ≫ l' ⟶ l ≫ 𝟙 b) → r ≫ 𝟙 a ⟶ 𝟙 b ≫ r') ((λ_ l').hom ≫ φ ≫ (ρ_ l).inv) ≫
        (λ_ r').hom ≫ (ρ_ r').inv)

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
l : a ⟶ b
r : b ⟶ a
adj : l ⊣ r
l' : a ⟶ b
r' : b ⟶ a
adj' : l' ⊣ r'
φ : l' ⟶ l
simp :
  (ρ_ (𝟙 a ≫ l')).inv ≫ Iso.hom (α_ (𝟙 a) l' (𝟙 b)) ≫ (λ_ (l' ≫ 𝟙 b)).hom ≫ (ρ_ l').hom ≫ φ ≫ (ρ_ l).inv =
    (λ_ l').hom ≫ φ ≫ (ρ_ l).inv
⊢ Eq (α := r ⟶ 𝟙 b ≫ r')
    ((conjugateEquiv adj (adj'.comp (Adjunction.id b)) : (a_1 : l' ≫ 𝟙 b ⟶ l) → r ⟶ 𝟙 b ≫ r') ((ρ_ l').hom ≫ φ) :
      r ⟶ 𝟙 b ≫ r')
    ((conjugateEquiv adj adj' : (a_1 : l' ⟶ l) → r ⟶ r') φ ≫ (λ_ r').inv : r ⟶ 𝟙 b ≫ r')

Tactic:
simp only [conjugateEquiv_apply, Category.assoc, mateEquiv_comp_id_right, id_whiskerLeft,
    Iso.inv_hom_id, Category.comp_id, Iso.hom_inv_id, Iso.cancel_iso_inv_left,
    EmbeddingLike.apply_eq_iff_eq]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Bicategory.mateEquiv_comp_id_right, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Bicategory.conjugateEquiv_apply, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Iso.cancel_iso_inv_left, CategoryTheory.Category.comp_id, EmbeddingLike.apply_eq_iff_eq, CategoryTheory.Bicategory.id_whiskerLeft
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
l : a ⟶ b
r : b ⟶ a
adj : l ⊣ r
l' : a ⟶ b
r' : b ⟶ a
adj' : l' ⊣ r'
φ : l' ⟶ l
⊢ (ρ_ (𝟙 a ≫ l')).inv ≫ Iso.hom (α_ (𝟙 a) l' (𝟙 b)) ≫ (λ_ (l' ≫ 𝟙 b)).hom ≫ (ρ_ l').hom ≫ φ ≫ (ρ_ l).inv =
    (λ_ l').hom ≫ φ ≫ (ρ_ l).inv

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
l₂' : b ⟶ c
r₂' : c ⟶ b
adj₂' : l₂' ⊣ r₂'
φ : l₂' ⟶ l₂
⊢ Eq (α := (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
    ((mateEquiv (adj₁.comp adj₂) (adj₁.comp adj₂') :
          (a_1 : 𝟙 a ≫ l₁ ≫ l₂' ⟶ (l₁ ≫ l₂) ≫ 𝟙 c) → (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
        (leftAdjointSquare.hcomp ((λ_ l₁).hom ≫ (ρ_ l₁).inv) ((λ_ l₂').hom ≫ φ ≫ (ρ_ l₂).inv)) :
      (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
    (rightAdjointSquare.hcomp (h := 𝟙 b)
        ((mateEquiv adj₁ adj₁ : (a_1 : 𝟙 a ≫ l₁ ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₁) ((λ_ l₁).hom ≫ (ρ_ l₁).inv))
        ((mateEquiv adj₂ adj₂' : (a : 𝟙 b ≫ l₂' ⟶ l₂ ≫ 𝟙 c) → r₂ ≫ 𝟙 b ⟶ 𝟙 c ≫ r₂') ((λ_ l₂').hom ≫ φ ≫ (ρ_ l₂).inv)) :
      (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)

Tactic:
have := mateEquiv_hcomp adj₁ adj₁ adj₂ adj₂' ((λ_ _).hom ≫ (ρ_ _).inv)
    ((λ_ _).hom ≫ φ ≫ (ρ_ _).inv)
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
l₂' : b ⟶ c
r₂' : c ⟶ b
adj₂' : l₂' ⊣ r₂'
φ : l₂' ⟶ l₂
this :
  Eq (α := (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
    ((mateEquiv (adj₁.comp adj₂) (adj₁.comp adj₂') :
          (a_1 : 𝟙 a ≫ l₁ ≫ l₂' ⟶ (l₁ ≫ l₂) ≫ 𝟙 c) → (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
        (Iso.inv (α_ (𝟙 a) l₁ l₂') ≫
          ((λ_ l₁).hom ≫ (ρ_ l₁).inv) ▷ l₂' ≫
            (α_ l₁ (𝟙 b) l₂').hom ≫ l₁ ◁ ((λ_ l₂').hom ≫ φ ≫ (ρ_ l₂).inv) ≫ (α_ l₁ l₂ (𝟙 c)).inv) :
      (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
    ((α_ r₂ r₁ (𝟙 a)).hom ≫
        r₂ ◁ (mateEquiv adj₁ adj₁ : (a_1 : 𝟙 a ≫ l₁ ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₁) ((λ_ l₁).hom ≫ (ρ_ l₁).inv) ≫
          (α_ r₂ (𝟙 b) r₁).inv ≫
            (mateEquiv adj₂ adj₂' : (a : 𝟙 b ≫ l₂' ⟶ l₂ ≫ 𝟙 c) → r₂ ≫ 𝟙 b ⟶ 𝟙 c ≫ r₂')
                  ((λ_ l₂').hom ≫ φ ≫ (ρ_ l₂).inv) ▷
                r₁ ≫
              Iso.hom (α_ (𝟙 c) r₂' r₁) :
      (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
⊢ Eq (α := (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
    ((mateEquiv (adj₁.comp adj₂) (adj₁.comp adj₂') :
          (a_1 : 𝟙 a ≫ l₁ ≫ l₂' ⟶ (l₁ ≫ l₂) ≫ 𝟙 c) → (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
        ((λ_ (l₁ ≫ l₂')).hom ≫ l₁ ◁ φ ≫ (ρ_ (l₁ ≫ l₂)).inv) :
      (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
    ((ρ_ (r₂ ≫ r₁)).hom ≫
        (ρ_ r₂).inv ▷ r₁ ≫
          (mateEquiv adj₂ adj₂' : (a : 𝟙 b ≫ l₂' ⟶ l₂ ≫ 𝟙 c) → r₂ ≫ 𝟙 b ⟶ 𝟙 c ≫ r₂') ((λ_ l₂').hom ≫ φ ≫ (ρ_ l₂).inv) ▷
              r₁ ≫
            Iso.hom (α_ (𝟙 c) r₂' r₁) :
      (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)

Tactic:
simp only [comp_whiskerRight, leftUnitor_whiskerRight, Category.assoc, whiskerLeft_comp,
    whiskerLeft_rightUnitor_inv, Iso.hom_inv_id, Category.comp_id, triangle_assoc,
    inv_hom_whiskerRight_assoc, Iso.inv_hom_id_assoc, mateEquiv_leftUnitor_hom_rightUnitor_inv,
    whiskerLeft_rightUnitor, triangle_assoc_comp_left_inv_assoc, Iso.hom_inv_id_assoc] at this

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Bicategory.inv_hom_whiskerRight_assoc, CategoryTheory.Bicategory.whiskerLeft_comp, CategoryTheory.Bicategory.comp_whiskerRight, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Bicategory.whiskerLeft_rightUnitor_inv, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Bicategory.leftUnitor_whiskerRight, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Bicategory.mateEquiv_leftUnitor_hom_rightUnitor_inv, CategoryTheory.Bicategory.whiskerLeft_rightUnitor, CategoryTheory.Bicategory.triangle_assoc, CategoryTheory.Bicategory.triangle_assoc_comp_left_inv_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
l₂' : b ⟶ c
r₂' : c ⟶ b
adj₂' : l₂' ⊣ r₂'
φ : l₂' ⟶ l₂
this :
  Eq (α := (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
    ((mateEquiv (adj₁.comp adj₂) (adj₁.comp adj₂') :
          (a_1 : 𝟙 a ≫ l₁ ≫ l₂' ⟶ (l₁ ≫ l₂) ≫ 𝟙 c) → (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
        ((λ_ (l₁ ≫ l₂')).hom ≫ l₁ ◁ φ ≫ (ρ_ (l₁ ≫ l₂)).inv) :
      (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
    ((ρ_ (r₂ ≫ r₁)).hom ≫
        (ρ_ r₂).inv ▷ r₁ ≫
          (mateEquiv adj₂ adj₂' : (a : 𝟙 b ≫ l₂' ⟶ l₂ ≫ 𝟙 c) → r₂ ≫ 𝟙 b ⟶ 𝟙 c ≫ r₂') ((λ_ l₂').hom ≫ φ ≫ (ρ_ l₂).inv) ▷
              r₁ ≫
            Iso.hom (α_ (𝟙 c) r₂' r₁) :
      (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂' ≫ r₁)
⊢ Eq (α := r₂ ≫ r₁ ⟶ r₂' ≫ r₁)
    ((conjugateEquiv (adj₁.comp adj₂) (adj₁.comp adj₂') : (a_1 : l₁ ≫ l₂' ⟶ l₁ ≫ l₂) → r₂ ≫ r₁ ⟶ r₂' ≫ r₁) (l₁ ◁ φ) :
      r₂ ≫ r₁ ⟶ r₂' ≫ r₁)
    ((conjugateEquiv adj₂ adj₂' : (a : l₂' ⟶ l₂) → r₂ ⟶ r₂') φ ▷ r₁ : r₂ ≫ r₁ ⟶ r₂' ≫ r₁)

Tactic:
simp [conjugateEquiv_apply, this]

Premises used: CategoryTheory.Bicategory.conjugateEquiv_apply
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₁' : a ⟶ b
r₁' : b ⟶ a
adj₁' : l₁' ⊣ r₁'
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
φ : l₁' ⟶ l₁
⊢ Eq (α := (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂ ≫ r₁')
    ((mateEquiv (adj₁.comp adj₂) (adj₁'.comp adj₂) :
          (a_1 : 𝟙 a ≫ l₁' ≫ l₂ ⟶ (l₁ ≫ l₂) ≫ 𝟙 c) → (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂ ≫ r₁')
        (leftAdjointSquare.hcomp ((λ_ l₁').hom ≫ φ ≫ (ρ_ l₁).inv) ((λ_ l₂).hom ≫ (ρ_ l₂).inv)) :
      (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂ ≫ r₁')
    (rightAdjointSquare.hcomp (h := 𝟙 b)
        ((mateEquiv adj₁ adj₁' : (a_1 : 𝟙 a ≫ l₁' ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₁') ((λ_ l₁').hom ≫ φ ≫ (ρ_ l₁).inv))
        ((mateEquiv adj₂ adj₂ : (a : 𝟙 b ≫ l₂ ⟶ l₂ ≫ 𝟙 c) → r₂ ≫ 𝟙 b ⟶ 𝟙 c ≫ r₂) ((λ_ l₂).hom ≫ (ρ_ l₂).inv)) :
      (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂ ≫ r₁')

Tactic:
have := mateEquiv_hcomp adj₁ adj₁' adj₂ adj₂
    ((λ_ _).hom ≫ φ ≫ (ρ_ _).inv) ((λ_ _).hom ≫ (ρ_ _).inv)
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₁' : a ⟶ b
r₁' : b ⟶ a
adj₁' : l₁' ⊣ r₁'
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
φ : l₁' ⟶ l₁
this :
  Eq (α := (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂ ≫ r₁')
    ((mateEquiv (adj₁.comp adj₂) (adj₁'.comp adj₂) :
          (a_1 : 𝟙 a ≫ l₁' ≫ l₂ ⟶ (l₁ ≫ l₂) ≫ 𝟙 c) → (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂ ≫ r₁')
        (Iso.inv (α_ (𝟙 a) l₁' l₂) ≫
          ((λ_ l₁').hom ≫ φ ≫ (ρ_ l₁).inv) ▷ l₂ ≫
            (α_ l₁ (𝟙 b) l₂).hom ≫ l₁ ◁ ((λ_ l₂).hom ≫ (ρ_ l₂).inv) ≫ (α_ l₁ l₂ (𝟙 c)).inv) :
      (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂ ≫ r₁')
    ((α_ r₂ r₁ (𝟙 a)).hom ≫
        r₂ ◁
            (mateEquiv adj₁ adj₁' : (a_1 : 𝟙 a ≫ l₁' ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₁')
              ((λ_ l₁').hom ≫ φ ≫ (ρ_ l₁).inv) ≫
          (α_ r₂ (𝟙 b) r₁').inv ≫
            (mateEquiv adj₂ adj₂ : (a : 𝟙 b ≫ l₂ ⟶ l₂ ≫ 𝟙 c) → r₂ ≫ 𝟙 b ⟶ 𝟙 c ≫ r₂) ((λ_ l₂).hom ≫ (ρ_ l₂).inv) ▷ r₁' ≫
              Iso.hom (α_ (𝟙 c) r₂ r₁') :
      (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂ ≫ r₁')
⊢ (mateEquiv (adj₁.comp adj₂) (adj₁'.comp adj₂) :
        (a_1 : 𝟙 a ≫ l₁' ≫ l₂ ⟶ (l₁ ≫ l₂) ≫ 𝟙 c) → (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂ ≫ r₁')
      ((λ_ (l₁' ≫ l₂)).hom ≫ φ ▷ l₂ ≫ (ρ_ (l₁ ≫ l₂)).inv) =
    (α_ r₂ r₁ (𝟙 a)).hom ≫
      r₂ ◁
          (mateEquiv adj₁ adj₁' : (a_1 : 𝟙 a ≫ l₁' ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₁')
            ((λ_ l₁').hom ≫ φ ≫ (ρ_ l₁).inv) ≫
        r₂ ◁ (λ_ r₁').hom ≫ (λ_ (r₂ ≫ r₁')).inv

Tactic:
simp only [comp_whiskerRight, leftUnitor_whiskerRight, Category.assoc, whiskerLeft_comp,
    whiskerLeft_rightUnitor_inv, Iso.hom_inv_id, Category.comp_id, triangle_assoc,
    inv_hom_whiskerRight_assoc, Iso.inv_hom_id_assoc, mateEquiv_leftUnitor_hom_rightUnitor_inv,
    leftUnitor_inv_whiskerRight, Iso.inv_hom_id, triangle_assoc_comp_right_assoc] at this

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Bicategory.inv_hom_whiskerRight_assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Bicategory.whiskerLeft_comp, CategoryTheory.Bicategory.comp_whiskerRight, CategoryTheory.Bicategory.leftUnitor_inv_whiskerRight, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Bicategory.whiskerLeft_rightUnitor_inv, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Bicategory.leftUnitor_whiskerRight, CategoryTheory.Bicategory.mateEquiv_leftUnitor_hom_rightUnitor_inv, CategoryTheory.Bicategory.triangle_assoc, CategoryTheory.Bicategory.triangle_assoc_comp_right_assoc
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₁' : a ⟶ b
r₁' : b ⟶ a
adj₁' : l₁' ⊣ r₁'
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
φ : l₁' ⟶ l₁
this :
  (mateEquiv (adj₁.comp adj₂) (adj₁'.comp adj₂) :
        (a_1 : 𝟙 a ≫ l₁' ≫ l₂ ⟶ (l₁ ≫ l₂) ≫ 𝟙 c) → (r₂ ≫ r₁) ≫ 𝟙 a ⟶ 𝟙 c ≫ r₂ ≫ r₁')
      ((λ_ (l₁' ≫ l₂)).hom ≫ φ ▷ l₂ ≫ (ρ_ (l₁ ≫ l₂)).inv) =
    (α_ r₂ r₁ (𝟙 a)).hom ≫
      r₂ ◁
          (mateEquiv adj₁ adj₁' : (a_1 : 𝟙 a ≫ l₁' ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₁')
            ((λ_ l₁').hom ≫ φ ≫ (ρ_ l₁).inv) ≫
        r₂ ◁ (λ_ r₁').hom ≫ (λ_ (r₂ ≫ r₁')).inv
⊢ Eq (α := r₂ ≫ r₁ ⟶ r₂ ≫ r₁')
    ((conjugateEquiv (adj₁.comp adj₂) (adj₁'.comp adj₂) : (a_1 : l₁' ≫ l₂ ⟶ l₁ ≫ l₂) → r₂ ≫ r₁ ⟶ r₂ ≫ r₁') (φ ▷ l₂) :
      r₂ ≫ r₁ ⟶ r₂ ≫ r₁')
    (r₂ ◁ (conjugateEquiv adj₁ adj₁' : (a_1 : l₁' ⟶ l₁) → r₁ ⟶ r₁') φ : r₂ ≫ r₁ ⟶ r₂ ≫ r₁')

Tactic:
simp [conjugateEquiv_apply, this]

Premises used: CategoryTheory.Bicategory.conjugateEquiv_apply
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₃ : l₃ ⊣ r₃
simp :
  (adj₁.unit ⊗≫
        l₁ ◁ (adj₂.unit ⊗≫ l₂ ◁ adj₃.unit ▷ r₂ ⊗≫ 𝟙 ((l₂ ≫ l₃) ≫ r₃ ≫ r₂)) ▷ r₁ ⊗≫
          𝟙 ((l₁ ≫ l₂ ≫ l₃) ≫ (r₃ ≫ r₂) ≫ r₁)) ≫
      (α_ l₁ (l₂ ≫ l₃) ((r₃ ≫ r₂) ≫ r₁)).hom ≫
        l₁ ◁ (α_ l₂ l₃ ((r₃ ≫ r₂) ≫ r₁)).hom ≫
          l₁ ◁ l₂ ◁ l₃ ◁ (α_ r₃ r₂ r₁).hom ≫
            l₁ ◁ l₂ ◁ l₃ ◁ (λ_ (r₃ ≫ r₂ ≫ r₁)).inv ≫
              l₁ ◁ (α_ l₂ l₃ (𝟙 d ≫ r₃ ≫ r₂ ≫ r₁)).inv ≫ (α_ l₁ (l₂ ≫ l₃) (𝟙 d ≫ r₃ ≫ r₂ ≫ r₁)).inv =
    ((adj₁.unit ⊗≫ l₁ ◁ adj₂.unit ▷ r₁ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ r₂ ≫ r₁)) ⊗≫
        ((α_ l₁ l₂ (𝟙 c ≫ r₂ ≫ r₁)).hom ≫
            l₁ ◁ l₂ ◁ Iso.inv (α_ (𝟙 c) r₂ r₁) ≫
              l₁ ◁ l₂ ◁ adj₃.unit ▷ r₂ ▷ r₁ ≫
                l₁ ◁ l₂ ◁ (α_ (l₃ ≫ r₃) r₂ r₁).hom ≫ (α_ l₁ l₂ ((l₃ ≫ r₃) ≫ r₂ ≫ r₁)).inv) ⊗≫
          𝟙 (((l₁ ≫ l₂) ≫ l₃) ≫ r₃ ≫ r₂ ≫ r₁)) ≫
      (λ_ (((l₁ ≫ l₂) ≫ l₃) ≫ r₃ ≫ r₂ ≫ r₁)).inv ≫
        Iso.inv (α_ (𝟙 a) ((l₁ ≫ l₂) ≫ l₃) (r₃ ≫ r₂ ≫ r₁)) ≫
          (α_ (𝟙 a ≫ (l₁ ≫ l₂) ≫ l₃) r₃ (r₂ ≫ r₁)).inv ≫
            (α_ ((𝟙 a ≫ (l₁ ≫ l₂) ≫ l₃) ≫ r₃) r₂ r₁).inv ≫
              Iso.hom (α_ (𝟙 a) ((l₁ ≫ l₂) ≫ l₃) r₃) ▷ r₂ ▷ r₁ ≫
                Iso.hom (α_ (𝟙 a) (((l₁ ≫ l₂) ≫ l₃) ≫ r₃) r₂) ▷ r₁ ≫
                  Iso.hom (α_ (𝟙 a) ((((l₁ ≫ l₂) ≫ l₃) ≫ r₃) ≫ r₂) r₁) ≫
                    (λ_ (((((l₁ ≫ l₂) ≫ l₃) ≫ r₃) ≫ r₂) ≫ r₁)).hom ≫
                      (α_ l₁ l₂ l₃).hom ▷ r₃ ▷ r₂ ▷ r₁ ≫
                        (ρ_ (l₁ ≫ l₂ ≫ l₃)).inv ▷ r₃ ▷ r₂ ▷ r₁ ≫
                          (α_ (((l₁ ≫ l₂ ≫ l₃) ≫ 𝟙 d) ≫ r₃) r₂ r₁).hom ≫
                            (α_ ((l₁ ≫ l₂ ≫ l₃) ≫ 𝟙 d) r₃ (r₂ ≫ r₁)).hom ≫ (α_ (l₁ ≫ l₂ ≫ l₃) (𝟙 d) (r₃ ≫ r₂ ≫ r₁)).hom
⊢ (conjugateEquiv (adj₁.comp (adj₂.comp adj₃)) ((adj₁.comp adj₂).comp adj₃) :
        (a_1 : (l₁ ≫ l₂) ≫ l₃ ⟶ l₁ ≫ l₂ ≫ l₃) → (r₃ ≫ r₂) ≫ r₁ ⟶ r₃ ≫ r₂ ≫ r₁)
      (α_ l₁ l₂ l₃).hom =
    (α_ r₃ r₂ r₁).hom

Tactic:
simp [← cancel_epi (ρ_ ((r₃ ≫ r₂) ≫ r₁)).hom, ← cancel_mono (λ_ (r₃ ≫ r₂ ≫ r₁)).inv,
    conjugateEquiv_apply, mateEquiv_eq_iff, Adjunction.homEquiv₁_symm_apply,
    Adjunction.homEquiv₂_apply]

Premises used: CategoryTheory.Bicategory.conjugateEquiv_apply, CategoryTheory.Bicategory.rightUnitor, CategoryTheory.Bicategory.Adjunction.homEquiv₂_apply, CategoryTheory.cancel_mono, CategoryTheory.Bicategory.leftUnitor, CategoryTheory.Bicategory.mateEquiv_eq_iff, CategoryTheory.CategoryStruct.comp, CategoryTheory.Bicategory.Adjunction.homEquiv₁_symm_apply, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
l₁ : a ⟶ b
r₁ : b ⟶ a
adj₁ : l₁ ⊣ r₁
l₂ : b ⟶ c
r₂ : c ⟶ b
adj₂ : l₂ ⊣ r₂
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₃ : l₃ ⊣ r₃
⊢ (adj₁.unit ⊗≫
        l₁ ◁ (adj₂.unit ⊗≫ l₂ ◁ adj₃.unit ▷ r₂ ⊗≫ 𝟙 ((l₂ ≫ l₃) ≫ r₃ ≫ r₂)) ▷ r₁ ⊗≫
          𝟙 ((l₁ ≫ l₂ ≫ l₃) ≫ (r₃ ≫ r₂) ≫ r₁)) ≫
      (α_ l₁ (l₂ ≫ l₃) ((r₃ ≫ r₂) ≫ r₁)).hom ≫
        l₁ ◁ (α_ l₂ l₃ ((r₃ ≫ r₂) ≫ r₁)).hom ≫
          l₁ ◁ l₂ ◁ l₃ ◁ (α_ r₃ r₂ r₁).hom ≫
            l₁ ◁ l₂ ◁ l₃ ◁ (λ_ (r₃ ≫ r₂ ≫ r₁)).inv ≫
              l₁ ◁ (α_ l₂ l₃ (𝟙 d ≫ r₃ ≫ r₂ ≫ r₁)).inv ≫ (α_ l₁ (l₂ ≫ l₃) (𝟙 d ≫ r₃ ≫ r₂ ≫ r₁)).inv =
    ((adj₁.unit ⊗≫ l₁ ◁ adj₂.unit ▷ r₁ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ r₂ ≫ r₁)) ⊗≫
        ((α_ l₁ l₂ (𝟙 c ≫ r₂ ≫ r₁)).hom ≫
            l₁ ◁ l₂ ◁ Iso.inv (α_ (𝟙 c) r₂ r₁) ≫
              l₁ ◁ l₂ ◁ adj₃.unit ▷ r₂ ▷ r₁ ≫
                l₁ ◁ l₂ ◁ (α_ (l₃ ≫ r₃) r₂ r₁).hom ≫ (α_ l₁ l₂ ((l₃ ≫ r₃) ≫ r₂ ≫ r₁)).inv) ⊗≫
          𝟙 (((l₁ ≫ l₂) ≫ l₃) ≫ r₃ ≫ r₂ ≫ r₁)) ≫
      (λ_ (((l₁ ≫ l₂) ≫ l₃) ≫ r₃ ≫ r₂ ≫ r₁)).inv ≫
        Iso.inv (α_ (𝟙 a) ((l₁ ≫ l₂) ≫ l₃) (r₃ ≫ r₂ ≫ r₁)) ≫
          (α_ (𝟙 a ≫ (l₁ ≫ l₂) ≫ l₃) r₃ (r₂ ≫ r₁)).inv ≫
            (α_ ((𝟙 a ≫ (l₁ ≫ l₂) ≫ l₃) ≫ r₃) r₂ r₁).inv ≫
              Iso.hom (α_ (𝟙 a) ((l₁ ≫ l₂) ≫ l₃) r₃) ▷ r₂ ▷ r₁ ≫
                Iso.hom (α_ (𝟙 a) (((l₁ ≫ l₂) ≫ l₃) ≫ r₃) r₂) ▷ r₁ ≫
                  Iso.hom (α_ (𝟙 a) ((((l₁ ≫ l₂) ≫ l₃) ≫ r₃) ≫ r₂) r₁) ≫
                    (λ_ (((((l₁ ≫ l₂) ≫ l₃) ≫ r₃) ≫ r₂) ≫ r₁)).hom ≫
                      (α_ l₁ l₂ l₃).hom ▷ r₃ ▷ r₂ ▷ r₁ ≫
                        (ρ_ (l₁ ≫ l₂ ≫ l₃)).inv ▷ r₃ ▷ r₂ ▷ r₁ ≫
                          (α_ (((l₁ ≫ l₂ ≫ l₃) ≫ 𝟙 d) ≫ r₃) r₂ r₁).hom ≫
                            (α_ ((l₁ ≫ l₂ ≫ l₃) ≫ 𝟙 d) r₃ (r₂ ≫ r₁)).hom ≫ (α_ (l₁ ≫ l₂ ≫ l₃) (𝟙 d) (r₃ ≫ r₂ ≫ r₁)).hom

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ l₂ l₃ : c ⟶ d
r₁ r₂ r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : l₃ ⟶ l₂
simp :
  Eq (α := r₁ ⟶ r₃)
    (((ρ_ r₁).inv ≫
        (mateEquiv adj₁ adj₂ : (a : 𝟙 c ≫ l₂ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ≫
          (λ_ r₂).hom) ≫
      (ρ_ r₂).inv ≫
        (mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫
          (λ_ r₃).hom)
    ((ρ_ r₁).inv ≫
      (mateEquiv adj₁ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ (β ≫ α) ≫ (ρ_ l₁).inv) ≫
        (λ_ r₃).hom)
⊢ Eq (α := r₁ ⟶ r₃)
    (CategoryStruct.comp (Y := r₂) ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α)
        ((conjugateEquiv adj₂ adj₃ : (a : l₃ ⟶ l₂) → r₂ ⟶ r₃) β) :
      r₁ ⟶ r₃)
    ((conjugateEquiv adj₁ adj₃ : (a : l₃ ⟶ l₁) → r₁ ⟶ r₃) (β ≫ α) : r₁ ⟶ r₃)

Tactic:
simp only [conjugateEquiv_apply]

Premises used: CategoryTheory.Bicategory.conjugateEquiv_apply
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ l₂ l₃ : c ⟶ d
r₁ r₂ r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : l₃ ⟶ l₂
dsimp :
  ((ρ_ r₁).inv ≫
        (mateEquiv adj₁ adj₂ : (a : 𝟙 c ≫ l₂ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ≫
          (λ_ r₂).hom) ≫
      (ρ_ r₂).inv ≫
        (mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫
          (λ_ r₃).hom =
    𝟙 r₁ ⊗≫
      bicategoricalComp (g := (𝟙 d ≫ 𝟙 d) ≫ r₃)
        ((α_ r₁ (𝟙 c) (𝟙 c)).inv ≫
          (mateEquiv adj₁ adj₂ : (a : 𝟙 c ≫ l₂ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ▷
              𝟙 c ≫
            Iso.hom (α_ (𝟙 d) r₂ (𝟙 c)) ≫
              𝟙 d ◁
                  (mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃)
                    ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫
                Iso.inv (α_ (𝟙 d) (𝟙 d) r₃))
        (𝟙 r₃)
⊢ ((ρ_ r₁).inv ≫
        (mateEquiv adj₁ adj₂ : (a : 𝟙 c ≫ l₂ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ≫
          (λ_ r₂).hom) ≫
      (ρ_ r₂).inv ≫
        (mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫
          (λ_ r₃).hom =
    bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 r₁)
      (bicategoricalComp (g := (𝟙 d ≫ 𝟙 d) ≫ r₃)
        (rightAdjointSquare.vcomp (r₂ := r₂)
          ((mateEquiv adj₁ adj₂ : (a : 𝟙 c ≫ l₂ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
          ((mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
        (𝟙 r₃))

Tactic:
dsimp only [rightAdjointSquare.vcomp]

Premises used: CategoryTheory.Bicategory.rightAdjointSquare.vcomp
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ l₂ l₃ : c ⟶ d
r₁ r₂ r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : l₃ ⟶ l₂
⊢ ((ρ_ r₁).inv ≫
        (mateEquiv adj₁ adj₂ : (a : 𝟙 c ≫ l₂ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ≫
          (λ_ r₂).hom) ≫
      (ρ_ r₂).inv ≫
        (mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫
          (λ_ r₃).hom =
    𝟙 r₁ ⊗≫
      bicategoricalComp (g := (𝟙 d ≫ 𝟙 d) ≫ r₃)
        ((α_ r₁ (𝟙 c) (𝟙 c)).inv ≫
          (mateEquiv adj₁ adj₂ : (a : 𝟙 c ≫ l₂ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ▷
              𝟙 c ≫
            Iso.hom (α_ (𝟙 d) r₂ (𝟙 c)) ≫
              𝟙 d ◁
                  (mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃)
                    ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫
                Iso.inv (α_ (𝟙 d) (𝟙 d) r₃))
        (𝟙 r₃)

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ l₂ l₃ : c ⟶ d
r₁ r₂ r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : l₃ ⟶ l₂
rw :
  bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 r₁)
      (bicategoricalComp (g := (𝟙 d ≫ 𝟙 d) ≫ r₃)
        ((mateEquiv adj₁ adj₃ : (a : (𝟙 c ≫ 𝟙 c) ≫ l₃ ⟶ l₁ ≫ 𝟙 d ≫ 𝟙 d) → r₁ ≫ 𝟙 c ≫ 𝟙 c ⟶ (𝟙 d ≫ 𝟙 d) ≫ r₃)
          (leftAdjointSquare.vcomp ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
        (𝟙 r₃)) =
    (ρ_ r₁).inv ≫
      (mateEquiv adj₁ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ (β ≫ α) ≫ (ρ_ l₁).inv) ≫
        (λ_ r₃).hom
⊢ bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 r₁)
      (bicategoricalComp (g := (𝟙 d ≫ 𝟙 d) ≫ r₃)
        (rightAdjointSquare.vcomp (r₂ := r₂)
          ((mateEquiv adj₁ adj₂ : (a : 𝟙 c ≫ l₂ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
          ((mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
        (𝟙 r₃)) =
    (ρ_ r₁).inv ≫
      (mateEquiv adj₁ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ (β ≫ α) ≫ (ρ_ l₁).inv) ≫
        (λ_ r₃).hom

Tactic:
rw [← mateEquiv_vcomp]

Premises used: CategoryTheory.Bicategory.mateEquiv_vcomp
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ l₂ l₃ : c ⟶ d
r₁ r₂ r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : l₃ ⟶ l₂
simp :
  𝟙 r₁ ⊗≫
      bicategoricalComp (h := r₁ ≫ (𝟙 c ≫ 𝟙 c) ≫ 𝟙 c) (𝟙 (r₁ ≫ 𝟙 c ≫ 𝟙 c))
          (bicategoricalComp (h := r₁ ≫ ((𝟙 c ≫ 𝟙 c) ≫ l₃) ≫ r₃) (r₁ ◁ (𝟙 c ≫ 𝟙 c) ◁ adj₃.unit)
            (r₁ ◁
                (Iso.hom (α_ (𝟙 c) (𝟙 c) l₃) ≫
                    𝟙 c ◁ ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫
                      Iso.inv (α_ (𝟙 c) l₂ (𝟙 d)) ≫ ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ▷ 𝟙 d ≫ (α_ l₁ (𝟙 d) (𝟙 d)).hom) ▷
                  r₃ ⊗≫
              adj₁.counit ▷ (𝟙 d ≫ 𝟙 d) ▷ r₃ ⊗≫ 𝟙 ((𝟙 d ≫ 𝟙 d) ≫ r₃))) ⊗≫
        𝟙 r₃ =
    (ρ_ r₁).inv ≫
      bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 (r₁ ≫ 𝟙 c))
          (r₁ ◁ 𝟙 c ◁ adj₃.unit ⊗≫
            r₁ ◁ ((λ_ l₃).hom ≫ (β ≫ α) ≫ (ρ_ l₁).inv) ▷ r₃ ⊗≫ adj₁.counit ▷ 𝟙 d ▷ r₃ ⊗≫ 𝟙 (𝟙 d ≫ r₃)) ≫
        (λ_ r₃).hom
⊢ bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 r₁)
      (bicategoricalComp (g := (𝟙 d ≫ 𝟙 d) ≫ r₃)
        ((mateEquiv adj₁ adj₃ : (a : (𝟙 c ≫ 𝟙 c) ≫ l₃ ⟶ l₁ ≫ 𝟙 d ≫ 𝟙 d) → r₁ ≫ 𝟙 c ≫ 𝟙 c ⟶ (𝟙 d ≫ 𝟙 d) ≫ r₃)
          (leftAdjointSquare.vcomp ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
        (𝟙 r₃)) =
    (ρ_ r₁).inv ≫
      (mateEquiv adj₁ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₁ ≫ 𝟙 d) → r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ (β ≫ α) ≫ (ρ_ l₁).inv) ≫
        (λ_ r₃).hom

Tactic:
simp only [leftAdjointSquare.vcomp, mateEquiv_apply']

Premises used: CategoryTheory.Bicategory.leftAdjointSquare.vcomp, CategoryTheory.Bicategory.mateEquiv_apply'