awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X₁ X₂) X₃ ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₂ Y₃))
    (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ Iso.hom (α_ Y₁ Y₂ Y₃)) (Iso.hom (α_ X₁ X₂ X₃) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))

Tactic:
apply associator_naturality

Premises used: CategoryTheory.Localization.Monoidal.associator_naturality
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X Y Z : C
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := Localization.instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := Localization.instCategoryLocalizedMonoidal L W ε)
          (Functor.obj (toMonoidalCategory L W ε) X) (Functor.obj (toMonoidalCategory L W ε) Y))
        (Functor.obj (toMonoidalCategory L W ε) Z))
      (Functor.obj (toMonoidalCategory L W ε)
        (tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z))))
    (Iso.hom (μ L W ε X Y) ▷ Functor.obj (toMonoidalCategory L W ε) Z ≫
      Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z) ≫
        Functor.map (toMonoidalCategory L W ε) (Iso.hom (α_ X Y Z)))
    (Iso.hom
        (α_ (Functor.obj (toMonoidalCategory L W ε) X) (Functor.obj (toMonoidalCategory L W ε) Y)
          (Functor.obj (toMonoidalCategory L W ε) Z)) ≫
      Functor.obj (toMonoidalCategory L W ε) X ◁ Iso.hom (μ L W ε Y Z) ≫
        Iso.hom (μ L W ε X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z)))

Tactic:
simp [associator_hom_app L W ε X Y Z]

