awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X X' Y Y' Z Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X' Y') Z')
    ((f ⊗ₘ g) ⊗ₘ h) (hom (α_ X Y Z) ≫ Iso.inv (α_ X Y Z) ≫ ((f ⊗ₘ g) ⊗ₘ h))
rw₁ rw₂ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X' Y') Z')
    ((f ⊗ₘ g) ⊗ₘ h) ((f ⊗ₘ g) ⊗ₘ h)
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X' Y') Z')
    ((f ⊗ₘ g) ⊗ₘ h) (hom (α_ X Y Z) ≫ (f ⊗ₘ g ⊗ₘ h) ≫ Iso.inv (α_ X' Y' Z'))

Tactic:
rw [associator_inv_naturality, hom_inv_id_assoc]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality, CategoryTheory.Iso.hom_inv_id_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X X' Y Y' Z Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) X' (tensorObj.{v, u} (𝒞 := inst) Y' Z'))
    (f ⊗ₘ g ⊗ₘ h) (Iso.inv (α_ X Y Z) ≫ hom (α_ X Y Z) ≫ (f ⊗ₘ g ⊗ₘ h))
rw₁ rw₂ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) X' (tensorObj.{v, u} (𝒞 := inst) Y' Z'))
    (f ⊗ₘ g ⊗ₘ h) (f ⊗ₘ g ⊗ₘ h)
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) X' (tensorObj.{v, u} (𝒞 := inst) Y' Z'))
    (f ⊗ₘ g ⊗ₘ h) (Iso.inv (α_ X Y Z) ≫ ((f ⊗ₘ g) ⊗ₘ h) ≫ hom (α_ X' Y' Z'))

Tactic:
rw [associator_naturality, inv_hom_id_assoc]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.MonoidalCategory.associator_naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z Z' : C
h : Z ⟶ Z'
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
      tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z'))
    (((𝟙 X ⊗ₘ 𝟙 Y) ⊗ₘ h) ≫ hom (α_ X Y Z')) (hom (α_ X Y Z) ≫ (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ h))
rw₁ rw₂ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
      tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z'))
    (hom (α_ X Y Z) ≫ (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ h)) (hom (α_ X Y Z) ≫ (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ h))
⊢ (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y) ⊗ₘ h) ≫ hom (α_ X Y Z') = hom (α_ X Y Z) ≫ (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ h)

Tactic:
rw [← id_tensorHom_id, associator_naturality]

Premises used: CategoryTheory.MonoidalCategory.associator_naturality, CategoryTheory.MonoidalCategory.id_tensorHom_id
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z X' : C
f : X ⟶ X'
rw :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X' Y) Z)
    ((f ⊗ₘ 𝟙 Y ⊗ₘ 𝟙 Z) ≫ Iso.inv (α_ X' Y Z)) (Iso.inv (α_ X Y Z) ≫ ((f ⊗ₘ 𝟙 Y) ⊗ₘ 𝟙 Z))
rw₁ rw₂ :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X' Y) Z)
    (Iso.inv (α_ X Y Z) ≫ ((f ⊗ₘ 𝟙 Y) ⊗ₘ 𝟙 Z)) (Iso.inv (α_ X Y Z) ≫ ((f ⊗ₘ 𝟙 Y) ⊗ₘ 𝟙 Z))
⊢ (f ⊗ₘ 𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.inv (α_ X' Y Z) = Iso.inv (α_ X Y Z) ≫ ((f ⊗ₘ 𝟙 Y) ⊗ₘ 𝟙 Z)

Tactic:
rw [← id_tensorHom_id, associator_inv_naturality]

Premises used: CategoryTheory.MonoidalCategory.associator_inv_naturality, CategoryTheory.MonoidalCategory.id_tensorHom_id
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) V X ⟶ tensorObj.{v, u} (𝒞 := inst) V Z) ((f.hom ⊗ₘ g) ≫ (f.inv ⊗ₘ h))
    ((𝟙 V ⊗ₘ g) ≫ (𝟙 V ⊗ₘ h))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) W X ⟶ tensorObj.{v, u} (𝒞 := inst) W Z) ((f.inv ⊗ₘ g) ≫ (f.hom ⊗ₘ h))
    ((𝟙 W ⊗ₘ g) ≫ (𝟙 W ⊗ₘ h))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X V ⟶ tensorObj.{v, u} (𝒞 := inst) Z V) ((g ⊗ₘ f.hom) ≫ (h ⊗ₘ f.inv))
    ((g ⊗ₘ 𝟙 V) ≫ (h ⊗ₘ 𝟙 V))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
V W X Y Z : C
f : V ≅ W
g : X ⟶ Y
h : Y ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X W ⟶ tensorObj.{v, u} (𝒞 := inst) Z W) ((g ⊗ₘ f.inv) ≫ (h ⊗ₘ f.hom))
    ((g ⊗ₘ 𝟙 W) ≫ (h ⊗ₘ 𝟙 W))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
V W X Y Z : C
f : V ⟶ W
inst_2 : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) V X ⟶ tensorObj.{v, u} (𝒞 := inst) V Z) ((f ⊗ₘ g) ≫ (inv f ⊗ₘ h))
    ((𝟙 V ⊗ₘ g) ≫ (𝟙 V ⊗ₘ h))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
