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 : 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₁ ⊗≫
      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

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₂
_ :
  ((ρ_ 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₃))
_₁ :
  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
⊢ 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)

Tactic:
calc
    _ = 𝟙 r₁ ⊗≫
          rightAdjointSquare.vcomp
            (mateEquiv adj₁ adj₂ ((λ_ _).hom ≫ α ≫ (ρ_ _).inv))
            (mateEquiv adj₂ adj₃ ((λ_ _).hom ≫ β ≫ (ρ_ _).inv)) ⊗≫ 𝟙 r₃ := by
      dsimp only [rightAdjointSquare.vcomp]
      bicategory
    _ = _ := by
      rw [← mateEquiv_vcomp]
      simp only [leftAdjointSquare.vcomp, mateEquiv_apply']
      bicategory

Premises used: CategoryTheory.Bicategory.rightUnitor, CategoryTheory.CategoryStruct.id, CategoryTheory.Bicategory.rightAdjointSquare.vcomp, CategoryTheory.Bicategory.leftUnitor, CategoryTheory.Bicategory.mateEquiv, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.Iso.inv
-- 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₃
α : r₁ ⟶ r₂
β : r₂ ⟶ r₃
rw :
  CategoryStruct.comp (Y := r₂)
      ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂)
        (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) α : l₂ ⟶ l₁))
      ((conjugateEquiv adj₂ adj₃ : (a : l₃ ⟶ l₂) → r₂ ⟶ r₃)
        (((conjugateEquiv adj₂ adj₃).symm : (a : r₂ ⟶ r₃) → l₃ ⟶ l₂) β : l₃ ⟶ l₂)) =
    α ≫ β
⊢ Eq (α := l₃ ⟶ l₁)
    (CategoryStruct.comp (Y := l₂) (((conjugateEquiv adj₂ adj₃).symm : (a : r₂ ⟶ r₃) → l₃ ⟶ l₂) β)
        (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) α) :
      l₃ ⟶ l₁)
    (((conjugateEquiv adj₁ adj₃).symm : (a : r₁ ⟶ r₃) → l₃ ⟶ l₁) (α ≫ β) : l₃ ⟶ l₁)

Tactic:
rw [Equiv.eq_symm_apply, ← conjugateEquiv_comp _ adj₂]

Premises used: Equiv.eq_symm_apply, CategoryTheory.Bicategory.conjugateEquiv_comp
-- 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₃
α : r₁ ⟶ r₂
β : r₂ ⟶ r₃
⊢ CategoryStruct.comp (Y := r₂)
      ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂)
        (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) α : l₂ ⟶ l₁))
      ((conjugateEquiv adj₂ adj₃ : (a : l₃ ⟶ l₂) → r₂ ⟶ r₃)
        (((conjugateEquiv adj₂ adj₃).symm : (a : r₂ ⟶ r₃) → l₃ ⟶ l₂) β : l₃ ⟶ l₂)) =
    α ≫ β

Tactic:
simp only [Equiv.apply_symm_apply]

Premises used: Equiv.apply_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₂
α : l₂ ⟶ l₁
β : l₁ ⟶ l₂
βα : β ≫ α = 𝟙 l₁
rw : Eq (α := r₁ ⟶ r₁) ((conjugateEquiv adj₁ adj₁ : (a : l₁ ⟶ l₁) → r₁ ⟶ r₁) (β ≫ α) : r₁ ⟶ r₁) (𝟙 r₁ : r₁ ⟶ r₁)
rw₁ : Eq (α := r₁ ⟶ r₁) ((conjugateEquiv adj₁ adj₁ : (a : l₁ ⟶ l₁) → r₁ ⟶ r₁) (𝟙 l₁) : r₁ ⟶ r₁) (𝟙 r₁ : r₁ ⟶ r₁)
rw₂ rw₃ : 𝟙 r₁ = 𝟙 r₁
⊢ 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₁)
    (𝟙 r₁ : r₁ ⟶ r₁)

Tactic:
rw [conjugateEquiv_comp, βα, conjugateEquiv_id]

