awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategoryStruct.{v, u} C
id_tensorHom_id : ∀ (X₁ X₂ : C), 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X₁ X₂)
id_tensorHom :
  ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ ⟶ Y₂),
    Eq (α := tensorObj.{v, u} (𝒞 := inst) X Y₁ ⟶ tensorObj.{v, u} (𝒞 := inst) X Y₂) (𝟙 X ⊗ₘ f) (X ◁ f)
tensorHom_id :
  ∀ {X₁ X₂ : C} (f : X₁ ⟶ X₂) (Y : C),
    Eq (α := tensorObj.{v, u} (𝒞 := inst) X₁ Y ⟶ tensorObj.{v, u} (𝒞 := inst) X₂ Y) (f ⊗ₘ 𝟙 Y) (f ▷ Y)
tensorHom_comp_tensorHom :
  ∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
    Eq (α := tensorObj.{v, u} (𝒞 := inst) X₁ X₂ ⟶ tensorObj.{v, u} (𝒞 := inst) Z₁ Z₂) ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))
      (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)
associator_naturality :
  ∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
    Eq (α :=
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X₁ X₂) X₃ ⟶
        tensorObj.{v, u} (𝒞 := inst) Y₁ (tensorObj.{v, u} (𝒞 := inst) Y₂ Y₃))
      (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ hom (α_ Y₁ Y₂ Y₃)) (hom (α_ X₁ X₂ X₃) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))
leftUnitor_naturality :
  ∀ {X Y : C} (f : X ⟶ Y), (𝟙 (tensorUnit.{v, u} C (𝒞 := inst)) ⊗ₘ f) ≫ hom (λ_ Y) = hom (λ_ X) ≫ f
rightUnitor_naturality :
  ∀ {X Y : C} (f : X ⟶ Y), (f ⊗ₘ 𝟙 (tensorUnit.{v, u} C (𝒞 := inst))) ≫ hom (ρ_ Y) = hom (ρ_ X) ≫ f
pentagon :
  ∀ (W X Y Z : C),
    (hom (α_ W X Y) ⊗ₘ 𝟙 Z) ≫ hom (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z) ≫ (𝟙 W ⊗ₘ hom (α_ X Y Z)) =
      hom (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) ≫ hom (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z))
triangle :
  ∀ (X Y : C),
    Eq.{v + 1} (α :=
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst))) Y ⟶
        tensorObj.{v, u} (𝒞 := inst) X Y)
      (hom (α_ X (tensorUnit.{v, u} C (𝒞 := inst)) Y) ≫ (𝟙 X ⊗ₘ hom (λ_ Y))) (hom (ρ_ X) ⊗ₘ 𝟙 Y)
X Y : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst))) Y ⟶
      tensorObj.{v, u} (𝒞 := inst) X Y)
    (hom (α_ X (tensorUnit.{v, u} C (𝒞 := inst)) Y) ≫ X ◁ hom (λ_ Y)) (hom (ρ_ X) ▷ Y)

Tactic:
simp [← id_tensorHom, ← tensorHom_id, triangle]
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y₁ Y₂ : C
f : Y₁ ⟶ Y₂
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X Y₁ ⟶ tensorObj.{v, u} (𝒞 := inst) X Y₂) (𝟙 X ⊗ₘ f) (X ◁ 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₁ X₂ : C
f : X₁ ⟶ X₂
Y : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X₁ Y ⟶ tensorObj.{v, u} (𝒞 := inst) X₂ Y) (f ⊗ₘ 𝟙 Y) (f ▷ Y)

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 : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) W X ⟶ tensorObj.{v, u} (𝒞 := inst) W Z) (W ◁ (f ≫ g)) (W ◁ f ≫ W ◁ g)

