awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} 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₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : g ≫ l₂ ⟶ l₁ ≫ h
rw :
  r₁ ◁ (((ρ_ g).inv ≫ g ◁ adj₂.unit ≫ (α_ g l₂ r₂).inv ≫ α ▷ r₂) ≫ (α_ l₁ h r₂).hom) ≫
      (α_ r₁ l₁ (h ≫ r₂)).inv ≫ adj₁.counit ▷ (h ≫ r₂) ≫ (λ_ (h ≫ r₂)).hom =
    𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂)
⊢ (mateEquiv adj₁ adj₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α =
    𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂)

Tactic:
rw [mateEquiv_apply, Adjunction.homEquiv₂_apply, Adjunction.homEquiv₁_apply]

Premises used: CategoryTheory.Bicategory.Adjunction.homEquiv₁_apply, CategoryTheory.Bicategory.Adjunction.homEquiv₂_apply, CategoryTheory.Bicategory.mateEquiv_apply
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} 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₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
α : g ≫ l₂ ⟶ l₁ ≫ h
⊢ r₁ ◁ (((ρ_ g).inv ≫ g ◁ adj₂.unit ≫ (α_ g l₂ r₂).inv ≫ α ▷ r₂) ≫ (α_ l₁ h r₂).hom) ≫
      (α_ r₁ l₁ (h ≫ r₂)).inv ≫ adj₁.counit ▷ (h ≫ r₂) ≫ (λ_ (h ≫ r₂)).hom =
    𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h ▷ r₂ ⊗≫ 𝟙 (h ≫ r₂)

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} 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₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
β : r₁ ≫ g ⟶ h ≫ r₂
rw :
  (((λ_ g).inv ≫ adj₁.unit ▷ g ≫ (α_ l₁ r₁ g).hom ≫ l₁ ◁ β) ≫ (α_ l₁ h r₂).inv) ▷ l₂ ≫
      (α_ (l₁ ≫ h) r₂ l₂).hom ≫ (l₁ ≫ h) ◁ adj₂.counit ≫ (ρ_ (l₁ ≫ h)).hom =
    𝟙 (g ≫ l₂) ⊗≫ adj₁.unit ▷ g ▷ l₂ ⊗≫ l₁ ◁ β ▷ l₂ ⊗≫ l₁ ◁ h ◁ adj₂.counit ⊗≫ 𝟙 (l₁ ≫ h)
⊢ (Equiv.symm (mateEquiv adj₁ adj₂) : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ≫ l₂ ⟶ l₁ ≫ h) β =
    𝟙 (g ≫ l₂) ⊗≫ adj₁.unit ▷ g ▷ l₂ ⊗≫ l₁ ◁ β ▷ l₂ ⊗≫ l₁ ◁ h ◁ adj₂.counit ⊗≫ 𝟙 (l₁ ≫ h)

Tactic:
rw [mateEquiv_symm_apply, Adjunction.homEquiv₂_symm_apply, Adjunction.homEquiv₁_symm_apply]

Premises used: CategoryTheory.Bicategory.Adjunction.homEquiv₂_symm_apply, CategoryTheory.Bicategory.mateEquiv_symm_apply, CategoryTheory.Bicategory.Adjunction.homEquiv₁_symm_apply
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} 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₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
β : r₁ ≫ g ⟶ h ≫ r₂
⊢ (((λ_ g).inv ≫ adj₁.unit ▷ g ≫ (α_ l₁ r₁ g).hom ≫ l₁ ◁ β) ≫ (α_ l₁ h r₂).inv) ▷ l₂ ≫
      (α_ (l₁ ≫ h) r₂ l₂).hom ≫ (l₁ ≫ h) ◁ adj₂.counit ≫ (ρ_ (l₁ ≫ h)).hom =
    𝟙 (g ≫ l₂) ⊗≫ adj₁.unit ▷ g ▷ l₂ ⊗≫ l₁ ◁ β ▷ l₂ ⊗≫ l₁ ◁ h ◁ adj₂.counit ⊗≫ 𝟙 (l₁ ≫ h)

Tactic:
bicategory
-- 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₂ : c ⟶ d
r₂ : d ⟶ c
adj₂ : l₂ ⊣ r₂
f : a ⟶ c
g : b ⟶ d
φ : f ≫ 𝟙 c ≫ l₂ ⟶ l₁ ≫ g
simp :
  r₁ ◁
        (((ρ_ f).inv ≫
            f ◁
                (Adjunction.comp
                    { unit := Iso.inv (ρ_ (𝟙 c)), counit := Iso.hom (ρ_ (𝟙 c)), left_triangle := ⋯,
                      right_triangle := ⋯ : Adjunction.{w, v, u} (𝟙 c) (𝟙 c) }
                    adj₂).unit ≫
              (α_ f (𝟙 c ≫ l₂) (r₂ ≫ 𝟙 c)).inv ≫ φ ▷ (r₂ ≫ 𝟙 c)) ≫
          (α_ l₁ g (r₂ ≫ 𝟙 c)).hom) ≫
      (α_ r₁ l₁ (g ≫ r₂ ≫ 𝟙 c)).inv ≫ adj₁.counit ▷ (g ≫ r₂ ≫ 𝟙 c) ≫ (λ_ (g ≫ r₂ ≫ 𝟙 c)).hom =
    (r₁ ◁ (((ρ_ f).inv ≫ f ◁ adj₂.unit ≫ (α_ f l₂ r₂).inv ≫ (f ◁ (λ_ l₂).inv ≫ φ) ▷ r₂) ≫ (α_ l₁ g r₂).hom) ≫
        (α_ r₁ l₁ (g ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ r₂) ≫ (λ_ (g ≫ r₂)).hom) ≫
      (ρ_ (g ≫ r₂)).inv ≫ (α_ g r₂ (𝟙 c)).hom
⊢ Eq (α := r₁ ≫ f ⟶ g ≫ r₂ ≫ 𝟙 c)
    ((mateEquiv adj₁ (Adjunction.comp (Adjunction.id c) adj₂) : (a_1 : f ≫ 𝟙 c ≫ l₂ ⟶ l₁ ≫ g) → r₁ ≫ f ⟶ g ≫ r₂ ≫ 𝟙 c)
        φ :
      r₁ ≫ f ⟶ g ≫ r₂ ≫ 𝟙 c)
    ((mateEquiv adj₁ adj₂ : (a_1 : f ≫ l₂ ⟶ l₁ ≫ g) → r₁ ≫ f ⟶ g ≫ r₂) (f ◁ (λ_ l₂).inv ≫ φ) ≫
        (ρ_ (g ≫ r₂)).inv ≫ (α_ g r₂ (𝟙 c)).hom :
      r₁ ≫ f ⟶ g ≫ r₂ ≫ 𝟙 c)

Tactic:
simp only [mateEquiv_apply, Adjunction.homEquiv₁_apply, Adjunction.homEquiv₂_apply,
    Adjunction.id]

Premises used: CategoryTheory.Bicategory.Adjunction.homEquiv₁_apply, CategoryTheory.Bicategory.Adjunction.homEquiv₂_apply, CategoryTheory.Bicategory.Adjunction.id, CategoryTheory.Bicategory.mateEquiv_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₂ : c ⟶ d
r₂ : d ⟶ c
adj₂ : l₂ ⊣ r₂
f : a ⟶ c
g : b ⟶ d
φ : f ≫ 𝟙 c ≫ l₂ ⟶ l₁ ≫ g
dsimp :
  r₁ ◁
        (((ρ_ f).inv ≫
            f ◁
                bicategoricalComp (h := 𝟙 c ≫ 𝟙 c ≫ 𝟙 c) (Iso.inv (ρ_ (𝟙 c)))
                  (𝟙 c ◁ adj₂.unit ▷ 𝟙 c ⊗≫ 𝟙 ((𝟙 c ≫ l₂) ≫ r₂ ≫ 𝟙 c)) ≫
              (α_ f (𝟙 c ≫ l₂) (r₂ ≫ 𝟙 c)).inv ≫ φ ▷ (r₂ ≫ 𝟙 c)) ≫
          (α_ l₁ g (r₂ ≫ 𝟙 c)).hom) ≫
      (α_ r₁ l₁ (g ≫ r₂ ≫ 𝟙 c)).inv ≫ adj₁.counit ▷ (g ≫ r₂ ≫ 𝟙 c) ≫ (λ_ (g ≫ r₂ ≫ 𝟙 c)).hom =
    (r₁ ◁ (((ρ_ f).inv ≫ f ◁ adj₂.unit ≫ (α_ f l₂ r₂).inv ≫ (f ◁ (λ_ l₂).inv ≫ φ) ▷ r₂) ≫ (α_ l₁ g r₂).hom) ≫
        (α_ r₁ l₁ (g ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ r₂) ≫ (λ_ (g ≫ r₂)).hom) ≫
      (ρ_ (g ≫ r₂)).inv ≫ (α_ g r₂ (𝟙 c)).hom
⊢ r₁ ◁
        (((ρ_ f).inv ≫
            f ◁
                (Adjunction.comp
                    { unit := Iso.inv (ρ_ (𝟙 c)), counit := Iso.hom (ρ_ (𝟙 c)), left_triangle := ⋯,
                      right_triangle := ⋯ : Adjunction.{w, v, u} (𝟙 c) (𝟙 c) }
                    adj₂).unit ≫
              (α_ f (𝟙 c ≫ l₂) (r₂ ≫ 𝟙 c)).inv ≫ φ ▷ (r₂ ≫ 𝟙 c)) ≫
          (α_ l₁ g (r₂ ≫ 𝟙 c)).hom) ≫
      (α_ r₁ l₁ (g ≫ r₂ ≫ 𝟙 c)).inv ≫ adj₁.counit ▷ (g ≫ r₂ ≫ 𝟙 c) ≫ (λ_ (g ≫ r₂ ≫ 𝟙 c)).hom =
    (r₁ ◁ (((ρ_ f).inv ≫ f ◁ adj₂.unit ≫ (α_ f l₂ r₂).inv ≫ (f ◁ (λ_ l₂).inv ≫ φ) ▷ r₂) ≫ (α_ l₁ g r₂).hom) ≫
        (α_ r₁ l₁ (g ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ r₂) ≫ (λ_ (g ≫ r₂)).hom) ≫
      (ρ_ (g ≫ r₂)).inv ≫ (α_ g r₂ (𝟙 c)).hom

Tactic:
dsimp
-- 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₂ : c ⟶ d
r₂ : d ⟶ c
adj₂ : l₂ ⊣ r₂
f : a ⟶ c
g : b ⟶ d
φ : f ≫ 𝟙 c ≫ l₂ ⟶ l₁ ≫ g
⊢ r₁ ◁
        (((ρ_ f).inv ≫
            f ◁
                bicategoricalComp (h := 𝟙 c ≫ 𝟙 c ≫ 𝟙 c) (Iso.inv (ρ_ (𝟙 c)))
                  (𝟙 c ◁ adj₂.unit ▷ 𝟙 c ⊗≫ 𝟙 ((𝟙 c ≫ l₂) ≫ r₂ ≫ 𝟙 c)) ≫
              (α_ f (𝟙 c ≫ l₂) (r₂ ≫ 𝟙 c)).inv ≫ φ ▷ (r₂ ≫ 𝟙 c)) ≫
          (α_ l₁ g (r₂ ≫ 𝟙 c)).hom) ≫
      (α_ r₁ l₁ (g ≫ r₂ ≫ 𝟙 c)).inv ≫ adj₁.counit ▷ (g ≫ r₂ ≫ 𝟙 c) ≫ (λ_ (g ≫ r₂ ≫ 𝟙 c)).hom =
    (r₁ ◁ (((ρ_ f).inv ≫ f ◁ adj₂.unit ≫ (α_ f l₂ r₂).inv ≫ (f ◁ (λ_ l₂).inv ≫ φ) ▷ r₂) ≫ (α_ l₁ g r₂).hom) ≫
        (α_ r₁ l₁ (g ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ r₂) ≫ (λ_ (g ≫ r₂)).hom) ≫
      (ρ_ (g ≫ r₂)).inv ≫ (α_ g r₂ (𝟙 c)).hom

Tactic:
bicategory
-- 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₂ : c ⟶ d
r₂ : d ⟶ c
adj₂ : l₂ ⊣ r₂
f : a ⟶ c
g : b ⟶ d
φ : f ≫ l₂ ≫ 𝟙 d ⟶ l₁ ≫ g
simp :
  r₁ ◁
        (((ρ_ f).inv ≫
            f ◁
                (adj₂.comp
                    { unit := Iso.inv (ρ_ (𝟙 d)), counit := Iso.hom (ρ_ (𝟙 d)), left_triangle := ⋯,
                      right_triangle := ⋯ : Adjunction.{w, v, u} (𝟙 d) (𝟙 d) }).unit ≫
              (α_ f (l₂ ≫ 𝟙 d) (𝟙 d ≫ r₂)).inv ≫ φ ▷ (𝟙 d ≫ r₂)) ≫
          (α_ l₁ g (𝟙 d ≫ r₂)).hom) ≫
      (α_ r₁ l₁ (g ≫ 𝟙 d ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ 𝟙 d ≫ r₂) ≫ (λ_ (g ≫ 𝟙 d ≫ r₂)).hom =
    (r₁ ◁
          (((ρ_ f).inv ≫ f ◁ adj₂.unit ≫ (α_ f l₂ r₂).inv ≫ ((ρ_ (f ≫ l₂)).inv ≫ (α_ f l₂ (𝟙 d)).hom ≫ φ) ▷ r₂) ≫
            (α_ l₁ g r₂).hom) ≫
        (α_ r₁ l₁ (g ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ r₂) ≫ (λ_ (g ≫ r₂)).hom) ≫
      g ◁ (λ_ r₂).inv
⊢ Eq (α := r₁ ≫ f ⟶ g ≫ 𝟙 d ≫ r₂)
    ((mateEquiv adj₁ (adj₂.comp (Adjunction.id d)) : (a_1 : f ≫ l₂ ≫ 𝟙 d ⟶ l₁ ≫ g) → r₁ ≫ f ⟶ g ≫ 𝟙 d ≫ r₂) φ :
      r₁ ≫ f ⟶ g ≫ 𝟙 d ≫ r₂)
    ((mateEquiv adj₁ adj₂ : (a_1 : f ≫ l₂ ⟶ l₁ ≫ g) → r₁ ≫ f ⟶ g ≫ r₂) ((ρ_ (f ≫ l₂)).inv ≫ (α_ f l₂ (𝟙 d)).hom ≫ φ) ≫
        g ◁ (λ_ r₂).inv :
      r₁ ≫ f ⟶ g ≫ 𝟙 d ≫ r₂)

Tactic:
simp only [mateEquiv_apply, Adjunction.homEquiv₁_apply, Adjunction.homEquiv₂_apply,
    Adjunction.id]

Premises used: CategoryTheory.Bicategory.Adjunction.homEquiv₁_apply, CategoryTheory.Bicategory.Adjunction.homEquiv₂_apply, CategoryTheory.Bicategory.Adjunction.id, CategoryTheory.Bicategory.mateEquiv_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₂ : c ⟶ d
r₂ : d ⟶ c
adj₂ : l₂ ⊣ r₂
f : a ⟶ c
g : b ⟶ d
φ : f ≫ l₂ ≫ 𝟙 d ⟶ l₁ ≫ g
dsimp :
  r₁ ◁
        (((ρ_ f).inv ≫
            f ◁
                bicategoricalComp (h := l₂ ≫ 𝟙 d ≫ r₂) adj₂.unit
                  (l₂ ◁ Iso.inv (ρ_ (𝟙 d)) ▷ r₂ ⊗≫ 𝟙 ((l₂ ≫ 𝟙 d) ≫ 𝟙 d ≫ r₂)) ≫
              (α_ f (l₂ ≫ 𝟙 d) (𝟙 d ≫ r₂)).inv ≫ φ ▷ (𝟙 d ≫ r₂)) ≫
          (α_ l₁ g (𝟙 d ≫ r₂)).hom) ≫
      (α_ r₁ l₁ (g ≫ 𝟙 d ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ 𝟙 d ≫ r₂) ≫ (λ_ (g ≫ 𝟙 d ≫ r₂)).hom =
    (r₁ ◁
          (((ρ_ f).inv ≫ f ◁ adj₂.unit ≫ (α_ f l₂ r₂).inv ≫ ((ρ_ (f ≫ l₂)).inv ≫ (α_ f l₂ (𝟙 d)).hom ≫ φ) ▷ r₂) ≫
            (α_ l₁ g r₂).hom) ≫
        (α_ r₁ l₁ (g ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ r₂) ≫ (λ_ (g ≫ r₂)).hom) ≫
      g ◁ (λ_ r₂).inv
⊢ r₁ ◁
        (((ρ_ f).inv ≫
            f ◁
                (adj₂.comp
                    { unit := Iso.inv (ρ_ (𝟙 d)), counit := Iso.hom (ρ_ (𝟙 d)), left_triangle := ⋯,
                      right_triangle := ⋯ : Adjunction.{w, v, u} (𝟙 d) (𝟙 d) }).unit ≫
              (α_ f (l₂ ≫ 𝟙 d) (𝟙 d ≫ r₂)).inv ≫ φ ▷ (𝟙 d ≫ r₂)) ≫
          (α_ l₁ g (𝟙 d ≫ r₂)).hom) ≫
      (α_ r₁ l₁ (g ≫ 𝟙 d ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ 𝟙 d ≫ r₂) ≫ (λ_ (g ≫ 𝟙 d ≫ r₂)).hom =
    (r₁ ◁
          (((ρ_ f).inv ≫ f ◁ adj₂.unit ≫ (α_ f l₂ r₂).inv ≫ ((ρ_ (f ≫ l₂)).inv ≫ (α_ f l₂ (𝟙 d)).hom ≫ φ) ▷ r₂) ≫
            (α_ l₁ g r₂).hom) ≫
        (α_ r₁ l₁ (g ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ r₂) ≫ (λ_ (g ≫ r₂)).hom) ≫
      g ◁ (λ_ r₂).inv

Tactic:
dsimp
-- 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₂ : c ⟶ d
r₂ : d ⟶ c
adj₂ : l₂ ⊣ r₂
f : a ⟶ c
g : b ⟶ d
φ : f ≫ l₂ ≫ 𝟙 d ⟶ l₁ ≫ g
⊢ r₁ ◁
        (((ρ_ f).inv ≫
            f ◁
                bicategoricalComp (h := l₂ ≫ 𝟙 d ≫ r₂) adj₂.unit
                  (l₂ ◁ Iso.inv (ρ_ (𝟙 d)) ▷ r₂ ⊗≫ 𝟙 ((l₂ ≫ 𝟙 d) ≫ 𝟙 d ≫ r₂)) ≫
              (α_ f (l₂ ≫ 𝟙 d) (𝟙 d ≫ r₂)).inv ≫ φ ▷ (𝟙 d ≫ r₂)) ≫
          (α_ l₁ g (𝟙 d ≫ r₂)).hom) ≫
      (α_ r₁ l₁ (g ≫ 𝟙 d ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ 𝟙 d ≫ r₂) ≫ (λ_ (g ≫ 𝟙 d ≫ r₂)).hom =
    (r₁ ◁
          (((ρ_ f).inv ≫ f ◁ adj₂.unit ≫ (α_ f l₂ r₂).inv ≫ ((ρ_ (f ≫ l₂)).inv ≫ (α_ f l₂ (𝟙 d)).hom ≫ φ) ▷ r₂) ≫
            (α_ l₁ g r₂).hom) ≫
        (α_ r₁ l₁ (g ≫ r₂)).inv ≫ adj₁.counit ▷ (g ≫ r₂) ≫ (λ_ (g ≫ r₂)).hom) ≫
      g ◁ (λ_ r₂).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 : 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₂
simp :
  𝟙 (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₂).inv ≫
      (𝟙 (r₁ ≫ g₁) ⊗≫ r₁ ◁ g₁ ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h₁ ▷ r₂ ⊗≫ 𝟙 (h₁ ≫ r₂)) ▷ g₂ ≫
        (α_ h₁ r₂ g₂).hom ≫
          h₁ ◁ (𝟙 (r₂ ≫ g₂) ⊗≫ r₂ ◁ g₂ ◁ adj₃.unit ⊗≫ r₂ ◁ β ▷ r₃ ⊗≫ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 (h₂ ≫ r₃)) ≫
            (α_ h₁ h₂ r₃).inv
⊢ Eq (α := r₁ ≫ g₁ ≫ g₂ ⟶ (h₁ ≫ h₂) ≫ r₃)
    ((mateEquiv adj₁ adj₃ : (a_1 : (g₁ ≫ g₂) ≫ l₃ ⟶ l₁ ≫ h₁ ≫ h₂) → r₁ ≫ g₁ ≫ g₂ ⟶ (h₁ ≫ h₂) ≫ r₃)
        (leftAdjointSquare.vcomp α β) :
      r₁ ≫ g₁ ≫ g₂ ⟶ (h₁ ≫ h₂) ≫ r₃)
    (rightAdjointSquare.vcomp (r₂ := r₂) ((mateEquiv adj₁ adj₂ : (a_1 : g₁ ≫ l₂ ⟶ l₁ ≫ h₁) → r₁ ≫ g₁ ⟶ h₁ ≫ r₂) α)
        ((mateEquiv adj₂ adj₃ : (a : g₂ ≫ l₃ ⟶ l₂ ≫ h₂) → r₂ ≫ g₂ ⟶ h₂ ≫ r₃) β) :
      r₁ ≫ g₁ ≫ g₂ ⟶ (h₁ ≫ h₂) ≫ r₃)

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

Premises used: CategoryTheory.Bicategory.rightAdjointSquare.vcomp, CategoryTheory.Bicategory.leftAdjointSquare.vcomp, 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 ⟶ 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₂
symm :
  (α_ r₁ g₁ g₂).inv ≫
      (𝟙 (r₁ ≫ g₁) ⊗≫ r₁ ◁ g₁ ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h₁ ▷ r₂ ⊗≫ 𝟙 (h₁ ≫ r₂)) ▷ g₂ ≫
        (α_ h₁ r₂ g₂).hom ≫
          h₁ ◁ (𝟙 (r₂ ≫ g₂) ⊗≫ r₂ ◁ g₂ ◁ adj₃.unit ⊗≫ r₂ ◁ β ▷ r₃ ⊗≫ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 (h₂ ≫ r₃)) ≫
            (α_ h₁ h₂ r₃).inv =
    𝟙 (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₁ 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₂).inv ≫
      (𝟙 (r₁ ≫ g₁) ⊗≫ r₁ ◁ g₁ ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h₁ ▷ r₂ ⊗≫ 𝟙 (h₁ ≫ r₂)) ▷ g₂ ≫
        (α_ h₁ r₂ g₂).hom ≫
          h₁ ◁ (𝟙 (r₂ ≫ g₂) ⊗≫ r₂ ◁ g₂ ◁ adj₃.unit ⊗≫ r₂ ◁ β ▷ r₃ ⊗≫ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 (h₂ ≫ r₃)) ≫
            (α_ h₁ h₂ r₃).inv

Tactic:
symm
-- 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₂).inv ≫
      (𝟙 (r₁ ≫ g₁) ⊗≫ r₁ ◁ g₁ ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ h₁ ▷ r₂ ⊗≫ 𝟙 (h₁ ≫ r₂)) ▷ g₂ ≫
        (α_ h₁ r₂ g₂).hom ≫
          h₁ ◁ (𝟙 (r₂ ≫ g₂) ⊗≫ r₂ ◁ g₂ ◁ adj₃.unit ⊗≫ r₂ ◁ β ▷ r₃ ⊗≫ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 (h₂ ≫ r₃)) ≫
            (α_ h₁ h₂ r₃).inv =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
        r₁ ◁ α ▷ r₂ ▷ g₂ ⊗≫
          (adj₁.counit ▷ (h₁ ≫ r₂ ≫ g₂ ≫ 𝟙 e) ≫ 𝟙 b ◁ h₁ ◁ r₂ ◁ g₂ ◁ adj₃.unit) ⊗≫
            h₁ ◁ r₂ ◁ β ▷ r₃ ⊗≫ h₁ ◁ adj₂.counit ▷ 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 ⟶ 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₁ ◁ adj₂.unit ▷ g₂ ⊗≫
        r₁ ◁ α ▷ r₂ ▷ g₂ ⊗≫
          ((r₁ ≫ l₁) ◁ h₁ ◁ r₂ ◁ g₂ ◁ adj₃.unit ≫ adj₁.counit ▷ (h₁ ≫ r₂ ≫ g₂ ≫ l₃ ≫ r₃)) ⊗≫
            h₁ ◁ r₂ ◁ β ▷ r₃ ⊗≫ h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
        r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ 𝟙 e) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ g₂ ◁ adj₃.unit) ⊗≫
          (adj₁.counit ▷ (h₁ ≫ r₂) ▷ (g₂ ≫ l₃) ≫ (𝟙 b ≫ h₁ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
            h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
        r₁ ◁ α ▷ r₂ ▷ g₂ ⊗≫
          (adj₁.counit ▷ (h₁ ≫ r₂ ≫ g₂ ≫ 𝟙 e) ≫ 𝟙 b ◁ h₁ ◁ r₂ ◁ g₂ ◁ adj₃.unit) ⊗≫
            h₁ ◁ r₂ ◁ β ▷ r₃ ⊗≫ h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
        r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ 𝟙 e) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ g₂ ◁ adj₃.unit) ⊗≫
          (adj₁.counit ▷ (h₁ ≫ r₂) ▷ (g₂ ≫ l₃) ≫ (𝟙 b ≫ h₁ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
            h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)

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 ⟶ 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₁ ◁ adj₂.unit ▷ g₂ ⊗≫
        r₁ ◁ α ▷ r₂ ▷ g₂ ⊗≫
          ((r₁ ≫ l₁) ◁ h₁ ◁ r₂ ◁ g₂ ◁ adj₃.unit ≫ adj₁.counit ▷ (h₁ ≫ r₂ ≫ g₂ ≫ l₃ ≫ r₃)) ⊗≫
            h₁ ◁ r₂ ◁ β ▷ r₃ ⊗≫ h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
        r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ 𝟙 e) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ g₂ ◁ adj₃.unit) ⊗≫
          (adj₁.counit ▷ (h₁ ≫ r₂) ▷ (g₂ ≫ l₃) ≫ (𝟙 b ≫ h₁ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
            h₁ ◁ adj₂.counit ▷ 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 ⟶ 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₁ ◁ adj₂.unit ▷ g₂ ⊗≫
        r₁ ◁ ((g₁ ≫ l₂) ◁ r₂ ◁ g₂ ◁ adj₃.unit ≫ α ▷ (r₂ ≫ g₂ ≫ l₃ ≫ r₃)) ⊗≫
          (((r₁ ≫ l₁) ≫ h₁ ≫ r₂) ◁ β ≫ adj₁.counit ▷ (h₁ ≫ r₂) ▷ (l₂ ≫ h₂)) ▷ r₃ ⊗≫
            h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ 𝟙 e) ≫ (l₂ ≫ r₂) ◁ g₂ ◁ adj₃.unit) ⊗≫
        r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ l₃) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ β) ▷ r₃ ⊗≫
          (adj₁.counit ▷ h₁ ▷ (r₂ ≫ l₂) ≫ (𝟙 b ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ adj₂.unit ▷ g₂ ⊗≫
        r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ 𝟙 e) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ g₂ ◁ adj₃.unit) ⊗≫
          (adj₁.counit ▷ (h₁ ≫ r₂) ▷ (g₂ ≫ l₃) ≫ (𝟙 b ≫ h₁ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
            h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ 𝟙 e) ≫ (l₂ ≫ r₂) ◁ g₂ ◁ adj₃.unit) ⊗≫
        r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ l₃) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ β) ▷ r₃ ⊗≫
          (adj₁.counit ▷ h₁ ▷ (r₂ ≫ l₂) ≫ (𝟙 b ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ 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 ⟶ 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₁ ◁ adj₂.unit ▷ g₂ ⊗≫
        r₁ ◁ ((g₁ ≫ l₂) ◁ r₂ ◁ g₂ ◁ adj₃.unit ≫ α ▷ (r₂ ≫ g₂ ≫ l₃ ≫ r₃)) ⊗≫
          (((r₁ ≫ l₁) ≫ h₁ ≫ r₂) ◁ β ≫ adj₁.counit ▷ (h₁ ≫ r₂) ▷ (l₂ ≫ h₂)) ▷ r₃ ⊗≫
            h₁ ◁ adj₂.counit ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ 𝟙 e) ≫ (l₂ ≫ r₂) ◁ g₂ ◁ adj₃.unit) ⊗≫
        r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ l₃) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ β) ▷ r₃ ⊗≫
          (adj₁.counit ▷ h₁ ▷ (r₂ ≫ l₂) ≫ (𝟙 b ≫ h₁) ◁ adj₂.counit) ▷ 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 ⟶ 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₁ ◁ (𝟙 c ◁ g₂ ◁ adj₃.unit ≫ adj₂.unit ▷ (g₂ ≫ l₃ ≫ r₃)) ⊗≫
        r₁ ◁ ((g₁ ≫ l₂) ◁ r₂ ◁ β ≫ α ▷ (r₂ ≫ l₂ ≫ h₂)) ▷ r₃ ⊗≫
          (((r₁ ≫ l₁) ≫ h₁) ◁ adj₂.counit ≫ adj₁.counit ▷ h₁ ▷ 𝟙 d) ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ l₃) ≫ (l₂ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
          r₁ ◁ (α ▷ (r₂ ≫ l₂) ≫ (l₁ ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)
⊢ 𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ 𝟙 e) ≫ (l₂ ≫ r₂) ◁ g₂ ◁ adj₃.unit) ⊗≫
        r₁ ◁ (α ▷ (r₂ ≫ g₂ ≫ l₃) ≫ (l₁ ≫ h₁) ◁ r₂ ◁ β) ▷ r₃ ⊗≫
          (adj₁.counit ▷ h₁ ▷ (r₂ ≫ l₂) ≫ (𝟙 b ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ l₃) ≫ (l₂ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
          r₁ ◁ (α ▷ (r₂ ≫ l₂) ≫ (l₁ ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ r₃ ⊗≫ adj₁.counit ▷ h₁ ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃)

Tactic:
rw [← whisker_exchange, ← 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 ⟶ 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₁ ◁ (𝟙 c ◁ g₂ ◁ adj₃.unit ≫ adj₂.unit ▷ (g₂ ≫ l₃ ≫ r₃)) ⊗≫
        r₁ ◁ ((g₁ ≫ l₂) ◁ r₂ ◁ β ≫ α ▷ (r₂ ≫ l₂ ≫ h₂)) ▷ r₃ ⊗≫
          (((r₁ ≫ l₁) ≫ h₁) ◁ adj₂.counit ≫ adj₁.counit ▷ h₁ ▷ 𝟙 d) ▷ h₂ ▷ r₃ ⊗≫ 𝟙 ((h₁ ≫ h₂) ≫ r₃) =
    𝟙 (r₁ ≫ g₁ ≫ g₂) ⊗≫
      r₁ ◁ g₁ ◁ g₂ ◁ adj₃.unit ⊗≫
        r₁ ◁ g₁ ◁ (adj₂.unit ▷ (g₂ ≫ l₃) ≫ (l₂ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
          r₁ ◁ (α ▷ (r₂ ≫ l₂) ≫ (l₁ ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ 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 ⟶ 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₁ ◁ (𝟙 c ◁ β ≫ adj₂.unit ▷ (l₂ ≫ h₂)) ▷ r₃ ⊗≫
          r₁ ◁ ((g₁ ≫ l₂) ◁ adj₂.counit ≫ α ▷ 𝟙 d) ▷ h₂ ▷ 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₁ ◁ (adj₂.unit ▷ (g₂ ≫ l₃) ≫ (l₂ ≫ r₂) ◁ β) ▷ r₃ ⊗≫
          r₁ ◁ (α ▷ (r₂ ≫ l₂) ≫ (l₁ ≫ h₁) ◁ adj₂.counit) ▷ h₂ ▷ 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₃)

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 ⟶ 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₁ ◁ (𝟙 c ◁ β ≫ adj₂.unit ▷ (l₂ ≫ h₂)) ▷ r₃ ⊗≫
          r₁ ◁ ((g₁ ≫ l₂) ◁ adj₂.counit ≫ α ▷ 𝟙 d) ▷ h₂ ▷ 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₃)

Tactic:
bicategory