Premises used: CategoryTheory.Bicategory.conjugateEquiv_id, CategoryTheory.Bicategory.conjugateEquiv_comp
-- 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₂
β : r₂ ⟶ r₁
αβ : α ≫ β = 𝟙 r₁
rw : Eq (α := l₁ ⟶ l₁) (((conjugateEquiv adj₁ adj₁).symm : (a : r₁ ⟶ r₁) → l₁ ⟶ l₁) (α ≫ β) : l₁ ⟶ l₁) (𝟙 l₁ : l₁ ⟶ l₁)
rw₁ : Eq (α := l₁ ⟶ l₁) (((conjugateEquiv adj₁ adj₁).symm : (a : r₁ ⟶ r₁) → l₁ ⟶ l₁) (𝟙 r₁) : l₁ ⟶ l₁) (𝟙 l₁ : l₁ ⟶ l₁)
rw₂ rw₃ : 𝟙 l₁ = 𝟙 l₁
⊢ Eq (α := l₁ ⟶ l₁)
    (CategoryStruct.comp (Y := l₂) (((conjugateEquiv adj₂ adj₁).symm : (a : r₂ ⟶ r₁) → l₁ ⟶ l₂) β)
        (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) α) :
      l₁ ⟶ l₁)
    (𝟙 l₁ : l₁ ⟶ l₁)

Tactic:
rw [conjugateEquiv_symm_comp, αβ, conjugateEquiv_symm_id]

Premises used: CategoryTheory.Bicategory.conjugateEquiv_symm_id, CategoryTheory.Bicategory.conjugateEquiv_symm_comp
-- 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₁
inst_1 : IsIso α
⊢ inv α ≫ α = 𝟙 l₁

Tactic:
simp
-- 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₁
inst_1 : IsIso α
⊢ α ≫ inv α = 𝟙 l₂

Tactic:
simp
-- 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₂
inst_1 : IsIso α
⊢ inv α ≫ α = 𝟙 r₂

Tactic:
simp
-- 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₂
inst_1 : IsIso α
⊢ α ≫ inv α = 𝟙 r₁

Tactic:
simp
-- 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₁
inst_1 : IsIso (X := r₁) ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α : r₁ ⟶ r₂)
this :
  IsIso (C := c ⟶ d) (X := l₂) (Y := l₁)
    (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁)
        ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α : r₁ ⟶ r₂) :
      l₂ ⟶ l₁)
⊢ IsIso α

Tactic:
simpa only [Equiv.symm_apply_apply] using this

Premises used: Equiv.symm_apply_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₁
inst_1 : IsIso (X := r₁) ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α : r₁ ⟶ r₂)
suffices :
  IsIso (C := c ⟶ d) (X := l₂) (Y := l₁)
    (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁)
        ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α : r₁ ⟶ r₂) :
      l₂ ⟶ l₁)
⊢ IsIso α

Tactic:
suffices IsIso ((conjugateEquiv adj₁ adj₂).symm (conjugateEquiv adj₁ adj₂ α))
    by simpa only [Equiv.symm_apply_apply] using this
-- 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₁
inst_1 : IsIso (X := r₁) ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α : r₁ ⟶ r₂)
⊢ IsIso (C := c ⟶ d) (X := l₂) (Y := l₁)
    (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁)
        ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α : r₁ ⟶ r₂) :
      l₂ ⟶ l₁)

Tactic:
infer_instance
-- 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₂
inst_1 : IsIso (X := l₂) (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) α : l₂ ⟶ l₁)
this :
  IsIso (C := d ⟶ c) (X := r₁) (Y := r₂)
    ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂)
        (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) α : l₂ ⟶ l₁) :
      r₁ ⟶ r₂)
⊢ IsIso α

Tactic:
simpa only [Equiv.apply_symm_apply] using this

Premises used: Equiv.apply_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₂
inst_1 : IsIso (X := l₂) (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) α : l₂ ⟶ l₁)
suffices :
  IsIso (C := d ⟶ c) (X := r₁) (Y := r₂)
    ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂)
        (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) α : l₂ ⟶ l₁) :
      r₁ ⟶ r₂)
⊢ IsIso α

Tactic:
suffices IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))
    by simpa only [Equiv.apply_symm_apply] using this