Tactic:
simp [← id_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
f : X ⟶ Y
rw : tensorUnit.{v, u} C (𝒞 := inst) ◁ f = (tensorUnit.{v, u} C (𝒞 := inst) ◁ f ≫ hom (λ_ Y)) ≫ Iso.inv (λ_ Y)
⊢ tensorUnit.{v, u} C (𝒞 := inst) ◁ f = hom (λ_ X) ≫ f ≫ Iso.inv (λ_ Y)

Tactic:
rw [← assoc, ← leftUnitor_naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.leftUnitor_naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
f : X ⟶ Y
⊢ tensorUnit.{v, u} C (𝒞 := inst) ◁ f = (tensorUnit.{v, u} C (𝒞 := inst) ◁ f ≫ hom (λ_ Y)) ≫ Iso.inv (λ_ Y)

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 Z' : C
f : Z ⟶ Z'
simp : 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y) ⊗ₘ f = hom (α_ X Y Z) ≫ (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ f) ≫ Iso.inv (α_ X Y Z')
⊢ tensorObj.{v, u} (𝒞 := inst) X Y ◁ f = hom (α_ X Y Z) ≫ X ◁ Y ◁ f ≫ Iso.inv (α_ X Y Z')

Tactic:
simp only [← id_tensorHom]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom
-- 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
f : Z ⟶ Z'
rw : 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y) ⊗ₘ f = (((𝟙 X ⊗ₘ 𝟙 Y) ⊗ₘ f) ≫ hom (α_ X Y Z')) ≫ Iso.inv (α_ X Y Z')
⊢ 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y) ⊗ₘ f = hom (α_ X Y Z) ≫ (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ f) ≫ Iso.inv (α_ X Y Z')

Tactic:
rw [← assoc, ← associator_naturality]

Premises used: CategoryTheory.Category.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
f : Z ⟶ Z'
⊢ 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y) ⊗ₘ f = (((𝟙 X ⊗ₘ 𝟙 Y) ⊗ₘ f) ≫ hom (α_ X Y Z')) ≫ Iso.inv (α_ X Y 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 : C
f : W ⟶ X
g : X ⟶ Y
Z : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) W Z ⟶ tensorObj.{v, u} (𝒞 := inst) Y Z) ((f ≫ g) ▷ Z) (f ▷ Z ≫ g ▷ Z)

Tactic:
simp [← tensorHom_id]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_id
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
f : X ⟶ Y
rw :
  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)) ((f ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫ hom (ρ_ Y)) ≫ Iso.inv (ρ_ 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)) (hom (ρ_ X) ≫ f ≫ Iso.inv (ρ_ Y))

Tactic:
rw [← assoc, ← rightUnitor_naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.rightUnitor_naturality
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
f : 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)) ((f ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫ hom (ρ_ Y)) ≫ Iso.inv (ρ_ Y))

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

Tactic:
simp only [← tensorHom_id]

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

Tactic:
rw [associator_naturality]

Premises used: 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 X' : C
f : X ⟶ X'
Y Z : C
⊢ f ⊗ₘ 𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z) = Iso.inv (α_ X Y Z) ≫ hom (α_ X Y Z) ≫ (f ⊗ₘ 𝟙 Y ⊗ₘ 𝟙 Z)

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

Tactic:
simp only [← id_tensorHom, ← tensorHom_id]

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

Tactic:
rw [← assoc, ← associator_naturality]

Premises used: CategoryTheory.Category.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 Y' : C
f : Y ⟶ Y'
Z : C
⊢ Eq (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y') Z)
    ((𝟙 X ⊗ₘ f) ⊗ₘ 𝟙 Z) ((((𝟙 X ⊗ₘ f) ⊗ₘ 𝟙 Z) ≫ hom (α_ X Y' Z)) ≫ Iso.inv (α_ X Y' 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 : Y ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (W ◁ g ≫ f ▷ Z) (f ▷ Y ≫ X ◁ g)

Tactic:
simp [← id_tensorHom, ← tensorHom_id]

Premises used: CategoryTheory.MonoidalCategory.id_tensorHom, CategoryTheory.MonoidalCategory.tensorHom_id
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X₁ Y₁ X₂ Y₂ : C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X₁ X₂ ⟶ tensorObj.{v, u} (𝒞 := inst) Y₁ Y₂) (f ⊗ₘ g) (X₁ ◁ g ≫ f ▷ Y₂)

Tactic:
whisker_exchange f g ▸ tensorHom_def f g

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange, Eq.rec, CategoryTheory.MonoidalCategory.tensorHom_def, Eq.symm
-- 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) W Z) (V ◁ g ≫ (f ⊗ₘ h)) (f ⊗ₘ g ≫ h)

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
V W X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : V ⟶ W
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X V ⟶ tensorObj.{v, u} (𝒞 := inst) Z W) (f ▷ V ≫ (g ⊗ₘ h)) (f ≫ g ⊗ₘ h)

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
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) W Z) ((f ⊗ₘ g) ≫ W ◁ h) (f ⊗ₘ g ≫ h)

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
V W X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : V ⟶ W
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X V ⟶ tensorObj.{v, u} (𝒞 := inst) Z W) ((f ⊗ₘ h) ≫ g ▷ W) (f ≫ g ⊗ₘ h)

