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 Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : Functor.obj L' X' ≅ X
e₂ : Functor.obj L' Y' ≅ Y
simp :
  Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X')
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
          (Functor.obj L' Y')) ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Y)
    (e₁.hom ⊗ₘ (ε.hom ⊗ₘ e₂.hom) ≫ Iso.hom (λ_ Y))
    (e₁.hom ⊗ₘ
      (Iso.hom (ε' L W ε) ≫
            𝟙 (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)) ⊗ₘ
          e₂.hom) ≫
        Iso.hom (λ_ Y))
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X')
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
          (Functor.obj L' Y')) ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Y)
    (e₁.hom ⊗ₘ (ε.hom ⊗ₘ e₂.hom) ≫ Iso.hom (λ_ Y))
    (Functor.obj L' X' ◁
        (Iso.hom (ε' L W ε) ▷ Functor.obj L' Y' ≫
          tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε) ◁ e₂.hom ≫
            Iso.hom (λ_ Y)) ≫
      e₁.hom ▷ Y)

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

Premises used: CategoryTheory.Localization.Monoidal.id_tensorHom, CategoryTheory.Localization.Monoidal.tensorHom_id, CategoryTheory.Category.comp_id, CategoryTheory.Localization.Monoidal.tensor_comp_assoc, 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 Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : Functor.obj L' X' ≅ X
e₂ : Functor.obj L' Y' ≅ Y
e_g :
  ε.hom =
    Iso.hom (ε' L W ε) ≫ 𝟙 (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε))
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X')
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
          (Functor.obj L' Y')) ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Y)
    (e₁.hom ⊗ₘ (ε.hom ⊗ₘ e₂.hom) ≫ Iso.hom (λ_ Y))
    (e₁.hom ⊗ₘ
      (Iso.hom (ε' L W ε) ≫
            𝟙 (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)) ⊗ₘ
          e₂.hom) ≫
        Iso.hom (λ_ Y))

Tactic:
congr 3
-- 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' : C
e₁ : Functor.obj L' X' ≅ X
e₂ : Functor.obj L' Y' ≅ Y
⊢ ε.hom =
    Iso.hom (ε' L W ε) ≫ 𝟙 (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε))

Tactic:
(comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.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 ε
X' Y' : C
e₁ : Functor.obj L' X' ≅ X
e₂ : Functor.obj L' Y' ≅ Y
⊢ ε.hom =
    Iso.hom (ε' L W ε) ≫ 𝟙 (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε))

Tactic:
exact (comp_id _).symm

Premises used: CategoryTheory.Category.comp_id, Eq.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 ε
X' Y' : C
e₁ : Functor.obj L' X' ≅ X
e₂ : Functor.obj L' Y' ≅ Y
simp :
  Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X
          (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)))
        Y ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Y)
    (Iso.hom (ρ_ X) ⊗ₘ 𝟙 Y)
    ((e₁.inv ⊗ₘ ε.inv) ≫
        Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom ⊗ₘ
      𝟙 Y)
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X
          (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)))
        Y ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Y)
    (Iso.hom (ρ_ X) ▷ Y)
    (((e₁.inv ⊗ₘ ε.inv) ⊗ₘ e₂.inv) ≫
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X')
            (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ◁
          e₂.hom ≫
        (Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X'))) ▷ Y ≫
          e₁.hom ▷ Y)

Tactic:
simp only [← tensorHom_id, ← id_tensorHom, ← tensor_comp, assoc, comp_id,
    id_comp, Iso.inv_hom_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, 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 Y : LocalizedMonoidal L W ε
X' Y' : C
e₁ : Functor.obj L' X' ≅ X
e₂ : Functor.obj L' Y' ≅ Y
e_f :
  Iso.hom (ρ_ X) =
    (e₁.inv ⊗ₘ ε.inv) ≫
      Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X
          (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)))
        Y ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Y)
    (Iso.hom (ρ_ X) ⊗ₘ 𝟙 Y)
    ((e₁.inv ⊗ₘ ε.inv) ≫
        Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫ Functor.map L' (Iso.hom (ρ_ X')) ≫ e₁.hom ⊗ₘ
      𝟙 Y)

