-- 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:
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
⊢ (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

Tactic:
ext k i₁ i₂ i₃ h

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 ≫ (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

Proof state:
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
⊢ i₂ + i₁ + i₃ = k

Tactic:
rw [add_comm i₂ i₁, h]

Result:
no goals

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 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

Tactic:
conv_lhs => rw [ιTensorObj₃'_associator_hom_assoc, ιTensorObj₃_eq X Y Z i₁ i₂ i₃ k h _ rfl,
  assoc, ι_tensorObjDesc_assoc, assoc, ← MonoidalCategory.id_tensorHom,
  BraidedCategory.braiding_naturality_assoc,
  BraidedCategory.braiding_tensor_right, assoc, assoc, assoc, assoc, Iso.hom_inv_id_assoc,
  MonoidalCategory.tensorHom_id,
  ← ιTensorObj₃'_eq_assoc Y Z X i₂ i₃ i₁ k (by rw [add_comm _ i₁, ← add_assoc, h]) _ rfl,
  ιTensorObj₃'_associator_hom, Iso.inv_hom_id_assoc]

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
⊢ 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

Proof state:
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
⊢ i₂ + i₃ + i₁ = k

Tactic:
rw [add_comm _ i₁, ← add_assoc, h]

Result:
no goals