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 : B
g₁ : a ⟶ c
g₂ : c ⟶ e
h₁ : b ⟶ d
h₂ : d ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : e ⟶ f
r₃ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g₁ ≫ l₂ ⟶ l₁ ≫ h₁
β : g₂ ≫ l₃ ⟶ l₂ ≫ h₂
rw :
  𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ β ▷ r₃ ⊗≫
          (r₁ ≫ g₁) ◁ ((λ_ l₂).hom ≫ (ρ_ l₂).inv) ▷ (h₂ ≫ r₃) ⊗≫
            r₁ ◁ α ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ (g₁ ≫ g₂) ◁ adj₃.unit ⊗≫
        r₁ ◁ ((α_ g₁ g₂ l₃).hom ≫ g₁ ◁ β ≫ (α_ g₁ l₂ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ r₃ ⊗≫
          adj₁.counit ▷ (h₁ ≫ h₂) ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ β ▷ r₃ ⊗≫
          (r₁ ≫ g₁) ◁ leftZigzag adj₂.unit adj₂.counit ▷ (h₂ ≫ r₃) ⊗≫
            r₁ ◁ α ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ (g₁ ≫ g₂) ◁ adj₃.unit ⊗≫
        r₁ ◁ ((α_ g₁ g₂ l₃).hom ≫ g₁ ◁ β ≫ (α_ g₁ l₂ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ r₃ ⊗≫
          adj₁.counit ▷ (h₁ ≫ h₂) ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)

Tactic:
rw [adj₂.left_triangle]

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

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d e f : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
simp :
  𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      (r₃ ≫ r₁) ◁ g ◁ (adj₂.comp adj₄).unit ⊗≫
        (r₃ ≫ r₁) ◁ leftAdjointSquare.hcomp α β ▷ (r₄ ≫ r₂) ⊗≫
          (adj₁.comp adj₃).counit ▷ k ▷ (r₄ ≫ r₂) ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    rightAdjointSquare.hcomp (𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂))
      (𝟙 (r₃ ≫ h) ⊗≫ r₃ ◁ h ◁ adj₄.unit ⊗≫ r₃ ◁ β ▷ r₄ ⊗≫ adj₃.counit ▷ k ▷ r₄ ⊗≫ 𝟙 (k ≫ 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:
simp only [mateEquiv_apply']

Premises used: CategoryTheory.Bicategory.mateEquiv_apply'
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d e f : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
dsimp :
  𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      (r₃ ≫ r₁) ◁ g ◁ (adj₂.unit ⊗≫ l₂ ◁ adj₄.unit ▷ r₂ ⊗≫ 𝟙 ((l₂ ≫ l₄) ≫ r₄ ≫ r₂)) ⊗≫
        (r₃ ≫ r₁) ◁ ((α_ g l₂ l₄).inv ≫ α ▷ l₄ ≫ (α_ l₁ h l₄).hom ≫ l₁ ◁ β ≫ (α_ l₁ l₃ k).inv) ▷ (r₄ ≫ r₂) ⊗≫
          (𝟙 ((r₃ ≫ r₁) ≫ l₁ ≫ l₃) ⊗≫ r₃ ◁ adj₁.counit ▷ l₃ ⊗≫ adj₃.counit) ▷ k ▷ (r₄ ≫ r₂) ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    (α_ r₃ r₁ g).hom ≫
      r₃ ◁ (𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂)) ≫
        (α_ r₃ h r₂).inv ≫
          (𝟙 (r₃ ≫ h) ⊗≫ r₃ ◁ h ◁ adj₄.unit ⊗≫ r₃ ◁ β ▷ r₄ ⊗≫ adj₃.counit ▷ k ▷ r₄ ⊗≫ 𝟙 (k ≫ r₄)) ▷ r₂ ≫
            (α_ k r₄ r₂).hom
⊢ 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      (r₃ ≫ r₁) ◁ g ◁ (adj₂.comp adj₄).unit ⊗≫
        (r₃ ≫ r₁) ◁ leftAdjointSquare.hcomp α β ▷ (r₄ ≫ r₂) ⊗≫
          (adj₁.comp adj₃).counit ▷ k ▷ (r₄ ≫ r₂) ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    rightAdjointSquare.hcomp (𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂))
      (𝟙 (r₃ ≫ h) ⊗≫ r₃ ◁ h ◁ adj₄.unit ⊗≫ r₃ ◁ β ▷ r₄ ⊗≫ adj₃.counit ▷ k ▷ r₄ ⊗≫ 𝟙 (k ≫ r₄))

Tactic:
dsimp [leftAdjointSquare.hcomp, rightAdjointSquare.hcomp]

Premises used: CategoryTheory.Bicategory.rightAdjointSquare.hcomp, CategoryTheory.Bicategory.leftAdjointSquare.hcomp
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d e f : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
⊢ 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      (r₃ ≫ r₁) ◁ g ◁ (adj₂.unit ⊗≫ l₂ ◁ adj₄.unit ▷ r₂ ⊗≫ 𝟙 ((l₂ ≫ l₄) ≫ r₄ ≫ r₂)) ⊗≫
        (r₃ ≫ r₁) ◁ ((α_ g l₂ l₄).inv ≫ α ▷ l₄ ≫ (α_ l₁ h l₄).hom ≫ l₁ ◁ β ≫ (α_ l₁ l₃ k).inv) ▷ (r₄ ≫ r₂) ⊗≫
          (𝟙 ((r₃ ≫ r₁) ≫ l₁ ≫ l₃) ⊗≫ r₃ ◁ adj₁.counit ▷ l₃ ⊗≫ adj₃.counit) ▷ k ▷ (r₄ ≫ r₂) ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ ((g ≫ l₂) ◁ adj₄.unit ≫ α ▷ (l₄ ≫ r₄)) ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ β ≫ adj₁.counit ▷ (l₃ ≫ k)) ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂)

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d e f : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
rw :
  𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ (α ▷ 𝟙 e ≫ (l₁ ≫ h) ◁ adj₄.unit) ▷ r₂ ⊗≫
          r₃ ◁ (adj₁.counit ▷ (h ≫ l₄) ≫ 𝟙 b ◁ β) ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ h ◁ adj₄.unit ≫ adj₁.counit ▷ (h ≫ l₄ ≫ r₄)) ▷ r₂ ⊗≫
            r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂)
