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 c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : b ⟶ c
r₂ : c ⟶ b
l₃ : d ⟶ e
r₃ : e ⟶ d
l₄ : e ⟶ f
r₄ : f ⟶ e
l₅ : x ⟶ y
r₅ : y ⟶ x
l₆ : y ⟶ z
r₆ : z ⟶ y
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
adj₅ : l₅ ⊣ r₅
adj₆ : l₆ ⊣ r₆
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
⊢ Eq (α := (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
    ((mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆) :
          (a_1 : (g₁ ≫ g₂) ≫ l₅ ≫ l₆ ⟶ (l₁ ≫ l₂) ≫ k₁ ≫ k₂) → (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
        (leftAdjointSquare.vcomp (leftAdjointSquare.hcomp α β) (leftAdjointSquare.hcomp γ δ)) :
      (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
    (rightAdjointSquare.vcomp (r₂ := r₄ ≫ r₃)
        ((mateEquiv (adj₁.comp adj₂) (adj₃.comp adj₄) :
            (a_1 : g₁ ≫ l₃ ≫ l₄ ⟶ (l₁ ≫ l₂) ≫ k₁) → (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
          (leftAdjointSquare.hcomp α β))
        ((mateEquiv (adj₃.comp adj₄) (adj₅.comp adj₆) :
            (a : g₂ ≫ l₅ ≫ l₆ ⟶ (l₃ ≫ l₄) ≫ k₂) → (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)
          (leftAdjointSquare.hcomp γ δ)) :
      (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)

Tactic:
have vcomp :=
    mateEquiv_vcomp (adj₁.comp adj₂) (adj₃.comp adj₄) (adj₅.comp adj₆)
      (leftAdjointSquare.hcomp α β) (leftAdjointSquare.hcomp γ δ)
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : b ⟶ c
r₂ : c ⟶ b
l₃ : d ⟶ e
r₃ : e ⟶ d
l₄ : e ⟶ f
r₄ : f ⟶ e
l₅ : x ⟶ y
r₅ : y ⟶ x
l₆ : y ⟶ z
r₆ : z ⟶ y
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
adj₅ : l₅ ⊣ r₅
adj₆ : l₆ ⊣ r₆
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
vcomp :
  Eq (α := (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
    ((mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆) :
          (a_1 : (g₁ ≫ g₂) ≫ l₅ ≫ l₆ ⟶ (l₁ ≫ l₂) ≫ k₁ ≫ k₂) → (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
        (leftAdjointSquare.vcomp (leftAdjointSquare.hcomp α β) (leftAdjointSquare.hcomp γ δ)) :
      (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
    (rightAdjointSquare.vcomp (r₂ := r₄ ≫ r₃)
        ((mateEquiv (adj₁.comp adj₂) (adj₃.comp adj₄) :
            (a_1 : g₁ ≫ l₃ ≫ l₄ ⟶ (l₁ ≫ l₂) ≫ k₁) → (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
          (leftAdjointSquare.hcomp α β))
        ((mateEquiv (adj₃.comp adj₄) (adj₅.comp adj₆) :
            (a : g₂ ≫ l₅ ≫ l₆ ⟶ (l₃ ≫ l₄) ≫ k₂) → (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)
          (leftAdjointSquare.hcomp γ δ)) :
      (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
⊢ Eq (α := (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
    ((mateEquiv (adj₁.comp adj₂) (adj₃.comp adj₄) :
          (a_1 : g₁ ≫ l₃ ≫ l₄ ⟶ (l₁ ≫ l₂) ≫ k₁) → (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
        (leftAdjointSquare.hcomp α β) :
      (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
    (rightAdjointSquare.hcomp (h := h₁) ((mateEquiv adj₁ adj₃ : (a_1 : g₁ ≫ l₃ ⟶ l₁ ≫ h₁) → r₁ ≫ g₁ ⟶ h₁ ≫ r₃) α)
        ((mateEquiv adj₂ adj₄ : (a : h₁ ≫ l₄ ⟶ l₂ ≫ k₁) → r₂ ≫ h₁ ⟶ k₁ ≫ r₄) β) :
      (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)

Tactic:
have hcomp1 := mateEquiv_hcomp adj₁ adj₃ adj₂ adj₄ α β
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : b ⟶ c
r₂ : c ⟶ b
l₃ : d ⟶ e
r₃ : e ⟶ d
l₄ : e ⟶ f
r₄ : f ⟶ e
l₅ : x ⟶ y
r₅ : y ⟶ x
l₆ : y ⟶ z
r₆ : z ⟶ y
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
adj₅ : l₅ ⊣ r₅
adj₆ : l₆ ⊣ r₆
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
vcomp :
  Eq (α := (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
    ((mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆) :
          (a_1 : (g₁ ≫ g₂) ≫ l₅ ≫ l₆ ⟶ (l₁ ≫ l₂) ≫ k₁ ≫ k₂) → (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
        (leftAdjointSquare.vcomp (leftAdjointSquare.hcomp α β) (leftAdjointSquare.hcomp γ δ)) :
      (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
    (rightAdjointSquare.vcomp (r₂ := r₄ ≫ r₃)
        ((mateEquiv (adj₁.comp adj₂) (adj₃.comp adj₄) :
            (a_1 : g₁ ≫ l₃ ≫ l₄ ⟶ (l₁ ≫ l₂) ≫ k₁) → (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
          (leftAdjointSquare.hcomp α β))
        ((mateEquiv (adj₃.comp adj₄) (adj₅.comp adj₆) :
            (a : g₂ ≫ l₅ ≫ l₆ ⟶ (l₃ ≫ l₄) ≫ k₂) → (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)
          (leftAdjointSquare.hcomp γ δ)) :
      (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
hcomp1 :
  Eq (α := (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
    ((mateEquiv (adj₁.comp adj₂) (adj₃.comp adj₄) :
          (a_1 : g₁ ≫ l₃ ≫ l₄ ⟶ (l₁ ≫ l₂) ≫ k₁) → (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
        (leftAdjointSquare.hcomp α β) :
      (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
    (rightAdjointSquare.hcomp (h := h₁) ((mateEquiv adj₁ adj₃ : (a_1 : g₁ ≫ l₃ ⟶ l₁ ≫ h₁) → r₁ ≫ g₁ ⟶ h₁ ≫ r₃) α)
        ((mateEquiv adj₂ adj₄ : (a : h₁ ≫ l₄ ⟶ l₂ ≫ k₁) → r₂ ≫ h₁ ⟶ k₁ ≫ r₄) β) :
      (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
⊢ Eq (α := (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)
    ((mateEquiv (adj₃.comp adj₄) (adj₅.comp adj₆) : (a : g₂ ≫ l₅ ≫ l₆ ⟶ (l₃ ≫ l₄) ≫ k₂) → (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)
        (leftAdjointSquare.hcomp γ δ) :
      (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)
    (rightAdjointSquare.hcomp (h := h₂) ((mateEquiv adj₃ adj₅ : (a : g₂ ≫ l₅ ⟶ l₃ ≫ h₂) → r₃ ≫ g₂ ⟶ h₂ ≫ r₅) γ)
        ((mateEquiv adj₄ adj₆ : (a : h₂ ≫ l₆ ⟶ l₄ ≫ k₂) → r₄ ≫ h₂ ⟶ k₂ ≫ r₆) δ) :
      (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)

Tactic:
have hcomp2 := mateEquiv_hcomp adj₃ adj₅ adj₄ adj₆ γ δ
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : b ⟶ c
r₂ : c ⟶ b
l₃ : d ⟶ e
r₃ : e ⟶ d
l₄ : e ⟶ f
r₄ : f ⟶ e
l₅ : x ⟶ y
r₅ : y ⟶ x
l₆ : y ⟶ z
r₆ : z ⟶ y
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
adj₅ : l₅ ⊣ r₅
adj₆ : l₆ ⊣ r₆
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
vcomp :
  Eq (α := (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
    ((mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆) :
          (a_1 : (g₁ ≫ g₂) ≫ l₅ ≫ l₆ ⟶ (l₁ ≫ l₂) ≫ k₁ ≫ k₂) → (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
        (leftAdjointSquare.vcomp (leftAdjointSquare.hcomp α β) (leftAdjointSquare.hcomp γ δ)) :
      (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
    (rightAdjointSquare.vcomp (r₂ := r₄ ≫ r₃)
        ((mateEquiv (adj₁.comp adj₂) (adj₃.comp adj₄) :
            (a_1 : g₁ ≫ l₃ ≫ l₄ ⟶ (l₁ ≫ l₂) ≫ k₁) → (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
          (leftAdjointSquare.hcomp α β))
        ((mateEquiv (adj₃.comp adj₄) (adj₅.comp adj₆) :
            (a : g₂ ≫ l₅ ≫ l₆ ⟶ (l₃ ≫ l₄) ≫ k₂) → (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)
          (leftAdjointSquare.hcomp γ δ)) :
      (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
hcomp1 :
  Eq (α := (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
    ((mateEquiv (adj₁.comp adj₂) (adj₃.comp adj₄) :
          (a_1 : g₁ ≫ l₃ ≫ l₄ ⟶ (l₁ ≫ l₂) ≫ k₁) → (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
        (leftAdjointSquare.hcomp α β) :
      (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
    (rightAdjointSquare.hcomp (h := h₁) ((mateEquiv adj₁ adj₃ : (a_1 : g₁ ≫ l₃ ⟶ l₁ ≫ h₁) → r₁ ≫ g₁ ⟶ h₁ ≫ r₃) α)
        ((mateEquiv adj₂ adj₄ : (a : h₁ ≫ l₄ ⟶ l₂ ≫ k₁) → r₂ ≫ h₁ ⟶ k₁ ≫ r₄) β) :
      (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
hcomp2 :
  Eq (α := (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)
    ((mateEquiv (adj₃.comp adj₄) (adj₅.comp adj₆) : (a : g₂ ≫ l₅ ≫ l₆ ⟶ (l₃ ≫ l₄) ≫ k₂) → (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)
        (leftAdjointSquare.hcomp γ δ) :
      (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)
    (rightAdjointSquare.hcomp (h := h₂) ((mateEquiv adj₃ adj₅ : (a : g₂ ≫ l₅ ⟶ l₃ ≫ h₂) → r₃ ≫ g₂ ⟶ h₂ ≫ r₅) γ)
        ((mateEquiv adj₄ adj₆ : (a : h₂ ≫ l₆ ⟶ l₄ ≫ k₂) → r₄ ≫ h₂ ⟶ k₂ ≫ r₆) δ) :
      (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)
⊢ Eq (α := (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
    ((mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆) :
          (a_1 : (g₁ ≫ g₂) ≫ l₅ ≫ l₆ ⟶ (l₁ ≫ l₂) ≫ k₁ ≫ k₂) → (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
        (leftAdjointSquare.vcomp (leftAdjointSquare.hcomp α β) (leftAdjointSquare.hcomp γ δ)) :
      (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
    (rightAdjointSquare.vcomp (r₂ := r₄ ≫ r₃)
        (rightAdjointSquare.hcomp (h := h₁) ((mateEquiv adj₁ adj₃ : (a_1 : g₁ ≫ l₃ ⟶ l₁ ≫ h₁) → r₁ ≫ g₁ ⟶ h₁ ≫ r₃) α)
          ((mateEquiv adj₂ adj₄ : (a : h₁ ≫ l₄ ⟶ l₂ ≫ k₁) → r₂ ≫ h₁ ⟶ k₁ ≫ r₄) β))
        (rightAdjointSquare.hcomp (h := h₂) ((mateEquiv adj₃ adj₅ : (a : g₂ ≫ l₅ ⟶ l₃ ≫ h₂) → r₃ ≫ g₂ ⟶ h₂ ≫ r₅) γ)
          ((mateEquiv adj₄ adj₆ : (a : h₂ ≫ l₆ ⟶ l₄ ≫ k₂) → r₄ ≫ h₂ ⟶ k₂ ≫ r₆) δ)) :
      (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)

Tactic:
rw [hcomp1, hcomp2] at vcomp
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d e f x y z : B
g₁ : a ⟶ d
h₁ : b ⟶ e
k₁ : c ⟶ f
g₂ : d ⟶ x
h₂ : e ⟶ y
k₂ : f ⟶ z
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : b ⟶ c
r₂ : c ⟶ b
l₃ : d ⟶ e
r₃ : e ⟶ d
l₄ : e ⟶ f
r₄ : f ⟶ e
l₅ : x ⟶ y
r₅ : y ⟶ x
l₆ : y ⟶ z
r₆ : z ⟶ y
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
adj₅ : l₅ ⊣ r₅
adj₆ : l₆ ⊣ r₆
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
vcomp :
  Eq (α := (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
    ((mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆) :
          (a_1 : (g₁ ≫ g₂) ≫ l₅ ≫ l₆ ⟶ (l₁ ≫ l₂) ≫ k₁ ≫ k₂) → (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
        (leftAdjointSquare.vcomp (leftAdjointSquare.hcomp α β) (leftAdjointSquare.hcomp γ δ)) :
      (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
    (rightAdjointSquare.vcomp (r₂ := r₄ ≫ r₃)
        (rightAdjointSquare.hcomp (h := h₁) ((mateEquiv adj₁ adj₃ : (a_1 : g₁ ≫ l₃ ⟶ l₁ ≫ h₁) → r₁ ≫ g₁ ⟶ h₁ ≫ r₃) α)
          ((mateEquiv adj₂ adj₄ : (a : h₁ ≫ l₄ ⟶ l₂ ≫ k₁) → r₂ ≫ h₁ ⟶ k₁ ≫ r₄) β))
        (rightAdjointSquare.hcomp (h := h₂) ((mateEquiv adj₃ adj₅ : (a : g₂ ≫ l₅ ⟶ l₃ ≫ h₂) → r₃ ≫ g₂ ⟶ h₂ ≫ r₅) γ)
          ((mateEquiv adj₄ adj₆ : (a : h₂ ≫ l₆ ⟶ l₄ ≫ k₂) → r₄ ≫ h₂ ⟶ k₂ ≫ r₆) δ)) :
      (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
hcomp1 :
  Eq (α := (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
    ((mateEquiv (adj₁.comp adj₂) (adj₃.comp adj₄) :
          (a_1 : g₁ ≫ l₃ ≫ l₄ ⟶ (l₁ ≫ l₂) ≫ k₁) → (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
        (leftAdjointSquare.hcomp α β) :
      (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
    (rightAdjointSquare.hcomp (h := h₁) ((mateEquiv adj₁ adj₃ : (a_1 : g₁ ≫ l₃ ⟶ l₁ ≫ h₁) → r₁ ≫ g₁ ⟶ h₁ ≫ r₃) α)
        ((mateEquiv adj₂ adj₄ : (a : h₁ ≫ l₄ ⟶ l₂ ≫ k₁) → r₂ ≫ h₁ ⟶ k₁ ≫ r₄) β) :
      (r₂ ≫ r₁) ≫ g₁ ⟶ k₁ ≫ r₄ ≫ r₃)
hcomp2 :
  Eq (α := (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)
    ((mateEquiv (adj₃.comp adj₄) (adj₅.comp adj₆) : (a : g₂ ≫ l₅ ≫ l₆ ⟶ (l₃ ≫ l₄) ≫ k₂) → (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)
        (leftAdjointSquare.hcomp γ δ) :
      (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)
    (rightAdjointSquare.hcomp (h := h₂) ((mateEquiv adj₃ adj₅ : (a : g₂ ≫ l₅ ⟶ l₃ ≫ h₂) → r₃ ≫ g₂ ⟶ h₂ ≫ r₅) γ)
        ((mateEquiv adj₄ adj₆ : (a : h₂ ≫ l₆ ⟶ l₄ ≫ k₂) → r₄ ≫ h₂ ⟶ k₂ ≫ r₆) δ) :
      (r₄ ≫ r₃) ≫ g₂ ⟶ k₂ ≫ r₆ ≫ r₅)
⊢ Eq (α := (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
    ((mateEquiv (adj₁.comp adj₂) (adj₅.comp adj₆) :
          (a_1 : (g₁ ≫ g₂) ≫ l₅ ≫ l₆ ⟶ (l₁ ≫ l₂) ≫ k₁ ≫ k₂) → (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
        (leftAdjointSquare.comp α β γ δ) :
      (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)
    (rightAdjointSquare.comp (e := e) (h₁ := h₁) (h₂ := h₂) (r₃ := r₃) (r₄ := r₄)
        ((mateEquiv adj₁ adj₃ : (a_1 : g₁ ≫ l₃ ⟶ l₁ ≫ h₁) → r₁ ≫ g₁ ⟶ h₁ ≫ r₃) α)
        ((mateEquiv adj₂ adj₄ : (a : h₁ ≫ l₄ ⟶ l₂ ≫ k₁) → r₂ ≫ h₁ ⟶ k₁ ≫ r₄) β)
        ((mateEquiv adj₃ adj₅ : (a : g₂ ≫ l₅ ⟶ l₃ ≫ h₂) → r₃ ≫ g₂ ⟶ h₂ ≫ r₅) γ)
        ((mateEquiv adj₄ adj₆ : (a : h₂ ≫ l₆ ⟶ l₄ ≫ k₂) → r₄ ≫ h₂ ⟶ k₂ ≫ r₆) δ) :
      (r₂ ≫ r₁) ≫ g₁ ≫ g₂ ⟶ (k₁ ≫ k₂) ≫ r₆ ≫ r₅)

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ⟶ l₁
rw :
  (ρ_ 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 =
    (ρ_ r₁).inv ≫ r₁ ◁ adj₂.unit ≫ r₁ ◁ α ▷ r₂ ≫ (α_ r₁ l₁ r₂).inv ≫ adj₁.counit ▷ r₂ ≫ (λ_ r₂).hom
⊢ (conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α =
    (ρ_ r₁).inv ≫ r₁ ◁ adj₂.unit ≫ r₁ ◁ α ▷ r₂ ≫ (α_ r₁ l₁ r₂).inv ≫ adj₁.counit ▷ r₂ ≫ (λ_ r₂).hom

Tactic:
rw [conjugateEquiv_apply, mateEquiv_apply']

Premises used: CategoryTheory.Bicategory.conjugateEquiv_apply, CategoryTheory.Bicategory.mateEquiv_apply'
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : l₂ ⟶ l₁
⊢ (ρ_ 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 =
    (ρ_ r₁).inv ≫ r₁ ◁ adj₂.unit ≫ r₁ ◁ α ▷ r₂ ≫ (α_ r₁ l₁ r₂).inv ≫ adj₁.counit ▷ 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₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : r₁ ⟶ r₂
⊢ Eq (α := l₂ ⟶ l₁) (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) α : l₂ ⟶ l₁)
    ((λ_ l₂).inv ≫
        (Equiv.symm (mateEquiv adj₁ adj₂) : (a : r₁ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₂) → 𝟙 c ≫ l₂ ⟶ l₁ ≫ 𝟙 d)
            ((ρ_ r₁).hom ≫ α ≫ (λ_ r₂).inv) ≫
          (ρ_ l₁).hom :
      l₂ ⟶ l₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : r₁ ⟶ r₂
rw :
  (λ_ l₂).inv ≫
      (𝟙 (𝟙 c ≫ l₂) ⊗≫
          adj₁.unit ▷ 𝟙 c ▷ l₂ ⊗≫
            bicategoricalComp (h := l₁ ≫ 𝟙 d ≫ r₂ ≫ l₂) (l₁ ◁ ((ρ_ r₁).hom ≫ α ≫ (λ_ r₂).inv) ▷ l₂)
              (l₁ ◁ 𝟙 d ◁ adj₂.counit ⊗≫ 𝟙 (l₁ ≫ 𝟙 d))) ≫
        (ρ_ l₁).hom =
    (λ_ l₂).inv ≫ adj₁.unit ▷ l₂ ≫ (α_ l₁ r₁ l₂).hom ≫ l₁ ◁ α ▷ l₂ ≫ l₁ ◁ adj₂.counit ≫ (ρ_ l₁).hom
⊢ ((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) α =
    (λ_ l₂).inv ≫ adj₁.unit ▷ l₂ ≫ (α_ l₁ r₁ l₂).hom ≫ l₁ ◁ α ▷ l₂ ≫ l₁ ◁ adj₂.counit ≫ (ρ_ l₁).hom

Tactic:
rw [conjugateEquiv_symm_apply, mateEquiv_symm_apply']

Premises used: CategoryTheory.Bicategory.mateEquiv_symm_apply', CategoryTheory.Bicategory.conjugateEquiv_symm_apply
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ l₂ : c ⟶ d
r₁ r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : r₁ ⟶ r₂
⊢ (λ_ l₂).inv ≫
      (𝟙 (𝟙 c ≫ l₂) ⊗≫
          adj₁.unit ▷ 𝟙 c ▷ l₂ ⊗≫
            bicategoricalComp (h := l₁ ≫ 𝟙 d ≫ r₂ ≫ l₂) (l₁ ◁ ((ρ_ r₁).hom ≫ α ≫ (λ_ r₂).inv) ▷ l₂)
              (l₁ ◁ 𝟙 d ◁ adj₂.counit ⊗≫ 𝟙 (l₁ ≫ 𝟙 d))) ≫
        (ρ_ l₁).hom =
    (λ_ l₂).inv ≫ adj₁.unit ▷ l₂ ≫ (α_ l₁ r₁ l₂).hom ≫ l₁ ◁ α ▷ l₂ ≫ l₁ ◁ adj₂.counit ≫ (ρ_ l₁).hom

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
rw :
  (ρ_ r₁).inv ≫
      bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 (r₁ ≫ 𝟙 c))
          (r₁ ◁ 𝟙 c ◁ adj₁.unit ⊗≫
            r₁ ◁ ((λ_ l₁).hom ≫ 𝟙 l₁ ≫ (ρ_ l₁).inv) ▷ r₁ ⊗≫ adj₁.counit ▷ 𝟙 d ▷ r₁ ⊗≫ 𝟙 (𝟙 d ≫ r₁)) ≫
        (λ_ r₁).hom =
    𝟙 r₁
⊢ Eq (α := r₁ ⟶ r₁) ((conjugateEquiv adj₁ adj₁ : (a : l₁ ⟶ l₁) → r₁ ⟶ r₁) (𝟙 l₁) : r₁ ⟶ r₁) (𝟙 r₁ : r₁ ⟶ r₁)

Tactic:
rw [conjugateEquiv_apply, mateEquiv_apply']

Premises used: CategoryTheory.Bicategory.conjugateEquiv_apply, CategoryTheory.Bicategory.mateEquiv_apply'
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
⊢ (ρ_ r₁).inv ≫
      bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 (r₁ ≫ 𝟙 c))
          (r₁ ◁ 𝟙 c ◁ adj₁.unit ⊗≫
            r₁ ◁ ((λ_ l₁).hom ≫ 𝟙 l₁ ≫ (ρ_ l₁).inv) ▷ r₁ ⊗≫ adj₁.counit ▷ 𝟙 d ▷ r₁ ⊗≫ 𝟙 (𝟙 d ≫ r₁)) ≫
        (λ_ r₁).hom =
    𝟙 r₁ ⊗≫ rightZigzag adj₁.unit adj₁.counit ⊗≫ 𝟙 r₁

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
rw : 𝟙 r₁ ⊗≫ ((ρ_ r₁).hom ≫ (λ_ r₁).inv) ⊗≫ 𝟙 r₁ = 𝟙 r₁
⊢ 𝟙 r₁ ⊗≫ rightZigzag adj₁.unit adj₁.counit ⊗≫ 𝟙 r₁ = 𝟙 r₁

Tactic:
rw [adj₁.right_triangle]

Premises used: CategoryTheory.Bicategory.Adjunction.right_triangle
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
⊢ 𝟙 r₁ ⊗≫ ((ρ_ r₁).hom ≫ (λ_ r₁).inv) ⊗≫ 𝟙 r₁ = 𝟙 r₁

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
_ :
  (ρ_ r₁).inv ≫
      bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 (r₁ ≫ 𝟙 c))
          (r₁ ◁ 𝟙 c ◁ adj₁.unit ⊗≫
            r₁ ◁ ((λ_ l₁).hom ≫ 𝟙 l₁ ≫ (ρ_ l₁).inv) ▷ r₁ ⊗≫ adj₁.counit ▷ 𝟙 d ▷ r₁ ⊗≫ 𝟙 (𝟙 d ≫ r₁)) ≫
        (λ_ r₁).hom =
    𝟙 r₁ ⊗≫ rightZigzag adj₁.unit adj₁.counit ⊗≫ 𝟙 r₁
_₁ : 𝟙 r₁ ⊗≫ rightZigzag adj₁.unit adj₁.counit ⊗≫ 𝟙 r₁ = 𝟙 r₁
⊢ (ρ_ r₁).inv ≫
      bicategoricalComp (h := r₁ ≫ 𝟙 c ≫ 𝟙 c) (𝟙 (r₁ ≫ 𝟙 c))
          (r₁ ◁ 𝟙 c ◁ adj₁.unit ⊗≫
            r₁ ◁ ((λ_ l₁).hom ≫ 𝟙 l₁ ≫ (ρ_ l₁).inv) ▷ r₁ ⊗≫ adj₁.counit ▷ 𝟙 d ▷ r₁ ⊗≫ 𝟙 (𝟙 d ≫ r₁)) ≫
        (λ_ r₁).hom =
    𝟙 r₁

Tactic:
calc
    _ = 𝟙 _ ⊗≫ rightZigzag adj₁.unit adj₁.counit ⊗≫ 𝟙 _ := by
      bicategory
    _ = 𝟙 r₁ := by
      rw [adj₁.right_triangle]
      bicategory

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Bicategory.rightZigzag, CategoryTheory.Bicategory.Adjunction.unit, CategoryTheory.Bicategory.Adjunction.counit
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c d : B
l₁ : c ⟶ d
r₁ : d ⟶ c
adj₁ : l₁ ⊣ r₁
rw : Eq.{w + 1} (α := r₁ ⟶ r₁) (𝟙 r₁) ((conjugateEquiv adj₁ adj₁ : (a : l₁ ⟶ l₁) → r₁ ⟶ r₁) (𝟙 l₁))
rw₁ rw₂ : 𝟙 r₁ = 𝟙 r₁
⊢ Eq (α := l₁ ⟶ l₁) (((conjugateEquiv adj₁ adj₁).symm : (a : r₁ ⟶ r₁) → l₁ ⟶ l₁) (𝟙 r₁) : l₁ ⟶ l₁) (𝟙 l₁ : l₁ ⟶ l₁)

Tactic:
rw [Equiv.symm_apply_eq, conjugateEquiv_id]

Premises used: Equiv.symm_apply_eq, CategoryTheory.Bicategory.conjugateEquiv_id
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : 𝟙 c ⟶ l
rw :
  (ρ_ r).inv ≫
      bicategoricalComp (h := r ≫ 𝟙 c ≫ 𝟙 c) (𝟙 (r ≫ 𝟙 c))
          (r ◁ 𝟙 c ◁ Adjunction.unit (Adjunction.id c) ⊗≫
            r ◁ (Iso.hom (λ_ (𝟙 c)) ≫ α ≫ (ρ_ l).inv) ▷ 𝟙 c ⊗≫ adj.counit ▷ 𝟙 c ▷ 𝟙 c ⊗≫ 𝟙 (𝟙 c ≫ 𝟙 c)) ≫
        Iso.hom (λ_ (𝟙 c)) =
    (ρ_ r).inv ≫ r ◁ α ≫ adj.counit
⊢ (conjugateEquiv adj (Adjunction.id c) : (a : 𝟙 c ⟶ l) → r ⟶ 𝟙 c) α = (ρ_ r).inv ≫ r ◁ α ≫ adj.counit

Tactic:
rw [conjugateEquiv_apply, mateEquiv_apply']

Premises used: CategoryTheory.Bicategory.conjugateEquiv_apply, CategoryTheory.Bicategory.mateEquiv_apply'
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : 𝟙 c ⟶ l
dsimp :
  (ρ_ r).inv ≫
      bicategoricalComp (h := r ≫ 𝟙 c ≫ 𝟙 c) (𝟙 (r ≫ 𝟙 c))
          (r ◁ 𝟙 c ◁ Iso.inv (ρ_ (𝟙 c)) ⊗≫
            r ◁ (Iso.hom (λ_ (𝟙 c)) ≫ α ≫ (ρ_ l).inv) ▷ 𝟙 c ⊗≫ adj.counit ▷ 𝟙 c ▷ 𝟙 c ⊗≫ 𝟙 (𝟙 c ≫ 𝟙 c)) ≫
        Iso.hom (λ_ (𝟙 c)) =
    (ρ_ r).inv ≫ r ◁ α ≫ adj.counit
⊢ (ρ_ r).inv ≫
      bicategoricalComp (h := r ≫ 𝟙 c ≫ 𝟙 c) (𝟙 (r ≫ 𝟙 c))
          (r ◁ 𝟙 c ◁ Adjunction.unit (Adjunction.id c) ⊗≫
            r ◁ (Iso.hom (λ_ (𝟙 c)) ≫ α ≫ (ρ_ l).inv) ▷ 𝟙 c ⊗≫ adj.counit ▷ 𝟙 c ▷ 𝟙 c ⊗≫ 𝟙 (𝟙 c ≫ 𝟙 c)) ≫
        Iso.hom (λ_ (𝟙 c)) =
    (ρ_ r).inv ≫ r ◁ α ≫ adj.counit

Tactic:
dsimp [Adjunction.id]

Premises used: CategoryTheory.Bicategory.Adjunction.id
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : 𝟙 c ⟶ l
⊢ (ρ_ r).inv ≫
      bicategoricalComp (h := r ≫ 𝟙 c ≫ 𝟙 c) (𝟙 (r ≫ 𝟙 c))
          (r ◁ 𝟙 c ◁ Iso.inv (ρ_ (𝟙 c)) ⊗≫
            r ◁ (Iso.hom (λ_ (𝟙 c)) ≫ α ≫ (ρ_ l).inv) ▷ 𝟙 c ⊗≫ adj.counit ▷ 𝟙 c ▷ 𝟙 c ⊗≫ 𝟙 (𝟙 c ≫ 𝟙 c)) ≫
        Iso.hom (λ_ (𝟙 c)) =
    (ρ_ r).inv ≫ r ◁ α ≫ adj.counit

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : r ⟶ 𝟙 c
rw :
  Iso.inv (λ_ (𝟙 c)) ≫
      (𝟙 (𝟙 c ≫ 𝟙 c) ⊗≫
          adj.unit ▷ 𝟙 c ▷ 𝟙 c ⊗≫
            bicategoricalComp (h := l ≫ 𝟙 c ≫ 𝟙 c ≫ 𝟙 c) (l ◁ ((ρ_ r).hom ≫ α ≫ Iso.inv (λ_ (𝟙 c))) ▷ 𝟙 c)
              (l ◁ 𝟙 c ◁ Adjunction.counit (Adjunction.id c) ⊗≫ 𝟙 (l ≫ 𝟙 c))) ≫
        (ρ_ l).hom =
    adj.unit ≫ l ◁ α ≫ (ρ_ l).hom
⊢ ((conjugateEquiv adj (Adjunction.id c)).symm : (a : r ⟶ 𝟙 c) → 𝟙 c ⟶ l) α = adj.unit ≫ l ◁ α ≫ (ρ_ l).hom

Tactic:
rw [conjugateEquiv_symm_apply, mateEquiv_symm_apply']

Premises used: CategoryTheory.Bicategory.mateEquiv_symm_apply', CategoryTheory.Bicategory.conjugateEquiv_symm_apply
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : r ⟶ 𝟙 c
dsimp :
  Iso.inv (λ_ (𝟙 c)) ≫
      (𝟙 (𝟙 c ≫ 𝟙 c) ⊗≫
          adj.unit ▷ 𝟙 c ▷ 𝟙 c ⊗≫
            bicategoricalComp (h := l ≫ 𝟙 c ≫ 𝟙 c ≫ 𝟙 c) (l ◁ ((ρ_ r).hom ≫ α ≫ Iso.inv (λ_ (𝟙 c))) ▷ 𝟙 c)
              (l ◁ 𝟙 c ◁ Iso.hom (ρ_ (𝟙 c)) ⊗≫ 𝟙 (l ≫ 𝟙 c))) ≫
        (ρ_ l).hom =
    adj.unit ≫ l ◁ α ≫ (ρ_ l).hom
⊢ Iso.inv (λ_ (𝟙 c)) ≫
      (𝟙 (𝟙 c ≫ 𝟙 c) ⊗≫
          adj.unit ▷ 𝟙 c ▷ 𝟙 c ⊗≫
            bicategoricalComp (h := l ≫ 𝟙 c ≫ 𝟙 c ≫ 𝟙 c) (l ◁ ((ρ_ r).hom ≫ α ≫ Iso.inv (λ_ (𝟙 c))) ▷ 𝟙 c)
              (l ◁ 𝟙 c ◁ Adjunction.counit (Adjunction.id c) ⊗≫ 𝟙 (l ≫ 𝟙 c))) ≫
        (ρ_ l).hom =
    adj.unit ≫ l ◁ α ≫ (ρ_ l).hom

Tactic:
dsimp [Adjunction.id]

Premises used: CategoryTheory.Bicategory.Adjunction.id
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
c : B
l r : c ⟶ c
adj : l ⊣ r
α : r ⟶ 𝟙 c
⊢ Iso.inv (λ_ (𝟙 c)) ≫
      (𝟙 (𝟙 c ≫ 𝟙 c) ⊗≫
          adj.unit ▷ 𝟙 c ▷ 𝟙 c ⊗≫
            bicategoricalComp (h := l ≫ 𝟙 c ≫ 𝟙 c ≫ 𝟙 c) (l ◁ ((ρ_ r).hom ≫ α ≫ Iso.inv (λ_ (𝟙 c))) ▷ 𝟙 c)
              (l ◁ 𝟙 c ◁ Iso.hom (ρ_ (𝟙 c)) ⊗≫ 𝟙 (l ≫ 𝟙 c))) ≫
        (ρ_ l).hom =
    adj.unit ≫ l ◁ α ≫ (ρ_ l).hom

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
⊢ (mateEquiv adj adj : (a_1 : 𝟙 a ≫ l ⟶ l ≫ 𝟙 b) → r ≫ 𝟙 a ⟶ 𝟙 b ≫ r) ((λ_ l).hom ≫ (ρ_ l).inv) =
    (ρ_ r).hom ≫ (λ_ r).inv

Tactic:
simp [← cancel_mono (λ_ r).hom,
    ← conjugateEquiv_id adj, conjugateEquiv_apply]

Premises used: CategoryTheory.Bicategory.conjugateEquiv_apply, CategoryTheory.cancel_mono, CategoryTheory.Bicategory.leftUnitor, CategoryTheory.Bicategory.conjugateEquiv_id, CategoryTheory.Iso.hom