-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
_ :
  Eq.{v_1 + 1} (α := Y ⟶ Y)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y)
      (Iso.inv (λ_ Y))
      (((η_ X Y ≫ Iso.inv (β_ Y X)) ▷ Y ≫ Iso.hom (α_ Y X Y) ≫ Y ◁ (Iso.hom (β_ X Y) ≫ ε_ X Y)) ≫ Iso.hom (ρ_ Y)))
    (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y) (𝟙 Y)
      (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y) (η_ X Y ▷ Y)
        (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
          (Iso.inv (β_ Y X) ▷ Y ⊗≫ Y ◁ Iso.hom (β_ X Y)) (Y ◁ ε_ X Y ⊗≫ 𝟙 Y))))
_₁ :
  Eq.{v_1 + 1} (α := Y ⟶ Y)
    (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y) (𝟙 Y)
      (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y) (η_ X Y ▷ Y)
        (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
          (Iso.inv (β_ Y X) ▷ Y ⊗≫ Y ◁ Iso.hom (β_ X Y)) (Y ◁ ε_ X Y ⊗≫ 𝟙 Y))))
    (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y) (𝟙 Y)
      (η_ X Y ▷ Y ⊗≫
        monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
          (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y Y))
            (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y))
            (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y)
              (X ◁ Iso.hom (β_ Y Y))
              (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y))
                (Iso.hom (β_ X Y) ▷ Y)
                (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y Y) X)
                  (Y ◁ Iso.inv (β_ Y X))
                  (Iso.inv (β_ Y Y) ▷ X ⊗≫
                    𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X)))))))
          (Y ◁ ε_ X Y ⊗≫ 𝟙 Y)))
_₂ :
  monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y) (𝟙 Y)
      (η_ X Y ▷ Y ⊗≫
        monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
          (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y Y))
            (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y))
            (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y)
              (X ◁ Iso.hom (β_ Y Y))
              (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y))
                (Iso.hom (β_ X Y) ▷ Y)
                (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y Y) X)
                  (Y ◁ Iso.inv (β_ Y X))
                  (Iso.inv (β_ Y Y) ▷ X ⊗≫
                    𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X)))))))
          (Y ◁ ε_ X Y ⊗≫ 𝟙 Y)) =
    monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y) (𝟙 Y)
      (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) Y)
        (η_ X Y ▷ Y ≫ Iso.hom (β_ (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y))
        ((Iso.inv (β_ Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X)) ≫ Y ◁ ε_ X Y) ⊗≫ 𝟙 Y))
_₃ :
  monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y) (𝟙 Y)
      (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) Y)
        (η_ X Y ▷ Y ≫ Iso.hom (β_ (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y))
        ((Iso.inv (β_ Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X)) ≫ Y ◁ ε_ X Y) ⊗≫ 𝟙 Y)) =
    𝟙 Y
⊢ Eq.{v_1 + 1} (α := Y ⟶ Y)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y)
      (Iso.inv (λ_ Y))
      (((η_ X Y ≫ Iso.inv (β_ Y X)) ▷ Y ≫ Iso.hom (α_ Y X Y) ≫ Y ◁ (Iso.hom (β_ X Y) ≫ ε_ X Y)) ≫ Iso.hom (ρ_ Y)))
    (𝟙 Y)

Tactic:
calc
    _ = 𝟙 Y ⊗≫ η_ X Y ▷ Y ⊗≫ ((β_ Y X).inv ▷ Y ⊗≫ Y ◁ (β_ X Y).hom) ≫ Y ◁ ε_ X Y ⊗≫ 𝟙 Y := by
      monoidal
    _ = 𝟙 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 := by
      congr 3
      on_goal 2 => simp [monoidalComp]
      simp only [monoidalComp, MonoidalCoherence.assoc_iso, MonoidalCoherence.whiskerRight_iso,
        MonoidalCoherence.refl_iso, whiskerRightIso_refl, Iso.trans_refl,
        MonoidalCoherence.assoc'_iso, Iso.refl_trans, Iso.symm_hom, comp_id, id_comp]
      iterate 2 rw [← IsIso.eq_inv_comp]
      repeat rw [← assoc]
      iterate 4 rw [← IsIso.comp_inv_eq]
      simpa using (yang_baxter Y X Y).symm
    _ = 𝟙 Y ⊗≫ (η_ X Y ▷ Y ≫ (β_ (X ⊗ Y) Y).hom) ⊗≫ ((β_ Y (Y ⊗ X)).inv ≫ Y ◁ ε_ X Y) ⊗≫ 𝟙 Y := by
      simp [monoidalComp, braiding_tensor_left_hom, braiding_tensor_right_inv]
    _ = _ := by
      rw [braiding_naturality_left, ← braiding_inv_naturality_left]
      simp [monoidalComp]

Premises used: CategoryTheory.MonoidalCategoryStruct.whiskerLeft, CategoryTheory.monoidalComp, CategoryTheory.CategoryStruct.id, CategoryTheory.MonoidalCategoryStruct.whiskerRight, CategoryTheory.ExactPairing.evaluation, CategoryTheory.MonoidalCategoryStruct.tensorObj, CategoryTheory.CategoryStruct.comp, CategoryTheory.BraidedCategory.braiding, CategoryTheory.ExactPairing.coevaluation, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv