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

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 ⊗≫ ((β_ X (𝟙_ C)).hom ≫ η_ X Y ▷ X) ⊗≫ (X ◁ ε_ X Y ≫ (β_ (𝟙_ C) X).inv) ⊗≫ 𝟙 X = 𝟙 X

Tactic:
simp [monoidalComp]

Result:
no goals

Proof state:
case e_g.e_g.e_f
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 X).inv ≫ (α_ X Y X).inv ≫ (β_ X Y).hom ▷ X =
    (α_ X X Y).inv ≫
      (β_ X X).hom ▷ Y ≫
        (α_ X X Y).hom ≫
          X ◁ (β_ X Y).hom ≫ (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv

Tactic:
rw [← IsIso.eq_inv_comp]

Result:
case e_g.e_g.e_f
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 X).inv ≫ (β_ X Y).hom ▷ X =
    inv (X ◁ (β_ Y X).inv) ≫
      (α_ X X Y).inv ≫
        (β_ X X).hom ▷ Y ≫
          (α_ X X Y).hom ≫
            X ◁ (β_ X Y).hom ≫ (α_ X Y X).inv ≫ (β_ Y X).inv ▷ X ≫ (α_ Y X X).hom ≫ Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv

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 ⊗≫ (X ◁ η_ X Y ≫ (β_ X (X ⊗ Y)).hom) ⊗≫ ((β_ (Y ⊗ X) X).inv ≫ ε_ X Y ▷ X) ⊗≫ 𝟙 X = 𝟙 X

Tactic:
rw [braiding_naturality_right, ← braiding_inv_naturality_right]

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
⊢ 𝟙 X ⊗≫ ((β_ X (𝟙_ C)).hom ≫ η_ X Y ▷ X) ⊗≫ (X ◁ ε_ X Y ≫ (β_ (𝟙_ C) X).inv) ⊗≫ 𝟙 X = 𝟙 X

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 ⊗≫
      X ◁ η_ X Y ⊗≫
        (𝟙 (X ⊗ X ⊗ Y) ⊗≫
            (β_ X X).hom ▷ Y ⊗≫ X ◁ (β_ X Y).hom ⊗≫ (β_ Y X).inv ▷ X ⊗≫ Y ◁ (β_ X X).inv ⊗≫ 𝟙 ((Y ⊗ X) ⊗ X)) ⊗≫
          ε_ X Y ▷ X ⊗≫ 𝟙 X =
    𝟙 X ⊗≫ (X ◁ η_ X Y ≫ (β_ X (X ⊗ Y)).hom) ⊗≫ ((β_ (Y ⊗ X) X).inv ≫ ε_ X Y ▷ X) ⊗≫ 𝟙 X

Tactic:
simp [monoidalComp, braiding_tensor_right, braiding_inv_tensor_left]

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 ◁ (η_ X Y ≫ (β_ Y X).inv) ≫ (α_ X Y X).inv ≫ ((β_ X Y).hom ≫ ε_ X Y) ▷ X = (ρ_ X).hom ≫ (λ_ X).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
⊢ (ρ_ X).inv ≫ (X ◁ (η_ X Y ≫ (β_ Y X).inv) ≫ (α_ X Y X).inv ≫ ((β_ X Y).hom ≫ ε_ X Y) ▷ X) ≫ (λ_ X).hom = 𝟙 X

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).inv ≫ (X ◁ (η_ X Y ≫ (β_ Y X).inv) ≫ (α_ X Y X).inv ≫ ((β_ X Y).hom ≫ ε_ X Y) ▷ X) ≫ (λ_ X).hom = 𝟙 X

