awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ : C
⊢ tensorμ X₁ X₂ Y₁ Y₂ ≫ tensorδ X₁ X₂ Y₁ Y₂ =
    𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂))

Tactic:
simp only [tensorμ, ← whiskerLeft_comp_assoc, tensorδ, assoc, Iso.inv_hom_id_assoc,
    Iso.hom_inv_id_assoc, hom_inv_whiskerRight_assoc, Iso.inv_hom_id, whiskerLeft_id, id_comp,
    Iso.hom_inv_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.MonoidalCategory.hom_inv_whiskerRight_assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.MonoidalCategory.tensorμ, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.MonoidalCategory.tensorδ, CategoryTheory.MonoidalCategory.whiskerLeft_id, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ : C
⊢ tensorδ X₁ X₂ Y₁ Y₂ ≫ tensorμ X₁ X₂ Y₁ Y₂ =
    𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂))

Tactic:
simp only [tensorδ, ← whiskerLeft_comp_assoc, tensorμ, assoc, Iso.inv_hom_id_assoc,
    Iso.hom_inv_id_assoc, inv_hom_whiskerRight_assoc, Iso.inv_hom_id, whiskerLeft_id, id_comp,
    Iso.hom_inv_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.MonoidalCategory.inv_hom_whiskerRight_assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.MonoidalCategory.tensorμ, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.MonoidalCategory.tensorδ, CategoryTheory.MonoidalCategory.whiskerLeft_id, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.Iso.hom_inv_id_assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
dsimp :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ V₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂))
    (((f₁ ⊗ₘ f₂) ⊗ₘ g₁ ⊗ₘ g₂) ≫
      Iso.hom (α_ Y₁ Y₂ (tensorObj.{v₁, u₁} (𝒞 := inst) V₁ V₂)) ≫
        Y₁ ◁ Iso.inv (α_ Y₂ V₁ V₂) ≫
          Y₁ ◁ Iso.hom (β_ Y₂ V₁) ▷ V₂ ≫
            Y₁ ◁ Iso.hom (α_ V₁ Y₂ V₂) ≫ Iso.inv (α_ Y₁ V₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂)))
    ((Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
        X₁ ◁ Iso.inv (α_ X₂ U₁ U₂) ≫
          X₁ ◁ Iso.hom (β_ X₂ U₁) ▷ U₂ ≫
            X₁ ◁ Iso.hom (α_ U₁ X₂ U₂) ≫ Iso.inv (α_ X₁ U₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ U₂))) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ V₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂))
    (((f₁ ⊗ₘ f₂) ⊗ₘ g₁ ⊗ₘ g₂) ≫ tensorμ Y₁ Y₂ V₁ V₂) (tensorμ X₁ X₂ U₁ U₂ ≫ ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂))

Tactic:
dsimp only [tensorμ]

Premises used: CategoryTheory.MonoidalCategory.tensorμ
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
simp_rw :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ V₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂))
    (((f₁ ⊗ₘ f₂) ⊗ₘ g₁ ⊗ₘ g₂) ≫
      Iso.hom (α_ Y₁ Y₂ (tensorObj.{v₁, u₁} (𝒞 := inst) V₁ V₂)) ≫
        (𝟙 Y₁ ⊗ₘ Iso.inv (α_ Y₂ V₁ V₂)) ≫
          (𝟙 Y₁ ⊗ₘ Iso.hom (β_ Y₂ V₁) ⊗ₘ 𝟙 V₂) ≫
            (𝟙 Y₁ ⊗ₘ Iso.hom (α_ V₁ Y₂ V₂)) ≫ Iso.inv (α_ Y₁ V₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂)))
    ((Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
        (𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫
          (𝟙 X₁ ⊗ₘ Iso.hom (β_ X₂ U₁) ⊗ₘ 𝟙 U₂) ≫
            (𝟙 X₁ ⊗ₘ Iso.hom (α_ U₁ X₂ U₂)) ≫ Iso.inv (α_ X₁ U₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ U₂))) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ V₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂))
    (((f₁ ⊗ₘ f₂) ⊗ₘ g₁ ⊗ₘ g₂) ≫
      Iso.hom (α_ Y₁ Y₂ (tensorObj.{v₁, u₁} (𝒞 := inst) V₁ V₂)) ≫
        Y₁ ◁ Iso.inv (α_ Y₂ V₁ V₂) ≫
          Y₁ ◁ Iso.hom (β_ Y₂ V₁) ▷ V₂ ≫
            Y₁ ◁ Iso.hom (α_ V₁ Y₂ V₂) ≫ Iso.inv (α_ Y₁ V₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂)))
    ((Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
        X₁ ◁ Iso.inv (α_ X₂ U₁ U₂) ≫
          X₁ ◁ Iso.hom (β_ X₂ U₁) ▷ U₂ ≫
            X₁ ◁ Iso.hom (α_ U₁ X₂ U₂) ≫ Iso.inv (α_ X₁ U₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ U₂))) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂))

