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 : C
rw :
  Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) ε.inv ≫
      CategoryStruct.comp (Y := Functor.obj (tensorRight (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L') X)
        (NatTrans.app
          (Iso.hom
            (Lifting.iso L' W (tensorRight (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
              (Functor.obj (Functor.flip (tensorBifunctor L W ε))
                (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
          X)
        (NatTrans.app (Functor.whiskerRight (Iso.hom (rightUnitorNatIso C)) L' ≫ L.leftUnitor.hom) X ≫
          NatTrans.app (Iso.inv (Lifting.iso L' W L' (𝟭 (LocalizedMonoidal L W ε)))) X) =
    Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) (Iso.inv (ε' L W ε)) ≫
      Iso.hom (μ L W ε X (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X))
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (Functor.obj (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) unit) (Functor.obj L' X))
    (Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) ε.inv ≫
        NatTrans.app
          (liftNatTrans L' W (tensorRight (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L') L'
            (Functor.obj (Functor.flip (tensorBifunctor L W ε)) (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
            (𝟭 (LocalizedMonoidal L W ε)) (Functor.whiskerRight (Iso.hom (rightUnitorNatIso C)) L' ≫ L.leftUnitor.hom))
          (Functor.obj L' X) :
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (Functor.obj (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) unit) (Functor.obj L' X))
    (Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) (Iso.inv (ε' L W ε)) ≫
        Iso.hom (μ L W ε X (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X)) :
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (Functor.obj (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) unit) (Functor.obj L' X))

Tactic:
rw [liftNatTrans_app]

Premises used: CategoryTheory.Localization.liftNatTrans_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 : C
dsimp :
  Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) ε.inv ≫
      CategoryStruct.comp (Y :=
        Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (NatTrans.app
          (Iso.hom
            (Lifting.iso L' W (tensorRight (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
              (Functor.obj (Functor.flip (tensorBifunctor L W ε))
                (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
          X)
        ((Functor.map L' (Iso.hom (ρ_ X)) ≫ 𝟙 (L.obj X)) ≫ 𝟙 (Functor.obj L' X)) =
    Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) (Iso.inv (ε' L W ε)) ≫
      Iso.hom (μ L W ε X (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X))
⊢ Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) ε.inv ≫
      CategoryStruct.comp (Y := Functor.obj (tensorRight (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L') X)
        (NatTrans.app
          (Iso.hom
            (Lifting.iso L' W (tensorRight (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
              (Functor.obj (Functor.flip (tensorBifunctor L W ε))
                (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
          X)
        (NatTrans.app (Functor.whiskerRight (Iso.hom (rightUnitorNatIso C)) L' ≫ L.leftUnitor.hom) X ≫
          NatTrans.app (Iso.inv (Lifting.iso L' W L' (𝟭 (LocalizedMonoidal L W ε)))) X) =
    Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) (Iso.inv (ε' L W ε)) ≫
      Iso.hom (μ L W ε X (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X))

Tactic:
dsimp
-- 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 : C
rw :
  Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) ε.inv ≫
      CategoryStruct.comp (Y :=
        Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (NatTrans.app
          (Iso.hom
            (Lifting.iso L' W (tensorRight (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
              (Functor.obj (Functor.flip (tensorBifunctor L W ε))
                (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
          X)
        (Functor.map L' (Iso.hom (ρ_ X)) ≫ 𝟙 (L.obj X) ≫ 𝟙 (Functor.obj L' X)) =
    Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) (Iso.inv (ε' L W ε)) ≫
      Iso.hom (μ L W ε X (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X))
⊢ Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) ε.inv ≫
      CategoryStruct.comp (Y :=
        Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (NatTrans.app
          (Iso.hom
            (Lifting.iso L' W (tensorRight (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
              (Functor.obj (Functor.flip (tensorBifunctor L W ε))
                (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
          X)
        ((Functor.map L' (Iso.hom (ρ_ X)) ≫ 𝟙 (L.obj X)) ≫ 𝟙 (Functor.obj L' X)) =
    Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) (Iso.inv (ε' L W ε)) ≫
      Iso.hom (μ L W ε X (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X))

Tactic:
rw [assoc]

Premises used: CategoryTheory.Category.assoc
-- 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 : C
change :
  Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) ε.inv ≫
      Iso.hom (μ L W ε X (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
        Functor.map L' (Iso.hom (ρ_ X)) ≫ 𝟙 (Functor.obj L' X) ≫ 𝟙 (Functor.obj L' X) =
    Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) (Iso.inv (ε' L W ε)) ≫
      Iso.hom (μ L W ε X (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X))
⊢ Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) ε.inv ≫
      CategoryStruct.comp (Y :=
        Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (NatTrans.app
          (Iso.hom
            (Lifting.iso L' W (tensorRight (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
              (Functor.obj (Functor.flip (tensorBifunctor L W ε))
                (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
          X)
        (Functor.map L' (Iso.hom (ρ_ X)) ≫ 𝟙 (L.obj X) ≫ 𝟙 (Functor.obj L' X)) =
    Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) (Iso.inv (ε' L W ε)) ≫
      Iso.hom (μ L W ε X (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X))

Tactic:
change _ ≫ (μ L W ε _ _).hom ≫ _ ≫ 𝟙 _ ≫ 𝟙 _ = _

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Localization.Monoidal.μ, CategoryTheory.Iso.hom
-- 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 : C
⊢ Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) ε.inv ≫
      Iso.hom (μ L W ε X (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
        Functor.map L' (Iso.hom (ρ_ X)) ≫ 𝟙 (Functor.obj L' X) ≫ 𝟙 (Functor.obj L' X) =
    Functor.map (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X)) (Iso.inv (ε' L W ε)) ≫
      Iso.hom (μ L W ε X (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X))

Tactic:
simp only [comp_id]

Premises used: CategoryTheory.Category.comp_id
-- 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₁ Y₂ : LocalizedMonoidal L W ε
f : Y₁ ⟶ Y₂
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Y₁ ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Y₂)
    (𝟙 X ⊗ₘ f) (X ◁ f)

Tactic:
simp +instances [monoidalCategoryStruct]

Premises used: CategoryTheory.Localization.Monoidal.monoidalCategoryStruct
-- 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₂ : LocalizedMonoidal L W ε
f : X₁ ⟶ X₂
Y : LocalizedMonoidal L W ε
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X₁ Y ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X₂ Y)
    (f ⊗ₘ 𝟙 Y) (f ▷ Y)

Tactic:
simp +instances [monoidalCategoryStruct]

Premises used: CategoryTheory.Localization.Monoidal.monoidalCategoryStruct
-- 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₁ X₂ Y₂ Z₂ : LocalizedMonoidal L W ε
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X₁ X₂ ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Z₁ Z₂)
    (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂) ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))

Tactic:
simp +instances [monoidalCategoryStruct]

Premises used: CategoryTheory.Localization.Monoidal.monoidalCategoryStruct
-- 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₂ : LocalizedMonoidal L W ε
⊢ 𝟙 X₁ ⊗ₘ 𝟙 X₂ = 𝟙 (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X₁ X₂)

Tactic:
simp +instances [monoidalCategoryStruct]

Premises used: CategoryTheory.Localization.Monoidal.monoidalCategoryStruct
-- 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
Q X Y Z : LocalizedMonoidal L W ε
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Q X ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Q Z)
    (Q ◁ (f ≫ g)) (Q ◁ f ≫ Q ◁ g)

Tactic:
simp only [← id_tensorHom, ← tensor_comp, comp_id]

Premises used: CategoryTheory.Localization.Monoidal.id_tensorHom, CategoryTheory.Category.comp_id, CategoryTheory.Localization.Monoidal.tensor_comp
-- 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
Q X Y Z : LocalizedMonoidal L W ε
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Q ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Z Q)
    ((f ≫ g) ▷ Q) (f ▷ Q ≫ g ▷ Q)

Tactic:
simp only [← tensorHom_id, ← tensor_comp, comp_id]

Premises used: CategoryTheory.Localization.Monoidal.tensorHom_id, CategoryTheory.Category.comp_id, CategoryTheory.Localization.Monoidal.tensor_comp
-- 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 : LocalizedMonoidal L W ε
⊢ X ◁ 𝟙 Y = 𝟙 (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Y)

Tactic:
simp +instances [monoidalCategoryStruct]

Premises used: CategoryTheory.Localization.Monoidal.monoidalCategoryStruct
-- 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 : LocalizedMonoidal L W ε
⊢ 𝟙 X ▷ Y = 𝟙 (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Y)

Tactic:
simp +instances [monoidalCategoryStruct]

Premises used: CategoryTheory.Localization.Monoidal.monoidalCategoryStruct
-- 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
Q X Y Z : LocalizedMonoidal L W ε
f : Q ⟶ X
g : Y ⟶ Z
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Q Y ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Z)
    (Q ◁ g ≫ f ▷ Z) (f ▷ Y ≫ X ◁ g)

Tactic:
simp only [← id_tensorHom, ← tensorHom_id, ← tensor_comp, id_comp, comp_id]

Premises used: CategoryTheory.Localization.Monoidal.id_tensorHom, CategoryTheory.Localization.Monoidal.tensorHom_id, CategoryTheory.Category.comp_id, CategoryTheory.Localization.Monoidal.tensor_comp, CategoryTheory.Category.id_comp
-- 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₃
⊢ ((Functor.obj (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).obj Y₂).map f₃ ≫
      ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app Y₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app X₃ ≫
      ((Functor.obj (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).obj Y₂).map f₃

Tactic:
have h₁ := (((associator L W ε).hom.app Y₁).app Y₂).naturality f₃
-- 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₃
h₁ :
  ((Functor.obj (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).obj Y₂).map f₃ ≫
      ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app Y₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app X₃ ≫
      ((Functor.obj (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).obj Y₂).map f₃
⊢ ((Functor.obj (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).map f₂ ≫
          (NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app
      X₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app X₂ ≫
          (Functor.obj (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).map f₂).app
      X₃

Tactic:
have h₂ := NatTrans.congr_app (((associator L W ε).hom.app Y₁).naturality f₂) X₃
-- 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₃
h₁ :
  ((Functor.obj (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).obj Y₂).map f₃ ≫
      ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app Y₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app X₃ ≫
      ((Functor.obj (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).obj Y₂).map f₃
h₂ :
  ((Functor.obj (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).map f₂ ≫
          (NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app
      X₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app X₂ ≫
          (Functor.obj (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).map f₂).app
      X₃
⊢ ((Functor.map (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) f₁ ≫
              NatTrans.app (Iso.hom (associator L W ε)) Y₁).app
          X₂).app
      X₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) X₁ ≫
              Functor.map (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) f₁).app
          X₂).app
      X₃

Tactic:
have h₃ := NatTrans.congr_app (NatTrans.congr_app ((associator L W ε).hom.naturality f₁) X₂) X₃
-- 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₃
h₁ :
  ((Functor.obj (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).obj Y₂).map f₃ ≫
      ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app Y₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app X₃ ≫
      ((Functor.obj (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).obj Y₂).map f₃
h₂ :
  ((Functor.obj (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).map f₂ ≫
          (NatTrans.app (Iso.hom (associator L W ε)) Y₁).app Y₂).app
      X₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) Y₁).app X₂ ≫
          (Functor.obj (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) Y₁).map f₂).app
      X₃
h₃ :
  ((Functor.map (bifunctorComp₁₂ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) f₁ ≫
              NatTrans.app (Iso.hom (associator L W ε)) Y₁).app
          X₂).app
      X₃ =
    ((NatTrans.app (Iso.hom (associator L W ε)) X₁ ≫
              Functor.map (bifunctorComp₂₃ (tensorBifunctor L W ε) (tensorBifunctor L W ε)) f₁).app
          X₂).app
      X₃
simp :
  NatTrans.app
        (Functor.map (tensorBifunctor L W ε) (NatTrans.app (Functor.map (tensorBifunctor L W ε) f₁) X₂) ≫
          Functor.map (tensorBifunctor L W ε) ((Functor.obj (tensorBifunctor L W ε) Y₁).map f₂))
        X₃ ≫
      (Functor.obj (tensorBifunctor L W ε) ((Functor.obj (tensorBifunctor L W ε) Y₁).obj Y₂)).map f₃ ≫
        (((Iso.app (associator L W ε) Y₁).app Y₂).app Y₃).hom =
    (((Iso.app (associator L W ε) X₁).app X₂).app X₃).hom ≫
      NatTrans.app (Functor.map (tensorBifunctor L W ε) f₁) ((Functor.obj (tensorBifunctor L W ε) X₂).obj X₃) ≫
        (Functor.obj (tensorBifunctor L W ε) Y₁).map (NatTrans.app (Functor.map (tensorBifunctor L W ε) f₂) X₃) ≫
          (Functor.obj (tensorBifunctor L W ε) Y₁).map ((Functor.obj (tensorBifunctor L W ε) Y₂).map f₃)
⊢ 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:
simp +instances only [monoidalCategoryStruct, Functor.map_comp, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Localization.Monoidal.monoidalCategoryStruct