awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
Goal:
C D : Cat
F : C ⟶ D
G : D ⟶ C
adj : F ⊣ G
⊢ (ofCat adj).toCat = adj

Tactic:
rfl

Premises used: CategoryTheory.Functor.toCatHom, CategoryTheory.Cat.of, CategoryTheory.Cat, CategoryTheory.Bundled.of, rfl, CategoryTheory.Adjunction.toCat
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
Goal:
C D : Type u
inst : Category.{v, u} C
inst_1 : Category.{v, u} D
F : Functor.{v, v, u, u} C D
G : Functor.{v, v, u, u} D C
adj : F ⊣ G
⊢ ofCat adj.toCat = adj

Tactic:
rfl

Premises used: CategoryTheory.Adjunction.ofCat, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
Goal:
C : Cat
⊢ Adjunction.ofCat (id C) = CategoryTheory.Adjunction.id

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.id, CategoryTheory.Adjunction.ofCat, CategoryTheory.NatTrans.id, CategoryTheory.Adjunction.id, rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
Goal:
C D E : Cat
F : C ⟶ D
G : D ⟶ C
adj : F ⊣ G
F' : D ⟶ E
G' : E ⟶ D
adj' : F' ⊣ G'
h :
  ∀ (x : (↑C : Type u)),
    (Adjunction.ofCat (adj.comp adj')).unit.app x = ((Adjunction.ofCat adj).comp (Adjunction.ofCat adj')).unit.app x
⊢ Adjunction.ofCat (adj.comp adj') = (Adjunction.ofCat adj).comp (Adjunction.ofCat adj')

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
Goal:
C D E : Cat
F : C ⟶ D
G : D ⟶ C
adj : F ⊣ G
F' : D ⟶ E
G' : E ⟶ D
adj' : F' ⊣ G'
x : (↑C : Type u)
⊢ (Adjunction.ofCat (adj.comp adj')).unit.app x = ((Adjunction.ofCat adj).comp (Adjunction.ofCat adj')).unit.app x

Tactic:
simp [bicategoricalComp]

Premises used: CategoryTheory.bicategoricalComp
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
Goal:
C D E F : Cat
G : C ⟶ E
H : D ⟶ F
L₁ : C ⟶ D
R₁ : D ⟶ C
L₂ : E ⟶ F
R₂ : F ⟶ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ≫ L₂ ⟶ L₁ ≫ H
w :
  ∀ (X : (↑D : Type u_2)),
    Eq (α := (R₁ ≫ G).toFunctor.obj X ⟶ (H ≫ R₂).toFunctor.obj X)
      (NatTrans.app (Cat.Hom₂.toNatTrans ((mateEquiv adj₁ adj₂ : (a : G ≫ L₂ ⟶ L₁ ≫ H) → R₁ ≫ G ⟶ H ≫ R₂) f)) X)
      (NatTrans.app
        ((CategoryTheory.mateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
            (a : TwoSquare G.toFunctor L₁.toFunctor L₂.toFunctor H.toFunctor) →
              TwoSquare R₁.toFunctor H.toFunctor G.toFunctor R₂.toFunctor)
          f.toNatTrans)
        X)
⊢ Eq (α := (R₁ ≫ G).toFunctor ⟶ (H ≫ R₂).toFunctor)
    (Cat.Hom₂.toNatTrans ((mateEquiv adj₁ adj₂ : (a : G ≫ L₂ ⟶ L₁ ≫ H) → R₁ ≫ G ⟶ H ≫ R₂) f))
    ((CategoryTheory.mateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
        (a : TwoSquare G.toFunctor L₁.toFunctor L₂.toFunctor H.toFunctor) →
          TwoSquare R₁.toFunctor H.toFunctor G.toFunctor R₂.toFunctor)
      f.toNatTrans)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