Tactic:
simp_rw [← id_tensorHom, ← tensorHom_id]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.MonoidalCategory.tensorHom_id
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
a : Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ g₁ ⊗ₘ g₂)
| ((f₁ ⊗ₘ f₂) ⊗ₘ g₁ ⊗ₘ g₂) ≫ Iso.hom (α_ Y₁ Y₂ (tensorObj.{v₁, u₁} (𝒞 := inst) V₁ V₂))

Tactic:
rw [associator_naturality]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
slice_lhs :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ V₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂))
    (((((Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ g₁ ⊗ₘ g₂)) ≫
            (𝟙 Y₁ ⊗ₘ Iso.inv (α_ Y₂ V₁ V₂))) ≫
          (𝟙 Y₁ ⊗ₘ Iso.hom (β_ Y₂ V₁) ⊗ₘ 𝟙 V₂)) ≫
        (𝟙 Y₁ ⊗ₘ Iso.hom (α_ V₁ Y₂ V₂))) ≫
      Iso.inv (α_ Y₁ V₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂)))
    ((Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
        (𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫
          (𝟙 X₁ ⊗ₘ Iso.hom (β_ X₂ U₁) ⊗ₘ 𝟙 U₂) ≫
            (𝟙 X₁ ⊗ₘ Iso.hom (α_ U₁ X₂ U₂)) ≫ Iso.inv (α_ X₁ U₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ U₂))) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ V₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂))
    (((f₁ ⊗ₘ f₂) ⊗ₘ g₁ ⊗ₘ g₂) ≫
      Iso.hom (α_ Y₁ Y₂ (tensorObj.{v₁, u₁} (𝒞 := inst) V₁ V₂)) ≫
        (𝟙 Y₁ ⊗ₘ Iso.inv (α_ Y₂ V₁ V₂)) ≫
          (𝟙 Y₁ ⊗ₘ Iso.hom (β_ Y₂ V₁) ⊗ₘ 𝟙 V₂) ≫
            (𝟙 Y₁ ⊗ₘ Iso.hom (α_ V₁ Y₂ V₂)) ≫ Iso.inv (α_ Y₁ V₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂)))
    ((Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
        (𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫
          (𝟙 X₁ ⊗ₘ Iso.hom (β_ X₂ U₁) ⊗ₘ 𝟙 U₂) ≫
            (𝟙 X₁ ⊗ₘ Iso.hom (α_ U₁ X₂ U₂)) ≫ Iso.inv (α_ X₁ U₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ U₂))) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂))

Tactic:
slice_lhs 1 2 => rw [associator_naturality]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
a : (𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫ (f₁ ⊗ₘ (f₂ ⊗ₘ g₁) ⊗ₘ g₂)
| (f₁ ⊗ₘ f₂ ⊗ₘ g₁ ⊗ₘ g₂) ≫ (𝟙 Y₁ ⊗ₘ Iso.inv (α_ Y₂ V₁ V₂))

Tactic:
rw [tensorHom_comp_tensorHom, comp_id f₁, ← id_comp f₁, associator_inv_naturality,
      ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
slice_lhs :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ V₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂))
    (Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
      ((((𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫ (f₁ ⊗ₘ (f₂ ⊗ₘ g₁) ⊗ₘ g₂)) ≫ (𝟙 Y₁ ⊗ₘ Iso.hom (β_ Y₂ V₁) ⊗ₘ 𝟙 V₂)) ≫
          (𝟙 Y₁ ⊗ₘ Iso.hom (α_ V₁ Y₂ V₂))) ≫
        Iso.inv (α_ Y₁ V₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂)))
    ((Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
        (𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫
          (𝟙 X₁ ⊗ₘ Iso.hom (β_ X₂ U₁) ⊗ₘ 𝟙 U₂) ≫
            (𝟙 X₁ ⊗ₘ Iso.hom (α_ U₁ X₂ U₂)) ≫ Iso.inv (α_ X₁ U₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ U₂))) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ V₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂))
    (((((Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ g₁ ⊗ₘ g₂)) ≫
            (𝟙 Y₁ ⊗ₘ Iso.inv (α_ Y₂ V₁ V₂))) ≫
          (𝟙 Y₁ ⊗ₘ Iso.hom (β_ Y₂ V₁) ⊗ₘ 𝟙 V₂)) ≫
        (𝟙 Y₁ ⊗ₘ Iso.hom (α_ V₁ Y₂ V₂))) ≫
      Iso.inv (α_ Y₁ V₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂)))
    ((Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
        (𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫
          (𝟙 X₁ ⊗ₘ Iso.hom (β_ X₂ U₁) ⊗ₘ 𝟙 U₂) ≫
            (𝟙 X₁ ⊗ₘ Iso.hom (α_ U₁ X₂ U₂)) ≫ Iso.inv (α_ X₁ U₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ U₂))) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂))

Tactic:
slice_lhs 2 3 =>
    rw [tensorHom_comp_tensorHom, comp_id f₁, ← id_comp f₁, associator_inv_naturality,
      ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
a : (𝟙 X₁ ⊗ₘ Iso.hom (β_ X₂ U₁) ⊗ₘ 𝟙 U₂) ≫ (f₁ ⊗ₘ (g₁ ⊗ₘ f₂) ⊗ₘ g₂)
| (f₁ ⊗ₘ (f₂ ⊗ₘ g₁) ⊗ₘ g₂) ≫ (𝟙 Y₁ ⊗ₘ Iso.hom (β_ Y₂ V₁) ⊗ₘ 𝟙 V₂)

Tactic:
rw [tensorHom_comp_tensorHom, tensorHom_comp_tensorHom, comp_id f₁, ← id_comp f₁, comp_id g₂,
      ← id_comp g₂, braiding_naturality, ← tensorHom_comp_tensorHom, ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.BraidedCategory.braiding_naturality, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
slice_lhs :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ V₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂))
    (Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
      (𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫
        (((𝟙 X₁ ⊗ₘ Iso.hom (β_ X₂ U₁) ⊗ₘ 𝟙 U₂) ≫ (f₁ ⊗ₘ (g₁ ⊗ₘ f₂) ⊗ₘ g₂)) ≫ (𝟙 Y₁ ⊗ₘ Iso.hom (α_ V₁ Y₂ V₂))) ≫
          Iso.inv (α_ Y₁ V₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂)))
    ((Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
        (𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫
          (𝟙 X₁ ⊗ₘ Iso.hom (β_ X₂ U₁) ⊗ₘ 𝟙 U₂) ≫
            (𝟙 X₁ ⊗ₘ Iso.hom (α_ U₁ X₂ U₂)) ≫ Iso.inv (α_ X₁ U₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ U₂))) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ V₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂))
    (Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
      ((((𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫ (f₁ ⊗ₘ (f₂ ⊗ₘ g₁) ⊗ₘ g₂)) ≫ (𝟙 Y₁ ⊗ₘ Iso.hom (β_ Y₂ V₁) ⊗ₘ 𝟙 V₂)) ≫
          (𝟙 Y₁ ⊗ₘ Iso.hom (α_ V₁ Y₂ V₂))) ≫
        Iso.inv (α_ Y₁ V₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂)))
    ((Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
        (𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫
          (𝟙 X₁ ⊗ₘ Iso.hom (β_ X₂ U₁) ⊗ₘ 𝟙 U₂) ≫
            (𝟙 X₁ ⊗ₘ Iso.hom (α_ U₁ X₂ U₂)) ≫ Iso.inv (α_ X₁ U₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ U₂))) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂))