V W X Y Z : C
f : V ⟶ W
inst_2 : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) W X ⟶ tensorObj.{v, u} (𝒞 := inst) W Z) ((inv f ⊗ₘ g) ≫ (f ⊗ₘ h))
    ((𝟙 W ⊗ₘ g) ≫ (𝟙 W ⊗ₘ h))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
V W X Y Z : C
f : V ⟶ W
inst_2 : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X V ⟶ tensorObj.{v, u} (𝒞 := inst) Z V) ((g ⊗ₘ f) ≫ (h ⊗ₘ inv f))
    ((g ⊗ₘ 𝟙 V) ≫ (h ⊗ₘ 𝟙 V))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
V W X Y Z : C
f : V ⟶ W
inst_2 : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X W ⟶ tensorObj.{v, u} (𝒞 := inst) Z W) ((g ⊗ₘ inv f) ≫ (h ⊗ₘ f))
    ((g ⊗ₘ 𝟙 W) ≫ (h ⊗ₘ 𝟙 W))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X Y Z : C
f : W ⟶ X
g : X ⟶ Y
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) W Z ⟶ tensorObj.{v, u} (𝒞 := inst) Y Z) (f ≫ g ⊗ₘ 𝟙 Z) ((f ⊗ₘ 𝟙 Z) ≫ (g ⊗ₘ 𝟙 Z))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X Y Z : C
f : W ⟶ X
g : X ⟶ Y
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Z W ⟶ tensorObj.{v, u} (𝒞 := inst) Z Y) (𝟙 Z ⊗ₘ f ≫ g) ((𝟙 Z ⊗ₘ f) ≫ (𝟙 Z ⊗ₘ g))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Y W ⟶ tensorObj.{v, u} (𝒞 := inst) Z X) ((𝟙 Y ⊗ₘ f) ≫ (g ⊗ₘ 𝟙 X)) (g ⊗ₘ f)

Tactic:
simp [tensorHom_def']

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def'
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X Y Z : C
f : W ⟶ X
g : Y ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Y W ⟶ tensorObj.{v, u} (𝒞 := inst) Z X) ((g ⊗ₘ 𝟙 W) ≫ (𝟙 Z ⊗ₘ f)) (g ⊗ₘ f)

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
f g : X ⟶ Y
⊢ Eq (α :=
      tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) X ⟶
        tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) Y)
      (𝟙 (tensorUnit.{v, u} C (𝒞 := inst)) ⊗ₘ f) (𝟙 (tensorUnit.{v, u} C (𝒞 := inst)) ⊗ₘ g) ↔
    f = g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
