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 : 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₂
dsimp :
  (mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α ≫
      h ◁
        ((ρ_ r₂).inv ≫
          (mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫
            (λ_ r₃).hom) =
    𝟙 (r₁ ≫ g) ⊗≫
      ((α_ r₁ g (𝟙 c)).inv ≫
          (mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α ▷ 𝟙 c ≫
            (α_ h r₂ (𝟙 c)).hom ≫
              h ◁
                  (mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃)
                    ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫
                (α_ h (𝟙 d) r₃).inv) ⊗≫
        𝟙 (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₃) β) =
    bicategoricalComp (h := r₁ ≫ g ≫ 𝟙 c) (𝟙 (r₁ ≫ g))
      (bicategoricalComp (g := (h ≫ 𝟙 d) ≫ r₃)
        (rightAdjointSquare.vcomp (r₂ := r₂) ((mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α)
          ((mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
        (𝟙 (h ≫ r₃)))

Tactic:
dsimp only [conjugateEquiv_apply, rightAdjointSquareConjugate.vcomp,
        rightAdjointSquare.vcomp]

Premises used: CategoryTheory.Bicategory.rightAdjointSquareConjugate.vcomp, CategoryTheory.Bicategory.conjugateEquiv_apply, CategoryTheory.Bicategory.rightAdjointSquare.vcomp
-- 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₂
⊢ (mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α ≫
      h ◁
        ((ρ_ r₂).inv ≫
          (mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫
            (λ_ r₃).hom) =
    𝟙 (r₁ ≫ g) ⊗≫
      ((α_ r₁ g (𝟙 c)).inv ≫
          (mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α ▷ 𝟙 c ≫
            (α_ h r₂ (𝟙 c)).hom ≫
              h ◁
                  (mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃)
                    ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫
                (α_ h (𝟙 d) r₃).inv) ⊗≫
        𝟙 (h ≫ r₃)

Tactic:
bicategory
-- 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₂
rw :
  bicategoricalComp (h := r₁ ≫ g ≫ 𝟙 c) (𝟙 (r₁ ≫ g))
      (bicategoricalComp (g := (h ≫ 𝟙 d) ≫ r₃)
        ((mateEquiv adj₁ adj₃ : (a_1 : (g ≫ 𝟙 c) ≫ l₃ ⟶ l₁ ≫ h ≫ 𝟙 d) → r₁ ≫ g ≫ 𝟙 c ⟶ (h ≫ 𝟙 d) ≫ r₃)
          (leftAdjointSquare.vcomp α ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
        (𝟙 (h ≫ r₃))) =
    (mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointSquareConjugate.vcomp α β)
⊢ bicategoricalComp (h := r₁ ≫ g ≫ 𝟙 c) (𝟙 (r₁ ≫ g))
      (bicategoricalComp (g := (h ≫ 𝟙 d) ≫ r₃)
        (rightAdjointSquare.vcomp (r₂ := r₂) ((mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α)
          ((mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
        (𝟙 (h ≫ r₃))) =
    (mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointSquareConjugate.vcomp α β)

Tactic:
rw [← mateEquiv_vcomp]

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

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

Premises used: CategoryTheory.Bicategory.leftAdjointSquareConjugate.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 : 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₂
⊢ 𝟙 (r₁ ≫ g) ⊗≫
      (𝟙 (r₁ ≫ g ≫ 𝟙 c) ⊗≫
          r₁ ◁ (g ≫ 𝟙 c) ◁ adj₃.unit ⊗≫
            r₁ ◁
                ((α_ g (𝟙 c) l₃).hom ≫
                    g ◁ ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv) ≫ (α_ g l₂ (𝟙 d)).inv ≫ α ▷ 𝟙 d ≫ (α_ l₁ h (𝟙 d)).hom) ▷
                  r₃ ⊗≫
              adj₁.counit ▷ (h ≫ 𝟙 d) ▷ r₃ ⊗≫ 𝟙 ((h ≫ 𝟙 d) ≫ r₃)) ⊗≫
        𝟙 (h ≫ r₃) =
    𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₃.unit ⊗≫ r₁ ◁ (g ◁ β ≫ α) ▷ 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
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₂
_ :
  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₃) β) =
    bicategoricalComp (h := r₁ ≫ g ≫ 𝟙 c) (𝟙 (r₁ ≫ g))
      (bicategoricalComp (g := (h ≫ 𝟙 d) ≫ r₃)
        (rightAdjointSquare.vcomp (r₂ := r₂) ((mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α)
          ((mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
        (𝟙 (h ≫ r₃)))
_₁ :
  bicategoricalComp (h := r₁ ≫ g ≫ 𝟙 c) (𝟙 (r₁ ≫ g))
      (bicategoricalComp (g := (h ≫ 𝟙 d) ≫ r₃)
        (rightAdjointSquare.vcomp (r₂ := r₂) ((mateEquiv adj₁ adj₂ : (a_1 : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α)
          ((mateEquiv adj₂ adj₃ : (a : 𝟙 c ≫ l₃ ⟶ l₂ ≫ 𝟙 d) → r₂ ≫ 𝟙 c ⟶ 𝟙 d ≫ r₃) ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)))
        (𝟙 (h ≫ r₃))) =
    (mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointSquareConjugate.vcomp α β)
⊢ 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 α β))

Tactic:
calc
    _ = 𝟙 _ ⊗≫
          rightAdjointSquare.vcomp
            (mateEquiv adj₁ adj₂ α)
            (mateEquiv adj₂ adj₃ ((λ_ l₃).hom ≫ β ≫ (ρ_ l₂).inv)) ⊗≫ 𝟙 _ := by
      dsimp only [conjugateEquiv_apply, rightAdjointSquareConjugate.vcomp,
        rightAdjointSquare.vcomp]
      bicategory
    _ = _ := by
      rw [← mateEquiv_vcomp]
      simp only [leftAdjointSquare.vcomp, mateEquiv_apply', leftAdjointSquareConjugate.vcomp]
      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
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : a ⟶ b
r₂ : b ⟶ a
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : g ≫ l₃ ⟶ l₂ ≫ h
symm :
  Eq.{w + 1} (α := r₁ ≫ g ⟶ h ≫ r₃)
    (rightAdjointConjugateSquare.vcomp (r₂ := r₂) ((conjugateEquiv adj₁ adj₂ : (a_1 : l₂ ⟶ l₁) → r₁ ⟶ r₂) α)
      ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β))
    ((mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointConjugateSquare.vcomp α β))
⊢ Eq (α := r₁ ≫ g ⟶ h ≫ r₃)
    ((mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointConjugateSquare.vcomp α β) :
      r₁ ≫ g ⟶ h ≫ r₃)
    (rightAdjointConjugateSquare.vcomp (r₂ := r₂) ((conjugateEquiv adj₁ adj₂ : (a_1 : l₂ ⟶ l₁) → r₁ ⟶ r₂) α)
        ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β) :
      r₁ ≫ g ⟶ h ≫ r₃)

Tactic:
symm
-- 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₂ : a ⟶ b
r₂ : b ⟶ a
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : g ≫ l₃ ⟶ l₂ ≫ h
dsimp :
  CategoryStruct.comp (Y := r₂ ≫ g)
      (((ρ_ r₁).inv ≫
          (mateEquiv adj₁ adj₂ : (a_1 : 𝟙 a ≫ l₂ ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ≫
            (λ_ r₂).hom) ▷
        g)
      ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β) =
    𝟙 (r₁ ≫ g) ⊗≫
      bicategoricalComp (g := (𝟙 b ≫ h) ≫ r₃)
        ((α_ r₁ (𝟙 a) g).inv ≫
          (mateEquiv adj₁ adj₂ : (a_1 : 𝟙 a ≫ l₂ ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ▷
              g ≫
            Iso.hom (α_ (𝟙 b) r₂ g) ≫
              𝟙 b ◁ (mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β ≫ Iso.inv (α_ (𝟙 b) h r₃))
        (𝟙 (h ≫ r₃))
⊢ rightAdjointConjugateSquare.vcomp (r₂ := r₂) ((conjugateEquiv adj₁ adj₂ : (a_1 : l₂ ⟶ l₁) → r₁ ⟶ r₂) α)
      ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β) =
    bicategoricalComp (h := r₁ ≫ 𝟙 a ≫ g) (𝟙 (r₁ ≫ g))
      (bicategoricalComp (g := (𝟙 b ≫ h) ≫ r₃)
        (rightAdjointSquare.vcomp (r₂ := r₂)
          ((mateEquiv adj₁ adj₂ : (a_1 : 𝟙 a ≫ l₂ ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
          ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β))
        (𝟙 (h ≫ r₃)))

Tactic:
dsimp only [conjugateEquiv_apply, rightAdjointConjugateSquare.vcomp, rightAdjointSquare.vcomp]

Premises used: CategoryTheory.Bicategory.rightAdjointConjugateSquare.vcomp, CategoryTheory.Bicategory.conjugateEquiv_apply, CategoryTheory.Bicategory.rightAdjointSquare.vcomp
-- 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₂ : a ⟶ b
r₂ : b ⟶ a
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : g ≫ l₃ ⟶ l₂ ≫ h
⊢ CategoryStruct.comp (Y := r₂ ≫ g)
      (((ρ_ r₁).inv ≫
          (mateEquiv adj₁ adj₂ : (a_1 : 𝟙 a ≫ l₂ ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ≫
            (λ_ r₂).hom) ▷
        g)
      ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β) =
    𝟙 (r₁ ≫ g) ⊗≫
      bicategoricalComp (g := (𝟙 b ≫ h) ≫ r₃)
        ((α_ r₁ (𝟙 a) g).inv ≫
          (mateEquiv adj₁ adj₂ : (a_1 : 𝟙 a ≫ l₂ ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ▷
              g ≫
            Iso.hom (α_ (𝟙 b) r₂ g) ≫
              𝟙 b ◁ (mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β ≫ Iso.inv (α_ (𝟙 b) h r₃))
        (𝟙 (h ≫ r₃))

Tactic:
bicategory
-- 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₂ : a ⟶ b
r₂ : b ⟶ a
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : g ≫ l₃ ⟶ l₂ ≫ h
rw :
  bicategoricalComp (h := r₁ ≫ 𝟙 a ≫ g) (𝟙 (r₁ ≫ g))
      (bicategoricalComp (g := (𝟙 b ≫ h) ≫ r₃)
        ((mateEquiv adj₁ adj₃ : (a_1 : (𝟙 a ≫ g) ≫ l₃ ⟶ l₁ ≫ 𝟙 b ≫ h) → r₁ ≫ 𝟙 a ≫ g ⟶ (𝟙 b ≫ h) ≫ r₃)
          (leftAdjointSquare.vcomp ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) β))
        (𝟙 (h ≫ r₃))) =
    (mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointConjugateSquare.vcomp α β)
⊢ bicategoricalComp (h := r₁ ≫ 𝟙 a ≫ g) (𝟙 (r₁ ≫ g))
      (bicategoricalComp (g := (𝟙 b ≫ h) ≫ r₃)
        (rightAdjointSquare.vcomp (r₂ := r₂)
          ((mateEquiv adj₁ adj₂ : (a_1 : 𝟙 a ≫ l₂ ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
          ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β))
        (𝟙 (h ≫ r₃))) =
    (mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointConjugateSquare.vcomp α β)

Tactic:
rw [← mateEquiv_vcomp]

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

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

Premises used: CategoryTheory.Bicategory.leftAdjointConjugateSquare.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 : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : a ⟶ b
r₂ : b ⟶ a
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : g ≫ l₃ ⟶ l₂ ≫ h
⊢ 𝟙 (r₁ ≫ g) ⊗≫
      (𝟙 (r₁ ≫ 𝟙 a ≫ g) ⊗≫
          bicategoricalComp (h := r₁ ≫ ((𝟙 a ≫ g) ≫ l₃) ≫ r₃) (r₁ ◁ (𝟙 a ≫ g) ◁ adj₃.unit)
            (r₁ ◁
                (Iso.hom (α_ (𝟙 a) g l₃) ≫
                    𝟙 a ◁ β ≫ Iso.inv (α_ (𝟙 a) l₂ h) ≫ ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv) ▷ h ≫ (α_ l₁ (𝟙 b) h).hom) ▷
                  r₃ ⊗≫
              adj₁.counit ▷ (𝟙 b ≫ h) ▷ r₃ ⊗≫ 𝟙 ((𝟙 b ≫ h) ≫ r₃))) ⊗≫
        𝟙 (h ≫ r₃) =
    𝟙 (r₁ ≫ g) ⊗≫ r₁ ◁ g ◁ adj₃.unit ⊗≫ r₁ ◁ (β ≫ α ▷ h) ▷ 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
a b c d : B
g : a ⟶ c
h : b ⟶ d
l₁ : a ⟶ b
r₁ : b ⟶ a
l₂ : a ⟶ b
r₂ : b ⟶ a
l₃ : c ⟶ d
r₃ : d ⟶ c
adj₁ : l₁ ⊣ r₁
adj₂ : l₂ ⊣ r₂
adj₃ : l₃ ⊣ r₃
α : l₂ ⟶ l₁
β : g ≫ l₃ ⟶ l₂ ≫ h
_ :
  rightAdjointConjugateSquare.vcomp (r₂ := r₂) ((conjugateEquiv adj₁ adj₂ : (a_1 : l₂ ⟶ l₁) → r₁ ⟶ r₂) α)
      ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β) =
    bicategoricalComp (h := r₁ ≫ 𝟙 a ≫ g) (𝟙 (r₁ ≫ g))
      (bicategoricalComp (g := (𝟙 b ≫ h) ≫ r₃)
        (rightAdjointSquare.vcomp (r₂ := r₂)
          ((mateEquiv adj₁ adj₂ : (a_1 : 𝟙 a ≫ l₂ ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
          ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β))
        (𝟙 (h ≫ r₃)))
_₁ :
  bicategoricalComp (h := r₁ ≫ 𝟙 a ≫ g) (𝟙 (r₁ ≫ g))
      (bicategoricalComp (g := (𝟙 b ≫ h) ≫ r₃)
        (rightAdjointSquare.vcomp (r₂ := r₂)
          ((mateEquiv adj₁ adj₂ : (a_1 : 𝟙 a ≫ l₂ ⟶ l₁ ≫ 𝟙 b) → r₁ ≫ 𝟙 a ⟶ 𝟙 b ≫ r₂) ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
          ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β))
        (𝟙 (h ≫ r₃))) =
    (mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointConjugateSquare.vcomp α β)
⊢ Eq.{w + 1} (α := r₁ ≫ g ⟶ h ≫ r₃)
    (rightAdjointConjugateSquare.vcomp (r₂ := r₂) ((conjugateEquiv adj₁ adj₂ : (a_1 : l₂ ⟶ l₁) → r₁ ⟶ r₂) α)
      ((mateEquiv adj₂ adj₃ : (a_1 : g ≫ l₃ ⟶ l₂ ≫ h) → r₂ ≫ g ⟶ h ≫ r₃) β))
    ((mateEquiv adj₁ adj₃ : (a_1 : g ≫ l₃ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₃) (leftAdjointConjugateSquare.vcomp α β))

Tactic:
calc
    _ = 𝟙 _ ⊗≫
          rightAdjointSquare.vcomp
            (mateEquiv adj₁ adj₂ ((λ_ l₂).hom ≫ α ≫ (ρ_ l₁).inv))
            (mateEquiv adj₂ adj₃ β) ⊗≫ 𝟙 _ := by
      dsimp only [conjugateEquiv_apply, rightAdjointConjugateSquare.vcomp, rightAdjointSquare.vcomp]
      bicategory
    _ = _ := by
      rw [← mateEquiv_vcomp]
      simp only [leftAdjointSquare.vcomp, mateEquiv_apply', leftAdjointConjugateSquare.vcomp]
      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.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
rw : f ◁ (η.hom ≫ η.inv) = 𝟙 (f ≫ g)
rw₁ : f ◁ 𝟙 g = 𝟙 (f ≫ g)
rw₂ rw₃ : 𝟙 (f ≫ g) = 𝟙 (f ≫ g)
⊢ f ◁ η.hom ≫ f ◁ η.inv = 𝟙 (f ≫ g)

Tactic:
rw [← whiskerLeft_comp, hom_inv_id, whiskerLeft_id]

Premises used: CategoryTheory.Bicategory.whiskerLeft_comp, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Bicategory.whiskerLeft_id
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
rw : (η.hom ≫ η.inv) ▷ h = 𝟙 (f ≫ h)
rw₁ : 𝟙 f ▷ h = 𝟙 (f ≫ h)
rw₂ rw₃ : 𝟙 (f ≫ h) = 𝟙 (f ≫ h)
⊢ η.hom ▷ h ≫ η.inv ▷ h = 𝟙 (f ≫ h)

Tactic:
rw [← comp_whiskerRight, hom_inv_id, id_whiskerRight]

Premises used: CategoryTheory.Bicategory.comp_whiskerRight, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Bicategory.id_whiskerRight
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
rw : f ◁ (η.inv ≫ η.hom) = 𝟙 (f ≫ h)
rw₁ : f ◁ 𝟙 h = 𝟙 (f ≫ h)
rw₂ rw₃ : 𝟙 (f ≫ h) = 𝟙 (f ≫ h)
⊢ f ◁ η.inv ≫ f ◁ η.hom = 𝟙 (f ≫ h)

Tactic:
rw [← whiskerLeft_comp, inv_hom_id, whiskerLeft_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Bicategory.whiskerLeft_comp, CategoryTheory.Bicategory.whiskerLeft_id
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
rw : (η.inv ≫ η.hom) ▷ h = 𝟙 (g ≫ h)
rw₁ : 𝟙 g ▷ h = 𝟙 (g ≫ h)
rw₂ rw₃ : 𝟙 (g ≫ h) = 𝟙 (g ≫ h)
⊢ η.inv ▷ h ≫ η.hom ▷ h = 𝟙 (g ≫ h)

Tactic:
rw [← comp_whiskerRight, inv_hom_id, id_whiskerRight]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Bicategory.comp_whiskerRight, CategoryTheory.Bicategory.id_whiskerRight
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h k : c ⟶ d
η : h ≅ k
⊢ f ◁ g ◁ η.hom ≫ f ◁ g ◁ η.inv = 𝟙 (f ≫ g ≫ h)

Tactic:
simp [← whiskerLeft_comp]

Premises used: CategoryTheory.Bicategory.whiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
k : c ⟶ d
⊢ η.hom ▷ h ▷ k ≫ η.inv ▷ h ▷ k = 𝟙 ((f ≫ h) ≫ k)

Tactic:
simp [← comp_whiskerRight]

Premises used: CategoryTheory.Bicategory.comp_whiskerRight
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f : a ⟶ b
g : b ⟶ c
h k : c ⟶ d
η : h ≅ k
⊢ f ◁ g ◁ η.inv ≫ f ◁ g ◁ η.hom = 𝟙 (f ≫ g ≫ k)

Tactic:
simp [← whiskerLeft_comp]

Premises used: CategoryTheory.Bicategory.whiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f g : a ⟶ b
η : f ≅ g
h : b ⟶ c
k : c ⟶ d
⊢ η.inv ▷ h ▷ k ≫ η.hom ▷ h ▷ k = 𝟙 ((g ≫ h) ≫ k)

Tactic:
simp [← comp_whiskerRight]

Premises used: CategoryTheory.Bicategory.comp_whiskerRight
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
k : c ⟶ d
⊢ f ◁ η.hom ▷ k ≫ f ◁ η.inv ▷ k = 𝟙 (f ≫ g ≫ k)

Tactic:
simp [← whiskerLeft_comp]

Premises used: CategoryTheory.Bicategory.whiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
k : c ⟶ d
⊢ f ◁ η.inv ▷ k ≫ f ◁ η.hom ▷ k = 𝟙 (f ≫ h ≫ k)

Tactic:
simp [← whiskerLeft_comp]

Premises used: CategoryTheory.Bicategory.whiskerLeft_comp
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d e : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
inst_1 : IsIso η
⊢ IsIso (f ◁ η)

Tactic:
(whiskerLeftIso f (asIso η)).isIso_hom

Premises used: CategoryTheory.Bicategory.whiskerLeftIso, CategoryTheory.Iso.isIso_hom, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
inst_1 : IsIso η
hom_inv_id : f ◁ η ≫ f ◁ inv η = 𝟙 (f ≫ g)
⊢ inv (f ◁ η) = f ◁ inv η

Tactic:
apply IsIso.inv_eq_of_hom_inv_id

Premises used: CategoryTheory.IsIso.inv_eq_of_hom_inv_id
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
inst_1 : IsIso η
⊢ f ◁ η ≫ f ◁ inv η = 𝟙 (f ≫ g)

Tactic:
simp only [← whiskerLeft_comp, whiskerLeft_id, IsIso.hom_inv_id]

Premises used: CategoryTheory.Bicategory.whiskerLeft_comp, CategoryTheory.Bicategory.whiskerLeft_id, CategoryTheory.IsIso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d e : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
inst_1 : IsIso η
⊢ IsIso (η ▷ h)

Tactic:
(whiskerRightIso (asIso η) h).isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, CategoryTheory.Bicategory.whiskerRightIso, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
inst_1 : IsIso η
hom_inv_id : η ▷ h ≫ inv η ▷ h = 𝟙 (f ≫ h)
⊢ inv (η ▷ h) = inv η ▷ h

Tactic:
apply IsIso.inv_eq_of_hom_inv_id

Premises used: CategoryTheory.IsIso.inv_eq_of_hom_inv_id
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f g : a ⟶ b
η : f ⟶ g
h : b ⟶ c
inst_1 : IsIso η
⊢ η ▷ h ≫ inv η ▷ h = 𝟙 (f ≫ h)

Tactic:
simp only [← comp_whiskerRight, id_whiskerRight, IsIso.hom_inv_id]

Premises used: CategoryTheory.Bicategory.comp_whiskerRight, CategoryTheory.Bicategory.id_whiskerRight, CategoryTheory.IsIso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Bicategory.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv (f ◁ (α_ g h i).inv ≫ (α_ f (g ≫ h) i).inv ≫ (α_ f g h).inv ▷ i) =
    inv ((α_ f g (h ≫ i)).inv ≫ (α_ (f ≫ g) h i).inv)

Tactic:
simp