Tactic:
slice_lhs 3 4 =>
    rw [tensorHom_comp_tensorHom, tensorHom_comp_tensorHom, comp_id f₁, ← id_comp f₁, comp_id g₂,
      ← id_comp g₂, braiding_naturality, ← tensorHom_comp_tensorHom, ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.BraidedCategory.braiding_naturality, CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
a : (𝟙 X₁ ⊗ₘ Iso.hom (α_ U₁ X₂ U₂)) ≫ (f₁ ⊗ₘ g₁ ⊗ₘ f₂ ⊗ₘ g₂)
| (f₁ ⊗ₘ (g₁ ⊗ₘ f₂) ⊗ₘ g₂) ≫ (𝟙 Y₁ ⊗ₘ Iso.hom (α_ V₁ Y₂ V₂))

Tactic:
rw [tensorHom_comp_tensorHom, comp_id f₁, ← id_comp f₁, associator_naturality,
      ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategory.associator_naturality, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
slice_lhs :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ V₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂))
    (Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
      (𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫
        (𝟙 X₁ ⊗ₘ Iso.hom (β_ X₂ U₁) ⊗ₘ 𝟙 U₂) ≫
          ((𝟙 X₁ ⊗ₘ Iso.hom (α_ U₁ X₂ U₂)) ≫ (f₁ ⊗ₘ g₁ ⊗ₘ f₂ ⊗ₘ g₂)) ≫
            Iso.inv (α_ Y₁ V₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂)))
    ((Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
        (𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫
          (𝟙 X₁ ⊗ₘ Iso.hom (β_ X₂ U₁) ⊗ₘ 𝟙 U₂) ≫
            (𝟙 X₁ ⊗ₘ Iso.hom (α_ U₁ X₂ U₂)) ≫ Iso.inv (α_ X₁ U₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ U₂))) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ V₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂))
    (Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
      (𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫
        (((𝟙 X₁ ⊗ₘ Iso.hom (β_ X₂ U₁) ⊗ₘ 𝟙 U₂) ≫ (f₁ ⊗ₘ (g₁ ⊗ₘ f₂) ⊗ₘ g₂)) ≫ (𝟙 Y₁ ⊗ₘ Iso.hom (α_ V₁ Y₂ V₂))) ≫
          Iso.inv (α_ Y₁ V₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂)))
    ((Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
        (𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫
          (𝟙 X₁ ⊗ₘ Iso.hom (β_ X₂ U₁) ⊗ₘ 𝟙 U₂) ≫
            (𝟙 X₁ ⊗ₘ Iso.hom (α_ U₁ X₂ U₂)) ≫ Iso.inv (α_ X₁ U₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ U₂))) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂))

Tactic:
slice_lhs 4 5 =>
    rw [tensorHom_comp_tensorHom, comp_id f₁, ← id_comp f₁, associator_naturality,
      ← tensorHom_comp_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_comp_tensorHom, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategory.associator_naturality, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
a : Iso.inv (α_ X₁ U₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ U₂)) ≫ ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂)
| (f₁ ⊗ₘ g₁ ⊗ₘ f₂ ⊗ₘ g₂) ≫ Iso.inv (α_ Y₁ V₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂))

Tactic:
rw [associator_inv_naturality]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
slice_lhs :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ V₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂))
    (Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
      (𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫
        (𝟙 X₁ ⊗ₘ Iso.hom (β_ X₂ U₁) ⊗ₘ 𝟙 U₂) ≫
          (𝟙 X₁ ⊗ₘ Iso.hom (α_ U₁ X₂ U₂)) ≫
            Iso.inv (α_ X₁ U₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ U₂)) ≫ ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂))
    ((Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
        (𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫
          (𝟙 X₁ ⊗ₘ Iso.hom (β_ X₂ U₁) ⊗ₘ 𝟙 U₂) ≫
            (𝟙 X₁ ⊗ₘ Iso.hom (α_ U₁ X₂ U₂)) ≫ Iso.inv (α_ X₁ U₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ U₂))) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ V₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂))
    (Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
      (𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫
        (𝟙 X₁ ⊗ₘ Iso.hom (β_ X₂ U₁) ⊗ₘ 𝟙 U₂) ≫
          ((𝟙 X₁ ⊗ₘ Iso.hom (α_ U₁ X₂ U₂)) ≫ (f₁ ⊗ₘ g₁ ⊗ₘ f₂ ⊗ₘ g₂)) ≫
            Iso.inv (α_ Y₁ V₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂)))
    ((Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
        (𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫
          (𝟙 X₁ ⊗ₘ Iso.hom (β_ X₂ U₁) ⊗ₘ 𝟙 U₂) ≫
            (𝟙 X₁ ⊗ₘ Iso.hom (α_ U₁ X₂ U₂)) ≫ Iso.inv (α_ X₁ U₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ U₂))) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂))