⊢ 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ ((g ≫ l₂) ◁ adj₄.unit ≫ α ▷ (l₄ ≫ r₄)) ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ β ≫ adj₁.counit ▷ (l₃ ≫ k)) ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ h ◁ adj₄.unit ≫ adj₁.counit ▷ (h ≫ l₄ ≫ r₄)) ▷ r₂ ⊗≫
            r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂)

Tactic:
rw [whisker_exchange, whisker_exchange]

Premises used: CategoryTheory.Bicategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d e f : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
⊢ 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ (α ▷ 𝟙 e ≫ (l₁ ≫ h) ◁ adj₄.unit) ▷ r₂ ⊗≫
          r₃ ◁ (adj₁.counit ▷ (h ≫ l₄) ≫ 𝟙 b ◁ β) ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ h ◁ adj₄.unit ≫ adj₁.counit ▷ (h ≫ l₄ ≫ r₄)) ▷ r₂ ⊗≫
            r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂)

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d e f : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
rw :
  𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
          r₃ ◁ (adj₁.counit ▷ (h ≫ 𝟙 e) ≫ 𝟙 b ◁ h ◁ adj₄.unit) ▷ r₂ ⊗≫
            r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    (α_ r₃ r₁ g).hom ≫
      r₃ ◁ (𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂)) ≫
        (α_ r₃ h r₂).inv ≫
          (𝟙 (r₃ ≫ h) ⊗≫ r₃ ◁ h ◁ adj₄.unit ⊗≫ r₃ ◁ β ▷ r₄ ⊗≫ adj₃.counit ▷ k ▷ r₄ ⊗≫ 𝟙 (k ≫ r₄)) ▷ r₂ ≫
            (α_ k r₄ r₂).hom
⊢ 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
          r₃ ◁ ((r₁ ≫ l₁) ◁ h ◁ adj₄.unit ≫ adj₁.counit ▷ (h ≫ l₄ ≫ r₄)) ▷ r₂ ⊗≫
            r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    (α_ r₃ r₁ g).hom ≫
      r₃ ◁ (𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂)) ≫
        (α_ r₃ h r₂).inv ≫
          (𝟙 (r₃ ≫ h) ⊗≫ r₃ ◁ h ◁ adj₄.unit ⊗≫ r₃ ◁ β ▷ r₄ ⊗≫ adj₃.counit ▷ k ▷ r₄ ⊗≫ 𝟙 (k ≫ r₄)) ▷ r₂ ≫
            (α_ k r₄ r₂).hom

Tactic:
rw [whisker_exchange]

