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

Tactic:
dsimp at h₁ h₂ h₃ ⊢
-- 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₁ : LocalizedMonoidal L W ε
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 ε) X₂ X₃))
    (f₁ ▷ X₂ ▷ X₃ ≫ Iso.hom (α_ Y₁ X₂ X₃))
    (Iso.hom (α_ X₁ X₂ X₃) ≫ f₁ ▷ tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X₂ X₃)

Tactic:
simp only [← tensorHom_id, associator_naturality, id_tensorHom_id]

Premises used: CategoryTheory.Localization.Monoidal.tensorHom_id, CategoryTheory.Localization.Monoidal.associator_naturality, CategoryTheory.Localization.Monoidal.id_tensorHom_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₁ X₂ X₃ Y₂ : LocalizedMonoidal L W ε
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 ε) X₁
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₂ X₃))
    ((X₁ ◁ f₂) ▷ X₃ ≫ Iso.hom (α_ X₁ Y₂ X₃)) (Iso.hom (α_ X₁ X₂ X₃) ≫ X₁ ◁ f₂ ▷ X₃)

Tactic:
simp only [← tensorHom_id, ← id_tensorHom, associator_naturality]

Premises used: CategoryTheory.Localization.Monoidal.id_tensorHom, CategoryTheory.Localization.Monoidal.tensorHom_id, 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₁ X₂ X₃ Y₃ : LocalizedMonoidal L W ε
f₃ : X₃ ⟶ Y₃
⊢ tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X₁ X₂ ◁ f₃ ≫ Iso.hom (α_ X₁ X₂ Y₃) =
    Iso.hom (α_ X₁ X₂ X₃) ≫ X₁ ◁ X₂ ◁ f₃

Tactic:
simp only [← id_tensorHom, ← id_tensorHom_id, associator_naturality]

Premises used: CategoryTheory.Localization.Monoidal.id_tensorHom, CategoryTheory.Localization.Monoidal.associator_naturality, CategoryTheory.Localization.Monoidal.id_tensorHom_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₁ X₂ X₃ Y₁ : LocalizedMonoidal L W ε
i : 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 ε) X₁
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X₂ X₃))
    (i.hom ▷ X₂ ▷ X₃ ≫
      Iso.hom (α_ Y₁ X₂ X₃) ≫ i.inv ▷ tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X₂ X₃)
    (Iso.hom (α_ X₁ X₂ X₃))

Tactic:
simp only [associator_naturality₁_assoc, ← whiskerRight_comp,
    Iso.hom_inv_id, whiskerRight_id, comp_id]

Premises used: CategoryTheory.Localization.Monoidal.whiskerRight_comp, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Localization.Monoidal.whiskerRight_id, CategoryTheory.Localization.Monoidal.associator_naturality₁_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₁ X₂ X₃ Y₂ : LocalizedMonoidal L W ε
i : 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 ε) X₁
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X₂ X₃))
    ((X₁ ◁ i.hom) ▷ X₃ ≫ Iso.hom (α_ X₁ Y₂ X₃) ≫ X₁ ◁ i.inv ▷ X₃) (Iso.hom (α_ X₁ X₂ X₃))

Tactic:
simp only [associator_naturality₂_assoc, ← whiskerLeft_comp, ← whiskerRight_comp,
    Iso.hom_inv_id, whiskerRight_id, whiskerLeft_id, comp_id]

Premises used: CategoryTheory.Localization.Monoidal.whiskerLeft_comp, CategoryTheory.Localization.Monoidal.whiskerRight_comp, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Localization.Monoidal.whiskerRight_id, CategoryTheory.Localization.Monoidal.associator_naturality₂_assoc, CategoryTheory.Localization.Monoidal.whiskerLeft_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₁ X₂ X₃ Y₃ : LocalizedMonoidal L W ε
i : X₃ ≅ Y₃
⊢ tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X₁ X₂ ◁ i.hom ≫
      Iso.hom (α_ X₁ X₂ Y₃) ≫ X₁ ◁ X₂ ◁ i.inv =
    Iso.hom (α_ X₁ X₂ X₃)

