awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Adjunction.Whiskering
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_3, v_2, u_3, u_2} E D
adj : F ⊣ G
X Y : Functor.{v_1, v_3, u_1, u_3} C E
f : X ⟶ Y
x : C
⊢ (map (obj (whiskeringRight C E D) G ⋙ obj (whiskeringRight C D E) F) f ≫
          (Y.associator G F).hom ≫ Y.whiskerLeft adj.counit ≫ Y.rightUnitor.hom).app
      x =
    NatTrans.app
      (((X.associator G F).hom ≫ X.whiskerLeft adj.counit ≫ X.rightUnitor.hom) ≫
        map (𝟭 (Functor.{v_1, v_3, u_1, u_3} C E)) f)
      x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Adjunction.Whiskering
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_3, v_2, u_3, u_2} E D
adj : F ⊣ G
X : Functor.{v_2, v_1, u_2, u_1} D C
w :
  ∀ (x : E),
    NatTrans.app
        (map (obj (whiskeringLeft E D C) G)
            (NatTrans.app
              {
                app := fun (X : Functor.{v_2, v_1, u_2, u_1} D C) ↦
                  (obj (𝟭 (Functor.{v_2, v_1, u_2, u_1} D C)) X).leftUnitor.inv ≫
                    whiskerRight adj.unit X ≫ (F.associator G X).hom,
                naturality := ⋯ }
              X) ≫
          NatTrans.app
            {
              app := fun (X : Functor.{v_3, v_1, u_3, u_1} E C) ↦
                (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom,
              naturality := ⋯ :
              NatTrans (C := Functor.{v_3, v_1, u_3, u_1} E C)
                (obj (whiskeringLeft D E C) F ⋙ obj (whiskeringLeft E D C) G) (𝟭 (Functor.{v_3, v_1, u_3, u_1} E C)) }
            (obj (obj (whiskeringLeft E D C) G) X))
        x =
      NatTrans.app (𝟙 (obj (obj (whiskeringLeft E D C) G) X)) x
⊢ map (obj (whiskeringLeft E D C) G)
        (NatTrans.app
          {
            app := fun (X : Functor.{v_2, v_1, u_2, u_1} D C) ↦
              (obj (𝟭 (Functor.{v_2, v_1, u_2, u_1} D C)) X).leftUnitor.inv ≫
                whiskerRight adj.unit X ≫ (F.associator G X).hom,
            naturality := ⋯ }
          X) ≫
      NatTrans.app
        {
          app := fun (X : Functor.{v_3, v_1, u_3, u_1} E C) ↦
            (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom,
          naturality := ⋯ :
          NatTrans (C := Functor.{v_3, v_1, u_3, u_1} E C) (obj (whiskeringLeft D E C) F ⋙ obj (whiskeringLeft E D C) G)
            (𝟭 (Functor.{v_3, v_1, u_3, u_1} E C)) }
        (obj (obj (whiskeringLeft E D C) G) X) =
    𝟙 (obj (obj (whiskeringLeft E D C) G) X)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Adjunction.Whiskering
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_3, v_2, u_3, u_2} E D
adj : F ⊣ G
X : Functor.{v_2, v_1, u_2, u_1} D C
x : E
⊢ NatTrans.app
      (map (obj (whiskeringLeft E D C) G)
          (NatTrans.app
            {
              app := fun (X : Functor.{v_2, v_1, u_2, u_1} D C) ↦
                (obj (𝟭 (Functor.{v_2, v_1, u_2, u_1} D C)) X).leftUnitor.inv ≫
                  whiskerRight adj.unit X ≫ (F.associator G X).hom,
              naturality := ⋯ }
            X) ≫
        NatTrans.app
          {
            app := fun (X : Functor.{v_3, v_1, u_3, u_1} E C) ↦
              (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom,
            naturality := ⋯ :
            NatTrans (C := Functor.{v_3, v_1, u_3, u_1} E C)
              (obj (whiskeringLeft D E C) F ⋙ obj (whiskeringLeft E D C) G) (𝟭 (Functor.{v_3, v_1, u_3, u_1} E C)) }
          (obj (obj (whiskeringLeft E D C) G) X))
      x =
    NatTrans.app (𝟙 (obj (obj (whiskeringLeft E D C) G) X)) x

Tactic:
simp [← X.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Adjunction.Whiskering
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_3, v_2, u_3, u_2} E D
adj : F ⊣ G
X : Functor.{v_3, v_1, u_3, u_1} E C
w :
  ∀ (x : D),
    NatTrans.app
        (NatTrans.app
            {
              app := fun (X : Functor.{v_2, v_1, u_2, u_1} D C) ↦
                (obj (𝟭 (Functor.{v_2, v_1, u_2, u_1} D C)) X).leftUnitor.inv ≫
                  whiskerRight adj.unit X ≫ (F.associator G X).hom,
              naturality := ⋯ :
              NatTrans (C := Functor.{v_2, v_1, u_2, u_1} D C) (𝟭 (Functor.{v_2, v_1, u_2, u_1} D C))
                (obj (whiskeringLeft E D C) G ⋙ obj (whiskeringLeft D E C) F) }
            (obj (obj (whiskeringLeft D E C) F) X) ≫
          map (obj (whiskeringLeft D E C) F)
            (NatTrans.app
              {
                app := fun (X : Functor.{v_3, v_1, u_3, u_1} E C) ↦
                  (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom,
                naturality := ⋯ }
              X))
        x =
      NatTrans.app (𝟙 (obj (obj (whiskeringLeft D E C) F) X)) x
⊢ NatTrans.app
        {
          app := fun (X : Functor.{v_2, v_1, u_2, u_1} D C) ↦
            (obj (𝟭 (Functor.{v_2, v_1, u_2, u_1} D C)) X).leftUnitor.inv ≫
              whiskerRight adj.unit X ≫ (F.associator G X).hom,
          naturality := ⋯ :
          NatTrans (C := Functor.{v_2, v_1, u_2, u_1} D C) (𝟭 (Functor.{v_2, v_1, u_2, u_1} D C))
            (obj (whiskeringLeft E D C) G ⋙ obj (whiskeringLeft D E C) F) }
        (obj (obj (whiskeringLeft D E C) F) X) ≫
      map (obj (whiskeringLeft D E C) F)
        (NatTrans.app
          {
            app := fun (X : Functor.{v_3, v_1, u_3, u_1} E C) ↦
              (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom,
            naturality := ⋯ }
          X) =
    𝟙 (obj (obj (whiskeringLeft D E C) F) X)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Adjunction.Whiskering
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_3, v_2, u_3, u_2} E D
adj : F ⊣ G
X : Functor.{v_3, v_1, u_3, u_1} E C
x : D
⊢ NatTrans.app
      (NatTrans.app
          {
            app := fun (X : Functor.{v_2, v_1, u_2, u_1} D C) ↦
              (obj (𝟭 (Functor.{v_2, v_1, u_2, u_1} D C)) X).leftUnitor.inv ≫
                whiskerRight adj.unit X ≫ (F.associator G X).hom,
            naturality := ⋯ :
            NatTrans (C := Functor.{v_2, v_1, u_2, u_1} D C) (𝟭 (Functor.{v_2, v_1, u_2, u_1} D C))
              (obj (whiskeringLeft E D C) G ⋙ obj (whiskeringLeft D E C) F) }
          (obj (obj (whiskeringLeft D E C) F) X) ≫
        map (obj (whiskeringLeft D E C) F)
          (NatTrans.app
            {
              app := fun (X : Functor.{v_3, v_1, u_3, u_1} E C) ↦
                (G.associator F X).inv ≫ whiskerRight adj.counit X ≫ X.leftUnitor.hom,
              naturality := ⋯ }
            X))
      x =
    NatTrans.app (𝟙 (obj (obj (whiskeringLeft D E C) F) X)) x

Tactic:
simp [← X.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
b : Adj.{w, v, u} B
⊢ { obj := b.obj } = b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : Adj.{w, v, u} B
α β : a ⟶ b
p : Hom₂ α β
rw :
  ((conjugateEquiv β.adj α.adj).symm : (a_1 : β.r ⟶ α.r) → α.l ⟶ β.l)
      ((conjugateEquiv β.adj α.adj : (a_1 : α.l ⟶ β.l) → β.r ⟶ α.r) p.τl : β.r ⟶ α.r) =
    p.τl
rw₁ rw₂ : p.τl = p.τl
⊢ ((conjugateEquiv β.adj α.adj).symm : (a_1 : β.r ⟶ α.r) → α.l ⟶ β.l) p.τr = p.τl

Tactic:
rw [← Hom₂.conjugateEquiv_τl, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, CategoryTheory.Bicategory.Adj.Hom₂.conjugateEquiv_τl
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 b_1 c_1 d : Adj.{w, v, u} B
a b c : a_1 ⟶ b_1
x : Hom₂ a b
y : Hom₂ b c
⊢ (conjugateEquiv c.adj a.adj : (a_2 : a.l ⟶ c.l) → c.r ⟶ a.r) (x.τl ≫ y.τl) = y.τr ≫ x.τr

Tactic:
simp [← conjugateEquiv_comp c.adj b.adj a.adj y.τl x.τl,
          Hom₂.conjugateEquiv_τl]

Premises used: CategoryTheory.Bicategory.Adj.Hom₂.τl, CategoryTheory.Bicategory.Adj.Hom.adj, CategoryTheory.Bicategory.Adj.Hom₂.conjugateEquiv_τl, CategoryTheory.Bicategory.conjugateEquiv_comp
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : Adj.{w, v, u} B
α β : a ⟶ b
x y : α ⟶ β
hl : x.τl = y.τl
⊢ x.τr = y.τr

Tactic:
simp only [← Hom₂.conjugateEquiv_τl, hl]

Premises used: CategoryTheory.Bicategory.Adj.Hom₂.conjugateEquiv_τl
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : Adj.{w, v, u} B
α β : a ⟶ b
el : α.l ≅ β.l
er : β.r ≅ α.r
h : (conjugateEquiv β.adj α.adj : (a_1 : α.l ⟶ β.l) → β.r ⟶ α.r) el.hom = er.hom
rw : (conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv ≫ er.hom = er.inv ≫ er.hom
rw₁ :
  Eq (α := α.r ⟶ α.r) ((conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv ≫ er.hom : α.r ⟶ α.r)
    (𝟙 α.r : α.r ⟶ α.r)
rw₂ :
  Eq (α := α.r ⟶ α.r)
    (CategoryStruct.comp (Y := β.r) ((conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv)
        ((conjugateEquiv β.adj α.adj : (a_1 : α.l ⟶ β.l) → β.r ⟶ α.r) el.hom) :
      α.r ⟶ α.r)
    (𝟙 α.r : α.r ⟶ α.r)
rw₃ :
  Eq (α := α.r ⟶ α.r) ((conjugateEquiv α.adj α.adj : (a_1 : α.l ⟶ α.l) → α.r ⟶ α.r) (el.hom ≫ el.inv) : α.r ⟶ α.r)
    (𝟙 α.r : α.r ⟶ α.r)
rw₄ :
  Eq (α := α.r ⟶ α.r) ((conjugateEquiv α.adj α.adj : (a_1 : α.l ⟶ α.l) → α.r ⟶ α.r) (𝟙 α.l) : α.r ⟶ α.r)
    (𝟙 α.r : α.r ⟶ α.r)
rw₅ rw₆ : 𝟙 α.r = 𝟙 α.r
⊢ (conjugateEquiv α.adj β.adj : (a_1 : β.l ⟶ α.l) → α.r ⟶ β.r) el.inv = er.inv

Tactic:
rw [← cancel_mono er.hom, Iso.inv_hom_id, ← h,
          conjugateEquiv_comp, Iso.hom_inv_id, conjugateEquiv_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Iso.hom_inv_id, CategoryTheory.cancel_mono, CategoryTheory.Bicategory.conjugateEquiv_id, CategoryTheory.Iso.hom, CategoryTheory.Bicategory.conjugateEquiv_comp
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : Adj.{w, v, u} B
α : a ⟶ b
⊢ (conjugateEquiv α.adj (𝟙 a ≫ α).adj : (a_1 : (𝟙 a ≫ α).l ⟶ α.l) → α.r ⟶ (𝟙 a ≫ α).r) (λ_ α.l).hom = (ρ_ α.r).symm.hom

Tactic:
simpa using conjugateEquiv_id_comp_right_apply α.adj α.adj (𝟙 _)

Premises used: CategoryTheory.Bicategory.conjugateEquiv_id_comp_right_apply, CategoryTheory.CategoryStruct.id, CategoryTheory.Bicategory.Adj.Hom.adj
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : Adj.{w, v, u} B
α : a ⟶ b
⊢ (conjugateEquiv α.adj (α ≫ 𝟙 b).adj : (a_1 : (α ≫ 𝟙 b).l ⟶ α.l) → α.r ⟶ (α ≫ 𝟙 b).r) (ρ_ α.l).hom = (λ_ α.r).symm.hom

Tactic:
simpa using conjugateEquiv_comp_id_right_apply α.adj α.adj (𝟙 _)

Premises used: CategoryTheory.Bicategory.conjugateEquiv_comp_id_right_apply, CategoryTheory.CategoryStruct.id, CategoryTheory.Bicategory.Adj.Hom.adj
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : Adj.{w, v, u} B
α : a ⟶ b
β β' : b ⟶ c
y : β ⟶ β'
⊢ (conjugateEquiv (α ≫ β').adj (α ≫ β).adj : (a_1 : (α ≫ β).l ⟶ (α ≫ β').l) → (α ≫ β').r ⟶ (α ≫ β).r) (α.l ◁ y.τl) =
    y.τr ▷ α.r

Tactic:
simp [conjugateEquiv_whiskerLeft, Hom₂.conjugateEquiv_τl]

Premises used: CategoryTheory.Bicategory.Adj.Hom₂.conjugateEquiv_τl, CategoryTheory.Bicategory.conjugateEquiv_whiskerLeft
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c d : Adj.{w, v, u} B
α α' : a ⟶ b
x : α ⟶ α'
β : b ⟶ c
⊢ (conjugateEquiv (α' ≫ β).adj (α ≫ β).adj : (a_1 : (α ≫ β).l ⟶ (α' ≫ β).l) → (α' ≫ β).r ⟶ (α ≫ β).r) (x.τl ▷ β.l) =
    β.r ◁ x.τr

Tactic:
simp [conjugateEquiv_whiskerRight, Hom₂.conjugateEquiv_τl]

Premises used: CategoryTheory.Bicategory.conjugateEquiv_whiskerRight, CategoryTheory.Bicategory.Adj.Hom₂.conjugateEquiv_τl
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 b_1 c d a b : Adj.{w, v, u} B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
rw : (e.hom ≫ e.inv).τl = 𝟙 adj₁.l
rw₁ : Hom₂.τl (𝟙 adj₁) = 𝟙 adj₁.l
rw₂ rw₃ : 𝟙 adj₁.l = 𝟙 adj₁.l
⊢ e.hom.τl ≫ e.inv.τl = 𝟙 adj₁.l

Tactic:
rw [← comp_τl, e.hom_inv_id, id_τl]

Premises used: CategoryTheory.Bicategory.Adj.id_τl, CategoryTheory.Bicategory.Adj.comp_τl, CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 b_1 c d a b : Adj.{w, v, u} B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
rw : (e.inv ≫ e.hom).τl = 𝟙 adj₂.l
rw₁ : Hom₂.τl (𝟙 adj₂) = 𝟙 adj₂.l
rw₂ rw₃ : 𝟙 adj₂.l = 𝟙 adj₂.l
⊢ e.inv.τl ≫ e.hom.τl = 𝟙 adj₂.l

Tactic:
rw [← comp_τl, e.inv_hom_id, id_τl]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Bicategory.Adj.id_τl, CategoryTheory.Bicategory.Adj.comp_τl
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 b_1 c d a b : Adj.{w, v, u} B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
rw : (e.hom ≫ e.inv).τr = 𝟙 adj₁.r
rw₁ : Hom₂.τr (𝟙 adj₁) = 𝟙 adj₁.r
rw₂ rw₃ : 𝟙 adj₁.r = 𝟙 adj₁.r
⊢ e.inv.τr ≫ e.hom.τr = 𝟙 adj₁.r

Tactic:
rw [← comp_τr, e.hom_inv_id, id_τr]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Bicategory.Adj.id_τr, CategoryTheory.Bicategory.Adj.comp_τr
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 b_1 c d a b : Adj.{w, v, u} B
adj₁ adj₂ : a ⟶ b
e : adj₁ ≅ adj₂
rw : (e.inv ≫ e.hom).τr = 𝟙 adj₂.r
rw₁ : Hom₂.τr (𝟙 adj₂) = 𝟙 adj₂.r
rw₂ rw₃ : 𝟙 adj₂.r = 𝟙 adj₂.r
⊢ e.hom.τr ≫ e.inv.τr = 𝟙 adj₂.r

Tactic:
rw [← comp_τr, e.inv_hom_id, id_τr]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.Bicategory.Adj.id_τr, CategoryTheory.Bicategory.Adj.comp_τr
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ (g ◁ η ⊗≫ ε ▷ g) ⊗≫ g ◁ η ⊗≫ ε ▷ g = g ◁ η ⊗≫ (ε ▷ g ▷ 𝟙 a ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
rw :
  g ◁ η ⊗≫ (((g ≫ f) ≫ g) ◁ η ≫ ε ▷ g ▷ (f ≫ g)) ⊗≫ ε ▷ g =
    𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g)
⊢ g ◁ η ⊗≫ (ε ▷ g ▷ 𝟙 a ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g =
    𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g)

Tactic:
rw [← whisker_exchange]

Premises used: CategoryTheory.Bicategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ g ◁ η ⊗≫ (((g ≫ f) ≫ g) ◁ η ≫ ε ▷ g ▷ (f ≫ g)) ⊗≫ ε ▷ g =
    𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g)

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
rw :
  𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (𝟙 a ◁ η ≫ η ▷ (f ≫ g)) ⊗≫ ((g ≫ f) ◁ ε ≫ ε ▷ 𝟙 b) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g) =
    g ◁ η ⊗≫ g ◁ (η ▷ f ⊗≫ f ◁ ε) ▷ g ⊗≫ ε ▷ g
⊢ 𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g) =
    g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g

Tactic:
rw [← whisker_exchange, ← whisker_exchange, leftZigzag]

Premises used: CategoryTheory.Bicategory.whisker_exchange, CategoryTheory.Bicategory.leftZigzag
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ 𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (𝟙 a ◁ η ≫ η ▷ (f ≫ g)) ⊗≫ ((g ≫ f) ◁ ε ≫ ε ▷ 𝟙 b) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g) =
    g ◁ η ⊗≫ g ◁ (η ▷ f ⊗≫ f ◁ ε) ▷ g ⊗≫ ε ▷ g

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
rw : g ◁ η ⊗≫ g ◁ ((λ_ f).hom ≫ (ρ_ f).inv) ▷ g ⊗≫ ε ▷ g = g ◁ η ⊗≫ ε ▷ g
⊢ g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g = g ◁ η ⊗≫ ε ▷ g

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
⊢ g ◁ η ⊗≫ g ◁ ((λ_ f).hom ≫ (ρ_ f).inv) ▷ g ⊗≫ ε ▷ g = g ◁ η ⊗≫ ε ▷ g

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ⟶ f ≫ g
ε : g ≫ f ⟶ 𝟙 b
h : leftZigzag η ε = (λ_ f).hom ≫ (ρ_ f).inv
_ : (g ◁ η ⊗≫ ε ▷ g) ⊗≫ g ◁ η ⊗≫ ε ▷ g = g ◁ η ⊗≫ (ε ▷ g ▷ 𝟙 a ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g
_₁ :
  g ◁ η ⊗≫ (ε ▷ g ▷ 𝟙 a ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g =
    𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g)
_₂ :
  𝟙 (g ≫ 𝟙 a) ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 (𝟙 b ≫ g) =
    g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g
_₃ : g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g = g ◁ η ⊗≫ ε ▷ g
⊢ (g ◁ η ⊗≫ ε ▷ g) ⊗≫ g ◁ η ⊗≫ ε ▷ g = g ◁ η ⊗≫ ε ▷ g

Tactic:
calc
    _ = g ◁ η ⊗≫ ((ε ▷ g ▷ 𝟙 a) ≫ (𝟙 b ≫ g) ◁ η) ⊗≫ ε ▷ g := by
      bicategory
    _ = 𝟙 _ ⊗≫ g ◁ (η ▷ 𝟙 a ≫ (f ≫ g) ◁ η) ⊗≫ (ε ▷ (g ≫ f) ≫ 𝟙 b ◁ ε) ▷ g ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]; bicategory
    _ = g ◁ η ⊗≫ g ◁ leftZigzag η ε ▷ g ⊗≫ ε ▷ g := by
      rw [← whisker_exchange, ← whisker_exchange, leftZigzag]; bicategory
    _ = g ◁ η ⊗≫ ε ▷ g := by
      rw [h]; bicategory

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Bicategory.whiskerRight, CategoryTheory.Bicategory.leftZigzag, CategoryTheory.CategoryStruct.comp, CategoryTheory.Bicategory.whiskerLeft
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 b c : B
f : a_1 ⟶ b
g : b ⟶ a_1
a : B
⊢ Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := a ⟶ a) (𝟙 a ≫ 𝟙 a) (𝟙 a ≫ 𝟙 a))
    (leftZigzag (Iso.inv (ρ_ (𝟙 a))) (Iso.hom (ρ_ (𝟙 a)))) (Iso.hom (λ_ (𝟙 a)) ≫ Iso.inv (ρ_ (𝟙 a)))

Tactic:
bicategory_coherence
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a_1 b c : B
f : a_1 ⟶ b
g : b ⟶ a_1
a : B
⊢ Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := a ⟶ a) (𝟙 a ≫ 𝟙 a) (𝟙 a ≫ 𝟙 a))
    (rightZigzag (Iso.inv (ρ_ (𝟙 a))) (Iso.hom (ρ_ (𝟙 a)))) (Iso.hom (ρ_ (𝟙 a)) ≫ Iso.inv (λ_ (𝟙 a)))

Tactic:
bicategory_coherence
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
dsimp :
  leftZigzag (adj₁.unit ⊗≫ f₁ ◁ adj₂.unit ▷ g₁ ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ g₂ ≫ g₁))
      (𝟙 ((g₂ ≫ g₁) ≫ f₁ ≫ f₂) ⊗≫ g₂ ◁ adj₁.counit ▷ f₂ ⊗≫ adj₂.counit) =
    𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
        f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)
⊢ leftZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) =
    𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
        f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)