Goal:
C D E F : Cat
G : C ⟶ E
H : D ⟶ F
L₁ : C ⟶ D
R₁ : D ⟶ C
L₂ : E ⟶ F
R₂ : F ⟶ E
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : G ≫ L₂ ⟶ L₁ ≫ H
X : (↑D : Type u_2)
⊢ Eq (α := (R₁ ≫ G).toFunctor.obj X ⟶ (H ≫ R₂).toFunctor.obj X)
    (NatTrans.app (Cat.Hom₂.toNatTrans ((mateEquiv adj₁ adj₂ : (a : G ≫ L₂ ⟶ L₁ ≫ H) → R₁ ≫ G ⟶ H ≫ R₂) f)) X)
    (NatTrans.app
      ((CategoryTheory.mateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
          (a : TwoSquare G.toFunctor L₁.toFunctor L₂.toFunctor H.toFunctor) →
            TwoSquare R₁.toFunctor H.toFunctor G.toFunctor R₂.toFunctor)
        f.toNatTrans)
      X)

Tactic:
simp [mateEquiv, Adjunction.homEquiv₁, Adjunction.homEquiv₂]

Premises used: CategoryTheory.Bicategory.Adjunction.homEquiv₁, CategoryTheory.Bicategory.mateEquiv, CategoryTheory.Bicategory.Adjunction.homEquiv₂
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
Goal:
C D : Cat
L₁ L₂ : C ⟶ D
R₁ R₂ : D ⟶ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : L₂ ⟶ L₁
dsimp :
  R₁.toFunctor.rightUnitor.inv ≫
      Cat.Hom₂.toNatTrans
          ((mateEquiv adj₁ adj₂ : (a : 𝟙 C ≫ L₂ ⟶ L₁ ≫ 𝟙 D) → R₁ ≫ 𝟙 C ⟶ 𝟙 D ≫ R₂) ((λ_ L₂).hom ≫ f ≫ (ρ_ L₁).inv)) ≫
        R₂.toFunctor.leftUnitor.hom =
    (CategoryTheory.conjugateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
        (a : L₂.toFunctor ⟶ L₁.toFunctor) → R₁.toFunctor ⟶ R₂.toFunctor)
      f.toNatTrans
⊢ Eq (α := R₁.toFunctor ⟶ R₂.toFunctor) (Cat.Hom₂.toNatTrans ((conjugateEquiv adj₁ adj₂ : (a : L₂ ⟶ L₁) → R₁ ⟶ R₂) f))
    ((CategoryTheory.conjugateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
        (a : L₂.toFunctor ⟶ L₁.toFunctor) → R₁.toFunctor ⟶ R₂.toFunctor)
      f.toNatTrans)

Tactic:
dsimp [Bicategory.conjugateEquiv]

Premises used: CategoryTheory.Bicategory.conjugateEquiv
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
Goal:
C D : Cat
L₁ L₂ : C ⟶ D
R₁ R₂ : D ⟶ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : L₂ ⟶ L₁
rw :
  Eq (α := R₁.toFunctor ⟶ R₂.toFunctor)
    (R₁.toFunctor.rightUnitor.inv ≫
      (CategoryTheory.mateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
            (a : TwoSquare (𝟙 C).toFunctor L₁.toFunctor L₂.toFunctor (𝟙 D).toFunctor) →
              TwoSquare R₁.toFunctor (𝟙 D).toFunctor (𝟙 C).toFunctor R₂.toFunctor)
          ((λ_ L₂).hom ≫ f ≫ (ρ_ L₁).inv).toNatTrans ≫
        R₂.toFunctor.leftUnitor.hom)
    ((CategoryTheory.conjugateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
        (a : L₂.toFunctor ⟶ L₁.toFunctor) → R₁.toFunctor ⟶ R₂.toFunctor)
      f.toNatTrans)
⊢ R₁.toFunctor.rightUnitor.inv ≫
      Cat.Hom₂.toNatTrans
          ((mateEquiv adj₁ adj₂ : (a : 𝟙 C ≫ L₂ ⟶ L₁ ≫ 𝟙 D) → R₁ ≫ 𝟙 C ⟶ 𝟙 D ≫ R₂) ((λ_ L₂).hom ≫ f ≫ (ρ_ L₁).inv)) ≫
        R₂.toFunctor.leftUnitor.hom =
    (CategoryTheory.conjugateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
        (a : L₂.toFunctor ⟶ L₁.toFunctor) → R₁.toFunctor ⟶ R₂.toFunctor)
      f.toNatTrans

Tactic:
rw [toNatTrans_mateEquiv]

Premises used: CategoryTheory.Bicategory.toNatTrans_mateEquiv
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
Goal:
C D : Cat
L₁ L₂ : C ⟶ D
R₁ R₂ : D ⟶ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : L₂ ⟶ L₁
w :
  ∀ (X : (↑D : Type u_2)),
    Eq (α := R₁.toFunctor.obj X ⟶ R₂.toFunctor.obj X)
      (NatTrans.app
        (R₁.toFunctor.rightUnitor.inv ≫
          (CategoryTheory.mateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
                (a : TwoSquare (𝟙 C).toFunctor L₁.toFunctor L₂.toFunctor (𝟙 D).toFunctor) →
                  TwoSquare R₁.toFunctor (𝟙 D).toFunctor (𝟙 C).toFunctor R₂.toFunctor)
              ((λ_ L₂).hom ≫ f ≫ (ρ_ L₁).inv).toNatTrans ≫
            R₂.toFunctor.leftUnitor.hom)
        X)
      (NatTrans.app
        ((CategoryTheory.conjugateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
            (a : L₂.toFunctor ⟶ L₁.toFunctor) → R₁.toFunctor ⟶ R₂.toFunctor)
          f.toNatTrans)
        X)
⊢ Eq (α := R₁.toFunctor ⟶ R₂.toFunctor)
    (R₁.toFunctor.rightUnitor.inv ≫
      (CategoryTheory.mateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
            (a : TwoSquare (𝟙 C).toFunctor L₁.toFunctor L₂.toFunctor (𝟙 D).toFunctor) →
              TwoSquare R₁.toFunctor (𝟙 D).toFunctor (𝟙 C).toFunctor R₂.toFunctor)
          ((λ_ L₂).hom ≫ f ≫ (ρ_ L₁).inv).toNatTrans ≫
        R₂.toFunctor.leftUnitor.hom)
    ((CategoryTheory.conjugateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
        (a : L₂.toFunctor ⟶ L₁.toFunctor) → R₁.toFunctor ⟶ R₂.toFunctor)
      f.toNatTrans)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
Goal:
C D : Cat
L₁ L₂ : C ⟶ D
R₁ R₂ : D ⟶ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
f : L₂ ⟶ L₁
X : (↑D : Type u_2)
⊢ Eq (α := R₁.toFunctor.obj X ⟶ R₂.toFunctor.obj X)
    (NatTrans.app
      (R₁.toFunctor.rightUnitor.inv ≫
        (CategoryTheory.mateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
              (a : TwoSquare (𝟙 C).toFunctor L₁.toFunctor L₂.toFunctor (𝟙 D).toFunctor) →
                TwoSquare R₁.toFunctor (𝟙 D).toFunctor (𝟙 C).toFunctor R₂.toFunctor)
            ((λ_ L₂).hom ≫ f ≫ (ρ_ L₁).inv).toNatTrans ≫
          R₂.toFunctor.leftUnitor.hom)
      X)
    (NatTrans.app
      ((CategoryTheory.conjugateEquiv (Adjunction.ofCat adj₁) (Adjunction.ofCat adj₂) :
          (a : L₂.toFunctor ⟶ L₁.toFunctor) → R₁.toFunctor ⟶ R₂.toFunctor)
        f.toNatTrans)
      X)