Tactic:
simp only [associator_naturality₃_assoc, ← whiskerLeft_comp,
    Iso.hom_inv_id, whiskerLeft_id, comp_id]

Premises used: CategoryTheory.Localization.Monoidal.whiskerLeft_comp, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Localization.Monoidal.whiskerLeft_id, CategoryTheory.Localization.Monoidal.associator_naturality₃_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
⊢ Functor.EssSurj (D := LocalizedMonoidal L W ε) L'

Tactic:
Localization.essSurj L' W

Premises used: CategoryTheory.Localization.essSurj, CategoryTheory.Localization.Monoidal.toMonoidalCategory
-- 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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
⊢ ∃ (X₁ : C), Nonempty.{v_2 + 1} (Functor.obj L' X₁ ≅ Y₁)

Tactic:
⟨_, ⟨(L').objObjPreimageIso Y₁⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Localization.Monoidal.toMonoidalCategory, CategoryTheory.Functor.objObjPreimageIso, Exists.intro
-- 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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
obtain : ∀ (X₁ : C) (e₁ : Functor.obj L' X₁ ≅ Y₁), Pentagon.{v_2, u_2} Y₁ Y₂ Y₃ Y₄
⊢ Pentagon.{v_2, u_2} Y₁ Y₂ Y₃ Y₄

Tactic:
obtain ⟨X₁, ⟨e₁⟩⟩ : ∃ X₁, Nonempty ((L').obj X₁ ≅ Y₁) := ⟨_, ⟨(L').objObjPreimageIso Y₁⟩⟩
-- 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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : Functor.obj L' X₁ ≅ Y₁
⊢ ∃ (X₂ : C), Nonempty.{v_2 + 1} (Functor.obj L' X₂ ≅ Y₂)

Tactic:
⟨_, ⟨(L').objObjPreimageIso Y₂⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Localization.Monoidal.toMonoidalCategory, CategoryTheory.Functor.objObjPreimageIso, Exists.intro
-- 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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : Functor.obj L' X₁ ≅ Y₁
obtain : ∀ (X₂ : C) (e₂ : Functor.obj L' X₂ ≅ Y₂), Pentagon.{v_2, u_2} Y₁ Y₂ Y₃ Y₄
⊢ Pentagon.{v_2, u_2} Y₁ Y₂ Y₃ Y₄

Tactic:
obtain ⟨X₂, ⟨e₂⟩⟩ : ∃ X₂, Nonempty ((L').obj X₂ ≅ Y₂) := ⟨_, ⟨(L').objObjPreimageIso Y₂⟩⟩
-- 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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : Functor.obj L' X₁ ≅ Y₁
X₂ : C
e₂ : Functor.obj L' X₂ ≅ Y₂
⊢ ∃ (X₃ : C), Nonempty.{v_2 + 1} (Functor.obj L' X₃ ≅ Y₃)

Tactic:
⟨_, ⟨(L').objObjPreimageIso Y₃⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Localization.Monoidal.toMonoidalCategory, CategoryTheory.Functor.objObjPreimageIso, Exists.intro
-- 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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : Functor.obj L' X₁ ≅ Y₁
X₂ : C
e₂ : Functor.obj L' X₂ ≅ Y₂
obtain : ∀ (X₃ : C) (e₃ : Functor.obj L' X₃ ≅ Y₃), Pentagon.{v_2, u_2} Y₁ Y₂ Y₃ Y₄
⊢ Pentagon.{v_2, u_2} Y₁ Y₂ Y₃ Y₄

Tactic:
obtain ⟨X₃, ⟨e₃⟩⟩ : ∃ X₃, Nonempty ((L').obj X₃ ≅ Y₃) := ⟨_, ⟨(L').objObjPreimageIso Y₃⟩⟩
-- 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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : Functor.obj L' X₁ ≅ Y₁
X₂ : C
e₂ : Functor.obj L' X₂ ≅ Y₂
X₃ : C
e₃ : Functor.obj L' X₃ ≅ Y₃
⊢ ∃ (X₄ : C), Nonempty.{v_2 + 1} (Functor.obj L' X₄ ≅ Y₄)

Tactic:
⟨_, ⟨(L').objObjPreimageIso Y₄⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Localization.Monoidal.toMonoidalCategory, CategoryTheory.Functor.objObjPreimageIso, Exists.intro
-- 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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : Functor.obj L' X₁ ≅ Y₁
X₂ : C
e₂ : Functor.obj L' X₂ ≅ Y₂
X₃ : C
e₃ : Functor.obj L' X₃ ≅ Y₃
obtain : ∀ (X₄ : C) (e₄ : Functor.obj L' X₄ ≅ Y₄), Pentagon.{v_2, u_2} Y₁ Y₂ Y₃ Y₄
⊢ Pentagon.{v_2, u_2} Y₁ Y₂ Y₃ Y₄

Tactic:
obtain ⟨X₄, ⟨e₄⟩⟩ : ∃ X₄, Nonempty ((L').obj X₄ ≅ Y₄) := ⟨_, ⟨(L').objObjPreimageIso Y₄⟩⟩
-- 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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : Functor.obj L' X₁ ≅ Y₁
X₂ : C
e₂ : Functor.obj L' X₂ ≅ Y₂
X₃ : C
e₃ : Functor.obj L' X₃ ≅ Y₃
X₄ : C
e₄ : Functor.obj L' X₄ ≅ Y₄
this :
  Pentagon.{v_2, u_2} (C := LocalizedMonoidal L W ε) (Functor.obj L' X₁) (Functor.obj L' X₂) (Functor.obj L' X₃)
    (Functor.obj L' X₄)
⊢ Iso.hom (α_ Y₁ Y₂ Y₃) ▷ Y₄ ≫
      Iso.hom (α_ Y₁ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₂ Y₃) Y₄) ≫
        Y₁ ◁ Iso.hom (α_ Y₂ Y₃ Y₄) =
    Iso.hom (α_ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂) Y₃ Y₄) ≫
      Iso.hom (α_ Y₁ Y₂ (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₃ Y₄))

Tactic:
Eq.trans ?_ (((((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫= this =≫
      (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom)).trans ?_)

Premises used: CategoryTheory.eq_whisker, CategoryTheory.MonoidalCategoryStruct.tensorHom, CategoryTheory.whisker_eq, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, Eq.trans
-- 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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : Functor.obj L' X₁ ≅ Y₁
X₂ : C
e₂ : Functor.obj L' X₂ ≅ Y₂
X₃ : C
e₃ : Functor.obj L' X₃ ≅ Y₃
X₄ : C
e₄ : Functor.obj L' X₄ ≅ Y₄
suffices :
  Pentagon.{v_2, u_2} (C := LocalizedMonoidal L W ε) (Functor.obj L' X₁) (Functor.obj L' X₂) (Functor.obj L' X₃)
    (Functor.obj L' X₄)
⊢ Pentagon.{v_2, u_2} Y₁ Y₂ Y₃ Y₄

Tactic:
suffices Pentagon ((L').obj X₁) ((L').obj X₂) ((L').obj X₃) ((L').obj X₄) by
    dsimp [Pentagon]
    refine Eq.trans ?_ (((((e₁.inv ⊗ₘ e₂.inv) ⊗ₘ e₃.inv) ⊗ₘ e₄.inv) ≫= this =≫
      (e₁.hom ⊗ₘ e₂.hom ⊗ₘ e₃.hom ⊗ₘ e₄.hom)).trans ?_)
    · rw [← id_tensorHom, ← id_tensorHom, ← tensorHom_id, ← tensorHom_id, assoc, assoc,
        ← tensor_comp, ← associator_naturality, id_comp, ← comp_id e₁.hom,
        tensor_comp, ← associator_naturality_assoc, ← comp_id (𝟙 ((L').obj X₄)),
        ← tensor_comp_assoc, associator_naturality, comp_id, comp_id,
        ← tensor_comp_assoc, assoc, e₄.inv_hom_id, ← tensor_comp, e₁.inv_hom_id,
        ← tensor_comp, e₂.inv_hom_id, e₃.inv_hom_id, id_tensorHom_id, id_tensorHom_id, comp_id]
    · rw [assoc, associator_naturality_assoc, associator_naturality_assoc,
        ← tensor_comp, e₁.inv_hom_id, ← tensor_comp, e₂.inv_hom_id, ← tensor_comp,
        e₃.inv_hom_id, e₄.inv_hom_id, id_tensorHom_id, id_tensorHom_id, id_tensorHom_id, 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
Y₁ Y₂ Y₃ Y₄ : LocalizedMonoidal L W ε
X₁ : C
e₁ : Functor.obj L' X₁ ≅ Y₁
X₂ : C
e₂ : Functor.obj L' X₂ ≅ Y₂
X₃ : C
e₃ : Functor.obj L' X₃ ≅ Y₃
X₄ : C
e₄ : Functor.obj L' X₄ ≅ Y₄
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₁)
          (Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃)))
        (Functor.obj L' X₄))
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₁)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
          (Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃)) (Functor.obj L' X₄))))
    ((Functor.obj L' X₁ ◁ Iso.inv (μ L W ε X₂ X₃)) ▷ Functor.obj L' X₄ ≫
      Iso.hom
          (α_ (Functor.obj L' X₁)
            (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₂) (Functor.obj L' X₃))
            (Functor.obj L' X₄)) ≫
        Functor.obj L' X₁ ◁ Iso.hom (μ L W ε X₂ X₃) ▷ Functor.obj L' X₄)
    (Iso.hom (α_ (Functor.obj L' X₁) (Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃)) (Functor.obj L' X₄)))

Tactic:
have : ((L').obj X₁ ◁ (μ L W ε X₂ X₃).inv) ▷ (L').obj X₄ ≫
      (α_ ((L').obj X₁) ((L').obj X₂ ⊗ (L').obj X₃) ((L').obj X₄)).hom ≫
        (L').obj X₁ ◁ (μ L W ε X₂ X₃).hom ▷ (L').obj X₄ =
          (α_ ((L').obj X₁) ((L').obj (X₂ ⊗ X₃)) ((L').obj X₄)).hom :=
    pentagon_aux₂ _ _ _ (μ L W ε X₂ X₃).symm
-- 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 ε
f : X ⟶ Y
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)) X ⟶
      Y)
    (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε) ◁ f ≫ Iso.hom (λ_ Y))
    (Iso.hom (λ_ 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 Y : LocalizedMonoidal L W ε
f : X ⟶ Y
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X
        (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)) ⟶
      Y)
    (f ▷ tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε) ≫ Iso.hom (ρ_ Y))
    (Iso.hom (ρ_ X) ≫ f)

Tactic:
(rightUnitor L W ε).hom.naturality f

Premises used: CategoryTheory.Localization.Monoidal.rightUnitor, CategoryTheory.NatTrans.naturality, 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₁ X₂ X₃ Y₁ Y₂ Y₃ : LocalizedMonoidal L W ε
i₁ : X₁ ≅ Y₁
i₂ : X₂ ≅ Y₂
i₃ : 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 ε) X₁
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X₂ X₃))
    (((i₁.hom ⊗ₘ i₂.hom) ⊗ₘ i₃.hom) ≫ Iso.hom (α_ Y₁ Y₂ Y₃) ≫ (i₁.inv ⊗ₘ i₂.inv ⊗ₘ i₃.inv)) (Iso.hom (α_ X₁ X₂ X₃))

Tactic:
simp only [associator_naturality_assoc, ← tensor_comp, Iso.hom_inv_id, id_tensorHom,
    whiskerLeft_id, comp_id]

Premises used: CategoryTheory.Localization.Monoidal.id_tensorHom, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Localization.Monoidal.associator_naturality_assoc, CategoryTheory.Localization.Monoidal.whiskerLeft_id, CategoryTheory.Localization.Monoidal.tensor_comp