f g : X ⟶ Y
⊢ Eq (α :=
      tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst)) ⟶
        tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst)))
      (f ⊗ₘ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst))) (g ⊗ₘ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst))) ↔
    f = g

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X : C × C × C
⊢ Functor.obj.{v, v, u, u} (leftAssocTensor C) X =
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X.1 X.2.1) X.2.2

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C × C × C
f : X ⟶ Y
⊢ Eq (α := Functor.obj.{v, v, u, u} (leftAssocTensor C) X ⟶ Functor.obj.{v, v, u, u} (leftAssocTensor C) Y)
    (Functor.map (leftAssocTensor C) f) ((f.1 ⊗ₘ f.2.1) ⊗ₘ f.2.2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X : C × C × C
⊢ Functor.obj.{v, v, u, u} (rightAssocTensor C) X =
    tensorObj.{v, u} (𝒞 := inst) X.1 (tensorObj.{v, u} (𝒞 := inst) X.2.1 X.2.2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C × C × C
f : X ⟶ Y
⊢ Eq (α := Functor.obj.{v, v, u, u} (rightAssocTensor C) X ⟶ Functor.obj.{v, v, u, u} (rightAssocTensor C) Y)
    (Functor.map (rightAssocTensor C) f) (f.1 ⊗ₘ f.2.1 ⊗ₘ f.2.2)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X_1 Y_1 Z_1 X Y Z Z' : C
f : Z ⟶ Z'
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (tensorLeft (tensorObj.{v, u} (𝒞 := inst) X Y)) Z ⟶
      Functor.obj.{v, v, u, u} (tensorLeft Y ⋙ tensorLeft X) Z')
    (Functor.map (tensorLeft (tensorObj.{v, u} (𝒞 := inst) X Y)) f ≫ hom (α_ X Y Z'))
    (hom (α_ X Y Z) ≫ Functor.map (tensorLeft Y ⋙ tensorLeft X) f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (tensorLeft (tensorObj.{v, u} (𝒞 := inst) X Y)) Z ⟶
      Functor.obj.{v, v, u, u} (tensorLeft Y ⋙ tensorLeft X) Z)
    (NatTrans.app (hom (tensorLeftTensor X Y)) Z) (hom (α_ X Y Z))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (tensorLeft Y ⋙ tensorLeft X) Z ⟶
      Functor.obj.{v, v, u, u} (tensorLeft (tensorObj.{v, u} (𝒞 := inst) X Y)) Z)
    (NatTrans.app (Iso.inv (tensorLeftTensor X Y)) Z) (Iso.inv (α_ X Y Z))

Tactic:
simp [tensorLeftTensor]

Premises used: CategoryTheory.MonoidalCategory.tensorLeftTensor
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X_1 Y_1 Z X Y : C
f g : X ⟶ Y
h :
  Eq (α :=
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (Functor.obj (tensoringLeft C) X) (Functor.obj (tensoringLeft C) Y))
    (Functor.map (tensoringLeft C) f) (Functor.map (tensoringLeft C) g)
⊢ Eq (α := (Y_2 : C) → tensorObj.{v, u} (𝒞 := inst) X Y_2 ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y_2)
    (fun (Y_2 : C) ↦ f ▷ Y_2) fun (Y_2 : C) ↦ g ▷ Y_2

Tactic:
injections h
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X_1 Y_1 Z X Y : C
f g : X ⟶ Y
h :
  Eq (α := (Y_2 : C) → tensorObj.{v, u} (𝒞 := inst) X Y_2 ⟶ tensorObj.{v, u} (𝒞 := inst) Y Y_2)
    (fun (Y_2 : C) ↦ f ▷ Y_2) fun (Y_2 : C) ↦ g ▷ Y_2
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst)) ⟶
      tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst)))
    (f ▷ tensorUnit.{v, u} C (𝒞 := inst)) (g ▷ tensorUnit.{v, u} C (𝒞 := inst))

Tactic:
replace h := congr_fun h (𝟙_ C)
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X_1 Y_1 Z X Y : C
f g : X ⟶ Y
h :
  Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst)) ⟶
      tensorObj.{v, u} (𝒞 := inst) Y (tensorUnit.{v, u} C (𝒞 := inst)))
    (f ▷ tensorUnit.{v, u} C (𝒞 := inst)) (g ▷ tensorUnit.{v, u} C (𝒞 := inst))
