-- Mathlib/CategoryTheory/GradedObject/Braiding.lean
lemma hexagon_forward [HasTensor X Y] [HasTensor Y X] [HasTensor Y Z]
    [HasTensor Z X] [HasTensor X Z]
    [HasTensor (tensorObj X Y) Z] [HasTensor X (tensorObj Y Z)]
    [HasTensor (tensorObj Y Z) X] [HasTensor Y (tensorObj Z X)]
    [HasTensor (tensorObj Y X) Z] [HasTensor Y (tensorObj X Z)]
    [HasGoodTensor₁₂Tensor X Y Z] [HasGoodTensorTensor₂₃ X Y Z]
    [HasGoodTensor₁₂Tensor Y Z X] [HasGoodTensorTensor₂₃ Y Z X]
    [HasGoodTensor₁₂Tensor Y X Z] [HasGoodTensorTensor₂₃ Y X Z] :
    (associator X Y Z).hom ≫ (braiding X (tensorObj Y Z)).hom ≫ (associator Y Z X).hom =
      whiskerRight (braiding X Y).hom Z ≫ (associator Y X Z).hom ≫
        whiskerLeft Y (braiding X Z).hom

Proof state:
case h.h
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{u_3, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
⊢ ιTensorObj₃' X Y Z i₁ i₂ i₃ k h ≫
      ((associator X Y Z).hom ≫ (braiding X (tensorObj Y Z)).hom ≫ (associator Y Z X).hom) k =
    ιTensorObj₃' X Y Z i₁ i₂ i₃ k h ≫
      (whiskerRight (braiding X Y).hom Z ≫ (associator Y X Z).hom ≫ whiskerLeft Y (braiding X Z).hom) k

Tactic:
dsimp [braiding]

Result:
case h.h
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{u_3, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
⊢ ιTensorObj₃' X Y Z i₁ i₂ i₃ k h ≫
      (associator X Y Z).hom k ≫
        (tensorObjDesc fun i j hij => (β_ (X i) (tensorObj Y Z j)).hom ≫ ιTensorObj (tensorObj Y Z) X j i k ⋯) ≫
          (associator Y Z X).hom k =
    ιTensorObj₃' X Y Z i₁ i₂ i₃ k h ≫
      whiskerRight (fun k => tensorObjDesc fun i j hij => (β_ (X i) (Y j)).hom ≫ ιTensorObj Y X j i k ⋯) Z k ≫
        (associator Y X Z).hom k ≫
          whiskerLeft Y (fun k => tensorObjDesc fun i j hij => (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) k

Proof state:
case h.h
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{u_3, u_2} C
inst✝¹⁸ : MonoidalCategory C
X Y Z : GradedObject I C
inst✝¹⁷ : BraidedCategory C
inst✝¹⁶ : X.HasTensor Y
inst✝¹⁵ : Y.HasTensor X
inst✝¹⁴ : Y.HasTensor Z
inst✝¹³ : Z.HasTensor X
inst✝¹² : X.HasTensor Z
inst✝¹¹ : (tensorObj X Y).HasTensor Z
inst✝¹⁰ : X.HasTensor (tensorObj Y Z)
inst✝⁹ : (tensorObj Y Z).HasTensor X
inst✝⁸ : Y.HasTensor (tensorObj Z X)
inst✝⁷ : (tensorObj Y X).HasTensor Z
inst✝⁶ : Y.HasTensor (tensorObj X Z)
inst✝⁵ : X.HasGoodTensor₁₂Tensor Y Z
inst✝⁴ : X.HasGoodTensorTensor₂₃ Y Z
inst✝³ : Y.HasGoodTensor₁₂Tensor Z X
inst✝² : Y.HasGoodTensorTensor₂₃ Z X
inst✝¹ : Y.HasGoodTensor₁₂Tensor X Z
inst✝ : Y.HasGoodTensorTensor₂₃ X Z
k i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = k
⊢ MonoidalCategoryStruct.whiskerRight (β_ (X i₁) (Y i₂)).hom (Z i₃) ≫
      (MonoidalCategoryStruct.associator (Y i₂) (X i₁) (Z i₃)).hom ≫
        MonoidalCategoryStruct.whiskerLeft (Y i₂) (β_ (X i₁) (Z i₃)).hom ≫ ιTensorObj₃ Y Z X i₂ i₃ i₁ k ⋯ =
    ιTensorObj₃' X Y Z i₁ i₂ i₃ k h ≫
      whiskerRight (fun k => tensorObjDesc fun i j hij => (β_ (X i) (Y j)).hom ≫ ιTensorObj Y X j i k ⋯) Z k ≫
        (associator Y X Z).hom k ≫
          whiskerLeft Y (fun k => tensorObjDesc fun i j hij => (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) k

Tactic:
conv_rhs => rw [ιTensorObj₃'_eq X Y Z i₁ i₂ i₃ k h _ rfl, assoc, ι_tensorHom_assoc,
  ← MonoidalCategory.tensorHom_id,
  ← MonoidalCategory.tensor_comp_assoc, id_comp, ι_tensorObjDesc,
  categoryOfGradedObjects_id, MonoidalCategory.comp_tensor_id, assoc,
  MonoidalCategory.tensorHom_id, MonoidalCategory.tensorHom_id,
  ← ιTensorObj₃'_eq_assoc Y X Z i₂ i₁ i₃ k
    (by rw [add_comm i₂ i₁, h]) (i₁ + i₂) (add_comm i₂ i₁),
  ιTensorObj₃'_associator_hom_assoc,
  ιTensorObj₃_eq Y X Z i₂ i₁ i₃ k (by rw [add_comm i₂ i₁, h]) _ rfl, assoc,
  ι_tensorHom, categoryOfGradedObjects_id, ← MonoidalCategory.tensorHom_id,
  ← MonoidalCategory.id_tensorHom,
  ← MonoidalCategory.id_tensor_comp_assoc,
  ι_tensorObjDesc, MonoidalCategory.id_tensor_comp, assoc,
  ← MonoidalCategory.id_tensor_comp_assoc, MonoidalCategory.tensorHom_id,
  MonoidalCategory.id_tensorHom, MonoidalCategory.whiskerLeft_comp, assoc,
  ← ιTensorObj₃_eq Y Z X i₂ i₃ i₁ k (by rw [add_comm _ i₁, ← add_assoc, h])
    (i₁ + i₃) (add_comm _ _ )]

Result:
no goals