-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Braided (goal)
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} (α := X ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)))
      (Iso.inv (ρ_ X))
      ((X ◁ (η_ X Y ≫ Iso.inv (β_ Y X)) ≫ Iso.inv (α_ X Y X) ≫ (Iso.hom (β_ X Y) ≫ ε_ X Y) ▷ X) ≫ Iso.hom (λ_ X)))
    (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorUnit.{v_1, u_1} C (𝒞 := inst_1))) (𝟙 X)
      (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y)) (X ◁ η_ X Y)
        (monoidalComp (X := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X) (Y :=
          tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X)
          (X ◁ Iso.inv (β_ Y X) ⊗≫ Iso.hom (β_ X Y) ▷ X) (ε_ X Y ▷ X ⊗≫ 𝟙 X))))
_₁ :
  Eq.{v_1 + 1} (α := X ⟶ X)
    (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorUnit.{v_1, u_1} C (𝒞 := inst_1))) (𝟙 X)
      (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y)) (X ◁ η_ X Y)
        (monoidalComp (X := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X) (Y :=
          tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X)
          (X ◁ Iso.inv (β_ Y X) ⊗≫ Iso.hom (β_ X Y) ▷ X) (ε_ X Y ▷ X ⊗≫ 𝟙 X))))
    (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorUnit.{v_1, u_1} C (𝒞 := inst_1))) (𝟙 X)
      (X ◁ η_ X Y ⊗≫
        monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X)
          (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X X) Y)
            (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y)))
            (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y))
              (Iso.hom (β_ X X) ▷ Y)
              (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) X)
                (X ◁ Iso.hom (β_ X Y))
                (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X X))
                  (Iso.inv (β_ Y X) ▷ X)
                  (Y ◁ Iso.inv (β_ X X) ⊗≫
                    𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X))))))
          (ε_ X Y ▷ X ⊗≫ 𝟙 X)))
_₂ :
  monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorUnit.{v_1, u_1} C (𝒞 := inst_1))) (𝟙 X)
      (X ◁ η_ X Y ⊗≫
        monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X)
          (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X X) Y)
            (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y)))
            (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y))
              (Iso.hom (β_ X X) ▷ Y)
              (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) X)
                (X ◁ Iso.hom (β_ X Y))
                (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X X))
                  (Iso.inv (β_ Y X) ▷ X)
                  (Y ◁ Iso.inv (β_ X X) ⊗≫
                    𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X))))))
          (ε_ X Y ▷ X ⊗≫ 𝟙 X)) =
    monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorUnit.{v_1, u_1} C (𝒞 := inst_1))) (𝟙 X)
      (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
        (X ◁ η_ X Y ≫ Iso.hom (β_ X (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y)))
        ((Iso.inv (β_ (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X) ≫ ε_ X Y ▷ X) ⊗≫ 𝟙 X))
⊢ Eq.{v_1 + 1} (α := X ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)))
      (Iso.inv (ρ_ X))
      ((X ◁ (η_ X Y ≫ Iso.inv (β_ Y X)) ≫ Iso.inv (α_ X Y X) ≫ (Iso.hom (β_ X Y) ≫ ε_ X Y) ▷ X) ≫ Iso.hom (λ_ X)))
    (𝟙 X)
have _₃ : monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorUnit.{v_1, u_1} C (𝒞 := inst_1))) (𝟙 X)
    (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
      (X ◁ η_ X Y ≫ Iso.hom (β_ X (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y)))
      ((Iso.inv (β_ (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X) ≫ ε_ X Y ▷ X) ⊗≫ 𝟙 X)) =
  𝟙 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_hom, braiding_tensor_left_inv]
    _ = _ := by
      rw [braiding_naturality_right, ← braiding_inv_naturality_right]
      simp [monoidalComp]