Tactic:
dsimp only [compUnit, compCounit]

Premises used: CategoryTheory.Bicategory.Adjunction.compCounit, CategoryTheory.Bicategory.Adjunction.compUnit
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ leftZigzag (adj₁.unit ⊗≫ f₁ ◁ adj₂.unit ▷ g₁ ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ g₂ ≫ g₁))
      (𝟙 ((g₂ ≫ g₁) ≫ f₁ ≫ f₂) ⊗≫ g₂ ◁ adj₁.counit ▷ f₂ ⊗≫ adj₂.counit) =
    𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
        f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
rw :
  𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
        f₁ ◁ (𝟙 b ◁ adj₁.counit ≫ adj₂.unit ▷ 𝟙 b) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
    𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      leftZigzag adj₁.unit adj₁.counit ▷ f₂ ⊗≫ f₁ ◁ leftZigzag adj₂.unit adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)
⊢ 𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
        f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
    𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      leftZigzag adj₁.unit adj₁.counit ▷ f₂ ⊗≫ f₁ ◁ leftZigzag adj₂.unit adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)

Tactic:
rw [← whisker_exchange]

Premises used: CategoryTheory.Bicategory.whisker_exchange
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
        f₁ ◁ (𝟙 b ◁ adj₁.counit ≫ adj₂.unit ▷ 𝟙 b) ▷ f₂ ⊗≫ (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
    𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      leftZigzag adj₁.unit adj₁.counit ▷ f₂ ⊗≫ f₁ ◁ leftZigzag adj₂.unit adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c)

Tactic:
bicategory
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
simp_rw :
  𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫ ((λ_ f₁).hom ≫ (ρ_ f₁).inv) ▷ f₂ ⊗≫ f₁ ◁ ((λ_ f₂).hom ≫ (ρ_ f₂).inv) ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
    (λ_ (f₁ ≫ f₂)).hom ≫ (ρ_ (f₁ ≫ f₂)).inv
⊢ 𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      leftZigzag adj₁.unit adj₁.counit ▷ f₂ ⊗≫ f₁ ◁ leftZigzag adj₂.unit adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
    (λ_ (f₁ ≫ f₂)).hom ≫ (ρ_ (f₁ ≫ f₂)).inv

Tactic:
simp_rw [left_triangle]

Premises used: CategoryTheory.Bicategory.Adjunction.left_triangle
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫ ((λ_ f₁).hom ≫ (ρ_ f₁).inv) ▷ f₂ ⊗≫ f₁ ◁ ((λ_ f₂).hom ≫ (ρ_ f₂).inv) ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
    (λ_ (f₁ ≫ f₂)).hom ≫ (ρ_ (f₁ ≫ f₂)).inv

Tactic:
bicategory