Tactic:
slice_lhs 5 6 => rw [associator_inv_naturality]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : U₁ ⟶ V₁
g₂ : U₂ ⟶ V₂
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ V₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂))
    (Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
      (𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫
        (𝟙 X₁ ⊗ₘ Iso.hom (β_ X₂ U₁) ⊗ₘ 𝟙 U₂) ≫
          (𝟙 X₁ ⊗ₘ Iso.hom (α_ U₁ X₂ U₂)) ≫
            Iso.inv (α_ X₁ U₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ U₂)) ≫ ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂))
    ((Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫
        (𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫
          (𝟙 X₁ ⊗ₘ Iso.hom (β_ X₂ U₁) ⊗ₘ 𝟙 U₂) ≫
            (𝟙 X₁ ⊗ₘ Iso.hom (α_ U₁ X₂ U₂)) ≫ Iso.inv (α_ X₁ U₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ U₂))) ≫
      ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂))

Tactic:
simp only [assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
Z₁ Z₂ : C
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂))
    (((f₁ ⊗ₘ f₂) ⊗ₘ 𝟙 Z₁ ⊗ₘ 𝟙 Z₂) ≫ tensorμ Y₁ Y₂ Z₁ Z₂) (tensorμ X₁ X₂ Z₁ Z₂ ≫ ((f₁ ⊗ₘ 𝟙 Z₁) ⊗ₘ f₂ ⊗ₘ 𝟙 Z₂))

Tactic:
tensorμ_natural f₁ f₂ (𝟙 Z₁) (𝟙 Z₂)

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.MonoidalCategory.tensorμ_natural
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
Z₁ Z₂ : C
h :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂))
    ((f₁ ⊗ₘ f₂) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂ ≫ tensorμ Y₁ Y₂ Z₁ Z₂)
    (((f₁ ⊗ₘ f₂) ⊗ₘ 𝟙 Z₁ ⊗ₘ 𝟙 Z₂) ≫ tensorμ Y₁ Y₂ Z₁ Z₂)
h₁ :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂))
    (tensorμ X₁ X₂ Z₁ Z₂ ≫ (f₁ ▷ Z₁ ⊗ₘ f₂ ▷ Z₂)) (tensorμ X₁ X₂ Z₁ Z₂ ≫ ((f₁ ⊗ₘ 𝟙 Z₁) ⊗ₘ f₂ ⊗ₘ 𝟙 Z₂))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂))
    ((f₁ ⊗ₘ f₂) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂ ≫ tensorμ Y₁ Y₂ Z₁ Z₂)
    (tensorμ X₁ X₂ Z₁ Z₂ ≫ (f₁ ▷ Z₁ ⊗ₘ f₂ ▷ Z₂))

Tactic:
convert! tensorμ_natural f₁ f₂ (𝟙 Z₁) (𝟙 Z₂) using 1

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.MonoidalCategory.tensorμ_natural
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
Z₁ Z₂ : C
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂))
    ((f₁ ⊗ₘ f₂) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂ ≫ tensorμ Y₁ Y₂ Z₁ Z₂)
    (((f₁ ⊗ₘ f₂) ⊗ₘ 𝟙 Z₁ ⊗ₘ 𝟙 Z₂) ≫ tensorμ Y₁ Y₂ Z₁ Z₂)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
Z₁ Z₂ : C
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) Z₁ Z₂) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Z₁) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Z₂))
    (tensorμ X₁ X₂ Z₁ Z₂ ≫ (f₁ ▷ Z₁ ⊗ₘ f₂ ▷ Z₂)) (tensorμ X₁ X₂ Z₁ Z₂ ≫ ((f₁ ⊗ₘ 𝟙 Z₁) ⊗ₘ f₂ ⊗ₘ 𝟙 Z₂))

Tactic:
simp