Tactic:
simp [tensorHom_def, whisker_exchange]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange, 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 Z : C
f : tensorUnit.{v, u} C (𝒞 := inst) ⟶ Y
g : X ⟶ Z
⊢ Iso.inv (λ_ X) ≫ (f ⊗ₘ g) = g ≫ Iso.inv (λ_ Z) ≫ f ▷ Z

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 Z : C
f : X ⟶ Y
g : tensorUnit.{v, u} C (𝒞 := inst) ⟶ Z
⊢ Iso.inv (ρ_ X) ≫ (f ⊗ₘ g) = f ≫ Iso.inv (ρ_ Y) ≫ Y ◁ g

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 Z : C
f : Y ≅ Z
rw : X ◁ (f.hom ≫ f.inv) = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y)
rw₁ : X ◁ 𝟙 Y = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y)
rw₂ rw₃ :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Y)
    (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y)) (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y))
⊢ X ◁ f.hom ≫ X ◁ f.inv = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y)

Tactic:
rw [← whiskerLeft_comp, hom_inv_id, whiskerLeft_id]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.Iso.hom_inv_id, CategoryTheory.MonoidalCategory.whiskerLeft_id
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
f : X ≅ Y
Z : C
rw : (f.hom ≫ f.inv) ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
rw₁ : 𝟙 X ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
rw₂ rw₃ :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) X Z)
    (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)) (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z))
⊢ f.hom ▷ Z ≫ f.inv ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)

Tactic:
rw [← comp_whiskerRight, hom_inv_id, id_whiskerRight]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.MonoidalCategory.id_whiskerRight
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
f : Y ≅ Z
rw : X ◁ (f.inv ≫ f.hom) = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
rw₁ : X ◁ 𝟙 Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
rw₂ rw₃ :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) X Z)
    (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)) (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z))
⊢ X ◁ f.inv ≫ X ◁ f.hom = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)

Tactic:
rw [← whiskerLeft_comp, inv_hom_id, whiskerLeft_id]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.whiskerLeft_id
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
f : X ≅ Y
Z : C
rw : (f.inv ≫ f.hom) ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z)
rw₁ : 𝟙 Y ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z)
rw₂ rw₃ :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) Y Z ⟶ tensorObj.{v, u} (𝒞 := inst) Y Z)
    (𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z)) (𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z))
⊢ f.inv ▷ Z ≫ f.hom ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z)

Tactic:
rw [← comp_whiskerRight, inv_hom_id, id_whiskerRight]

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.MonoidalCategory.id_whiskerRight
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
f : Y ⟶ Z
inst_2 : IsIso f
rw : X ◁ (f ≫ inv f) = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y)
rw₁ : X ◁ 𝟙 Y = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y)
rw₂ rw₃ :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Y)
    (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y)) (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y))
⊢ X ◁ f ≫ X ◁ inv f = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Y)

Tactic:
rw [← whiskerLeft_comp, IsIso.hom_inv_id, whiskerLeft_id]

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.whiskerLeft_id, CategoryTheory.IsIso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsIso f
Z : C
rw : (f ≫ inv f) ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
rw₁ : 𝟙 X ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
rw₂ rw₃ :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) X Z)
    (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)) (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z))
⊢ f ▷ Z ≫ inv f ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)

Tactic:
rw [← comp_whiskerRight, IsIso.hom_inv_id, id_whiskerRight]

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.MonoidalCategory.id_whiskerRight, CategoryTheory.IsIso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
f : Y ⟶ Z
inst_2 : IsIso f
rw : X ◁ (inv f ≫ f) = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
rw₁ : X ◁ 𝟙 Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)
rw₂ rw₃ :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) X Z)
    (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)) (𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z))
⊢ X ◁ inv f ≫ X ◁ f = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X Z)

Tactic:
rw [← whiskerLeft_comp, IsIso.inv_hom_id, whiskerLeft_id]

Premises used: CategoryTheory.IsIso.inv_hom_id, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.whiskerLeft_id
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
f : X ⟶ Y
inst_2 : IsIso f
Z : C
rw : (inv f ≫ f) ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z)
rw₁ : 𝟙 Y ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z)
rw₂ rw₃ :
  Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) Y Z ⟶ tensorObj.{v, u} (𝒞 := inst) Y Z)
    (𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z)) (𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z))
⊢ inv f ▷ Z ≫ f ▷ Z = 𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Z)

Tactic:
rw [← comp_whiskerRight, IsIso.inv_hom_id, id_whiskerRight]

Premises used: CategoryTheory.IsIso.inv_hom_id, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.MonoidalCategory.id_whiskerRight
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
f : Y ⟶ Z
inst_2 : IsIso f
⊢ IsIso (X := tensorObj.{v, u} (𝒞 := inst) X Y) (X ◁ f)