-- 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₂
inst_1 : IsIso (X := l₂) (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) α : l₂ ⟶ l₁)
⊢ IsIso (C := d ⟶ c) (X := r₁) (Y := r₂)
    ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂)
        (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) α : l₂ ⟶ l₁) :
      r₁ ⟶ r₂)

Tactic:
infer_instance
-- 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 : Eq (α := r₁ ⟶ r₁) ((conjugateEquiv adj₁ adj₁ : (a : l₁ ⟶ l₁) → r₁ ⟶ r₁) (α.inv ≫ α.hom) : r₁ ⟶ r₁) (𝟙 r₁ : r₁ ⟶ r₁)
rw₁ : Eq (α := r₁ ⟶ r₁) ((conjugateEquiv adj₁ adj₁ : (a : l₁ ⟶ l₁) → r₁ ⟶ r₁) (𝟙 l₁) : r₁ ⟶ r₁) (𝟙 r₁ : r₁ ⟶ r₁)
rw₂ rw₃ : 𝟙 r₁ = 𝟙 r₁
⊢ Eq (α := r₁ ⟶ r₁)
    (CategoryStruct.comp (Y := r₂) ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α.hom)
        ((conjugateEquiv adj₂ adj₁ : (a : l₁ ⟶ l₂) → r₂ ⟶ r₁) α.inv) :
      r₁ ⟶ r₁)
    (𝟙 r₁ : r₁ ⟶ r₁)