⊢ f = g

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X_1 Y_1 Z X Y : C
f g : X ⟶ Y
h :
  Eq (α :=
    Quiver.Hom (V := Functor.{v, v, u, u} C C) (Functor.obj (tensoringRight C) X) (Functor.obj (tensoringRight C) Y))
    (Functor.map (tensoringRight C) f) (Functor.map (tensoringRight C) g)
⊢ Eq (α :=
    (j : C) →
      Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) j) X ⟶
        Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) j) Y)
    (fun (j : C) ↦ Functor.map (Functor.obj (curriedTensor C) j) f) fun (j : C) ↦
    Functor.map (Functor.obj (curriedTensor C) j) g

Tactic:
injections h
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X_1 Y_1 Z X Y : C
f g : X ⟶ Y
h :
  Eq (α :=
    (j : C) →
      Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) j) X ⟶
        Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) j) Y)
    (fun (j : C) ↦ Functor.map (Functor.obj (curriedTensor C) j) f) fun (j : C) ↦
    Functor.map (Functor.obj (curriedTensor C) j) g
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) (tensorUnit.{v, u} C (𝒞 := inst))) X ⟶
      Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) (tensorUnit.{v, u} C (𝒞 := inst))) Y)
    (Functor.map (Functor.obj (curriedTensor C) (tensorUnit.{v, u} C (𝒞 := inst))) f)
    (Functor.map (Functor.obj (curriedTensor C) (tensorUnit.{v, u} C (𝒞 := inst))) g)

Tactic:
replace h := congr_fun h (𝟙_ C)
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X_1 Y_1 Z X Y : C
f g : X ⟶ Y
h :
  Eq (α :=
    Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) (tensorUnit.{v, u} C (𝒞 := inst))) X ⟶
      Functor.obj.{v, v, u, u} (Functor.obj (curriedTensor C) (tensorUnit.{v, u} C (𝒞 := inst))) Y)
    (Functor.map (Functor.obj (curriedTensor C) (tensorUnit.{v, u} C (𝒞 := inst))) f)
    (Functor.map (Functor.obj (curriedTensor C) (tensorUnit.{v, u} C (𝒞 := inst))) g)
⊢ f = g

Tactic:
simpa using h
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X_1 Y_1 Z_1 X Y Z Z' : C
f : Z ⟶ Z'
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (tensorRight (tensorObj.{v, u} (𝒞 := inst) X Y)) Z ⟶
      Functor.obj.{v, v, u, u} (tensorRight X ⋙ tensorRight Y) Z')
    (Functor.map (tensorRight (tensorObj.{v, u} (𝒞 := inst) X Y)) f ≫
      hom
        ((fun (Z : C) ↦
            (Iso.symm (α_ Z X Y) :
              tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) X Y) ≅
                tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z X) Y))
          Z'))
    (hom
        ((fun (Z : C) ↦
            (Iso.symm (α_ Z X Y) :
              tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) X Y) ≅
                tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z X) Y))
          Z) ≫
      Functor.map (tensorRight X ⋙ tensorRight Y) f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (tensorRight (tensorObj.{v, u} (𝒞 := inst) X Y)) Z ⟶
      Functor.obj.{v, v, u, u} (tensorRight X ⋙ tensorRight Y) Z)
    (NatTrans.app (hom (tensorRightTensor X Y)) Z) (Iso.inv (α_ Z X Y))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    Functor.obj.{v, v, u, u} (tensorRight X ⋙ tensorRight Y) Z ⟶
      Functor.obj.{v, v, u, u} (tensorRight (tensorObj.{v, u} (𝒞 := inst) X Y)) Z)
    (NatTrans.app (Iso.inv (tensorRightTensor X Y)) Z) (hom (α_ Z X Y))

Tactic:
simp [tensorRightTensor]