Tactic:
congr
-- 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₁ : C), Nonempty.{v_2 + 1} (Functor.obj L' X₁ ≅ X)

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

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
X Y : LocalizedMonoidal L W ε
obtain :
  ∀ (X' : C) (e₁ : Functor.obj L' X' ≅ X),
    Eq (α :=
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
          (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X
            (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)))
          Y ⟶
        tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Y)
      (Iso.hom (α_ X (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)) Y) ≫
        X ◁ Iso.hom (λ_ Y))
      (Iso.hom (ρ_ X) ▷ Y)
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X
          (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)))
        Y ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X Y)
    (Iso.hom (α_ X (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)) Y) ≫
      X ◁ Iso.hom (λ_ Y))
    (Iso.hom (ρ_ X) ▷ Y)

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

Tactic:
obtain ⟨Y', ⟨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
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : Functor.obj L' X' ≅ X
Y' : C
e₂ : Functor.obj L' Y' ≅ 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' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (Functor.obj L' Y'))
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X')
        (Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y'))))
    (Iso.hom (α_ (Functor.obj L' X') (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (Functor.obj L' Y')) ≫
      (𝟙 (Functor.obj L' X') ⊗ₘ Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y')))
    (((Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⊗ₘ 𝟙 (Functor.obj L' Y')) ≫
        Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) Y') ≫
          Functor.map L' (Iso.hom (α_ X' (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y')) ≫
            Iso.inv (μ L W ε X' (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y')) ≫
              (𝟙 (Functor.obj L' X') ⊗ₘ Iso.inv (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y'))) ≫
      (𝟙 (Functor.obj L' X') ⊗ₘ Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y')))

Tactic:
have h₁ := (associator_hom_app L W ε X' (𝟙_ _) Y' =≫
    (𝟙 ((L').obj X') ⊗ₘ (μ L W ε (𝟙_ C) Y').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 Y : LocalizedMonoidal L W ε
X' : C
e₁ : Functor.obj L' X' ≅ X
Y' : C
e₂ : Functor.obj L' Y' ≅ Y
h₁ :
  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' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (Functor.obj L' Y'))
      (Functor.obj L'
        (tensorObj.{v_1, u_1} (𝒞 := inst) X'
          (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y'))))
    (Iso.hom (α_ (Functor.obj L' X') (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (Functor.obj L' Y')) ≫
      Functor.obj L' X' ◁ Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y') ≫
        Iso.hom (μ L W ε X' (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y')))
    ((Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⊗ₘ 𝟙 (Functor.obj L' Y')) ≫
      Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) Y') ≫
        Functor.map L' (Iso.hom (α_ X' (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y')))
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (Functor.obj L' Y'))
      (Functor.obj L' Y'))
    (Iso.hom (ε' L W ε) ▷ Functor.obj L' Y' ≫ Iso.hom (λ_ (Functor.obj L' Y')))
    (Iso.hom (ε' L W ε) ▷ Functor.obj L' Y' ≫
      Iso.inv (ε' L W ε) ▷ Functor.obj L' Y' ≫
        Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y') ≫ Functor.map L' (Iso.hom (λ_ Y')))

Tactic:
have h₂ := (ε' L W ε).hom ▷ (L').obj Y' ≫= leftUnitor_hom_app L W ε 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
X Y : LocalizedMonoidal L W ε
X' : C
e₁ : Functor.obj L' X' ≅ X
Y' : C
e₂ : Functor.obj L' Y' ≅ Y
h₁ :
  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' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (Functor.obj L' Y'))
      (Functor.obj L'
        (tensorObj.{v_1, u_1} (𝒞 := inst) X'
          (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y'))))
    (Iso.hom (α_ (Functor.obj L' X') (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (Functor.obj L' Y')) ≫
      Functor.obj L' X' ◁ Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y') ≫
        Iso.hom (μ L W ε X' (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y')))
    ((Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⊗ₘ 𝟙 (Functor.obj L' Y')) ≫
      Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) Y') ≫
        Functor.map L' (Iso.hom (α_ X' (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y')))
h₂ :
  Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (Functor.obj L' Y'))
      (Functor.obj L' Y'))
    (Iso.hom (ε' L W ε) ▷ Functor.obj L' Y' ≫ Iso.hom (λ_ (Functor.obj L' Y')))
    (Iso.hom (ε' L W ε) ▷ Functor.obj L' Y' ≫
      Iso.inv (ε' L W ε) ▷ Functor.obj L' Y' ≫
        Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y') ≫ Functor.map L' (Iso.hom (λ_ Y')))
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (Functor.obj L' Y'))
      (Functor.obj L' Y'))
    (Iso.hom (ε' L W ε) ▷ Functor.obj L' Y' ≫ Iso.hom (λ_ (Functor.obj L' Y')))
    (Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y') ≫ Functor.map L' (Iso.hom (λ_ Y')))

Tactic:
simp only [← whiskerRight_comp_assoc, Iso.hom_inv_id, whiskerRight_id, id_comp] at h₂

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Localization.Monoidal.whiskerRight_id, CategoryTheory.Localization.Monoidal.whiskerRight_comp_assoc, 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 Y : LocalizedMonoidal L W ε
X' : C
e₁ : Functor.obj L' X' ≅ X
Y' : C
e₂ : Functor.obj L' Y' ≅ Y
h₁ :
  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' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (Functor.obj L' Y'))
      (Functor.obj L'
        (tensorObj.{v_1, u_1} (𝒞 := inst) X'
          (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y'))))
    (Iso.hom (α_ (Functor.obj L' X') (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (Functor.obj L' Y')) ≫
      Functor.obj L' X' ◁ Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y') ≫
        Iso.hom (μ L W ε X' (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y')))
    ((Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⊗ₘ 𝟙 (Functor.obj L' Y')) ≫
      Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) Y') ≫
        Functor.map L' (Iso.hom (α_ X' (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y')))
h₂ :
  Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (Functor.obj L' Y'))
      (Functor.obj L' Y'))
    (Iso.hom (ε' L W ε) ▷ Functor.obj L' Y' ≫ Iso.hom (λ_ (Functor.obj L' Y')))
    (Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y') ≫ Functor.map L' (Iso.hom (λ_ 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' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (Functor.obj L' Y'))
      (Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X' Y')))
    (((Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⊗ₘ 𝟙 (Functor.obj L' Y')) ≫
        Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) Y')) ≫
      Functor.map L' (Iso.hom (α_ X' (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y') ≫ X' ◁ Iso.hom (λ_ Y')))
    (((Iso.hom (μ L W ε X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ⊗ₘ 𝟙 (Functor.obj L' Y')) ≫
        Iso.hom (μ L W ε (tensorObj.{v_1, u_1} (𝒞 := inst) X' (tensorUnit.{v_1, u_1} C (𝒞 := inst))) Y')) ≫
      Functor.map L' (Iso.hom (ρ_ X') ▷ Y'))

Tactic:
have h₃ := (((μ L W ε _ _).hom ⊗ₘ 𝟙 _) ≫ (μ L W ε _ _).hom) ≫=
    ((L').congr_map (MonoidalCategory.triangle X' 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
X₁ Y₁ X₂ Y₂ : LocalizedMonoidal L W ε
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) X₁ X₂ ⟶
      tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) Y₁ Y₂)
    (f ⊗ₘ g) (f ▷ X₂ ≫ Y₁ ◁ 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₁ 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₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)

Tactic:
simp +instances [monoidalCategoryStruct]

Premises used: CategoryTheory.Localization.Monoidal.monoidalCategoryStruct