mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, 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.associator (X i₁) (Y i₂) (Z i₃)).hom ≫
    (MonoidalCategoryStruct.whiskerLeft (X i₁) (ιTensorObj Y Z i₂ i₃ (i₂ + i₃) ⋯) ≫
        ιTensorObj X (tensorObj Y Z) i₁ (i₂ + i₃) 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

Tactic:
assoc,

Goal state after:
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, 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.associator (X i₁) (Y i₂) (Z i₃)).hom ≫
    MonoidalCategoryStruct.whiskerLeft (X i₁) (ιTensorObj Y Z i₂ i₃ (i₂ + i₃) ⋯) ≫
      ιTensorObj X (tensorObj Y Z) i₁ (i₂ + i₃) 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
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, 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.associator (X i₁) (Y i₂) (Z i₃)).hom ≫
    MonoidalCategoryStruct.whiskerLeft (X i₁) (ιTensorObj Y Z i₂ i₃ (i₂ + i₃) ⋯) ≫
      ((β_ (X i₁) (tensorObj Y Z (i₂ + i₃))).hom ≫ ιTensorObj (tensorObj Y Z) X (i₂ + i₃) i₁ k ⋯) ≫
        (associator Y Z X).hom k

Tactic:
assoc,

Goal state after:
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, 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.associator (X i₁) (Y i₂) (Z i₃)).hom ≫
    MonoidalCategoryStruct.whiskerLeft (X i₁) (ιTensorObj Y Z i₂ i₃ (i₂ + i₃) ⋯) ≫
      (β_ (X i₁) (tensorObj Y Z (i₂ + i₃))).hom ≫
        ιTensorObj (tensorObj Y Z) X (i₂ + i₃) i₁ k ⋯ ≫ (associator Y Z X).hom k
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, 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.associator (X i₁) (Y i₂) (Z i₃)).hom ≫
    ((MonoidalCategoryStruct.associator (X i₁) (Y i₂) (Z i₃)).inv ≫
        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 ≫
              (MonoidalCategoryStruct.associator (Y i₂) (Z i₃) (X i₁)).inv) ≫
      MonoidalCategoryStruct.tensorHom (ιTensorObj Y Z i₂ i₃ (i₂ + i₃) ⋯) (𝟙 (X i₁)) ≫
        ιTensorObj (tensorObj Y Z) X (i₂ + i₃) i₁ k ⋯ ≫ (associator Y Z X).hom k

Tactic:
assoc,

Goal state after:
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, 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.associator (X i₁) (Y i₂) (Z i₃)).hom ≫
    (MonoidalCategoryStruct.associator (X i₁) (Y i₂) (Z i₃)).inv ≫
      (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 ≫
              (MonoidalCategoryStruct.associator (Y i₂) (Z i₃) (X i₁)).inv) ≫
        MonoidalCategoryStruct.tensorHom (ιTensorObj Y Z i₂ i₃ (i₂ + i₃) ⋯) (𝟙 (X i₁)) ≫
          ιTensorObj (tensorObj Y Z) X (i₂ + i₃) i₁ k ⋯ ≫ (associator Y Z X).hom k
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, 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.associator (X i₁) (Y i₂) (Z i₃)).hom ≫
    (MonoidalCategoryStruct.associator (X i₁) (Y i₂) (Z i₃)).inv ≫
      (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 ≫
              (MonoidalCategoryStruct.associator (Y i₂) (Z i₃) (X i₁)).inv) ≫
        MonoidalCategoryStruct.tensorHom (ιTensorObj Y Z i₂ i₃ (i₂ + i₃) ⋯) (𝟙 (X i₁)) ≫
          ιTensorObj (tensorObj Y Z) X (i₂ + i₃) i₁ k ⋯ ≫ (associator Y Z X).hom k

Tactic:
assoc,

Goal state after:
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, 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.associator (X i₁) (Y i₂) (Z i₃)).hom ≫
    (MonoidalCategoryStruct.associator (X i₁) (Y i₂) (Z i₃)).inv ≫
      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 ≫
              (MonoidalCategoryStruct.associator (Y i₂) (Z i₃) (X i₁)).inv) ≫
          MonoidalCategoryStruct.tensorHom (ιTensorObj Y Z i₂ i₃ (i₂ + i₃) ⋯) (𝟙 (X i₁)) ≫
            ιTensorObj (tensorObj Y Z) X (i₂ + i₃) i₁ k ⋯ ≫ (associator Y Z X).hom k
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, 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.associator (X i₁) (Y i₂) (Z i₃)).hom ≫
    (MonoidalCategoryStruct.associator (X i₁) (Y i₂) (Z i₃)).inv ≫
      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 ≫
              (MonoidalCategoryStruct.associator (Y i₂) (Z i₃) (X i₁)).inv) ≫
          MonoidalCategoryStruct.tensorHom (ιTensorObj Y Z i₂ i₃ (i₂ + i₃) ⋯) (𝟙 (X i₁)) ≫
            ιTensorObj (tensorObj Y Z) X (i₂ + i₃) i₁ k ⋯ ≫ (associator Y Z X).hom k

Tactic:
assoc,