Premises used: CategoryTheory.MonoidalCategory.tensorRightTensor
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X Y Z : C
C₁ : Type u₁
inst_2 : Category.{v₁, u₁} C₁
inst_3 : MonoidalCategory.{v₁, u₁} C₁
C₂ : Type u₂
inst_4 : Category.{v₂, u₂} C₂
inst_5 : MonoidalCategory.{v₂, u₂} C₂
⊢ ∀ {X₁ Y₁ X₂ Y₂ : C₁ × C₂} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
    Eq (α :=
      (tensorObj.{v₁, u₁} (𝒞 := inst_2) X₁.1 X₂.1, tensorObj.{v₂, u₂} (𝒞 := inst_4) X₁.2 X₂.2) ⟶
        (tensorObj.{v₁, u₁} (𝒞 := inst_2) Y₁.1 Y₂.1, tensorObj.{v₂, u₂} (𝒞 := inst_4) Y₁.2 Y₂.2))
      ((f.1 ⊗ₘ g.1) ×ₘ f.2 ⊗ₘ g.2) ((f.1 ▷ X₂.1 ×ₘ f.2 ▷ X₂.2) ≫ (Y₁.1 ◁ g.1 ×ₘ Y₁.2 ◁ g.2))

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
J : Type u_1
inst : Category.{v_1, u_1} J
C : Type u_2
inst_1 : Category.{v_2, u_2} C
inst_2 : MonoidalCategory.{v_2, u_2} C
F G F' G' : Functor.{v_1, v_2, u_1, u_2} J C
α : F ⟶ F'
β : G ⟶ G'
X Y X' Y' : J
f : X ⟶ Y
g : X' ⟶ Y'
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (G.obj X') ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) (F'.obj Y) (G'.obj Y'))
    ((F.map f ⊗ₘ G.map g) ≫ (α.app Y ⊗ₘ β.app Y')) ((α.app X ⊗ₘ β.app X') ≫ (F'.map f ⊗ₘ G'.map g))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
J : Type u_1
inst : Category.{v_1, u_1} J
C : Type u_2
inst_1 : Category.{v_2, u_2} C
inst_2 : MonoidalCategory.{v_2, u_2} C
F G F' G' : Functor.{v_1, v_2, u_1, u_2} J C
α : F ⟶ F'
β : G ⟶ G'
X Y : J
f : X ⟶ Y
X' : J
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (G.obj X') ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) (F'.obj Y) (G'.obj X'))
    (F.map f ▷ G.obj X' ≫ (α.app Y ⊗ₘ β.app X')) ((α.app X ⊗ₘ β.app X') ≫ F'.map f ▷ G'.obj X')

Tactic:
simpa using tensor_naturality α β f (𝟙 X')

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.NatTrans.tensor_naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
J : Type u_1
inst : Category.{v_1, u_1} J
C : Type u_2
inst_1 : Category.{v_2, u_2} C
inst_2 : MonoidalCategory.{v_2, u_2} C
F G F' G' : Functor.{v_1, v_2, u_1, u_2} J C
α : F ⟶ F'
β : G ⟶ G'
X' Y' : J
f : X' ⟶ Y'
X : J
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (G.obj X') ⟶ tensorObj.{v_2, u_2} (𝒞 := inst_1) (F'.obj X) (G'.obj Y'))
    (F.obj X ◁ G.map f ≫ (α.app X ⊗ₘ β.app Y')) ((α.app X ⊗ₘ β.app X') ≫ F'.obj X ◁ G'.map f)

Tactic:
simpa using tensor_naturality α β (𝟙 X) f

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.NatTrans.tensor_naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : ObjectProperty.{v, u} C
tensorUnit : P (MonoidalCategoryStruct.tensorUnit.{v, u} C (𝒞 := inst))
tensorObj : ∀ (X Y : C), P X → P Y → P (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) X Y)
X₁ Y₁ X₂ Y₂ : P.FullSubcategory
x : X₁ ⟶ Y₁
x_1 : X₂ ⟶ Y₂
h :
  Eq.{v + 1} (α :=
    (FullSubcategory.mk (P := P)
            (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) (X₁.obj (P := P)) (X₂.obj (P := P))) ⋯).obj
        (P := P) ⟶
      (FullSubcategory.mk (P := P)
            (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) (Y₁.obj (P := P)) (Y₂.obj (P := P))) ⋯).obj
        (P := P))
    (InducedCategory.Hom.hom (homMk (P := P) (x.hom ⊗ₘ x_1.hom)))
    (InducedCategory.Hom.hom
      (CategoryStruct.comp (Y :=
        FullSubcategory.mk (P := P)
          (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) (Y₁.obj (P := P)) (X₂.obj (P := P))) ⋯)
        (homMk (P := P) (x.hom ▷ X₂.obj (P := P))) (homMk (P := P) (Y₁.obj (P := P) ◁ x_1.hom))))