Tactic:
simp [CategoryTheory.conjugateEquiv]

Premises used: CategoryTheory.conjugateEquiv
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
Goal:
C₁ C₂ : Adj Cat
α : C₁ ⟶ C₂
X : (↑C₁.obj : Type u)
⊢ α.l.toFunctor.map (α.adj.unit.toNatTrans.app X) ≫ α.adj.counit.toNatTrans.app (α.l.toFunctor.obj X) =
    𝟙 (α.l.toFunctor.obj X)

Tactic:
(Adjunction.ofCat α.adj).left_triangle_components _

Premises used: CategoryTheory.Adjunction.ofCat, CategoryTheory.Bicategory.Adj.Hom.adj, CategoryTheory.Adjunction.left_triangle_components
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
Goal:
C₁ C₂ : Adj Cat
α : C₁ ⟶ C₂
X : (↑C₂.obj : Type u)
⊢ α.adj.unit.toNatTrans.app (α.r.toFunctor.obj X) ≫ α.r.toFunctor.map (α.adj.counit.toNatTrans.app X) =
    𝟙 (α.r.toFunctor.obj X)

Tactic:
(Adjunction.ofCat α.adj).right_triangle_components _

Premises used: CategoryTheory.Adjunction.ofCat, CategoryTheory.Bicategory.Adj.Hom.adj, CategoryTheory.Adjunction.right_triangle_components
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
Goal:
C₁ C₂ : Adj Cat
α : C₁ ⟶ C₂
X Y : (↑C₁.obj : Type u)
f : X ⟶ Y
⊢ α.adj.unit.toNatTrans.app X ≫ α.r.toFunctor.map (α.l.toFunctor.map f) = f ≫ α.adj.unit.toNatTrans.app Y

Tactic:
(Adjunction.ofCat α.adj).unit_naturality f

Premises used: CategoryTheory.Adjunction.ofCat, CategoryTheory.Adjunction.unit_naturality, CategoryTheory.Bicategory.Adj.Hom.adj
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
Goal:
C₁ C₂ : Adj Cat
α : C₁ ⟶ C₂
X Y : (↑C₂.obj : Type u)
f : X ⟶ Y
⊢ α.l.toFunctor.map (α.r.toFunctor.map f) ≫ α.adj.counit.toNatTrans.app Y = α.adj.counit.toNatTrans.app X ≫ f

Tactic:
(Adjunction.ofCat α.adj).counit_naturality f

Premises used: CategoryTheory.Adjunction.counit_naturality, CategoryTheory.Adjunction.ofCat, CategoryTheory.Bicategory.Adj.Hom.adj
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
γ : g ⟶ l ≫ h
⊢ (fun (β : r ≫ g ⟶ h) ↦ (λ_ g).inv ≫ adj.unit ▷ g ≫ (α_ l r g).hom ≫ l ◁ β)
      ((fun (γ : g ⟶ l ≫ h) ↦ r ◁ γ ≫ (α_ r l h).inv ≫ adj.counit ▷ h ≫ (λ_ h).hom) γ) =
    𝟙 g ⊗≫ (adj.unit ▷ g ≫ (l ≫ r) ◁ γ) ⊗≫ l ◁ adj.counit ▷ h ⊗≫ 𝟙 (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 : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
γ : g ⟶ l ≫ h
rw :
  𝟙 g ⊗≫ (𝟙 b ◁ γ ≫ adj.unit ▷ (l ≫ h)) ⊗≫ l ◁ adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h) =
    γ ⊗≫ leftZigzag adj.unit adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h)