Goal state after:
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, 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.associator (X i₁) (Y i₂) (Z i₃)).hom ≫
    (MonoidalCategoryStruct.associator (X i₁) (Y i₂) (Z i₃)).inv ≫
      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 ≫
              (MonoidalCategoryStruct.associator (Y i₂) (Z i₃) (X i₁)).inv) ≫
            MonoidalCategoryStruct.tensorHom (ιTensorObj Y Z i₂ i₃ (i₂ + i₃) ⋯) (𝟙 (X i₁)) ≫
              ιTensorObj (tensorObj Y Z) X (i₂ + i₃) i₁ k ⋯ ≫ (associator Y Z X).hom k
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, 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.associator (X i₁) (Y i₂) (Z i₃)).hom ≫
    (MonoidalCategoryStruct.associator (X i₁) (Y i₂) (Z i₃)).inv ≫
      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 ≫
              (MonoidalCategoryStruct.associator (Y i₂) (Z i₃) (X i₁)).inv) ≫
            MonoidalCategoryStruct.tensorHom (ιTensorObj Y Z i₂ i₃ (i₂ + i₃) ⋯) (𝟙 (X i₁)) ≫
              ιTensorObj (tensorObj Y Z) X (i₂ + i₃) i₁ k ⋯ ≫ (associator Y Z X).hom k

Tactic:
assoc,

Goal state after:
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, 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.associator (X i₁) (Y i₂) (Z i₃)).hom ≫
    (MonoidalCategoryStruct.associator (X i₁) (Y i₂) (Z i₃)).inv ≫
      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 ≫
            (MonoidalCategoryStruct.associator (Y i₂) (Z i₃) (X i₁)).inv ≫
              MonoidalCategoryStruct.tensorHom (ιTensorObj Y Z i₂ i₃ (i₂ + i₃) ⋯) (𝟙 (X i₁)) ≫
                ιTensorObj (tensorObj Y Z) X (i₂ + i₃) i₁ k ⋯ ≫ (associator Y Z X).hom k
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, 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 (ιTensorObj X Y i₁ i₂ (i₁ + i₂) ⋯) (Z i₃) ≫
      ιTensorObj (tensorObj X Y) Z (i₁ + i₂) i₃ k ⋯) ≫
    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:
assoc,

Goal state after:
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, 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 (ιTensorObj X Y i₁ i₂ (i₁ + i₂) ⋯) (Z i₃) ≫
    ιTensorObj (tensorObj X Y) Z (i₁ + i₂) i₃ k ⋯ ≫
      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
Module: Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Goal state before:
pp: case hst
C : Type u₁
inst✝⁹ : Category.{u₂, u₁} C
F : C ⥤ FintypeCat
G : Type u_1
inst✝⁸ : Group G
inst✝⁷ : (X : C) → MulAction G (F.obj X).obj
inst✝⁶ : IsNaturalSMul F G
inst✝⁵ : GaloisCategory C
inst✝⁴ : FiberFunctor F
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : ∀ (X : C), ContinuousSMul G (F.obj X).obj
h : ∀ (X : C) [IsGalois X], MulAction.IsPretransitive G (F.obj X).obj
t : Aut F
gi : PointedGaloisObject F → G
hgi : ∀ (X : PointedGaloisObject F) (x : (F.obj X.obj).obj), gi X • x = (ConcreteCategory.hom (t.hom.app X.obj)) x
cl : PointedGaloisObject F → Set G := ⋯
c : Set G := ⋯
⊢ ∀ (u : Finset (PointedGaloisObject F)), (Set.univ ∩ ⋂ i ∈ u, cl i).Nonempty

Tactic:
· intro s
      rw [Set.univ_inter]
      obtain ⟨gs, hgs⟩ :=
        toAut_surjective_isGalois_finite_family F G t (fun X : s ↦ X.val.obj) h
      use gs
      simp only [Set.mem_iInter]
      intro X hXmem
      rw [mem_leftCoset_iff, SetLike.mem_coe, MulAction.mem_stabilizer_iff, mul_smul,
        hgs ⟨X, hXmem⟩, ← hgi X, inv_smul_smul]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, 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.tensorHom (β_ (X i₁) (Y i₂)).hom (𝟙 (Z i₃)) ≫
      MonoidalCategoryStruct.tensorHom (ιTensorObj Y X i₂ i₁ (i₁ + i₂) ⋯) (𝟙 (Z i₃))) ≫
    ιTensorObj (tensorObj Y X) Z (i₁ + i₂) i₃ 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:
assoc,

Goal state after:
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, 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.tensorHom (β_ (X i₁) (Y i₂)).hom (𝟙 (Z i₃)) ≫
    MonoidalCategoryStruct.tensorHom (ιTensorObj Y X i₂ i₁ (i₁ + i₂) ⋯) (𝟙 (Z i₃)) ≫
      ιTensorObj (tensorObj Y X) Z (i₁ + i₂) i₃ 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
Module: Mathlib.CategoryTheory.GradedObject.Braiding

Goal state before:
pp: I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, 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₂) (ιTensorObj X Z i₁ i₃ (i₁ + i₃) ⋯) ≫
          ιTensorObj Y (tensorObj X Z) i₂ (i₁ + i₃) k ⋯) ≫
        whiskerLeft Y (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) k

Tactic:
assoc,

Goal state after:
I : Type u_1
inst✝²⁰ : AddCommMonoid I
C : Type u_2
inst✝¹⁹ : Category.{v_1, 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₂) (ιTensorObj X Z i₁ i₃ (i₁ + i₃) ⋯) ≫
        ιTensorObj Y (tensorObj X Z) i₂ (i₁ + i₃) k ⋯ ≫
          whiskerLeft Y (fun k ↦ tensorObjDesc fun i j hij ↦ (β_ (X i) (Z j)).hom ≫ ιTensorObj Z X j i k ⋯) k