⊢ Eq.{v + 1} (α :=
    FullSubcategory.mk (P := P)
        (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) (X₁.obj (P := P)) (X₂.obj (P := P))) ⋯ ⟶
      FullSubcategory.mk (P := P)
        (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) (Y₁.obj (P := P)) (Y₂.obj (P := P))) ⋯)
    (homMk (P := P) (x.hom ⊗ₘ x_1.hom))
    (CategoryStruct.comp (Y :=
      FullSubcategory.mk (P := P)
        (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) (Y₁.obj (P := P)) (X₂.obj (P := P))) ⋯)
      (homMk (P := P) (x.hom ▷ X₂.obj (P := P))) (homMk (P := P) (Y₁.obj (P := P) ◁ x_1.hom)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : ObjectProperty.{v, u} C
tensorUnit : P (MonoidalCategoryStruct.tensorUnit.{v, u} C (𝒞 := inst))
tensorObj : ∀ (X Y : C), P X → P Y → P (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) X Y)
X₁ Y₁ X₂ Y₂ : P.FullSubcategory
x : X₁ ⟶ Y₁
x_1 : X₂ ⟶ Y₂
⊢ Eq.{v + 1} (α :=
    (FullSubcategory.mk (P := P)
            (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) (X₁.obj (P := P)) (X₂.obj (P := P))) ⋯).obj
        (P := P) ⟶
      (FullSubcategory.mk (P := P)
            (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) (Y₁.obj (P := P)) (Y₂.obj (P := P))) ⋯).obj
        (P := P))
    (InducedCategory.Hom.hom (homMk (P := P) (x.hom ⊗ₘ x_1.hom)))
    (InducedCategory.Hom.hom
      (CategoryStruct.comp (Y :=
        FullSubcategory.mk (P := P)
          (MonoidalCategoryStruct.tensorObj.{v, u} (𝒞 := inst) (Y₁.obj (P := P)) (X₂.obj (P := P))) ⋯)
        (homMk (P := P) (x.hom ▷ X₂.obj (P := P))) (homMk (P := P) (Y₁.obj (P := P) ◁ x_1.hom))))

Tactic:
apply tensorHom_def

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Center.{v₁, u₁} C
f g : X ⟶ Y
w : f.f = g.f
mk :
  ∀ (f : X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ⟶ Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
    (comm :
      ∀ (U : C),
        f ▷ U ≫ (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
          (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫ U ◁ f)
    (w : { f := f, comm := comm : X.Hom Y }.f = g.f), { f := f, comm := comm : X.Hom Y } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Center.{v₁, u₁} C
g : X ⟶ Y
f : X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ⟶ Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)
comm :
  ∀ (U : C),
    f ▷ U ≫ (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
      (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫ U ◁ f
w : { f := f, comm := comm : X.Hom Y }.f = g.f
mk :
  ∀ (f_1 : X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ⟶ Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
    (comm_1 :
      ∀ (U : C),
        f_1 ▷ U ≫ (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
          (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫ U ◁ f_1)
    (w : { f := f, comm := comm : X.Hom Y }.f = { f := f_1, comm := comm_1 }.f),
    { f := f, comm := comm : X.Hom Y } = { f := f_1, comm := comm_1 }
⊢ { f := f, comm := comm : X.Hom Y } = g

Tactic:
cases g