awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_9 : F.LaxBraided
inst_10 : G.LaxBraided
X Y : C
⊢ Eq (α :=
    tensorObj.{v₃, u₃} (𝒞 := inst_6) (G.obj (F.obj X)) (G.obj (F.obj Y)) ⟶
      G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)))
    (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Y))) (μ G (F.obj X) (F.obj Y))
      (G.map (Iso.hom (β_ (F.obj X) (F.obj Y))) ≫ G.map (μ F Y X)))
    (Iso.hom (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj X))) (μ G (F.obj Y) (F.obj X))
        (G.map (μ F Y X)))
have slice_lhs : Eq (α :=
  tensorObj.{v₃, u₃} (𝒞 := inst_6) (G.obj (F.obj X)) (G.obj (F.obj Y)) ⟶
    G.obj (F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X)))
  (CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj X)))
    (Iso.hom (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))) ≫ μ G (F.obj Y) (F.obj X)) (G.map (μ F Y X)))
  (Iso.hom (β_ (G.obj (F.obj X)) (G.obj (F.obj Y))) ≫
    CategoryStruct.comp (Y := G.obj (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj X))) (μ G (F.obj Y) (F.obj X))
      (G.map (μ F Y X)))
Tactic: slice_lhs 1 2 => rw [braided]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F G : Functor.{v₁, v₂, u₁, u₂} C D
i : F ≅ G
inst_9 : F.LaxBraided
inst_10 : G.LaxMonoidal
inst_11 : NatTrans.IsMonoidal i.hom
X Y : C
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (G.obj X) (G.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
    (μ G X Y ≫ G.map (Iso.hom (β_ X Y))) (Iso.hom (β_ (G.obj X) (G.obj Y)) ≫ μ G Y X)
have this : ∀ (X Y : C),
  Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (G.obj X) (G.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (μ G X Y)
    ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
Tactic: have (X Y : C) : μ G X Y = (i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app _ := by
      simp [NatTrans.IsMonoidal.tensor X Y, tensorHom_comp_tensorHom_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
F G : Functor.{v₁, v₂, u₁, u₂} C D
i : F ≅ G
inst_9 : F.LaxBraided
inst_10 : G.LaxMonoidal
inst_11 : NatTrans.IsMonoidal i.hom
X Y : C
this :
  ∀ (X Y : C),
    Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (G.obj X) (G.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
      (μ G X Y) ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
⊢ Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (G.obj X) (G.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
    (μ G X Y ≫ G.map (Iso.hom (β_ X Y))) (Iso.hom (β_ (G.obj X) (G.obj Y)) ≫ μ G Y X)
have rw : Eq (α := tensorObj.{v₂, u₂} (𝒞 := inst_3) (G.obj X) (G.obj Y) ⟶ G.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
  (((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) ≫ G.map (Iso.hom (β_ X Y)))
  ((i.inv.app X ⊗ₘ i.inv.app Y) ≫ μ F X Y ≫ F.map (Iso.hom (β_ X Y)) ≫ i.hom.app (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
Tactic: rw [this X Y, this Y X, ← braiding_naturality_assoc, ← Functor.LaxBraided.braided_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_6 : F.Braided
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
    (F.map (Iso.hom (β_ X Y)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Y)) (δ F X Y)
      (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X))
have rw : Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
  (F.map (Iso.hom (β_ X Y)))
  (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Y)) (δ F X Y)
    (μ F X Y ≫ F.map (Iso.hom (β_ X Y))))
Tactic: rw [← Functor.Braided.braided, δ_μ_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : C
inst_6 : F.Braided
rw :
  Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
    (F.map (Iso.hom (β_ X Y)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Y)) (δ F X Y)
      (μ F X Y ≫ F.map (Iso.hom (β_ X Y))))
⊢ Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
    (F.map (Iso.hom (β_ X Y)))
    (CategoryStruct.comp (Y := tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Y)) (δ F X Y)
      (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X))
have rw₁ : Eq (α := F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
  (F.map (Iso.hom (β_ X Y))) (F.map (Iso.hom (β_ X Y)))
Tactic: rw [← Functor.Braided.braided, δ_μ_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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₂))
    (((f₁ ⊗ₘ f₂) ⊗ₘ g₁ ⊗ₘ g₂) ≫ tensorμ Y₁ Y₂ V₁ V₂) (tensorμ X₁ X₂ U₁ U₂ ≫ ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂))
have 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₂))
Tactic: dsimp only [tensorμ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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₂))
    (((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₂))
have 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₂))
Tactic: simp_rw [← id_tensorHom, ← tensorHom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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₂
| ((f₁ ⊗ₘ f₂) ⊗ₘ g₁ ⊗ₘ g₂) ≫ Iso.hom (α_ Y₁ Y₂ (tensorObj.{v₁, u₁} (𝒞 := inst) V₁ V₂))
have a : Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) U₁ U₂)) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ g₁ ⊗ₘ g₂)
Tactic: rw [associator_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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₂))
    (((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₂))
have 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₂))
Tactic: slice_lhs 1 2 => rw [associator_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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₂
| (f₁ ⊗ₘ f₂ ⊗ₘ g₁ ⊗ₘ g₂) ≫ (𝟙 Y₁ ⊗ₘ Iso.inv (α_ Y₂ V₁ V₂))
have a : (𝟙 X₁ ⊗ₘ Iso.inv (α_ X₂ U₁ U₂)) ≫ (f₁ ⊗ₘ (f₂ ⊗ₘ g₁) ⊗ₘ g₂)
Tactic: rw [tensorHom_comp_tensorHom, comp_id f₁, ← id_comp f₁, associator_inv_naturality,
      ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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₂)) ≫ (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₂))