Tactic:
rw [conjugateEquiv_comp, Iso.inv_hom_id, conjugateEquiv_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Bicategory.conjugateEquiv_id, CategoryTheory.Bicategory.conjugateEquiv_comp
-- 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 : Eq (α := r₂ ⟶ r₂) ((conjugateEquiv adj₂ adj₂ : (a : l₂ ⟶ l₂) → r₂ ⟶ r₂) (α.hom ≫ α.inv) : r₂ ⟶ r₂) (𝟙 r₂ : r₂ ⟶ r₂)
rw₁ : Eq (α := r₂ ⟶ r₂) ((conjugateEquiv adj₂ adj₂ : (a : l₂ ⟶ l₂) → r₂ ⟶ r₂) (𝟙 l₂) : r₂ ⟶ r₂) (𝟙 r₂ : r₂ ⟶ r₂)
rw₂ rw₃ : 𝟙 r₂ = 𝟙 r₂
⊢ Eq (α := r₂ ⟶ r₂)
    (CategoryStruct.comp (Y := r₁) ((conjugateEquiv adj₂ adj₁ : (a : l₁ ⟶ l₂) → r₂ ⟶ r₁) α.inv)
        ((conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α.hom) :
      r₂ ⟶ r₂)
    (𝟙 r₂ : r₂ ⟶ r₂)

Tactic:
rw [conjugateEquiv_comp, Iso.hom_inv_id, conjugateEquiv_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Bicategory.conjugateEquiv_id, CategoryTheory.Bicategory.conjugateEquiv_comp
-- 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 :
  Eq (α := l₂ ⟶ l₂) (((conjugateEquiv adj₂ adj₂).symm : (a : r₂ ⟶ r₂) → l₂ ⟶ l₂) (β.inv ≫ β.hom) : l₂ ⟶ l₂)
    (𝟙 l₂ : l₂ ⟶ l₂)
rw₁ : Eq (α := l₂ ⟶ l₂) (((conjugateEquiv adj₂ adj₂).symm : (a : r₂ ⟶ r₂) → l₂ ⟶ l₂) (𝟙 r₂) : l₂ ⟶ l₂) (𝟙 l₂ : l₂ ⟶ l₂)
rw₂ rw₃ : 𝟙 l₂ = 𝟙 l₂
⊢ Eq (α := l₂ ⟶ l₂)
    (CategoryStruct.comp (Y := l₁) (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) β.hom)
        (((conjugateEquiv adj₂ adj₁).symm : (a : r₂ ⟶ r₁) → l₁ ⟶ l₂) β.inv) :
      l₂ ⟶ l₂)
    (𝟙 l₂ : l₂ ⟶ l₂)

Tactic:
rw [conjugateEquiv_symm_comp, Iso.inv_hom_id, conjugateEquiv_symm_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Bicategory.conjugateEquiv_symm_id, CategoryTheory.Bicategory.conjugateEquiv_symm_comp
-- 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 :
  Eq (α := l₁ ⟶ l₁) (((conjugateEquiv adj₁ adj₁).symm : (a : r₁ ⟶ r₁) → l₁ ⟶ l₁) (β.hom ≫ β.inv) : l₁ ⟶ l₁)
    (𝟙 l₁ : l₁ ⟶ l₁)
rw₁ : Eq (α := l₁ ⟶ l₁) (((conjugateEquiv adj₁ adj₁).symm : (a : r₁ ⟶ r₁) → l₁ ⟶ l₁) (𝟙 r₁) : l₁ ⟶ l₁) (𝟙 l₁ : l₁ ⟶ l₁)
rw₂ rw₃ : 𝟙 l₁ = 𝟙 l₁
⊢ Eq (α := l₁ ⟶ l₁)
    (CategoryStruct.comp (Y := l₂) (((conjugateEquiv adj₂ adj₁).symm : (a : r₂ ⟶ r₁) → l₁ ⟶ l₂) β.inv)
        (((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) β.hom) :
      l₁ ⟶ l₁)
    (𝟙 l₁ : l₁ ⟶ l₁)

Tactic:
rw [conjugateEquiv_symm_comp, Iso.hom_inv_id, conjugateEquiv_symm_id]

Premises used: CategoryTheory.Bicategory.conjugateEquiv_symm_id, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Bicategory.conjugateEquiv_symm_comp
-- 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₁
⊢ (fun (β : r₁ ≅ r₂) ↦
        ({ hom := ((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) β.hom,
            inv := ((conjugateEquiv adj₂ adj₁).symm : (a : r₂ ⟶ r₁) → l₁ ⟶ l₂) β.inv, hom_inv_id := ⋯,
            inv_hom_id := ⋯ } :
          l₂ ≅ l₁))
      ((fun (α : l₂ ≅ l₁) ↦
          ({ hom := (conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α.hom,
              inv := (conjugateEquiv adj₂ adj₁ : (a : l₁ ⟶ l₂) → r₂ ⟶ r₁) α.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ } :
            r₁ ≅ r₂))
        α) =
    α

Tactic:
simp only [Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_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₂
⊢ (fun (α : l₂ ≅ l₁) ↦
        ({ hom := (conjugateEquiv adj₁ adj₂ : (a : l₂ ⟶ l₁) → r₁ ⟶ r₂) α.hom,
            inv := (conjugateEquiv adj₂ adj₁ : (a : l₁ ⟶ l₂) → r₂ ⟶ r₁) α.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ } :
          r₁ ≅ r₂))
      ((fun (β : r₁ ≅ r₂) ↦
          ({ hom := ((conjugateEquiv adj₁ adj₂).symm : (a : r₁ ⟶ r₂) → l₂ ⟶ l₁) β.hom,
              inv := ((conjugateEquiv adj₂ adj₁).symm : (a : r₂ ⟶ r₁) → l₁ ⟶ l₂) β.inv, hom_inv_id := ⋯,
              inv_hom_id := ⋯ } :
            l₂ ≅ l₁))
        α) =
    α

Tactic:
simp only [Equiv.apply_symm_apply]

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

Tactic:
simp only [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
a b c d : B
f₁ : a ⟶ c
u₁ : c ⟶ a
f₂ : b ⟶ d
u₂ : d ⟶ b
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : f₁ ⊣ u₁
adj₄ : f₂ ⊣ u₂
α : f₁ ≫ l₂ ⟶ l₁ ≫ f₂
dsimp :
  𝟙 (u₂ ≫ r₁) ⊗≫
      u₂ ◁ r₁ ◁ adj₃.unit ⊗≫
        u₂ ◁ (𝟙 (r₁ ≫ f₁) ⊗≫ r₁ ◁ f₁ ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ f₂ ▷ r₂ ⊗≫ 𝟙 (f₂ ≫ r₂)) ▷ u₁ ⊗≫
          adj₄.counit ▷ r₂ ▷ u₁ ⊗≫ 𝟙 (r₂ ≫ u₁) =
    (ρ_ (u₂ ≫ r₁)).inv ≫
      bicategoricalComp (h := (u₂ ≫ r₁) ≫ 𝟙 a ≫ 𝟙 a) (𝟙 ((u₂ ≫ r₁) ≫ 𝟙 a))
          ((u₂ ≫ r₁) ◁ 𝟙 a ◁ (adj₃.unit ⊗≫ f₁ ◁ adj₂.unit ▷ u₁ ⊗≫ 𝟙 ((f₁ ≫ l₂) ≫ r₂ ≫ u₁)) ⊗≫
            (u₂ ≫ r₁) ◁ ((λ_ (f₁ ≫ l₂)).hom ≫ α ≫ (ρ_ (l₁ ≫ f₂)).inv) ▷ (r₂ ≫ u₁) ⊗≫
              (𝟙 ((u₂ ≫ r₁) ≫ l₁ ≫ f₂) ⊗≫ u₂ ◁ adj₁.counit ▷ f₂ ⊗≫ adj₄.counit) ▷ 𝟙 d ▷ (r₂ ≫ u₁) ⊗≫
                𝟙 (𝟙 d ≫ r₂ ≫ u₁)) ≫
        (λ_ (r₂ ≫ u₁)).hom
⊢ 𝟙 (u₂ ≫ r₁) ⊗≫
      u₂ ◁ r₁ ◁ adj₃.unit ⊗≫
        u₂ ◁ (𝟙 (r₁ ≫ f₁) ⊗≫ r₁ ◁ f₁ ◁ adj₂.unit ⊗≫ r₁ ◁ α ▷ r₂ ⊗≫ adj₁.counit ▷ f₂ ▷ r₂ ⊗≫ 𝟙 (f₂ ≫ r₂)) ▷ u₁ ⊗≫
          adj₄.counit ▷ r₂ ▷ u₁ ⊗≫ 𝟙 (r₂ ≫ u₁) =
    (ρ_ (u₂ ≫ r₁)).inv ≫
      bicategoricalComp (h := (u₂ ≫ r₁) ≫ 𝟙 a ≫ 𝟙 a) (𝟙 ((u₂ ≫ r₁) ≫ 𝟙 a))
          ((u₂ ≫ r₁) ◁ 𝟙 a ◁ (adj₃.comp adj₂).unit ⊗≫
            (u₂ ≫ r₁) ◁ ((λ_ (f₁ ≫ l₂)).hom ≫ α ≫ (ρ_ (l₁ ≫ f₂)).inv) ▷ (r₂ ≫ u₁) ⊗≫
              (adj₁.comp adj₄).counit ▷ 𝟙 d ▷ (r₂ ≫ u₁) ⊗≫ 𝟙 (𝟙 d ≫ r₂ ≫ u₁)) ≫
        (λ_ (r₂ ≫ u₁)).hom

Tactic:
dsimp [Adjunction.comp]

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

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f₁ : a ⟶ c
u₁ : c ⟶ a
f₂ : b ⟶ d
u₂ : d ⟶ b
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : f₁ ⊣ u₁
adj₄ : f₂ ⊣ u₂
α : u₂ ≫ r₁ ⟶ r₂ ≫ u₁
rw :
  (mateEquiv adj₄ adj₃ : (a_1 : r₁ ≫ f₁ ⟶ f₂ ≫ r₂) → u₂ ≫ r₁ ⟶ r₂ ≫ u₁)
      ((mateEquiv adj₁ adj₂ : (a_1 : f₁ ≫ l₂ ⟶ l₁ ≫ f₂) → r₁ ≫ f₁ ⟶ f₂ ≫ r₂)
          ((Equiv.symm (mateEquiv adj₁ adj₂) : (a_1 : r₁ ≫ f₁ ⟶ f₂ ≫ r₂) → f₁ ≫ l₂ ⟶ l₁ ≫ f₂)
              ((Equiv.symm (mateEquiv adj₄ adj₃) : (a_1 : u₂ ≫ r₁ ⟶ r₂ ≫ u₁) → r₁ ≫ f₁ ⟶ f₂ ≫ r₂) α :
                r₁ ≫ f₁ ⟶ f₂ ≫ r₂) :
            f₁ ≫ l₂ ⟶ l₁ ≫ f₂) :
        r₁ ≫ f₁ ⟶ f₂ ≫ r₂) =
    α
⊢ Eq (α := f₁ ≫ l₂ ⟶ l₁ ≫ f₂)
    ((Equiv.symm (mateEquiv adj₁ adj₂) : (a_1 : r₁ ≫ f₁ ⟶ f₂ ≫ r₂) → f₁ ≫ l₂ ⟶ l₁ ≫ f₂)
        ((Equiv.symm (mateEquiv adj₄ adj₃) : (a_1 : u₂ ≫ r₁ ⟶ r₂ ≫ u₁) → r₁ ≫ f₁ ⟶ f₂ ≫ r₂) α : r₁ ≫ f₁ ⟶ f₂ ≫ r₂) :
      f₁ ≫ l₂ ⟶ l₁ ≫ f₂)
    (((conjugateEquiv (adj₁.comp adj₄) (adj₃.comp adj₂)).symm : (a_1 : u₂ ≫ r₁ ⟶ r₂ ≫ u₁) → f₁ ≫ l₂ ⟶ l₁ ≫ f₂) α :
      f₁ ≫ l₂ ⟶ l₁ ≫ f₂)

Tactic:
rw [Equiv.eq_symm_apply, ← iterated_mateEquiv_conjugateEquiv]

Premises used: CategoryTheory.Bicategory.iterated_mateEquiv_conjugateEquiv, Equiv.eq_symm_apply
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f₁ : a ⟶ c
u₁ : c ⟶ a
f₂ : b ⟶ d
u₂ : d ⟶ b
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : f₁ ⊣ u₁
adj₄ : f₂ ⊣ u₂
α : u₂ ≫ r₁ ⟶ r₂ ≫ u₁
⊢ (mateEquiv adj₄ adj₃ : (a_1 : r₁ ≫ f₁ ⟶ f₂ ≫ r₂) → u₂ ≫ r₁ ⟶ r₂ ≫ u₁)
      ((mateEquiv adj₁ adj₂ : (a_1 : f₁ ≫ l₂ ⟶ l₁ ≫ f₂) → r₁ ≫ f₁ ⟶ f₂ ≫ r₂)
          ((Equiv.symm (mateEquiv adj₁ adj₂) : (a_1 : r₁ ≫ f₁ ⟶ f₂ ≫ r₂) → f₁ ≫ l₂ ⟶ l₁ ≫ f₂)
              ((Equiv.symm (mateEquiv adj₄ adj₃) : (a_1 : u₂ ≫ r₁ ⟶ r₂ ≫ u₁) → r₁ ≫ f₁ ⟶ f₂ ≫ r₂) α :
                r₁ ≫ f₁ ⟶ f₂ ≫ r₂) :
            f₁ ≫ l₂ ⟶ l₁ ≫ f₂) :
        r₁ ≫ f₁ ⟶ f₂ ≫ r₂) =
    α

Tactic:
simp only [Equiv.apply_symm_apply]

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : c ⟶ d
r₂ : d ⟶ c
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : g ≫ l₂ ⟶ l₁ ≫ h
β : l₃ ⟶ l₂
symm :
  Eq.{w + 1} (α := r₁ ≫ g ⟶ h ≫ r₃)
    (rightAdjointSquareConjugate.vcomp (r₂ := r₂) ((mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α)
      ((conjugateEquiv adj₂ adj₃ : (a : l₃ ⟶ l₂) → r₂ ⟶ r₃) β))
    ((mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointSquareConjugate.vcomp α β))
⊢ Eq (α := r₁ ≫ g ⟶ h ≫ r₃)
    ((mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointSquareConjugate.vcomp α β) :
      r₁ ≫ g ⟶ h ≫ r₃)
    (rightAdjointSquareConjugate.vcomp (r₂ := r₂) ((mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α)
        ((conjugateEquiv adj₂ adj₃ : (a : l₃ ⟶ l₂) → r₂ ⟶ r₃) β) :
      r₁ ≫ g ⟶ h ≫ r₃)

Tactic:
symm