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

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
P : Prop
inst_2 : Decidable P
X Y Z : C
f : P → (Y ⟶ Z)
f' : ¬P → (Y ⟶ Z)
pos : ∀ (h : P), Eq (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (X ◁ f h) (X ◁ f h)
neg : ∀ (h : ¬P), Eq (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (X ◁ f' h) (X ◁ f' h)
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z)
    (X ◁ if h : P then f h else f' h) (if h : P then X ◁ f h else X ◁ f' h)

Tactic:
split_ifs
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : Prop
inst_2 : Decidable P
X Y Z : C
f : P → (Y ⟶ Z)
f' : ¬P → (Y ⟶ Z)
h : P
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (X ◁ f h) (X ◁ f h)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : Prop
inst_2 : Decidable P
X Y Z : C
f : P → (Y ⟶ Z)
f' : ¬P → (Y ⟶ Z)
h : ¬P
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (X ◁ f' h) (X ◁ f' h)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : Prop
inst_2 : Decidable P
X Y : C
f : P → (X ⟶ Y)
f' : ¬P → (X ⟶ Y)
Z : C
pos : ∀ (h : P), Eq (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) Y Z) (f h ▷ Z) (f h ▷ Z)
neg : ∀ (h : ¬P), Eq (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) Y Z) (f' h ▷ Z) (f' h ▷ Z)
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) Y Z)
    ((if h : P then f h else f' h) ▷ Z) (if h : P then f h ▷ Z else f' h ▷ Z)

Tactic:
split_ifs
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : Prop
inst_2 : Decidable P
X Y : C
f : P → (X ⟶ Y)
f' : ¬P → (X ⟶ Y)
Z : C
h : P
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) Y Z) (f h ▷ Z) (f h ▷ Z)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : Prop
inst_2 : Decidable P
X Y : C
f : P → (X ⟶ Y)
f' : ¬P → (X ⟶ Y)
Z : C
h : ¬P
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) Y Z) (f' h ▷ Z) (f' h ▷ Z)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : Prop
inst_2 : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
pos : ∀ (h : P), Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (f ⊗ₘ g h) (f ⊗ₘ g h)
neg : ∀ (h : ¬P), Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (f ⊗ₘ g' h) (f ⊗ₘ g' h)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (f ⊗ₘ if h : P then g h else g' h)
    (if h : P then f ⊗ₘ g h else f ⊗ₘ g' h)

Tactic:
split_ifs
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : Prop
inst_2 : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h : P
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (f ⊗ₘ g h) (f ⊗ₘ g h)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : Prop
inst_2 : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h : ¬P
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) W Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (f ⊗ₘ g' h) (f ⊗ₘ g' h)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : Prop
inst_2 : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
pos : ∀ (h : P), Eq (α := tensorObj.{v, u} (𝒞 := inst) Y W ⟶ tensorObj.{v, u} (𝒞 := inst) Z X) (g h ⊗ₘ f) (g h ⊗ₘ f)
neg : ∀ (h : ¬P), Eq (α := tensorObj.{v, u} (𝒞 := inst) Y W ⟶ tensorObj.{v, u} (𝒞 := inst) Z X) (g' h ⊗ₘ f) (g' h ⊗ₘ f)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Y W ⟶ tensorObj.{v, u} (𝒞 := inst) Z X) ((if h : P then g h else g' h) ⊗ₘ f)
    (if h : P then g h ⊗ₘ f else g' h ⊗ₘ f)

Tactic:
split_ifs
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : Prop
inst_2 : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h : P
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Y W ⟶ tensorObj.{v, u} (𝒞 := inst) Z X) (g h ⊗ₘ f) (g h ⊗ₘ f)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
P : Prop
inst_2 : Decidable P
W X Y Z : C
f : W ⟶ X
g : P → (Y ⟶ Z)
g' : ¬P → (Y ⟶ Z)
h : ¬P
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) Y W ⟶ tensorObj.{v, u} (𝒞 := inst) Z X) (g' h ⊗ₘ f) (g' h ⊗ₘ f)

Tactic:
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
f : Y = Z
refl : Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Y) (X ◁ eqToHom ⋯) (eqToHom ⋯)
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (X ◁ eqToHom f) (eqToHom ⋯)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) X Y) (X ◁ eqToHom ⋯) (eqToHom ⋯)

Tactic:
simp only [whiskerLeft_id, eqToHom_refl]

Premises used: CategoryTheory.eqToHom_refl, 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
refl : Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (eqToHom ⋯ ▷ Z) (eqToHom ⋯)
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) Y Z) (eqToHom f ▷ Z) (eqToHom ⋯)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Z : C
⊢ Eq.{v + 1} (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) X Z) (eqToHom ⋯ ▷ Z) (eqToHom ⋯)

