-- Mathlib/CategoryTheory/Monoidal/Rigid/Braided.lean
theorem evaluation_coevaluation_braided' [inst : ExactPairing X Y] :
    (η_ X Y ≫ (β_ Y X).inv) ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ ((β_ X Y).hom ≫ ε_ X Y) =
      (λ_ Y).hom ≫ (ρ_ Y).inv

Proof state:
case e_g.e_g.e_a
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ ε_ X Y ⊗≫ 𝟙 Y = ⊗𝟙.hom ≫ Y ◁ ε_ X Y ⊗≫ 𝟙 Y

Tactic:
simp [monoidalComp]

Result:
no goals

Proof state:
case e_g.e_g.e_a
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ ((Y ◁ (β_ X Y).hom ≫ inv (α_ Y Y X).hom) ≫ inv ((β_ Y Y).inv ▷ X)) ≫ inv (α_ Y Y X).inv =
    ((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
          (β_ X Y).hom ▷ Y) ≫
        (α_ Y X Y).hom) ≫
      Y ◁ (β_ Y X).inv

Tactic:
rw [← IsIso.comp_inv_eq]

Result:
case e_g.e_g.e_a
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (((Y ◁ (β_ X Y).hom ≫ inv (α_ Y Y X).hom) ≫ inv ((β_ Y Y).inv ▷ X)) ≫ inv (α_ Y Y X).inv) ≫ inv (Y ◁ (β_ Y X).inv) =
    (((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
        (β_ X Y).hom ▷ Y) ≫
      (α_ Y X Y).hom

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (λ_ Y).inv ≫ ((η_ X Y ≫ (β_ Y X).inv) ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ ((β_ X Y).hom ≫ ε_ X Y)) ≫ (ρ_ Y).hom =
    𝟙 Y ⊗≫ η_ X Y ▷ Y ⊗≫ ((β_ Y X).inv ▷ Y ⊗≫ Y ◁ (β_ X Y).hom) ≫ Y ◁ ε_ X Y ⊗≫ 𝟙 Y

Tactic:
monoidal

Result:
no goals

Proof state:
case e_g.e_g.e_a
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (((Y ◁ (β_ X Y).hom ≫ inv (α_ Y Y X).hom) ≫ inv ((β_ Y Y).inv ▷ X)) ≫ inv (α_ Y Y X).inv) ≫ inv (Y ◁ (β_ Y X).inv) =
    (((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
        (β_ X Y).hom ▷ Y) ≫
      (α_ Y X Y).hom

Tactic:
simpa using (yang_baxter Y X Y).symm

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (η_ X Y ≫ (β_ Y X).inv) ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ ((β_ X Y).hom ≫ ε_ X Y) = (λ_ Y).hom ≫ (ρ_ Y).inv

Tactic:
rw [Iso.eq_comp_inv, ← Iso.inv_comp_eq_id]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (λ_ Y).inv ≫ ((η_ X Y ≫ (β_ Y X).inv) ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ ((β_ X Y).hom ≫ ε_ X Y)) ≫ (ρ_ Y).hom = 𝟙 Y

Proof state:
case e_g.e_g.e_a
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    ((((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
              (β_ X Y).hom ▷ Y) ≫
            (α_ Y X Y).hom) ≫
          Y ◁ (β_ Y X).inv) ≫
        (α_ Y Y X).inv) ≫
      (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
rw [← assoc]

Result:
case e_g.e_g.e_a
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    (((((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
                (β_ X Y).hom ▷ Y) ≫
              (α_ Y X Y).hom) ≫
            Y ◁ (β_ Y X).inv) ≫
          (α_ Y Y X).inv) ≫
        (β_ Y Y).inv ▷ X) ≫
      (α_ Y Y X).hom

Proof state:
case e_g.e_g.e_a
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (β_ Y X).inv ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ X Y).hom =
    (α_ X Y Y).hom ≫
      X ◁ (β_ Y Y).hom ≫
        (α_ X Y Y).inv ≫
          (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
iterate 2 rw [← IsIso.eq_inv_comp]

Result:
case e_g.e_g.e_a
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    inv (α_ Y X Y).hom ≫
      inv ((β_ Y X).inv ▷ Y) ≫
        (α_ X Y Y).hom ≫
          X ◁ (β_ Y Y).hom ≫
            (α_ X Y Y).inv ≫
              (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Proof state:
case e_g.e_g.e_a
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    (((((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
                (β_ X Y).hom ▷ Y) ≫
              (α_ Y X Y).hom) ≫
            Y ◁ (β_ Y X).inv) ≫
          (α_ Y Y X).inv) ≫
        (β_ Y Y).inv ▷ X) ≫
      (α_ Y Y X).hom

Tactic:
iterate 4 rw [← IsIso.comp_inv_eq]

Result:
case e_g.e_g.e_a
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ (((Y ◁ (β_ X Y).hom ≫ inv (α_ Y Y X).hom) ≫ inv ((β_ Y Y).inv ▷ X)) ≫ inv (α_ Y Y X).inv) ≫ inv (Y ◁ (β_ Y X).inv) =
    (((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
        (β_ X Y).hom ▷ Y) ≫
      (α_ Y X Y).hom

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ 𝟙 Y ⊗≫ ((β_ (𝟙_ C) Y).hom ≫ Y ◁ η_ X Y) ⊗≫ (ε_ X Y ▷ Y ≫ (β_ Y (𝟙_ C)).inv) ⊗≫ 𝟙 Y = 𝟙 Y

Tactic:
simp [monoidalComp]

Result:
no goals

Proof state:
case e_g.e_g.e_a
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    inv (α_ Y X Y).hom ≫
      inv ((β_ Y X).inv ▷ Y) ≫
        (α_ X Y Y).hom ≫
          X ◁ (β_ Y Y).hom ≫
            (α_ X Y Y).inv ≫
              (β_ X Y).hom ▷ Y ≫ (α_ Y X Y).hom ≫ Y ◁ (β_ Y X).inv ≫ (α_ Y Y X).inv ≫ (β_ Y Y).inv ▷ X ≫ (α_ Y Y X).hom

Tactic:
repeat rw [← assoc]

Result:
case e_g.e_g.e_a
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ Y ◁ (β_ X Y).hom =
    (((((((((inv (α_ Y X Y).hom ≫ inv ((β_ Y X).inv ▷ Y)) ≫ (α_ X Y Y).hom) ≫ X ◁ (β_ Y Y).hom) ≫ (α_ X Y Y).inv) ≫
                (β_ X Y).hom ▷ Y) ≫
              (α_ Y X Y).hom) ≫
            Y ◁ (β_ Y X).inv) ≫
          (α_ Y Y X).inv) ≫
        (β_ Y Y).inv ▷ X) ≫
      (α_ Y Y X).hom

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y : C
inst : ExactPairing X Y
⊢ 𝟙 Y ⊗≫
      η_ X Y ▷ Y ⊗≫
        (𝟙 ((X ⊗ Y) ⊗ Y) ⊗≫
            X ◁ (β_ Y Y).hom ⊗≫ (β_ X Y).hom ▷ Y ⊗≫ Y ◁ (β_ Y X).inv ⊗≫ (β_ Y Y).inv ▷ X ⊗≫ 𝟙 (Y ⊗ Y ⊗ X)) ⊗≫
          Y ◁ ε_ X Y ⊗≫ 𝟙 Y =
    𝟙 Y ⊗≫ (η_ X Y ▷ Y ≫ (β_ (X ⊗ Y) Y).hom) ⊗≫ ((β_ Y (Y ⊗ X)).inv ≫ Y ◁ ε_ X Y) ⊗≫ 𝟙 Y

Tactic:
simp [monoidalComp, braiding_tensor_left, braiding_inv_tensor_right]

Result:
no goals