⊢ 𝟙 g ⊗≫ (adj.unit ▷ g ≫ (l ≫ r) ◁ γ) ⊗≫ l ◁ adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h) =
    γ ⊗≫ leftZigzag adj.unit adj.counit ▷ h ⊗≫ 𝟙 (l ≫ h)

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

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 : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
γ : g ⟶ l ≫ h
⊢ γ ⊗≫ ((λ_ l).hom ≫ (ρ_ l).inv) ▷ h ⊗≫ 𝟙 (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 : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
β : r ≫ g ⟶ h
⊢ (fun (γ : g ⟶ l ≫ h) ↦ r ◁ γ ≫ (α_ r l h).inv ≫ adj.counit ▷ h ≫ (λ_ h).hom)
      ((fun (β : r ≫ g ⟶ h) ↦ (λ_ g).inv ≫ adj.unit ▷ g ≫ (α_ l r g).hom ≫ l ◁ β) β) =
    𝟙 (r ≫ g) ⊗≫ r ◁ adj.unit ▷ g ⊗≫ ((r ≫ l) ◁ β ≫ adj.counit ▷ h) ⊗≫ 𝟙 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 : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
β : r ≫ g ⟶ h
rw :
  𝟙 (r ≫ g) ⊗≫ r ◁ adj.unit ▷ g ⊗≫ (adj.counit ▷ (r ≫ g) ≫ 𝟙 c ◁ β) ⊗≫ 𝟙 h =
    𝟙 (r ≫ g) ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β
⊢ 𝟙 (r ≫ g) ⊗≫ r ◁ adj.unit ▷ g ⊗≫ ((r ≫ l) ◁ β ≫ adj.counit ▷ h) ⊗≫ 𝟙 h =
    𝟙 (r ≫ g) ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β

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 : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : b ⟶ d
h : c ⟶ d
β : r ≫ g ⟶ h
⊢ 𝟙 (r ≫ g) ⊗≫ r ◁ adj.unit ▷ g ⊗≫ (adj.counit ▷ (r ≫ g) ≫ 𝟙 c ◁ β) ⊗≫ 𝟙 h =
    𝟙 (r ≫ g) ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β

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

Tactic:
rw [adj.right_triangle]

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

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

Tactic:
calc
      _ = 𝟙 _ ⊗≫ r ◁ adj.unit ▷ g ⊗≫ ((r ≫ l) ◁ β ≫ adj.counit ▷ h) ⊗≫ 𝟙 _ := by
        bicategory
      _ = 𝟙 _ ⊗≫ rightZigzag adj.unit adj.counit ▷ g ⊗≫ β := by
        rw [whisker_exchange]
        bicategory
      _ = β := by
        rw [adj.right_triangle]
        bicategory

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Bicategory.whiskerRight, CategoryTheory.Bicategory.rightZigzag, CategoryTheory.CategoryStruct.comp, CategoryTheory.Bicategory.Adjunction.unit, CategoryTheory.Bicategory.whiskerLeft, CategoryTheory.Bicategory.Adjunction.counit
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
α : g ≫ l ⟶ h
⊢ (fun (γ : g ⟶ h ≫ r) ↦ γ ▷ l ≫ (α_ h r l).hom ≫ h ◁ adj.counit ≫ (ρ_ h).hom)
      ((fun (α : g ≫ l ⟶ h) ↦ (ρ_ g).inv ≫ g ◁ adj.unit ≫ (α_ g l r).inv ≫ α ▷ r) α) =
    𝟙 (g ≫ l) ⊗≫ g ◁ adj.unit ▷ l ⊗≫ (α ▷ (r ≫ l) ≫ h ◁ adj.counit) ⊗≫ 𝟙 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 : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
α : g ≫ l ⟶ h
rw :
  𝟙 (g ≫ l) ⊗≫ g ◁ adj.unit ▷ l ⊗≫ ((g ≫ l) ◁ adj.counit ≫ α ▷ 𝟙 c) ⊗≫ 𝟙 h =
    𝟙 (g ≫ l) ⊗≫ g ◁ leftZigzag adj.unit adj.counit ⊗≫ α
⊢ 𝟙 (g ≫ l) ⊗≫ g ◁ adj.unit ▷ l ⊗≫ (α ▷ (r ≫ l) ≫ h ◁ adj.counit) ⊗≫ 𝟙 h =
    𝟙 (g ≫ l) ⊗≫ g ◁ leftZigzag adj.unit adj.counit ⊗≫ α

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 : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
α : g ≫ l ⟶ h
⊢ 𝟙 (g ≫ l) ⊗≫ g ◁ adj.unit ▷ l ⊗≫ ((g ≫ l) ◁ adj.counit ≫ α ▷ 𝟙 c) ⊗≫ 𝟙 h =
    𝟙 (g ≫ l) ⊗≫ g ◁ leftZigzag adj.unit adj.counit ⊗≫ α

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

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 : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
α : g ≫ l ⟶ h
⊢ 𝟙 (g ≫ l) ⊗≫ g ◁ ((λ_ l).hom ≫ (ρ_ l).inv) ⊗≫ α = α

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
γ : g ⟶ h ≫ r
⊢ (fun (α : g ≫ l ⟶ h) ↦ (ρ_ g).inv ≫ g ◁ adj.unit ≫ (α_ g l r).inv ≫ α ▷ r)
      ((fun (γ : g ⟶ h ≫ r) ↦ γ ▷ l ≫ (α_ h r l).hom ≫ h ◁ adj.counit ≫ (ρ_ h).hom) γ) =
    𝟙 g ⊗≫ (g ◁ adj.unit ≫ γ ▷ (l ≫ r)) ⊗≫ h ◁ adj.counit ▷ 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
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
γ : g ⟶ h ≫ r
rw :
  𝟙 g ⊗≫ (γ ▷ 𝟙 b ≫ (h ≫ r) ◁ adj.unit) ⊗≫ h ◁ adj.counit ▷ r ⊗≫ 𝟙 (h ≫ r) =
    𝟙 g ⊗≫ γ ⊗≫ h ◁ rightZigzag adj.unit adj.counit ⊗≫ 𝟙 (h ≫ r)
⊢ 𝟙 g ⊗≫ (g ◁ adj.unit ≫ γ ▷ (l ≫ r)) ⊗≫ h ◁ adj.counit ▷ r ⊗≫ 𝟙 (h ≫ r) =
    𝟙 g ⊗≫ γ ⊗≫ h ◁ rightZigzag adj.unit adj.counit ⊗≫ 𝟙 (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 : B
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
γ : g ⟶ h ≫ r
⊢ 𝟙 g ⊗≫ (γ ▷ 𝟙 b ≫ (h ≫ r) ◁ adj.unit) ⊗≫ h ◁ adj.counit ▷ r ⊗≫ 𝟙 (h ≫ r) =
    𝟙 g ⊗≫ γ ⊗≫ h ◁ rightZigzag adj.unit adj.counit ⊗≫ 𝟙 (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
l : b ⟶ c
r : c ⟶ b
adj : l ⊣ r
g : a ⟶ b
h : a ⟶ c
γ : g ⟶ h ≫ r
rw : 𝟙 g ⊗≫ γ ⊗≫ h ◁ ((ρ_ r).hom ≫ (λ_ r).inv) ⊗≫ 𝟙 (h ≫ r) = γ
⊢ 𝟙 g ⊗≫ γ ⊗≫ h ◁ rightZigzag adj.unit adj.counit ⊗≫ 𝟙 (h ≫ r) = γ

Tactic:
rw [adj.right_triangle]

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

Tactic:
rw [eq_comm, ← adj₁.homEquiv₁.symm.injective.eq_iff']

Premises used: Function.Injective.eq_iff', CategoryTheory.Bicategory.Adjunction.homEquiv₁, eq_comm, Equiv.injective, Equiv.symm
-- 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 ⟶ h ≫ r₂
conv_lhs :
  Eq (α := g ⟶ l₁ ≫ h ≫ r₂) ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
      ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂)
          ((mateEquiv adj₁ adj₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α : r₁ ≫ g ⟶ h ≫ r₂) :
        g ⟶ l₁ ≫ h ≫ r₂) ↔
    Eq (α := g ⟶ l₁ ≫ h ≫ r₂)
      ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
      ((adj₂.homEquiv₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → g ⟶ (l₁ ≫ h) ≫ r₂) α ≫ (α_ l₁ h r₂).hom : g ⟶ l₁ ≫ h ≫ r₂)
⊢ (mateEquiv adj₁ adj₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α = β ↔
    Eq (α := g ⟶ l₁ ≫ h ≫ r₂)
      ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
      ((adj₂.homEquiv₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → g ⟶ (l₁ ≫ h) ≫ r₂) α ≫ (α_ l₁ h r₂).hom : g ⟶ l₁ ≫ h ≫ r₂)

Tactic:
conv_lhs => rw [eq_comm, ← adj₁.homEquiv₁.symm.injective.eq_iff']

Premises used: Function.Injective.eq_iff', CategoryTheory.Bicategory.Adjunction.homEquiv₁, eq_comm, Equiv.injective, Equiv.symm
-- 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 ⟶ h ≫ r₂
rw :
  Eq (α := g ⟶ l₁ ≫ h ≫ r₂) ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
      ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂)
          ((adj₁.homEquiv₁ : (a : g ⟶ l₁ ≫ h ≫ r₂) → r₁ ≫ g ⟶ h ≫ r₂)
              ((adj₂.homEquiv₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → g ⟶ (l₁ ≫ h) ≫ r₂) α ≫ (α_ l₁ h r₂).hom : g ⟶ l₁ ≫ h ≫ r₂) :
            r₁ ≫ g ⟶ h ≫ r₂) :
        g ⟶ l₁ ≫ h ≫ r₂) ↔
    Eq (α := g ⟶ l₁ ≫ h ≫ r₂)
      ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
      ((adj₂.homEquiv₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → g ⟶ (l₁ ≫ h) ≫ r₂) α ≫ (α_ l₁ h r₂).hom : g ⟶ l₁ ≫ h ≫ r₂)
rw₁ rw₂ :
  Eq (α := g ⟶ l₁ ≫ h ≫ r₂) ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
      ((adj₂.homEquiv₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → g ⟶ (l₁ ≫ h) ≫ r₂) α ≫ (α_ l₁ h r₂).hom : g ⟶ l₁ ≫ h ≫ r₂) ↔
    Eq (α := g ⟶ l₁ ≫ h ≫ r₂)
      ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
      ((adj₂.homEquiv₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → g ⟶ (l₁ ≫ h) ≫ r₂) α ≫ (α_ l₁ h r₂).hom : g ⟶ l₁ ≫ h ≫ r₂)
⊢ Eq (α := g ⟶ l₁ ≫ h ≫ r₂) ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
      ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂)
          ((mateEquiv adj₁ adj₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → r₁ ≫ g ⟶ h ≫ r₂) α : r₁ ≫ g ⟶ h ≫ r₂) :
        g ⟶ l₁ ≫ h ≫ r₂) ↔
    Eq (α := g ⟶ l₁ ≫ h ≫ r₂)
      ((Equiv.symm adj₁.homEquiv₁ : (a : r₁ ≫ g ⟶ h ≫ r₂) → g ⟶ l₁ ≫ h ≫ r₂) β : g ⟶ l₁ ≫ h ≫ r₂)
      ((adj₂.homEquiv₂ : (a : g ≫ l₂ ⟶ l₁ ≫ h) → g ⟶ (l₁ ≫ h) ≫ r₂) α ≫ (α_ l₁ h r₂).hom : g ⟶ l₁ ≫ h ≫ r₂)

Tactic:
rw [mateEquiv_apply, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, CategoryTheory.Bicategory.mateEquiv_apply