Premises used: CategoryTheory.Bicategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d e f : B
g : a ⟶ d
h : b ⟶ e
k : c ⟶ f
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : d ⟶ e
r₂ : e ⟶ d
l₃ : b ⟶ c
r₃ : c ⟶ b
l₄ : e ⟶ f
r₄ : f ⟶ e
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
adj₄ : l₄ ⊣ r₄
α : g ≫ l₂ ⟶ l₁ ≫ h
β : h ≫ l₄ ⟶ l₃ ≫ k
⊢ 𝟙 ((r₃ ≫ r₁) ≫ g) ⊗≫
      r₃ ◁ r₁ ◁ g ◁ adj₂.unit ⊗≫
        r₃ ◁ r₁ ◁ α ▷ r₂ ⊗≫
          r₃ ◁ (adj₁.counit ▷ (h ≫ 𝟙 e) ≫ 𝟙 b ◁ h ◁ adj₄.unit) ▷ r₂ ⊗≫
            r₃ ◁ β ▷ r₄ ▷ r₂ ⊗≫ adj₃.counit ▷ k ▷ r₄ ▷ r₂ ⊗≫ 𝟙 (k ≫ r₄ ≫ r₂) =
    (α_ r₃ r₁ g).hom ≫
      r₃ ◁ (𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂)) ≫
        (α_ r₃ h r₂).inv ≫
          (𝟙 (r₃ ≫ h) ⊗≫ r₃ ◁ h ◁ adj₄.unit ⊗≫ r₃ ◁ β ▷ r₄ ⊗≫ adj₃.counit ▷ k ▷ r₄ ⊗≫ 𝟙 (k ≫ r₄)) ▷ r₂ ≫
            (α_ k r₄ r₂).hom

Tactic:
bicategory
-- 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
l₂ : b ⟶ c
l₃ : d ⟶ e
l₄ : e ⟶ f
l₅ : x ⟶ y
l₆ : y ⟶ z
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
⊢ comp α β γ δ = vcomp (hcomp α β) (hcomp γ δ)

Tactic:
rfl

