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₁ X₂ Y₂ : C
f₁ : (X₁, Y₁).1 ⟶ (X₂, Y₂).1
f₂ : (X₁, Y₁).2 ⟶ (X₂, Y₂).2
hf₁ : W (f₁, f₂).1
hf₂ : W (f₁, f₂).2
this_1 :
  IsIso (C := LocalizedMonoidal L W ε) (X := Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) (X₁, Y₁).1 Y₁))
    (Functor.map L' (f₁ ▷ Y₁))
this :
  IsIso (C := LocalizedMonoidal L W ε) (X := Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ (X₁, Y₁).2))
    (Functor.map L' (X₂ ◁ f₂))
dsimp :
  IsIso (C := D) (X :=
    (Functor.obj (L' : Functor.{v_1, v_2, u_1, u_2} C (LocalizedMonoidal L W ε))
        (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₁) :
      D))
    (Functor.map L' (f₁ ▷ Y₁) ≫ Functor.map L' (X₂ ◁ f₂))
⊢ IsIso (X :=
    Functor.obj
      (Functor.obj Functor.uncurry (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) L') :
        Functor.{v_1, v_2, u_1, u_2} (C × C) D)
      (X₁, Y₁))
    (Y :=
    Functor.obj
      (Functor.obj Functor.uncurry (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) L') :
        Functor.{v_1, v_2, u_1, u_2} (C × C) D)
      (X₂, Y₂))
    (Functor.map (Functor.obj Functor.uncurry (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) L'))
        (f₁, f₂) :
      Functor.obj
          (Functor.obj Functor.uncurry (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) L') :
            Functor.{v_1, v_2, u_1, u_2} (C × C) D)
          (X₁, Y₁) ⟶
        Functor.obj
          (Functor.obj Functor.uncurry (curriedTensor C ⋙ Functor.obj (Functor.whiskeringRight C C D) L') :
            Functor.{v_1, v_2, u_1, u_2} (C × C) D)
          (X₂, Y₂))

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₁ Y₁ X₂ Y₂ : C
f₁ : (X₁, Y₁).1 ⟶ (X₂, Y₂).1
f₂ : (X₁, Y₁).2 ⟶ (X₂, Y₂).2
hf₁ : W (f₁, f₂).1
hf₂ : W (f₁, f₂).2
this_1 :
  IsIso (C := LocalizedMonoidal L W ε) (X := Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) (X₁, Y₁).1 Y₁))
    (Functor.map L' (f₁ ▷ Y₁))
this :
  IsIso (C := LocalizedMonoidal L W ε) (X := Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ (X₁, Y₁).2))
    (Functor.map L' (X₂ ◁ f₂))
⊢ IsIso (C := D) (X :=
    (Functor.obj (L' : Functor.{v_1, v_2, u_1, u_2} C (LocalizedMonoidal L W ε))
        (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₁) :
      D))
    (Functor.map L' (f₁ ▷ Y₁) ≫ Functor.map L' (X₂ ◁ f₂))

Tactic:
infer_instance
-- 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
⊢ Lifting (D := LocalizedMonoidal L W ε) L' W (tensorLeft X ⋙ L')
    (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' X))

Tactic:
apply Lifting₂.liftingLift₂ (hF := isInvertedBy₂ L W ε)

Premises used: CategoryTheory.Localization.Monoidal.isInvertedBy₂, CategoryTheory.Localization.Lifting₂.liftingLift₂
-- 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 : C
⊢ Lifting (D := LocalizedMonoidal L W ε) L' W (tensorRight Y ⋙ L')
    (Functor.obj (Functor.flip (tensorBifunctor L W ε)) (Functor.obj L' Y))

Tactic:
apply Lifting₂.liftingLift₂Flip (hF := isInvertedBy₂ L W ε)

Premises used: CategoryTheory.Localization.Lifting₂.liftingLift₂Flip, CategoryTheory.Localization.Monoidal.isInvertedBy₂
-- 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₂ : C
f : X₁ ⟶ X₂
Y : C
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₁) (Functor.obj L' Y))
      (Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ Y)))
    (Functor.map L' f ▷ Functor.obj L' Y ≫ Iso.hom (μ L W ε X₂ Y)) (Iso.hom (μ L W ε X₁ Y) ≫ Functor.map L' (f ▷ Y))

Tactic:
NatTrans.naturality_app (tensorBifunctorIso L W ε).hom Y f

Premises used: CategoryTheory.NatTrans.naturality_app, CategoryTheory.Localization.Monoidal.tensorBifunctorIso, 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₂ : C
f : X₁ ⟶ X₂
Y : C
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε) (Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y))
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X₂) (Functor.obj L' Y)))
    (Iso.inv (μ L W ε X₁ Y) ≫ Functor.map L' f ▷ Functor.obj L' Y) (Functor.map L' (f ▷ Y) ≫ Iso.inv (μ L W ε X₂ Y))

Tactic:
simp [Iso.eq_comp_inv]

Premises used: CategoryTheory.Iso.eq_comp_inv
-- 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₂ : C
g : Y₁ ⟶ Y₂
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X) (Functor.obj L' Y₁))
      (Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y₂)))
    (Functor.obj L' X ◁ Functor.map L' g ≫ Iso.hom (μ L W ε X Y₂)) (Iso.hom (μ L W ε X Y₁) ≫ Functor.map L' (X ◁ g))

Tactic:
((tensorBifunctorIso L W ε).hom.app X).naturality g

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Localization.Monoidal.tensorBifunctorIso, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.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₁ Y₂ : C
g : Y₁ ⟶ Y₂
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε) (Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) X Y₁))
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X) (Functor.obj L' Y₂)))
    (Iso.inv (μ L W ε X Y₁) ≫ Functor.obj L' X ◁ Functor.map L' g) (Functor.map L' (X ◁ g) ≫ Iso.inv (μ L W ε X Y₂))

Tactic:
simp [Iso.eq_comp_inv]

Premises used: CategoryTheory.Iso.eq_comp_inv
-- 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 : C
dsimp :
  Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))
    (NatTrans.app (Functor.map (tensorBifunctor L W ε) ε.inv) (Functor.obj L' Y) ≫
        NatTrans.app
          (liftNatTrans L' W (tensorLeft (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L') L'
            (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
            (𝟭 (LocalizedMonoidal L W ε)) (Functor.whiskerRight (Iso.hom (leftUnitorNatIso C)) L' ≫ L.leftUnitor.hom))
          (Functor.obj L' Y) :
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))
    (NatTrans.app (Functor.map (tensorBifunctor L W ε) (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)) :
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε)
        (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)) (Functor.obj L' Y))
      (Functor.obj L' Y))
    (Iso.hom (λ_ (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:
dsimp +instances [monoidalCategoryStruct, leftUnitor]

Premises used: CategoryTheory.Localization.Monoidal.monoidalCategoryStruct, CategoryTheory.Localization.Monoidal.leftUnitor
-- 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 : C
rw :
  Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))
    (NatTrans.app (Functor.map (tensorBifunctor L W ε) ε.inv) (Functor.obj L' Y) ≫
        CategoryStruct.comp (Y := Functor.obj (tensorLeft (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L') Y)
          (NatTrans.app
            (Iso.hom
              (Lifting.iso L' W (tensorLeft (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
                (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
            Y)
          (NatTrans.app (Functor.whiskerRight (Iso.hom (leftUnitorNatIso C)) L' ≫ L.leftUnitor.hom) Y ≫
            NatTrans.app (Iso.inv (Lifting.iso L' W L' (𝟭 (LocalizedMonoidal L W ε)))) Y) :
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))
    (NatTrans.app (Functor.map (tensorBifunctor L W ε) (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)) :
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))
    (NatTrans.app (Functor.map (tensorBifunctor L W ε) ε.inv) (Functor.obj L' Y) ≫
        NatTrans.app
          (liftNatTrans L' W (tensorLeft (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L') L'
            (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
            (𝟭 (LocalizedMonoidal L W ε)) (Functor.whiskerRight (Iso.hom (leftUnitorNatIso C)) L' ≫ L.leftUnitor.hom))
          (Functor.obj L' Y) :
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))
    (NatTrans.app (Functor.map (tensorBifunctor L W ε) (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)) :
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))

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
Y : C
dsimp :
  NatTrans.app (Functor.map (tensorBifunctor L W ε) ε.inv) (Functor.obj L' Y) ≫
      CategoryStruct.comp (Y :=
        Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y))
        (NatTrans.app
          (Iso.hom
            (Lifting.iso L' W (tensorLeft (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
              (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
          Y)
        ((Functor.map L' (Iso.hom (λ_ Y)) ≫ 𝟙 (L.obj Y)) ≫ 𝟙 (Functor.obj L' Y)) =
    NatTrans.app (Functor.map (tensorBifunctor L W ε) (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 ε)
      (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))
    (NatTrans.app (Functor.map (tensorBifunctor L W ε) ε.inv) (Functor.obj L' Y) ≫
        CategoryStruct.comp (Y := Functor.obj (tensorLeft (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L') Y)
          (NatTrans.app
            (Iso.hom
              (Lifting.iso L' W (tensorLeft (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
                (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
            Y)
          (NatTrans.app (Functor.whiskerRight (Iso.hom (leftUnitorNatIso C)) L' ≫ L.leftUnitor.hom) Y ≫
            NatTrans.app (Iso.inv (Lifting.iso L' W L' (𝟭 (LocalizedMonoidal L W ε)))) Y) :
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))
    (NatTrans.app (Functor.map (tensorBifunctor L W ε) (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)) :
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (Functor.obj (Functor.obj (tensorBifunctor L W ε) unit) (Functor.obj L' Y)) (Functor.obj L' Y))

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
Y : C
rw :
  NatTrans.app (Functor.map (tensorBifunctor L W ε) ε.inv) (Functor.obj L' Y) ≫
      CategoryStruct.comp (Y :=
        Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y))
        (NatTrans.app
          (Iso.hom
            (Lifting.iso L' W (tensorLeft (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
              (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
          Y)
        (Functor.map L' (Iso.hom (λ_ Y)) ≫ 𝟙 (L.obj Y) ≫ 𝟙 (Functor.obj L' Y)) =
    NatTrans.app (Functor.map (tensorBifunctor L W ε) (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))
⊢ NatTrans.app (Functor.map (tensorBifunctor L W ε) ε.inv) (Functor.obj L' Y) ≫
      CategoryStruct.comp (Y :=
        Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y))
        (NatTrans.app
          (Iso.hom
            (Lifting.iso L' W (tensorLeft (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
              (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
          Y)
        ((Functor.map L' (Iso.hom (λ_ Y)) ≫ 𝟙 (L.obj Y)) ≫ 𝟙 (Functor.obj L' Y)) =
    NatTrans.app (Functor.map (tensorBifunctor L W ε) (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:
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
Y : C
change :
  NatTrans.app (Functor.map (tensorBifunctor L W ε) ε.inv) (Functor.obj L' Y) ≫
      Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y) ≫
        Functor.map L' (Iso.hom (λ_ Y)) ≫ 𝟙 (Functor.obj L' Y) ≫ 𝟙 (Functor.obj L' Y) =
    NatTrans.app (Functor.map (tensorBifunctor L W ε) (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))
⊢ NatTrans.app (Functor.map (tensorBifunctor L W ε) ε.inv) (Functor.obj L' Y) ≫
      CategoryStruct.comp (Y :=
        Functor.obj L' (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y))
        (NatTrans.app
          (Iso.hom
            (Lifting.iso L' W (tensorLeft (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ⋙ L')
              (Functor.obj (tensorBifunctor L W ε) (Functor.obj L' (tensorUnit.{v_1, u_1} C (𝒞 := inst))))))
          Y)
        (Functor.map L' (Iso.hom (λ_ Y)) ≫ 𝟙 (L.obj Y) ≫ 𝟙 (Functor.obj L' Y)) =
    NatTrans.app (Functor.map (tensorBifunctor L W ε) (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:
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
Y : C
⊢ NatTrans.app (Functor.map (tensorBifunctor L W ε) ε.inv) (Functor.obj L' Y) ≫
      Iso.hom (μ L W ε (tensorUnit.{v_1, u_1} C (𝒞 := inst)) Y) ≫
        Functor.map L' (Iso.hom (λ_ Y)) ≫ 𝟙 (Functor.obj L' Y) ≫ 𝟙 (Functor.obj L' Y) =
    NatTrans.app (Functor.map (tensorBifunctor L W ε) (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:
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 : C
dsimp :
  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))
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (tensorObj.{v_2, u_2} (𝒞 := instCategoryLocalizedMonoidal L W ε) (Functor.obj L' X)
        (tensorUnit.{v_2, u_2} (LocalizedMonoidal L W ε) (𝒞 := instCategoryLocalizedMonoidal L W ε)))
      (Functor.obj L' X))
    (Iso.hom (ρ_ (Functor.obj L' X)))
    (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 +instances [monoidalCategoryStruct, rightUnitor]

Premises used: CategoryTheory.Localization.Monoidal.rightUnitor, CategoryTheory.Localization.Monoidal.monoidalCategoryStruct