Tactic:
(whiskerLeftIso X (asIso f)).isIso_hom

Premises used: CategoryTheory.MonoidalCategory.whiskerLeftIso, CategoryTheory.Iso.isIso_hom, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X : C
⊢ whiskerLeftIso W (Iso.refl X) = Iso.refl (tensorObj.{v, u} (𝒞 := inst) W X)

Tactic:
Iso.ext (whiskerLeft_id W X)

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_id, CategoryTheory.Iso.ext
-- 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 : X ≅ Y
g : Y ≅ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) W X ≅ tensorObj.{v, u} (𝒞 := inst) W Z) (whiskerLeftIso W (f ≪≫ g))
    (whiskerLeftIso W f ≪≫ whiskerLeftIso W g)

Tactic:
Iso.ext (whiskerLeft_comp W f.hom g.hom)

Premises used: CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.Iso.ext, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
W X Y : C
f : X ≅ Y
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ≅ tensorObj.{v, u} (𝒞 := inst) W X) (Iso.symm (whiskerLeftIso W f))
    (whiskerLeftIso W f.symm)

Tactic:
rfl

Premises used: CategoryTheory.MonoidalCategory.whiskerLeftIso, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
inst_2 : IsIso f
⊢ IsIso (X := tensorObj.{v, u} (𝒞 := inst) X Z) (f ▷ Z)

Tactic:
(whiskerRightIso (asIso f) Z).isIso_hom

Premises used: CategoryTheory.MonoidalCategory.whiskerRightIso, CategoryTheory.Iso.isIso_hom, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X W : C
⊢ whiskerRightIso (Iso.refl X) W = Iso.refl (tensorObj.{v, u} (𝒞 := inst) X W)

Tactic:
Iso.ext (id_whiskerRight X W)

Premises used: CategoryTheory.MonoidalCategory.id_whiskerRight, CategoryTheory.Iso.ext
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y Z : C
f : X ≅ Y
g : Y ≅ Z
W : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X W ≅ tensorObj.{v, u} (𝒞 := inst) Z W) (whiskerRightIso (f ≪≫ g) W)
    (whiskerRightIso f W ≪≫ whiskerRightIso g W)

Tactic:
Iso.ext (comp_whiskerRight f.hom g.hom W)

Premises used: CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.Iso.ext, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
f : X ≅ Y
W : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Y W ≅ tensorObj.{v, u} (𝒞 := inst) X W) (Iso.symm (whiskerRightIso f W))
    (whiskerRightIso f.symm W)

Tactic:
rfl

Premises used: CategoryTheory.MonoidalCategory.whiskerRightIso, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y X' Y' : C
f : X ≅ Y
g : X' ≅ Y'
⊢ (f.hom ⊗ₘ g.hom) ≫ (f.inv ⊗ₘ g.inv) = 𝟙 (tensorObj.{v, u} (𝒞 := inst) X X')

Tactic:
simp [Iso.hom_inv_id, Iso.hom_inv_id]

Premises used: CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y X' Y' : C
f : X ≅ Y
g : X' ≅ Y'
⊢ (f.inv ⊗ₘ g.inv) ≫ (f.hom ⊗ₘ g.hom) = 𝟙 (tensorObj.{v, u} (𝒞 := inst) Y Y')

Tactic:
simp [Iso.inv_hom_id, Iso.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y X' Y' : C
f : X ≅ Y
g : X' ≅ Y'
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X X' ≅ tensorObj.{v, u} (𝒞 := inst) Y Y') (f ⊗ᵢ g) (f ▷ᵢ X' ≪≫ Y ◁ᵢ g)

Tactic:
Iso.ext (tensorHom_def f.hom g.hom)

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.Iso.ext, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y X' Y' : C
f : X ≅ Y
g : X' ≅ Y'
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X X' ≅ tensorObj.{v, u} (𝒞 := inst) Y Y') (f ⊗ᵢ g) (X ◁ᵢ g ≪≫ f ▷ᵢ Y')

Tactic:
Iso.ext (tensorHom_def' f.hom g.hom)

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def', CategoryTheory.Iso.ext, CategoryTheory.Iso.hom
-- 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
inst_2 : IsIso f
g : Y ⟶ Z
inst_3 : IsIso g
⊢ IsIso (X := tensorObj.{v, u} (𝒞 := inst) W Y) (f ⊗ₘ g)

Tactic:
(asIso f ⊗ᵢ asIso g).isIso_hom

Premises used: CategoryTheory.MonoidalCategory.tensorIso, CategoryTheory.Iso.isIso_hom, CategoryTheory.asIso