awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁.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)
_₁ :
  𝟙 (𝟙 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)
_₂ :
  𝟙 (𝟙 a ≫ f₁ ≫ f₂) ⊗≫
      leftZigzag adj₁.unit adj₁.counit ▷ f₂ ⊗≫ f₁ ◁ leftZigzag adj₂.unit adj₂.counit ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ 𝟙 c) =
    (λ_ (f₁ ≫ f₂)).hom ≫ (ρ_ (f₁ ≫ f₂)).inv
⊢ leftZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = (λ_ (f₁ ≫ f₂)).hom ≫ (ρ_ (f₁ ≫ f₂)).inv

Tactic:
calc
    _ = 𝟙 _ ⊗≫
          adj₁.unit ▷ (f₁ ≫ f₂) ⊗≫
            f₁ ◁ (adj₂.unit ▷ (g₁ ≫ f₁) ≫ (f₂ ≫ g₂) ◁ adj₁.counit) ▷ f₂ ⊗≫
              (f₁ ≫ f₂) ◁ adj₂.counit ⊗≫ 𝟙 _ := by
      dsimp only [compUnit, compCounit]; bicategory
    _ = 𝟙 _ ⊗≫
          (leftZigzag adj₁.unit adj₁.counit) ▷ f₂ ⊗≫
            f₁ ◁ (leftZigzag adj₂.unit adj₂.counit) ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]; bicategory
    _ = _ := by
      simp_rw [left_triangle]; bicategory

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Bicategory.whiskerRight, CategoryTheory.Bicategory.leftZigzag, CategoryTheory.CategoryStruct.comp, CategoryTheory.Bicategory.Adjunction.unit, CategoryTheory.Bicategory.whiskerLeft, CategoryTheory.Bicategory.Adjunction.counit
-- 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 :
  rightZigzag (adj₁.unit ⊗≫ f₁ ◁ adj₂.unit ▷ g₁ ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ g₂ ≫ g₁))
      (𝟙 ((g₂ ≫ g₁) ≫ f₁ ≫ f₂) ⊗≫ g₂ ◁ adj₁.counit ▷ f₂ ⊗≫ adj₂.counit) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)
⊢ rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)

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₂
⊢ rightZigzag (adj₁.unit ⊗≫ f₁ ◁ adj₂.unit ▷ g₁ ⊗≫ 𝟙 ((f₁ ≫ f₂) ≫ g₂ ≫ g₁))
      (𝟙 ((g₂ ≫ g₁) ≫ f₁ ≫ f₂) ⊗≫ g₂ ◁ adj₁.counit ▷ f₂ ⊗≫ adj₂.counit) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)

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 :
  𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ (adj₁.counit ▷ 𝟙 b ≫ 𝟙 b ◁ adj₂.unit) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)