Premises used: CategoryTheory.Localization.Monoidal.associator_hom_app
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X Y Z : C
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := Localization.instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := Localization.instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X)
          (Functor.obj L' Y))
        (Functor.obj L' Z))
      (tensorObj.{v_2, u_2} (𝒞 := Localization.instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X)
        (tensorObj.{v_2, u_2} (𝒞 := Localization.instCategoryLocalizedMonoidal L W ε) (Functor.obj L' Y)
          (Functor.obj L' Z))))
    (Iso.hom (α_ (Functor.obj L' X) (Functor.obj L' Y) (Functor.obj L' Z)))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_2, u_2} (𝒞 := Localization.instCategoryLocalizedMonoidal L W ε)
        (Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) (Functor.obj L' Z))
      (Functor.LaxMonoidal.μ L' X Y ▷ Functor.obj L' Z)
      (Functor.LaxMonoidal.μ L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z ≫
        Functor.map L' (Iso.hom (α_ X Y Z)) ≫
          Functor.OplaxMonoidal.δ L' X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z) ≫
            Functor.obj L' X ◁ Functor.OplaxMonoidal.δ L' Y Z))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
X Y Z : C
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := Localization.instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X)
        (tensorObj.{v_2, u_2} (𝒞 := Localization.instCategoryLocalizedMonoidal L W ε) (Functor.obj L' Y)
          (Functor.obj L' Z)))
      (tensorObj.{v_2, u_2} (𝒞 := Localization.instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := Localization.instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X)
          (Functor.obj L' Y))
        (Functor.obj L' Z)))
    (Iso.inv (α_ (Functor.obj L' X) (Functor.obj L' Y) (Functor.obj L' Z)))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_2, u_2} (𝒞 := Localization.instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X)
        (Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z)))
      (Functor.obj L' X ◁ Functor.LaxMonoidal.μ L' Y Z)
      (Functor.LaxMonoidal.μ L' X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z) ≫
        Functor.map L' (Iso.inv (α_ X Y Z)) ≫
          Functor.OplaxMonoidal.δ L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z ≫
            Functor.OplaxMonoidal.δ L' X Y ▷ Functor.obj L' Z))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
⊢ IsLocalization (D := LocalizedMonoidal L W ε) L' W

Tactic:
inferInstanceAs (L.IsLocalization W)

Premises used: _private.0.CategoryTheory.Localization.Monoidal.instIsLocalizationLocalizedMonoidalToMonoidalCategory_1._proof_1
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
inst_5 : BraidedCategory.{v_1, u_1} C
X Y : C
simp :
  Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε) (obj (obj (tensorBifunctor L W ε) (obj L' X)) (obj L' Y))
      (obj (obj (tensorBifunctor L W ε) (obj L' Y)) (obj L' X)))
    (CategoryStruct.comp (Y := obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y))
        (NatTrans.app
          (NatTrans.app
            (Iso.hom
              (Lifting₂.iso L' L' W W (curriedTensor C ⋙ obj (whiskeringRight C C (LocalizedMonoidal L W ε)) L')
                (tensorBifunctor L W ε)))
            X)
          Y)
        (Functor.map L' (Iso.hom (β_ X Y)) ≫
          NatTrans.app
            (NatTrans.app
              (Iso.inv
                (Lifting₂.iso L' L' W W
                  (Functor.flip (curriedTensor C) ⋙ obj (whiskeringRight C C (LocalizedMonoidal L W ε)) L')
                  (Functor.flip (tensorBifunctor L W ε))))
              X)
            Y) :
      Quiver.Hom (V := LocalizedMonoidal L W ε) (obj (obj (tensorBifunctor L W ε) (obj L' X)) (obj L' Y))
        (obj (obj (tensorBifunctor L W ε) (obj L' Y)) (obj L' X)))
    (CategoryStruct.comp (Y := obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) (LaxMonoidal.μ L' X Y)
        (Functor.map L' (Iso.hom (β_ X Y)) ≫ OplaxMonoidal.δ L' Y X) :
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' X) (obj L' Y))
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' Y) (obj L' X)))
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε) (obj (obj (tensorBifunctor L W ε) (obj L' X)) (obj L' Y))
      (obj (obj (Functor.flip (tensorBifunctor L W ε)) (obj L' X)) (obj L' Y)))
    (NatTrans.app (NatTrans.app (Iso.hom (braidingNatIso L W ε)) (obj L' X)) (obj L' Y))
    (CategoryStruct.comp (Y := obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) (LaxMonoidal.μ L' X Y)
      (Functor.map L' (Iso.hom (β_ X Y)) ≫ OplaxMonoidal.δ L' Y X))

Tactic:
simp [braidingNatIso, lift₂NatIso]

Premises used: CategoryTheory.Localization.Monoidal.braidingNatIso, CategoryTheory.Localization.lift₂NatIso
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
inst_5 : BraidedCategory.{v_1, u_1} C
X Y : C
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε) (obj (obj (tensorBifunctor L W ε) (obj L' X)) (obj L' Y))
      (obj (obj (tensorBifunctor L W ε) (obj L' Y)) (obj L' X)))
    (CategoryStruct.comp (Y := obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y))
        (NatTrans.app
          (NatTrans.app
            (Iso.hom
              (Lifting₂.iso L' L' W W (curriedTensor C ⋙ obj (whiskeringRight C C (LocalizedMonoidal L W ε)) L')
                (tensorBifunctor L W ε)))
            X)
          Y)
        (Functor.map L' (Iso.hom (β_ X Y)) ≫
          NatTrans.app
            (NatTrans.app
              (Iso.inv
                (Lifting₂.iso L' L' W W
                  (Functor.flip (curriedTensor C) ⋙ obj (whiskeringRight C C (LocalizedMonoidal L W ε)) L')
                  (Functor.flip (tensorBifunctor L W ε))))
              X)
            Y) :
      Quiver.Hom (V := LocalizedMonoidal L W ε) (obj (obj (tensorBifunctor L W ε) (obj L' X)) (obj L' Y))
        (obj (obj (tensorBifunctor L W ε) (obj L' Y)) (obj L' X)))
    (CategoryStruct.comp (Y := obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) (LaxMonoidal.μ L' X Y)
        (Functor.map L' (Iso.hom (β_ X Y)) ≫ OplaxMonoidal.δ L' Y X) :
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' X) (obj L' Y))
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' Y) (obj L' X)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
inst_5 : BraidedCategory.{v_1, u_1} C
X Y Z : C
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (obj (obj (tensorBifunctor L W ε) (obj L' X))
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' Y) (obj L' Z)))
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z))
        (obj L' X)))
    (NatTrans.app (NatTrans.app (Iso.hom (braidingNatIso L W ε)) (obj L' X))
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' Y) (obj L' Z)) ≫
      LaxMonoidal.μ L' Y Z ▷ obj L' X)
    (obj L' X ◁ LaxMonoidal.μ L' Y Z ≫
      NatTrans.app (NatTrans.app (Iso.hom (braidingNatIso L W ε)) (obj L' X))
        (obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z)))

Tactic:
(((braidingNatIso L W ε).hom.app ((L').obj X)).naturality ((Functor.LaxMonoidal.μ (L') Y Z))).symm

Premises used: CategoryTheory.Localization.Monoidal.braidingNatIso, CategoryTheory.Localization.Monoidal.toMonoidalCategory, CategoryTheory.Functor.LaxMonoidal.μ, CategoryTheory.NatTrans.naturality, Eq.symm, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
inst_5 : BraidedCategory.{v_1, u_1} C
X Y Z : C
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (obj
        (obj (tensorBifunctor L W ε)
          (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' X) (obj L' Y)))
        (obj L' Z))
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' Z)
        (obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y))))
    (NatTrans.app
        (NatTrans.app (Iso.hom (braidingNatIso L W ε))
          (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' X) (obj L' Y)))
        (obj L' Z) ≫
      obj L' Z ◁ LaxMonoidal.μ L' X Y)
    (LaxMonoidal.μ L' X Y ▷ obj L' Z ≫
      NatTrans.app (NatTrans.app (Iso.hom (braidingNatIso L W ε)) (obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)))
        (obj L' Z))

Tactic:
(NatTrans.congr_app ((braidingNatIso L W ε).hom.naturality
    ((Functor.LaxMonoidal.μ (L') X Y))) ((L').obj Z)).symm

Premises used: CategoryTheory.Localization.Monoidal.braidingNatIso, CategoryTheory.NatTrans.congr_app, CategoryTheory.Localization.Monoidal.toMonoidalCategory, CategoryTheory.Functor.LaxMonoidal.μ, CategoryTheory.NatTrans.naturality, Eq.symm, CategoryTheory.Iso.hom, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
inst_5 : BraidedCategory.{v_1, u_1} C
X Y Z : C
a :
  LaxMonoidal.μ L' X Y ▷ obj L' Z ≫
    LaxMonoidal.μ L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z ≫ Functor.map L' (Iso.hom (β_ X Y) ▷ Z)
| CategoryStruct.comp (Y := obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) (LaxMonoidal.μ L' X Y)
        (Functor.map L' (Iso.hom (β_ X Y)) ≫ OplaxMonoidal.δ L' Y X) ▷
      obj L' Z ≫
    LaxMonoidal.μ L' Y X ▷ obj L' Z ≫ LaxMonoidal.μ L' (tensorObj.{v_1, u_1} (𝒞 := inst) Y X) Z

Tactic:
simp only [Functor.flip_obj_obj, Functor.CoreMonoidal.toMonoidal_toLaxMonoidal,
      Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, comp_whiskerRight, assoc,
      Functor.Monoidal.whiskerRight_δ_μ_assoc, Functor.LaxMonoidal.μ_natural_left]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.CoreMonoidal.toMonoidal_toLaxMonoidal, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.Functor.flip_obj_obj, CategoryTheory.Functor.LaxMonoidal.μ_natural_left, CategoryTheory.Functor.Monoidal.whiskerRight_δ_μ_assoc, CategoryTheory.Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
inst_5 : BraidedCategory.{v_1, u_1} C
X Y Z : C
a :
  obj L' X ◁ LaxMonoidal.μ L' Y Z ≫
    CategoryStruct.comp (Y := obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z)))
      (LaxMonoidal.μ L' X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z))
      (Functor.map L' (Iso.hom (β_ X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z))) ≫
        OplaxMonoidal.δ L' (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z) X)
| NatTrans.app (NatTrans.app (Iso.hom (braidingNatIso L W ε)) (obj L' X))
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' Y) (obj L' Z)) ≫
    LaxMonoidal.μ L' Y Z ▷ obj L' X

Tactic:
rw [braidingNatIso_hom_app_naturality_μ_left, braidingNatIso_hom_app]

Premises used: CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app, CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_left
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
inst_5 : BraidedCategory.{v_1, u_1} C
X Y Z : C
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' X) (obj L' Y)) (obj L' Z))
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' Y)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' Z) (obj L' X))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y))
        (obj L' Z))
      (LaxMonoidal.μ L' X Y ▷ obj L' Z)
      (LaxMonoidal.μ L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z ≫
        Functor.map L' (Iso.hom (α_ X Y Z)) ≫
          OplaxMonoidal.δ L' X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z) ≫
            obj L' X ◁ OplaxMonoidal.δ L' Y Z ≫
              CategoryStruct.comp (Y :=
                tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' Y)
                  (obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) Z X)))
                ((((obj L' X ◁ LaxMonoidal.μ L' Y Z ≫
                        CategoryStruct.comp (Y :=
                          obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z)))
                          (LaxMonoidal.μ L' X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z))
                          (Functor.map L' (Iso.hom (β_ X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z))) ≫
                            OplaxMonoidal.δ L' (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z) X)) ≫
                      LaxMonoidal.μ L' (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z) X) ≫
                    Functor.map L' (Iso.hom (α_ Y Z X))) ≫
                  OplaxMonoidal.δ L' Y (tensorObj.{v_1, u_1} (𝒞 := inst) Z X))
                (obj L' Y ◁ OplaxMonoidal.δ L' Z X)))
    (CategoryStruct.comp (Y :=
        tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' Y)
          (obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Z)))
        (((LaxMonoidal.μ L' X Y ▷ obj L' Z ≫
              LaxMonoidal.μ L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z ≫ Functor.map L' (Iso.hom (β_ X Y) ▷ Z)) ≫
            Functor.map L' (Iso.hom (α_ Y X Z))) ≫
          OplaxMonoidal.δ L' Y (tensorObj.{v_1, u_1} (𝒞 := inst) X Z))
        (obj L' Y ◁ OplaxMonoidal.δ L' X Z) ≫
      obj L' Y ◁
        CategoryStruct.comp (Y := obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) Z X))
          (LaxMonoidal.μ L' X Z ≫ Functor.map L' (Iso.hom (β_ X Z))) (OplaxMonoidal.δ L' Z X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
inst_5 : BraidedCategory.{v_1, u_1} C
X Y Z : C
a :
  CategoryStruct.comp (Y :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' X)
      (obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z)))
    (obj L' X ◁ LaxMonoidal.μ L' Y Z)
    (obj L' X ◁ Functor.map L' (Iso.hom (β_ Y Z)) ≫
      obj L' X ◁ OplaxMonoidal.δ L' Z Y ≫
        obj L' X ◁ LaxMonoidal.μ L' Z Y ≫ LaxMonoidal.μ L' X (tensorObj.{v_1, u_1} (𝒞 := inst) Z Y))
| obj L' X ◁
      CategoryStruct.comp (Y := obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z)) (LaxMonoidal.μ L' Y Z)
        (Functor.map L' (Iso.hom (β_ Y Z)) ≫ OplaxMonoidal.δ L' Z Y) ≫
    obj L' X ◁ LaxMonoidal.μ L' Z Y ≫ LaxMonoidal.μ L' X (tensorObj.{v_1, u_1} (𝒞 := inst) Z Y)

Tactic:
simp only [Functor.flip_obj_obj, Functor.CoreMonoidal.toMonoidal_toLaxMonoidal,
      Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal, MonoidalCategory.whiskerLeft_comp, assoc,
      Functor.Monoidal.whiskerLeft_δ_μ, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.Functor.CoreMonoidal.toMonoidal_toLaxMonoidal, CategoryTheory.Category.comp_id, CategoryTheory.Functor.Monoidal.whiskerLeft_δ_μ, CategoryTheory.Functor.flip_obj_obj, CategoryTheory.Functor.CoreMonoidal.toMonoidal_toOplaxMonoidal
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
inst_5 : BraidedCategory.{v_1, u_1} C
X Y Z : C
a :
  LaxMonoidal.μ L' X Y ▷ obj L' Z ≫
    CategoryStruct.comp (Y := obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z))
      (LaxMonoidal.μ L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z)
      (Functor.map L' (Iso.hom (β_ (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z)) ≫
        OplaxMonoidal.δ L' Z (tensorObj.{v_1, u_1} (𝒞 := inst) X Y))
| NatTrans.app
      (NatTrans.app (Iso.hom (braidingNatIso L W ε))
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (obj L' X) (obj L' Y)))
      (obj L' Z) ≫
    obj L' Z ◁ LaxMonoidal.μ L' X Y

Tactic:
rw [braidingNatIso_hom_app_naturality_μ_right, braidingNatIso_hom_app]

Premises used: CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app, CategoryTheory.Localization.Monoidal.braidingNatIso_hom_app_naturality_μ_right