Tactic:
calc
  _ = 𝟙 X ⊗≫ X ◁ η_ X Y ⊗≫ (X ◁ (β_ Y X).inv ⊗≫ (β_ X Y).hom ▷ X) ⊗≫ ε_ X Y ▷ X ⊗≫ 𝟙 X := by
    monoidal
  _ = 𝟙 X ⊗≫ X ◁ η_ X Y ⊗≫ (𝟙 (X ⊗ X ⊗ Y) ⊗≫ (β_ X X).hom ▷ Y ⊗≫ X ◁ (β_ X Y).hom
        ⊗≫ (β_ Y X).inv ▷ X ⊗≫ Y ◁ (β_ X X).inv ⊗≫ 𝟙 ((Y ⊗ X) ⊗ X)) ⊗≫ ε_ X Y ▷ X ⊗≫ 𝟙 X := by
    congr 3
    simp only [monoidalComp, MonoidalCoherence.assoc'_iso, MonoidalCoherence.whiskerRight_iso,
      MonoidalCoherence.refl_iso, whiskerRightIso_refl, Iso.refl_trans, Iso.symm_hom,
      MonoidalCoherence.assoc_iso, Iso.trans_refl, comp_id, id_comp]
    rw [← IsIso.eq_inv_comp]
    repeat rw [← assoc]
    iterate 5 rw [← IsIso.comp_inv_eq]
    simpa using yang_baxter X Y X
  _ = 𝟙 X ⊗≫ (X ◁ η_ X Y ≫ (β_ X (X ⊗ Y)).hom) ⊗≫ ((β_ (Y ⊗ X) X).inv ≫ ε_ X Y ▷ X) ⊗≫ 𝟙 X := by
    simp [monoidalComp, braiding_tensor_right, braiding_inv_tensor_left]
  _ = _ := by
    rw [braiding_naturality_right, ← braiding_inv_naturality_right]
    simp [monoidalComp]

Result:
no goals

Proof state:
case e_g.e_g.e_f
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 X).inv ≫ (β_ X Y).hom ▷ X) ≫ inv (α_ Y X X).inv) ≫ inv (Y ◁ (β_ X X).inv)) ≫ inv (α_ Y X X).hom) ≫
      inv ((β_ Y X).inv ▷ X) =
    ((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
      (α_ X Y X).inv

Tactic:
rw [← IsIso.comp_inv_eq]

Result:
case e_g.e_g.e_f
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 X).inv ≫ (β_ X Y).hom ▷ X) ≫ inv (α_ Y X X).inv) ≫ inv (Y ◁ (β_ X X).inv)) ≫ inv (α_ Y X X).hom) ≫
        inv ((β_ Y X).inv ▷ X)) ≫
      inv (α_ X Y X).inv =
    (((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom

Proof state:
case e_g.e_g.e_f
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 X).inv ≫ (β_ X Y).hom ▷ X =
    (((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
            (α_ X Y X).inv) ≫
          (β_ Y X).inv ▷ X) ≫
        (α_ Y X X).hom) ≫
      Y ◁ (β_ X X).inv ≫ (α_ Y X X).inv

Tactic:
rw [← assoc]

Result:
case e_g.e_g.e_f
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 X).inv ≫ (β_ X Y).hom ▷ X =
    ((((((((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom) ≫
              (α_ X Y X).inv) ≫
            (β_ Y X).inv ▷ X) ≫
          (α_ Y X X).hom) ≫
        Y ◁ (β_ X X).inv) ≫
      (α_ Y X X).inv

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 ⊗≫ X ◁ η_ X Y ⊗≫ (X ◁ (β_ Y X).inv ⊗≫ (β_ X Y).hom ▷ X) ⊗≫ ε_ X Y ▷ X ⊗≫ 𝟙 X =
    𝟙 X ⊗≫
      X ◁ η_ X Y ⊗≫
        (𝟙 (X ⊗ X ⊗ Y) ⊗≫
            (β_ X X).hom ▷ Y ⊗≫ X ◁ (β_ X Y).hom ⊗≫ (β_ Y X).inv ▷ X ⊗≫ Y ◁ (β_ X X).inv ⊗≫ 𝟙 ((Y ⊗ X) ⊗ X)) ⊗≫
          ε_ X Y ▷ X ⊗≫ 𝟙 X

Tactic:
congr 3

Result:
case e_g.e_g.e_f
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 X).inv ⊗≫ (β_ X Y).hom ▷ X =
    𝟙 (X ⊗ X ⊗ Y) ⊗≫ (β_ X X).hom ▷ Y ⊗≫ X ◁ (β_ X Y).hom ⊗≫ (β_ Y X).inv ▷ X ⊗≫ Y ◁ (β_ X X).inv ⊗≫ 𝟙 ((Y ⊗ X) ⊗ X)

Proof state:
case e_g.e_g.e_f
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 X).inv ≫ (β_ X Y).hom ▷ X) ≫ inv (α_ Y X X).inv) ≫ inv (Y ◁ (β_ X X).inv)) ≫ inv (α_ Y X X).hom) ≫
        inv ((β_ Y X).inv ▷ X)) ≫
      inv (α_ X Y X).inv =
    (((inv (X ◁ (β_ Y X).inv) ≫ (α_ X X Y).inv) ≫ (β_ X X).hom ▷ Y) ≫ (α_ X X Y).hom) ≫ X ◁ (β_ X Y).hom

Tactic:
simpa using yang_baxter X Y X

Result:
no goals