Premises used: rfl, CategoryTheory.Bicategory.leftAdjointSquare.comp
-- 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
l₂ : b ⟶ c
l₃ : d ⟶ e
l₄ : e ⟶ f
l₅ : x ⟶ y
l₆ : y ⟶ z
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
dsimp :
  (α_ g₁ g₂ (l₅ ≫ l₆)).hom ≫
      g₁ ◁ ((α_ g₂ l₅ l₆).inv ≫ γ ▷ l₆ ≫ (α_ l₃ h₂ l₆).hom ≫ l₃ ◁ δ ≫ (α_ l₃ l₄ k₂).inv) ≫
        (α_ g₁ (l₃ ≫ l₄) k₂).inv ≫
          ((α_ g₁ l₃ l₄).inv ≫ α ▷ l₄ ≫ (α_ l₁ h₁ l₄).hom ≫ l₁ ◁ β ≫ (α_ l₁ l₂ k₁).inv) ▷ k₂ ≫
            (α_ (l₁ ≫ l₂) k₁ k₂).hom =
    (α_ (g₁ ≫ g₂) l₅ l₆).inv ≫
      ((α_ g₁ g₂ l₅).hom ≫ g₁ ◁ γ ≫ (α_ g₁ l₃ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ l₆ ≫
        (α_ l₁ (h₁ ≫ h₂) l₆).hom ≫
          l₁ ◁ ((α_ h₁ h₂ l₆).hom ≫ h₁ ◁ δ ≫ (α_ h₁ l₄ k₂).inv ≫ β ▷ k₂ ≫ (α_ l₂ k₁ k₂).hom) ≫ (α_ l₁ l₂ (k₁ ≫ k₂)).inv
⊢ comp α β γ δ = hcomp (vcomp α γ) (vcomp β δ)

Tactic:
dsimp only [comp, vcomp, hcomp]

Premises used: CategoryTheory.Bicategory.leftAdjointSquare.hcomp, CategoryTheory.Bicategory.leftAdjointSquare.vcomp, CategoryTheory.Bicategory.leftAdjointSquare.comp
-- 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
l₂ : b ⟶ c
l₃ : d ⟶ e
l₄ : e ⟶ f
l₅ : x ⟶ y
l₆ : y ⟶ z
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
⊢ (α_ g₁ g₂ (l₅ ≫ l₆)).hom ≫
      g₁ ◁ ((α_ g₂ l₅ l₆).inv ≫ γ ▷ l₆ ≫ (α_ l₃ h₂ l₆).hom ≫ l₃ ◁ δ ≫ (α_ l₃ l₄ k₂).inv) ≫
        (α_ g₁ (l₃ ≫ l₄) k₂).inv ≫
          ((α_ g₁ l₃ l₄).inv ≫ α ▷ l₄ ≫ (α_ l₁ h₁ l₄).hom ≫ l₁ ◁ β ≫ (α_ l₁ l₂ k₁).inv) ▷ k₂ ≫
            (α_ (l₁ ≫ l₂) k₁ k₂).hom =
    𝟙 ((g₁ ≫ g₂) ≫ l₅ ≫ l₆) ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ ((g₁ ≫ l₃) ◁ δ ≫ α ▷ (l₄ ≫ k₂)) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ k₁ ≫ k₂)

Tactic:
bicategory
-- 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
l₂ : b ⟶ c
l₃ : d ⟶ e
l₄ : e ⟶ f
l₅ : x ⟶ y
l₆ : y ⟶ z
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
rw :
  𝟙 ((g₁ ≫ g₂) ≫ l₅ ≫ l₆) ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ (α ▷ (h₂ ≫ l₆) ≫ (l₁ ≫ h₁) ◁ δ) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ k₁ ≫ k₂) =
    (α_ (g₁ ≫ g₂) l₅ l₆).inv ≫
      ((α_ g₁ g₂ l₅).hom ≫ g₁ ◁ γ ≫ (α_ g₁ l₃ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ l₆ ≫
        (α_ l₁ (h₁ ≫ h₂) l₆).hom ≫
          l₁ ◁ ((α_ h₁ h₂ l₆).hom ≫ h₁ ◁ δ ≫ (α_ h₁ l₄ k₂).inv ≫ β ▷ k₂ ≫ (α_ l₂ k₁ k₂).hom) ≫ (α_ l₁ l₂ (k₁ ≫ k₂)).inv
⊢ 𝟙 ((g₁ ≫ g₂) ≫ l₅ ≫ l₆) ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ ((g₁ ≫ l₃) ◁ δ ≫ α ▷ (l₄ ≫ k₂)) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ k₁ ≫ k₂) =
    (α_ (g₁ ≫ g₂) l₅ l₆).inv ≫
      ((α_ g₁ g₂ l₅).hom ≫ g₁ ◁ γ ≫ (α_ g₁ l₃ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ l₆ ≫
        (α_ l₁ (h₁ ≫ h₂) l₆).hom ≫
          l₁ ◁ ((α_ h₁ h₂ l₆).hom ≫ h₁ ◁ δ ≫ (α_ h₁ l₄ k₂).inv ≫ β ▷ k₂ ≫ (α_ l₂ k₁ k₂).hom) ≫ (α_ l₁ l₂ (k₁ ≫ k₂)).inv

Tactic:
rw [whisker_exchange]

Premises used: CategoryTheory.Bicategory.whisker_exchange
-- 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
l₂ : b ⟶ c
l₃ : d ⟶ e
l₄ : e ⟶ f
l₅ : x ⟶ y
l₆ : y ⟶ z
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
⊢ 𝟙 ((g₁ ≫ g₂) ≫ l₅ ≫ l₆) ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ (α ▷ (h₂ ≫ l₆) ≫ (l₁ ≫ h₁) ◁ δ) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ k₁ ≫ k₂) =
    (α_ (g₁ ≫ g₂) l₅ l₆).inv ≫
      ((α_ g₁ g₂ l₅).hom ≫ g₁ ◁ γ ≫ (α_ g₁ l₃ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ l₆ ≫
        (α_ l₁ (h₁ ≫ h₂) l₆).hom ≫
          l₁ ◁ ((α_ h₁ h₂ l₆).hom ≫ h₁ ◁ δ ≫ (α_ h₁ l₄ k₂).inv ≫ β ▷ k₂ ≫ (α_ l₂ k₁ k₂).hom) ≫ (α_ l₁ l₂ (k₁ ≫ k₂)).inv

Tactic:
bicategory
-- 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
l₂ : b ⟶ c
l₃ : d ⟶ e
l₄ : e ⟶ f
l₅ : x ⟶ y
l₆ : y ⟶ z
α : g₁ ≫ l₃ ⟶ l₁ ≫ h₁
β : h₁ ≫ l₄ ⟶ l₂ ≫ k₁
γ : g₂ ≫ l₅ ⟶ l₃ ≫ h₂
δ : h₂ ≫ l₆ ⟶ l₄ ≫ k₂
_ :
  (α_ g₁ g₂ (l₅ ≫ l₆)).hom ≫
      g₁ ◁ ((α_ g₂ l₅ l₆).inv ≫ γ ▷ l₆ ≫ (α_ l₃ h₂ l₆).hom ≫ l₃ ◁ δ ≫ (α_ l₃ l₄ k₂).inv) ≫
        (α_ g₁ (l₃ ≫ l₄) k₂).inv ≫
          ((α_ g₁ l₃ l₄).inv ≫ α ▷ l₄ ≫ (α_ l₁ h₁ l₄).hom ≫ l₁ ◁ β ≫ (α_ l₁ l₂ k₁).inv) ▷ k₂ ≫
            (α_ (l₁ ≫ l₂) k₁ k₂).hom =
    𝟙 ((g₁ ≫ g₂) ≫ l₅ ≫ l₆) ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ ((g₁ ≫ l₃) ◁ δ ≫ α ▷ (l₄ ≫ k₂)) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ k₁ ≫ k₂)
_₁ :
  𝟙 ((g₁ ≫ g₂) ≫ l₅ ≫ l₆) ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ ((g₁ ≫ l₃) ◁ δ ≫ α ▷ (l₄ ≫ k₂)) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 ((l₁ ≫ l₂) ≫ k₁ ≫ k₂) =
    (α_ (g₁ ≫ g₂) l₅ l₆).inv ≫
      ((α_ g₁ g₂ l₅).hom ≫ g₁ ◁ γ ≫ (α_ g₁ l₃ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ l₆ ≫
        (α_ l₁ (h₁ ≫ h₂) l₆).hom ≫
          l₁ ◁ ((α_ h₁ h₂ l₆).hom ≫ h₁ ◁ δ ≫ (α_ h₁ l₄ k₂).inv ≫ β ▷ k₂ ≫ (α_ l₂ k₁ k₂).hom) ≫ (α_ l₁ l₂ (k₁ ≫ k₂)).inv
⊢ (α_ g₁ g₂ (l₅ ≫ l₆)).hom ≫
      g₁ ◁ ((α_ g₂ l₅ l₆).inv ≫ γ ▷ l₆ ≫ (α_ l₃ h₂ l₆).hom ≫ l₃ ◁ δ ≫ (α_ l₃ l₄ k₂).inv) ≫
        (α_ g₁ (l₃ ≫ l₄) k₂).inv ≫
          ((α_ g₁ l₃ l₄).inv ≫ α ▷ l₄ ≫ (α_ l₁ h₁ l₄).hom ≫ l₁ ◁ β ≫ (α_ l₁ l₂ k₁).inv) ▷ k₂ ≫
            (α_ (l₁ ≫ l₂) k₁ k₂).hom =
    (α_ (g₁ ≫ g₂) l₅ l₆).inv ≫
      ((α_ g₁ g₂ l₅).hom ≫ g₁ ◁ γ ≫ (α_ g₁ l₃ h₂).inv ≫ α ▷ h₂ ≫ (α_ l₁ h₁ h₂).hom) ▷ l₆ ≫
        (α_ l₁ (h₁ ≫ h₂) l₆).hom ≫
          l₁ ◁ ((α_ h₁ h₂ l₆).hom ≫ h₁ ◁ δ ≫ (α_ h₁ l₄ k₂).inv ≫ β ▷ k₂ ≫ (α_ l₂ k₁ k₂).hom) ≫ (α_ l₁ l₂ (k₁ ≫ k₂)).inv

Tactic:
calc
    _ = 𝟙 _ ⊗≫ g₁ ◁ γ ▷ l₆ ⊗≫ ((g₁ ≫ l₃) ◁ δ ≫ α ▷ (l₄ ≫ k₂)) ⊗≫ l₁ ◁ β ▷ k₂ ⊗≫ 𝟙 _ := by
      bicategory
    _ = _ := by
      rw [whisker_exchange]
      bicategory

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Bicategory.whiskerRight, CategoryTheory.CategoryStruct.comp, CategoryTheory.Bicategory.whiskerLeft
-- 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
r₁ : b ⟶ a
r₂ : c ⟶ b
r₃ : e ⟶ d
r₄ : f ⟶ e
r₅ : y ⟶ x
r₆ : z ⟶ y
α : r₁ ≫ g₁ ⟶ h₁ ≫ r₃
β : r₂ ≫ h₁ ⟶ k₁ ≫ r₄
γ : r₃ ≫ g₂ ⟶ h₂ ≫ r₅
δ : r₄ ≫ h₂ ⟶ k₂ ≫ r₆
⊢ comp α β γ δ = vcomp (hcomp α β) (hcomp γ δ)

Tactic:
rfl

Premises used: CategoryTheory.Bicategory.rightAdjointSquare.comp, rfl
-- 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
r₁ : b ⟶ a
r₂ : c ⟶ b
r₃ : e ⟶ d
r₄ : f ⟶ e
r₅ : y ⟶ x
r₆ : z ⟶ y
α : r₁ ≫ g₁ ⟶ h₁ ≫ r₃
β : r₂ ≫ h₁ ⟶ k₁ ≫ r₄
γ : r₃ ≫ g₂ ⟶ h₂ ≫ r₅
δ : r₄ ≫ h₂ ⟶ k₂ ≫ r₆
dsimp :
  (α_ (r₂ ≫ r₁) g₁ g₂).inv ≫
      ((α_ r₂ r₁ g₁).hom ≫ r₂ ◁ α ≫ (α_ r₂ h₁ r₃).inv ≫ β ▷ r₃ ≫ (α_ k₁ r₄ r₃).hom) ▷ g₂ ≫
        (α_ k₁ (r₄ ≫ r₃) g₂).hom ≫
          k₁ ◁ ((α_ r₄ r₃ g₂).hom ≫ r₄ ◁ γ ≫ (α_ r₄ h₂ r₅).inv ≫ δ ▷ r₅ ≫ (α_ k₂ r₆ r₅).hom) ≫
            (α_ k₁ k₂ (r₆ ≫ r₅)).inv =
    (α_ r₂ r₁ (g₁ ≫ g₂)).hom ≫
      r₂ ◁ ((α_ r₁ g₁ g₂).inv ≫ α ▷ g₂ ≫ (α_ h₁ r₃ g₂).hom ≫ h₁ ◁ γ ≫ (α_ h₁ h₂ r₅).inv) ≫
        (α_ r₂ (h₁ ≫ h₂) r₅).inv ≫
          ((α_ r₂ h₁ h₂).inv ≫ β ▷ h₂ ≫ (α_ k₁ r₄ h₂).hom ≫ k₁ ◁ δ ≫ (α_ k₁ k₂ r₆).inv) ▷ r₅ ≫ (α_ (k₁ ≫ k₂) r₆ r₅).hom
⊢ comp α β γ δ = hcomp (vcomp α γ) (vcomp β δ)

Tactic:
dsimp only [comp, vcomp, hcomp]

Premises used: CategoryTheory.Bicategory.rightAdjointSquare.hcomp, CategoryTheory.Bicategory.rightAdjointSquare.vcomp, CategoryTheory.Bicategory.rightAdjointSquare.comp
-- 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
r₁ : b ⟶ a
r₂ : c ⟶ b
r₃ : e ⟶ d
r₄ : f ⟶ e
r₅ : y ⟶ x
r₆ : z ⟶ y
α : r₁ ≫ g₁ ⟶ h₁ ≫ r₃
β : r₂ ≫ h₁ ⟶ k₁ ≫ r₄
γ : r₃ ≫ g₂ ⟶ h₂ ≫ r₅
δ : r₄ ≫ h₂ ⟶ k₂ ≫ r₆
⊢ (α_ (r₂ ≫ r₁) g₁ g₂).inv ≫
      ((α_ r₂ r₁ g₁).hom ≫ r₂ ◁ α ≫ (α_ r₂ h₁ r₃).inv ≫ β ▷ r₃ ≫ (α_ k₁ r₄ r₃).hom) ▷ g₂ ≫
        (α_ k₁ (r₄ ≫ r₃) g₂).hom ≫
          k₁ ◁ ((α_ r₄ r₃ g₂).hom ≫ r₄ ◁ γ ≫ (α_ r₄ h₂ r₅).inv ≫ δ ▷ r₅ ≫ (α_ k₂ r₆ r₅).hom) ≫
            (α_ k₁ k₂ (r₆ ≫ r₅)).inv =
    𝟙 ((r₂ ≫ r₁) ≫ g₁ ≫ g₂) ⊗≫ r₂ ◁ α ▷ g₂ ⊗≫ (β ▷ (r₃ ≫ g₂) ≫ (k₁ ≫ r₄) ◁ γ) ⊗≫ k₁ ◁ δ ▷ r₅ ⊗≫ 𝟙 ((k₁ ≫ k₂) ≫ r₆ ≫ r₅)

Tactic:
bicategory
-- 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
r₁ : b ⟶ a
r₂ : c ⟶ b
r₃ : e ⟶ d
r₄ : f ⟶ e
r₅ : y ⟶ x
r₆ : z ⟶ y
α : r₁ ≫ g₁ ⟶ h₁ ≫ r₃
β : r₂ ≫ h₁ ⟶ k₁ ≫ r₄
γ : r₃ ≫ g₂ ⟶ h₂ ≫ r₅
δ : r₄ ≫ h₂ ⟶ k₂ ≫ r₆
rw :
  𝟙 ((r₂ ≫ r₁) ≫ g₁ ≫ g₂) ⊗≫ r₂ ◁ α ▷ g₂ ⊗≫ ((r₂ ≫ h₁) ◁ γ ≫ β ▷ (h₂ ≫ r₅)) ⊗≫ k₁ ◁ δ ▷ r₅ ⊗≫ 𝟙 ((k₁ ≫ k₂) ≫ r₆ ≫ r₅) =
    (α_ r₂ r₁ (g₁ ≫ g₂)).hom ≫
      r₂ ◁ ((α_ r₁ g₁ g₂).inv ≫ α ▷ g₂ ≫ (α_ h₁ r₃ g₂).hom ≫ h₁ ◁ γ ≫ (α_ h₁ h₂ r₅).inv) ≫
        (α_ r₂ (h₁ ≫ h₂) r₅).inv ≫
          ((α_ r₂ h₁ h₂).inv ≫ β ▷ h₂ ≫ (α_ k₁ r₄ h₂).hom ≫ k₁ ◁ δ ≫ (α_ k₁ k₂ r₆).inv) ▷ r₅ ≫ (α_ (k₁ ≫ k₂) r₆ r₅).hom
⊢ 𝟙 ((r₂ ≫ r₁) ≫ g₁ ≫ g₂) ⊗≫ r₂ ◁ α ▷ g₂ ⊗≫ (β ▷ (r₃ ≫ g₂) ≫ (k₁ ≫ r₄) ◁ γ) ⊗≫ k₁ ◁ δ ▷ r₅ ⊗≫ 𝟙 ((k₁ ≫ k₂) ≫ r₆ ≫ r₅) =
    (α_ r₂ r₁ (g₁ ≫ g₂)).hom ≫
      r₂ ◁ ((α_ r₁ g₁ g₂).inv ≫ α ▷ g₂ ≫ (α_ h₁ r₃ g₂).hom ≫ h₁ ◁ γ ≫ (α_ h₁ h₂ r₅).inv) ≫
        (α_ r₂ (h₁ ≫ h₂) r₅).inv ≫
          ((α_ r₂ h₁ h₂).inv ≫ β ▷ h₂ ≫ (α_ k₁ r₄ h₂).hom ≫ k₁ ◁ δ ≫ (α_ k₁ k₂ r₆).inv) ▷ r₅ ≫ (α_ (k₁ ≫ k₂) r₆ r₅).hom

Tactic:
rw [← whisker_exchange]

Premises used: CategoryTheory.Bicategory.whisker_exchange
-- 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
r₁ : b ⟶ a
r₂ : c ⟶ b
r₃ : e ⟶ d
r₄ : f ⟶ e
r₅ : y ⟶ x
r₆ : z ⟶ y
α : r₁ ≫ g₁ ⟶ h₁ ≫ r₃
β : r₂ ≫ h₁ ⟶ k₁ ≫ r₄
γ : r₃ ≫ g₂ ⟶ h₂ ≫ r₅
δ : r₄ ≫ h₂ ⟶ k₂ ≫ r₆
⊢ 𝟙 ((r₂ ≫ r₁) ≫ g₁ ≫ g₂) ⊗≫ r₂ ◁ α ▷ g₂ ⊗≫ ((r₂ ≫ h₁) ◁ γ ≫ β ▷ (h₂ ≫ r₅)) ⊗≫ k₁ ◁ δ ▷ r₅ ⊗≫ 𝟙 ((k₁ ≫ k₂) ≫ r₆ ≫ r₅) =
    (α_ r₂ r₁ (g₁ ≫ g₂)).hom ≫
      r₂ ◁ ((α_ r₁ g₁ g₂).inv ≫ α ▷ g₂ ≫ (α_ h₁ r₃ g₂).hom ≫ h₁ ◁ γ ≫ (α_ h₁ h₂ r₅).inv) ≫
        (α_ r₂ (h₁ ≫ h₂) r₅).inv ≫
          ((α_ r₂ h₁ h₂).inv ≫ β ▷ h₂ ≫ (α_ k₁ r₄ h₂).hom ≫ k₁ ◁ δ ≫ (α_ k₁ k₂ r₆).inv) ▷ r₅ ≫ (α_ (k₁ ≫ k₂) r₆ r₅).hom

Tactic:
bicategory
-- 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
r₁ : b ⟶ a
r₂ : c ⟶ b
r₃ : e ⟶ d
r₄ : f ⟶ e
r₅ : y ⟶ x
r₆ : z ⟶ y
α : r₁ ≫ g₁ ⟶ h₁ ≫ r₃
β : r₂ ≫ h₁ ⟶ k₁ ≫ r₄
γ : r₃ ≫ g₂ ⟶ h₂ ≫ r₅
δ : r₄ ≫ h₂ ⟶ k₂ ≫ r₆
_ :
  (α_ (r₂ ≫ r₁) g₁ g₂).inv ≫
      ((α_ r₂ r₁ g₁).hom ≫ r₂ ◁ α ≫ (α_ r₂ h₁ r₃).inv ≫ β ▷ r₃ ≫ (α_ k₁ r₄ r₃).hom) ▷ g₂ ≫
        (α_ k₁ (r₄ ≫ r₃) g₂).hom ≫
          k₁ ◁ ((α_ r₄ r₃ g₂).hom ≫ r₄ ◁ γ ≫ (α_ r₄ h₂ r₅).inv ≫ δ ▷ r₅ ≫ (α_ k₂ r₆ r₅).hom) ≫
            (α_ k₁ k₂ (r₆ ≫ r₅)).inv =
    𝟙 ((r₂ ≫ r₁) ≫ g₁ ≫ g₂) ⊗≫ r₂ ◁ α ▷ g₂ ⊗≫ (β ▷ (r₃ ≫ g₂) ≫ (k₁ ≫ r₄) ◁ γ) ⊗≫ k₁ ◁ δ ▷ r₅ ⊗≫ 𝟙 ((k₁ ≫ k₂) ≫ r₆ ≫ r₅)
_₁ :
  𝟙 ((r₂ ≫ r₁) ≫ g₁ ≫ g₂) ⊗≫ r₂ ◁ α ▷ g₂ ⊗≫ (β ▷ (r₃ ≫ g₂) ≫ (k₁ ≫ r₄) ◁ γ) ⊗≫ k₁ ◁ δ ▷ r₅ ⊗≫ 𝟙 ((k₁ ≫ k₂) ≫ r₆ ≫ r₅) =
    (α_ r₂ r₁ (g₁ ≫ g₂)).hom ≫
      r₂ ◁ ((α_ r₁ g₁ g₂).inv ≫ α ▷ g₂ ≫ (α_ h₁ r₃ g₂).hom ≫ h₁ ◁ γ ≫ (α_ h₁ h₂ r₅).inv) ≫
        (α_ r₂ (h₁ ≫ h₂) r₅).inv ≫
          ((α_ r₂ h₁ h₂).inv ≫ β ▷ h₂ ≫ (α_ k₁ r₄ h₂).hom ≫ k₁ ◁ δ ≫ (α_ k₁ k₂ r₆).inv) ▷ r₅ ≫ (α_ (k₁ ≫ k₂) r₆ r₅).hom
⊢ (α_ (r₂ ≫ r₁) g₁ g₂).inv ≫
      ((α_ r₂ r₁ g₁).hom ≫ r₂ ◁ α ≫ (α_ r₂ h₁ r₃).inv ≫ β ▷ r₃ ≫ (α_ k₁ r₄ r₃).hom) ▷ g₂ ≫
        (α_ k₁ (r₄ ≫ r₃) g₂).hom ≫
          k₁ ◁ ((α_ r₄ r₃ g₂).hom ≫ r₄ ◁ γ ≫ (α_ r₄ h₂ r₅).inv ≫ δ ▷ r₅ ≫ (α_ k₂ r₆ r₅).hom) ≫
            (α_ k₁ k₂ (r₆ ≫ r₅)).inv =
    (α_ r₂ r₁ (g₁ ≫ g₂)).hom ≫
      r₂ ◁ ((α_ r₁ g₁ g₂).inv ≫ α ▷ g₂ ≫ (α_ h₁ r₃ g₂).hom ≫ h₁ ◁ γ ≫ (α_ h₁ h₂ r₅).inv) ≫
        (α_ r₂ (h₁ ≫ h₂) r₅).inv ≫
          ((α_ r₂ h₁ h₂).inv ≫ β ▷ h₂ ≫ (α_ k₁ r₄ h₂).hom ≫ k₁ ◁ δ ≫ (α_ k₁ k₂ r₆).inv) ▷ r₅ ≫ (α_ (k₁ ≫ k₂) r₆ r₅).hom

Tactic:
calc
    _ = 𝟙 _ ⊗≫ r₂ ◁ α ▷ g₂ ⊗≫ (β ▷ (r₃ ≫ g₂) ≫ (k₁ ≫ r₄) ◁ γ) ⊗≫ k₁ ◁ δ ▷ r₅ ⊗≫ 𝟙 _ := by
      bicategory
    _ = _ := by
      rw [← whisker_exchange]
      bicategory

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Bicategory.whiskerRight, CategoryTheory.CategoryStruct.comp, CategoryTheory.Bicategory.whiskerLeft