⊢ 𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ 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 c : B
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ 𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ (adj₁.counit ▷ 𝟙 b ≫ 𝟙 b ◁ adj₂.unit) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)

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 :
  𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫ g₂ ◁ ((ρ_ g₁).hom ≫ (λ_ g₁).inv) ⊗≫ ((ρ_ g₂).hom ≫ (λ_ g₂).inv) ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    (ρ_ (g₂ ≫ g₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv
⊢ 𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    (ρ_ (g₂ ≫ g₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv

Tactic:
simp_rw [right_triangle]

Premises used: CategoryTheory.Bicategory.Adjunction.right_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₂
⊢ 𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫ g₂ ◁ ((ρ_ g₁).hom ≫ (λ_ g₁).inv) ⊗≫ ((ρ_ g₂).hom ≫ (λ_ g₂).inv) ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    (ρ_ (g₂ ≫ g₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv

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₂
_ :
  rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)
_₁ :
  𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
        g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫ adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁)
_₂ :
  𝟙 ((g₂ ≫ g₁) ≫ 𝟙 a) ⊗≫
      g₂ ◁ rightZigzag adj₁.unit adj₁.counit ⊗≫ rightZigzag adj₂.unit adj₂.counit ▷ g₁ ⊗≫ 𝟙 (𝟙 c ≫ g₂ ≫ g₁) =
    (ρ_ (g₂ ≫ g₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv
⊢ rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = (ρ_ (g₂ ≫ g₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv

Tactic:
calc
    _ = 𝟙 _ ⊗≫
          (g₂ ≫ g₁) ◁ adj₁.unit ⊗≫
            g₂ ◁ ((g₁ ≫ f₁) ◁ adj₂.unit ≫ adj₁.counit ▷ (f₂ ≫ g₂)) ▷ g₁ ⊗≫
              adj₂.counit ▷ (g₂ ≫ g₁) ⊗≫ 𝟙 _ := by
      dsimp only [compUnit, compCounit]; bicategory
    _ = 𝟙 _ ⊗≫
          g₂ ◁ (rightZigzag adj₁.unit adj₁.counit) ⊗≫
            (rightZigzag adj₂.unit adj₂.counit) ▷ g₁ ⊗≫ 𝟙 _ := by
      rw [whisker_exchange]; bicategory
    _ = _ := by
      simp_rw [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.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b c : B
f : a ⟶ b
g : b ⟶ a
f₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ leftZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = (λ_ (f₁ ≫ f₂)).hom ≫ (ρ_ (f₁ ≫ f₂)).inv

Tactic:
apply comp_left_triangle_aux

Premises used: CategoryTheory.Bicategory.Adjunction.comp_left_triangle_aux
-- 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₁ : a ⟶ b
g₁ : b ⟶ a
f₂ : b ⟶ c
g₂ : c ⟶ b
adj₁ : f₁ ⊣ g₁
adj₂ : f₂ ⊣ g₂
⊢ rightZigzag (adj₁.compUnit adj₂) (adj₁.compCounit adj₂) = (ρ_ (g₂ ≫ g₁)).hom ≫ (λ_ (g₂ ≫ g₁)).inv

Tactic:
apply comp_right_triangle_aux

Premises used: CategoryTheory.Bicategory.Adjunction.comp_right_triangle_aux
-- 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
⊢ (leftZigzagIso η ε).hom = leftZigzag η.hom ε.hom

Tactic:
rfl

Premises used: CategoryTheory.bicategoricalComp, rfl
-- 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
⊢ (rightZigzagIso η ε).hom = rightZigzag η.hom ε.hom

Tactic:
rfl

Premises used: CategoryTheory.bicategoricalComp, rfl
-- 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
⊢ (leftZigzagIso η ε).inv = rightZigzag ε.inv η.inv

Tactic:
simp [bicategoricalComp, bicategoricalIsoComp]

Premises used: CategoryTheory.bicategoricalComp, CategoryTheory.bicategoricalIsoComp
-- 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
⊢ (rightZigzagIso η ε).inv = leftZigzag ε.inv η.inv

Tactic:
simp [bicategoricalComp, bicategoricalIsoComp]

Premises used: CategoryTheory.bicategoricalComp, CategoryTheory.bicategoricalIsoComp
-- 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
⊢ (leftZigzagIso η ε).symm = rightZigzagIso ε.symm η.symm

Tactic:
Iso.ext (leftZigzagIso_inv η ε)

Premises used: CategoryTheory.Bicategory.leftZigzagIso_inv, CategoryTheory.Iso.ext
-- 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
⊢ (rightZigzagIso η ε).symm = leftZigzagIso ε.symm η.symm

Tactic:
Iso.ext (rightZigzagIso_inv η ε)

Premises used: CategoryTheory.Bicategory.rightZigzagIso_inv, CategoryTheory.Iso.ext
-- 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
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ IsIso (leftZigzag η.hom ε.hom)

Tactic:
inferInstanceAs <| IsIso (leftZigzagIso η ε).hom

Premises used: _private.0.CategoryTheory.Bicategory.instIsIsoHomLeftZigzagHom._proof_1
-- 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
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ IsIso (rightZigzag η.hom ε.hom)

Tactic:
inferInstanceAs <| IsIso (rightZigzagIso η ε).hom

Premises used: _private.0.CategoryTheory.Bicategory.instIsIsoHomRightZigzagHom._proof_1
-- 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 η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv
rw :
  (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ rightZigzag η.hom ε.hom =
    (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ (ρ_ g).hom ≫ (λ_ g).inv
⊢ rightZigzag η.hom ε.hom = (ρ_ g).hom ≫ (λ_ g).inv

Tactic:
rw [← cancel_epi (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv)]

Premises used: CategoryTheory.Bicategory.rightUnitor, CategoryTheory.Bicategory.leftUnitor, CategoryTheory.Bicategory.rightZigzag, CategoryTheory.CategoryStruct.comp, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- 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 η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv
⊢ (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ rightZigzag η.hom ε.hom =
    rightZigzag η.hom ε.hom ⊗≫ rightZigzag η.hom ε.hom

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 η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv
⊢ rightZigzag η.hom ε.hom ⊗≫ rightZigzag η.hom ε.hom = rightZigzag η.hom ε.hom

Tactic:
rightZigzag_idempotent_of_left_triangle _ _ h

Premises used: CategoryTheory.Bicategory.rightZigzag_idempotent_of_left_triangle
-- 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 η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv
⊢ rightZigzag η.hom ε.hom = (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ (ρ_ g).hom ≫ (λ_ g).inv

Tactic:
simp
-- 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 η.hom ε.hom = (λ_ f).hom ≫ (ρ_ f).inv
_ :
  (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ rightZigzag η.hom ε.hom =
    rightZigzag η.hom ε.hom ⊗≫ rightZigzag η.hom ε.hom
_₁ : rightZigzag η.hom ε.hom = (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ (ρ_ g).hom ≫ (λ_ g).inv
⊢ (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ rightZigzag η.hom ε.hom =
    (rightZigzag η.hom ε.hom ≫ (λ_ g).hom ≫ (ρ_ g).inv) ≫ (ρ_ g).hom ≫ (λ_ g).inv

Tactic:
calc
    _ = rightZigzag η.hom ε.hom ⊗≫ rightZigzag η.hom ε.hom := by bicategory
    _ = rightZigzag η.hom ε.hom := rightZigzag_idempotent_of_left_triangle _ _ h
    _ = _ := by simp

Premises used: CategoryTheory.Bicategory.rightZigzag, CategoryTheory.Bicategory.rightZigzag_idempotent_of_left_triangle, CategoryTheory.Iso.hom
-- 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
w : (leftZigzagIso η (adjointifyCounit η ε)).hom = (λ_ f ≪≫ (ρ_ f).symm).hom
⊢ leftZigzagIso η (adjointifyCounit η ε) = λ_ f ≪≫ (ρ_ f).symm

Tactic:
apply Iso.ext

Premises used: CategoryTheory.Iso.ext
-- 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
w : leftZigzag η.hom (g ◁ ((ρ_ f).inv ≫ rightZigzag ε.inv η.inv ≫ (λ_ f).hom) ≫ ε.hom) = (λ_ f).hom ≫ (ρ_ f).inv
⊢ (leftZigzagIso η (adjointifyCounit η ε)).hom = (λ_ f ≪≫ (ρ_ f).symm).hom

Tactic:
dsimp [adjointifyCounit, bicategoricalIsoComp]

Premises used: CategoryTheory.bicategoricalIsoComp, CategoryTheory.Bicategory.adjointifyCounit
-- 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
⊢ leftZigzag η.hom (g ◁ ((ρ_ f).inv ≫ rightZigzag ε.inv η.inv ≫ (λ_ f).hom) ≫ ε.hom) =
    𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom

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
rw :
  𝟙 (𝟙 a ≫ f) ⊗≫ (𝟙 a ◁ f ◁ ε.inv ≫ η.hom ▷ (f ≫ g ≫ f)) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom

Tactic:
rw [← whisker_exchange η.hom (f ◁ ε.inv)]

Premises used: CategoryTheory.Bicategory.whisker_exchange, CategoryTheory.Bicategory.whiskerLeft, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- 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
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ (𝟙 a ◁ f ◁ ε.inv ≫ η.hom ▷ (f ≫ g ≫ f)) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom

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
rw :
  𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (𝟙 a ◁ η.inv ≫ η.hom ▷ 𝟙 a) ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom

Tactic:
rw [← whisker_exchange η.hom η.inv]

Premises used: CategoryTheory.Bicategory.whisker_exchange, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- 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
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (𝟙 a ◁ η.inv ≫ η.hom ▷ 𝟙 a) ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom

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
rw : 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ 𝟙 (f ≫ g) ▷ f ⊗≫ f ◁ ε.hom = 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom)
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom = 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom)

Tactic:
rw [Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id
-- 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
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ 𝟙 (f ≫ g) ▷ f ⊗≫ f ◁ ε.hom = 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom)

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
rw : 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ 𝟙 (𝟙 b) = (λ_ f).hom ≫ (ρ_ f).inv
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom) = (λ_ f).hom ≫ (ρ_ f).inv

Tactic:
rw [Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id
-- 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
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ 𝟙 (𝟙 b) = (λ_ f).hom ≫ (ρ_ f).inv

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
_ :
  leftZigzag η.hom (g ◁ ((ρ_ f).inv ≫ rightZigzag ε.inv η.inv ≫ (λ_ f).hom) ≫ ε.hom) =
    𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom
_₁ :
  𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom
_₂ :
  𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom
_₃ : 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom = 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom)
_₄ : 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom) = (λ_ f).hom ≫ (ρ_ f).inv
⊢ leftZigzag η.hom (g ◁ ((ρ_ f).inv ≫ rightZigzag ε.inv η.inv ≫ (λ_ f).hom) ≫ ε.hom) = (λ_ f).hom ≫ (ρ_ f).inv

Tactic:
calc
    _ = 𝟙 _ ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫
          f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom := by
      bicategory
    _ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom := by
      rw [← whisker_exchange η.hom (f ◁ ε.inv)]; bicategory
    _ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom := by
      rw [← whisker_exchange η.hom η.inv]; bicategory
    _ = 𝟙 _ ⊗≫ f ◁ (ε.inv ≫ ε.hom) := by
      rw [Iso.inv_hom_id]; bicategory
    _ = _ := by
      rw [Iso.inv_hom_id]; bicategory

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Bicategory.whiskerRight, CategoryTheory.CategoryStruct.comp, CategoryTheory.Bicategory.whiskerLeft, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- 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_1 ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
a : B
w :
  Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := a ⟶ a) (𝟙 a ≫ 𝟙 a) (𝟙 a ≫ 𝟙 a))
    (Iso.hom (leftZigzagIso (Iso.symm (ρ_ (𝟙 a))) (ρ_ (𝟙 a)))) (Iso.hom (λ_ (𝟙 a) ≪≫ Iso.symm (ρ_ (𝟙 a))))
⊢ Eq.{w + 1} (α := Iso.{w, v} (C := a ⟶ a) (𝟙 a ≫ 𝟙 a) (𝟙 a ≫ 𝟙 a)) (leftZigzagIso (Iso.symm (ρ_ (𝟙 a))) (ρ_ (𝟙 a)))
    (λ_ (𝟙 a) ≪≫ Iso.symm (ρ_ (𝟙 a)))

Tactic:
ext
-- 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_1 ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
a : B
⊢ Eq.{w + 1} (α := Quiver.Hom.{w, v} (V := a ⟶ a) (𝟙 a ≫ 𝟙 a) (𝟙 a ≫ 𝟙 a))
    (Iso.hom (leftZigzagIso (Iso.symm (ρ_ (𝟙 a))) (ρ_ (𝟙 a)))) (Iso.hom (λ_ (𝟙 a) ≪≫ Iso.symm (ρ_ (𝟙 a))))

Tactic:
simp [bicategoricalIsoComp]

Premises used: CategoryTheory.bicategoricalIsoComp
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
e : Equivalence.{w, v, u} a b
⊢ leftZigzag e.unit.hom e.counit.hom = (λ_ e.hom).hom ≫ (ρ_ e.hom).inv

Tactic:
congrArg Iso.hom e.left_triangle

Premises used: congrArg, CategoryTheory.Bicategory.Equivalence.left_triangle, CategoryTheory.Iso.hom, CategoryTheory.bicategoricalComp
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
e : Equivalence.{w, v, u} a b
⊢ rightZigzagIso e.unit e.counit = ρ_ e.inv ≪≫ (λ_ e.inv).symm

Tactic:
Iso.ext (right_triangle_of_left_triangle e.unit e.counit e.left_triangle_hom)

Premises used: CategoryTheory.Bicategory.right_triangle_of_left_triangle, CategoryTheory.Bicategory.Equivalence.unit, CategoryTheory.Bicategory.Equivalence.counit, CategoryTheory.Iso.ext, CategoryTheory.Bicategory.Equivalence.left_triangle_hom
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
Goal:
B : Type u
inst : Bicategory.{w, v, u} B
a b : B
e : Equivalence.{w, v, u} a b
⊢ rightZigzag e.unit.hom e.counit.hom = (ρ_ e.inv).hom ≫ (λ_ e.inv).inv

Tactic:
congrArg Iso.hom e.right_triangle

Premises used: congrArg, CategoryTheory.Bicategory.Equivalence.right_triangle, CategoryTheory.Iso.hom, CategoryTheory.bicategoricalComp
-- 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
adj : f ⊣ g
⊢ IsLeftAdjoint f

Tactic:
⟨⟨g, adj⟩⟩

Premises used: CategoryTheory.Bicategory.IsLeftAdjoint.mk', CategoryTheory.Bicategory.RightAdjoint.mk, Nonempty.intro
-- 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
adj : f ⊣ g
⊢ IsRightAdjoint g

Tactic:
⟨⟨f, adj⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Bicategory.IsRightAdjoint.mk', CategoryTheory.Bicategory.LeftAdjoint.mk
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
Goal:
C_1 D_1 E : Type u
inst : Category.{v, u} C_1
inst_1 : Category.{v, u} D_1
inst_2 : Category.{v, u} E
F_1 : Functor.{v, v, u, u} C_1 D_1
G_1 : Functor.{v, v, u, u} D_1 C_1
adj_1 : F_1 ⊣ G_1
F' : Functor.{v, v, u, u} D_1 E
G' : Functor.{v, v, u, u} E D_1
adj' : F' ⊣ G'
C D : Cat
F : C ⟶ D
G : D ⟶ C
adj : F ⊣ G
X : (↑C : Type u_2)
⊢ F.toFunctor.map (adj.unit.toNatTrans.app X) ≫ adj.counit.toNatTrans.app (F.toFunctor.obj X) = 𝟙 (F.toFunctor.obj X)

Tactic:
simpa using congr($(adj.left_triangle).toNatTrans.app X)
-- Module: Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
Goal:
C_1 D_1 E : Type u
inst : Category.{v, u} C_1
inst_1 : Category.{v, u} D_1
inst_2 : Category.{v, u} E
F_1 : Functor.{v, v, u, u} C_1 D_1
G_1 : Functor.{v, v, u, u} D_1 C_1
adj_1 : F_1 ⊣ G_1
F' : Functor.{v, v, u, u} D_1 E
G' : Functor.{v, v, u, u} E D_1
adj' : F' ⊣ G'
C D : Cat
F : C ⟶ D
G : D ⟶ C
adj : F ⊣ G
X : (↑D : Type u_2)
⊢ adj.unit.toNatTrans.app (G.toFunctor.obj X) ≫ G.toFunctor.map (adj.counit.toNatTrans.app X) = 𝟙 (G.toFunctor.obj X)

Tactic:
simpa using congr($(adj.right_triangle).toNatTrans.app X)