Tactic:
simp only [id_whiskerRight, eqToHom_refl]

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

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'
⊢ f = Iso.inv (λ_ X) ≫ tensorUnit.{v, u} C (𝒞 := inst) ◁ f ≫ hom (λ_ X')

Tactic:
simp only [id_whiskerLeft, assoc, inv_hom_id, comp_id, inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.MonoidalCategory.id_whiskerLeft, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc
-- 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'
⊢ Eq (α := X ⟶ tensorObj.{v, u} (𝒞 := inst) X' (tensorUnit.{v, u} C (𝒞 := inst))) (f ≫ Iso.inv (ρ_ X'))
    (Iso.inv (ρ_ X) ≫ f ▷ tensorUnit.{v, u} C (𝒞 := inst))

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 : X ⟶ Y
⊢ f =
    CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst))) (Iso.inv (ρ_ X))
      (f ▷ tensorUnit.{v, u} C (𝒞 := inst) ≫ hom (ρ_ 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 : 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
W X Y Z : C
⊢ inv (W ◁ Iso.inv (α_ X Y Z) ≫ Iso.inv (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z) ≫ Iso.inv (α_ W X Y) ▷ Z) =
    inv (Iso.inv (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.inv (α_ (tensorObj.{v, u} (𝒞 := inst) W 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
rw :
  (W ◁ Iso.inv (α_ X Y Z) ≫
        Iso.inv (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z) ≫
          Iso.inv (α_ W X Y) ▷ Z ≫ hom (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z)) ≫
      Iso.inv (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) =
    (W ◁ Iso.inv (α_ X Y Z) ≫ W ◁ hom (α_ X Y Z) ≫ Iso.inv (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z))) ≫
      Iso.inv (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z)
⊢ Iso.inv (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z) ≫
      Iso.inv (α_ W X Y) ▷ Z ≫ hom (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) =
    W ◁ hom (α_ X Y Z) ≫ Iso.inv (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z))

Tactic:
rw [← cancel_epi (W ◁ (α_ X Y Z).inv), ← cancel_mono (α_ (W ⊗ X) Y Z).inv]

Premises used: CategoryTheory.MonoidalCategoryStruct.whiskerLeft, CategoryTheory.cancel_mono, CategoryTheory.MonoidalCategoryStruct.tensorObj, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- 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
⊢ (W ◁ Iso.inv (α_ X Y Z) ≫
        Iso.inv (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z) ≫
          Iso.inv (α_ W X Y) ▷ Z ≫ hom (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z)) ≫
      Iso.inv (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) =
    (W ◁ Iso.inv (α_ X Y Z) ≫ W ◁ hom (α_ X Y Z) ≫ Iso.inv (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z))) ≫
      Iso.inv (α_ (tensorObj.{v, u} (𝒞 := inst) W 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
⊢ inv
      (Iso.inv (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) ≫
        hom (α_ W X Y) ▷ Z ≫ hom (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z)) =
    inv (hom (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ W ◁ 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
⊢ W ◁ hom (α_ X Y Z) ≫
      Iso.inv (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.inv (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) =
    Iso.inv (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z) ≫ Iso.inv (α_ W X Y) ▷ Z

Tactic:
simp [← cancel_epi (W ◁ (α_ X Y Z).inv)]

Premises used: CategoryTheory.MonoidalCategoryStruct.whiskerLeft, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- 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
⊢ inv
      (hom (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) ≫
        hom (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ W ◁ Iso.inv (α_ X Y Z)) =
    inv (hom (α_ W X Y) ▷ Z ≫ hom (α_ W (tensorObj.{v, u} (𝒞 := inst) 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
rw :
  (Iso.inv (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫
        hom (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫
          W ◁ Iso.inv (α_ X Y Z) ≫ Iso.inv (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z)) ≫
      Iso.inv (α_ W X Y) ▷ Z =
    (Iso.inv (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫
        Iso.inv (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) ≫ hom (α_ W X Y) ▷ Z) ≫
      Iso.inv (α_ W X Y) ▷ Z
⊢ hom (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫
      W ◁ Iso.inv (α_ X Y Z) ≫ Iso.inv (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z) =
    Iso.inv (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) ≫ hom (α_ W X Y) ▷ Z

Tactic:
rw [← cancel_epi (α_ W X (Y ⊗ Z)).inv, ← cancel_mono ((α_ W X Y).inv ▷ Z)]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.MonoidalCategoryStruct.whiskerRight, CategoryTheory.MonoidalCategoryStruct.tensorObj, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- 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
⊢ (Iso.inv (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫
        hom (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫
          W ◁ Iso.inv (α_ X Y Z) ≫ Iso.inv (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z)) ≫
      Iso.inv (α_ W X Y) ▷ Z =
    (Iso.inv (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫
        Iso.inv (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) ≫ hom (α_ W X Y) ▷ Z) ≫
      Iso.inv (α_ W 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
⊢ inv
      (hom (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z) ≫
        W ◁ hom (α_ X Y Z) ≫ Iso.inv (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z))) =
    inv (Iso.inv (α_ W X Y) ▷ Z ≫ hom (α_ (tensorObj.{v, u} (𝒞 := inst) W 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
⊢ Iso.inv (α_ W X Y) ▷ Z ≫
      hom (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) ≫ hom (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z)) =
    hom (α_ W (tensorObj.{v, u} (𝒞 := inst) X Y) Z) ≫ W ◁ hom (α_ X Y Z)

Tactic:
simp [← cancel_epi ((α_ W X Y).hom ▷ Z)]

Premises used: CategoryTheory.MonoidalCategoryStruct.whiskerRight, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.cancel_epi, 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
⊢ inv
      (Iso.inv (α_ W X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫
        Iso.inv (α_ (tensorObj.{v, u} (𝒞 := inst) W X) Y Z) ≫ hom (α_ W X Y) ▷ Z) =
    inv (W ◁ Iso.inv (α_ X Y Z) ≫ Iso.inv (α_ W (tensorObj.{v, u} (𝒞 := inst) 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
X Y : C
rw :
  Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) Y) ⟶
      tensorObj.{v, u} (𝒞 := inst) X Y)
    (Iso.inv (α_ X (tensorUnit.{v, u} C (𝒞 := inst)) Y) ≫
      hom (α_ X (tensorUnit.{v, u} C (𝒞 := inst)) Y) ≫ X ◁ hom (λ_ Y))
    (X ◁ hom (λ_ Y))
rw₁ rw₂ :
  Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) Y) ⟶
      tensorObj.{v, u} (𝒞 := inst) X Y)
    (X ◁ hom (λ_ Y)) (X ◁ hom (λ_ Y))
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) Y) ⟶
      tensorObj.{v, u} (𝒞 := inst) X Y)
    (Iso.inv (α_ X (tensorUnit.{v, u} C (𝒞 := inst)) Y) ≫ hom (ρ_ X) ▷ Y) (X ◁ hom (λ_ Y))

Tactic:
rw [← triangle, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.MonoidalCategory.triangle
-- Module: Mathlib.CategoryTheory.Monoidal.Category
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
X Y : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X Y ⟶
      tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) (tensorUnit.{v, u} C (𝒞 := inst)) Y))
    (Iso.inv (ρ_ X) ▷ Y ≫ hom (α_ X (tensorUnit.{v, u} C (𝒞 := inst)) Y)) (X ◁ Iso.inv (λ_ Y))

Tactic:
simp [← cancel_mono (X ◁ (λ_ Y).hom)]

Premises used: CategoryTheory.MonoidalCategoryStruct.whiskerLeft, CategoryTheory.MonoidalCategoryStruct.leftUnitor, CategoryTheory.cancel_mono, 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
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X Y ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X (tensorUnit.{v, u} C (𝒞 := inst))) Y)
    (X ◁ Iso.inv (λ_ Y) ≫ Iso.inv (α_ X (tensorUnit.{v, u} C (𝒞 := inst)) Y)) (Iso.inv (ρ_ X) ▷ Y)

Tactic:
simp [← cancel_mono ((ρ_ X).hom ▷ Y)]

Premises used: CategoryTheory.MonoidalCategoryStruct.rightUnitor, CategoryTheory.cancel_mono, CategoryTheory.MonoidalCategoryStruct.whiskerRight, 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
⊢ inv (Iso.inv (λ_ X) ▷ Y) =
    inv (Iso.inv (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y)) ≫ Iso.inv (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X 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 : C
⊢ inv (X ◁ Iso.inv (ρ_ Y)) =
    inv (Iso.inv (ρ_ (tensorObj.{v, u} (𝒞 := inst) X Y)) ≫ hom (α_ X Y (tensorUnit.{v, u} C (𝒞 := inst))))

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
⊢ hom (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y)) = Iso.inv (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X Y) ≫ hom (λ_ X) ▷ 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 : C
⊢ Iso.inv (λ_ (tensorObj.{v, u} (𝒞 := inst) X Y)) = Iso.inv (λ_ X) ▷ Y ≫ hom (α_ (tensorUnit.{v, u} C (𝒞 := inst)) X 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 : C
⊢ hom (ρ_ (tensorObj.{v, u} (𝒞 := inst) X Y)) = hom (α_ X Y (tensorUnit.{v, u} C (𝒞 := inst))) ≫ X ◁ hom (ρ_ 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 : C
⊢ Iso.inv (ρ_ (tensorObj.{v, u} (𝒞 := inst) X Y)) =
    X ◁ Iso.inv (ρ_ Y) ≫ Iso.inv (α_ X Y (tensorUnit.{v, u} C (𝒞 := inst)))

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

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def