have 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₂))
Tactic: slice_lhs 2 3 =>
    rw [tensorHom_comp_tensorHom, comp_id f₁, ← id_comp f₁, associator_inv_naturality,
      ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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₂
| (f₁ ⊗ₘ (f₂ ⊗ₘ g₁) ⊗ₘ g₂) ≫ (𝟙 Y₁ ⊗ₘ Iso.hom (β_ Y₂ V₁) ⊗ₘ 𝟙 V₂)
have a : (𝟙 X₁ ⊗ₘ Iso.hom (β_ X₂ U₁) ⊗ₘ 𝟙 U₂) ≫ (f₁ ⊗ₘ (g₁ ⊗ₘ f₂) ⊗ₘ g₂)
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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₂)) ≫ (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₂))
have 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₂))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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₂
| (f₁ ⊗ₘ (g₁ ⊗ₘ f₂) ⊗ₘ g₂) ≫ (𝟙 Y₁ ⊗ₘ Iso.hom (α_ V₁ Y₂ V₂))
have a : (𝟙 X₁ ⊗ₘ Iso.hom (α_ U₁ X₂ U₂)) ≫ (f₁ ⊗ₘ g₁ ⊗ₘ f₂ ⊗ₘ g₂)
Tactic: rw [tensorHom_comp_tensorHom, comp_id f₁, ← id_comp f₁, associator_naturality,
      ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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₂) ≫ (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₂))
have 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₂))
Tactic: slice_lhs 4 5 =>
    rw [tensorHom_comp_tensorHom, comp_id f₁, ← id_comp f₁, associator_naturality,
      ← tensorHom_comp_tensorHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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₂
| (f₁ ⊗ₘ g₁ ⊗ₘ f₂ ⊗ₘ g₂) ≫ Iso.inv (α_ Y₁ V₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ V₂))
have a : Iso.inv (α_ X₁ U₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ U₂)) ≫ ((f₁ ⊗ₘ g₁) ⊗ₘ f₂ ⊗ₘ g₂)
Tactic: rw [associator_inv_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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₂)) ≫ (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₂))
have 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₂))
Tactic: slice_lhs 5 6 => rw [associator_inv_naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
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₂)
    (tensorμ X₁ X₂ Z₁ Z₂ ≫ (f₁ ▷ Z₁ ⊗ₘ f₂ ▷ Z₂))
have 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₂)
Tactic: convert! tensorμ_natural f₁ f₂ (𝟙 Z₁) (𝟙 Z₂) using 1