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

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
inst_5 : BraidedCategory.{v_1, u_1} C
refine_1 :
  Eq (α :=
    Quiver.Hom (V :=
      LocalizedMonoidal L W ε ⥤
        LocalizedMonoidal L W ε ⥤ Functor.{v_2, v_2, u_2, u_2} (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε))
      (bifunctorComp₁₂ (curriedTensor (LocalizedMonoidal L W ε)) (curriedTensor (LocalizedMonoidal L W ε)))
      (Hexagon.functor₂₃₁' (LocalizedMonoidal L W ε)))
    (Iso.hom (curriedAssociatorNatIso (LocalizedMonoidal L W ε)) ≫
      ofBifunctor.Forward.firstMap₂ (braidingNatIso L W ε) ≫ ofBifunctor.Forward.firstMap₃ (LocalizedMonoidal L W ε))
    (ofBifunctor.Forward.secondMap₁ (braidingNatIso L W ε) ≫
      ofBifunctor.Forward.secondMap₂ (LocalizedMonoidal L W ε) ≫ ofBifunctor.Forward.secondMap₃ (braidingNatIso L W ε))
refine_2 :
  Eq (α :=
    Quiver.Hom (V :=
      LocalizedMonoidal L W ε ⥤
        LocalizedMonoidal L W ε ⥤ Functor.{v_2, v_2, u_2, u_2} (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε))
      (bifunctorComp₂₃ (curriedTensor (LocalizedMonoidal L W ε)) (curriedTensor (LocalizedMonoidal L W ε)))
      (Hexagon.functor₃₁₂ (LocalizedMonoidal L W ε)))
    (Iso.inv (curriedAssociatorNatIso (LocalizedMonoidal L W ε)) ≫
      ofBifunctor.Reverse.firstMap₂ (braidingNatIso L W ε) ≫ ofBifunctor.Reverse.firstMap₃ (LocalizedMonoidal L W ε))
    (ofBifunctor.Reverse.secondMap₁ (braidingNatIso L W ε) ≫
      ofBifunctor.Reverse.secondMap₂ (LocalizedMonoidal L W ε) ≫ ofBifunctor.Reverse.secondMap₃ (braidingNatIso L W ε))
⊢ BraidedCategory.{v_2, u_2} (LocalizedMonoidal L W ε)

Tactic:
refine .ofBifunctor (braidingNatIso L W ε) ?_ ?_
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
inst_5 : BraidedCategory.{v_1, u_1} C
refine_1 :
  ∀ (X₁ X₂ X₃ : C),
    Eq (α :=
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (obj.{v_2, v_2, u_2, u_2}
          (obj
            (obj (bifunctorComp₁₂ (curriedTensor (LocalizedMonoidal L W ε)) (curriedTensor (LocalizedMonoidal L W ε)))
              (obj L' X₁))
            (obj L' X₂))
          (obj L' X₃))
        (obj.{v_2, v_2, u_2, u_2} (obj (obj (Hexagon.functor₂₃₁' (LocalizedMonoidal L W ε)) (obj L' X₁)) (obj L' X₂))
          (obj L' X₃)))
      (NatTrans.app
        (NatTrans.app
          (NatTrans.app
            (Iso.hom (curriedAssociatorNatIso (LocalizedMonoidal L W ε)) ≫
              ofBifunctor.Forward.firstMap₂ (braidingNatIso L W ε) ≫
                ofBifunctor.Forward.firstMap₃ (LocalizedMonoidal L W ε))
            (obj L' X₁))
          (obj L' X₂))
        (obj L' X₃))
      (NatTrans.app
        (NatTrans.app
          (NatTrans.app
            (ofBifunctor.Forward.secondMap₁ (braidingNatIso L W ε) ≫
              ofBifunctor.Forward.secondMap₂ (LocalizedMonoidal L W ε) ≫
                ofBifunctor.Forward.secondMap₃ (braidingNatIso L W ε))
            (obj L' X₁))
          (obj L' X₂))
        (obj L' X₃))
⊢ Eq (α :=
    Quiver.Hom (V :=
      LocalizedMonoidal L W ε ⥤
        LocalizedMonoidal L W ε ⥤ Functor.{v_2, v_2, u_2, u_2} (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε))
      (bifunctorComp₁₂ (curriedTensor (LocalizedMonoidal L W ε)) (curriedTensor (LocalizedMonoidal L W ε)))
      (Hexagon.functor₂₃₁' (LocalizedMonoidal L W ε)))
    (Iso.hom (curriedAssociatorNatIso (LocalizedMonoidal L W ε)) ≫
      ofBifunctor.Forward.firstMap₂ (braidingNatIso L W ε) ≫ ofBifunctor.Forward.firstMap₃ (LocalizedMonoidal L W ε))
    (ofBifunctor.Forward.secondMap₁ (braidingNatIso L W ε) ≫
      ofBifunctor.Forward.secondMap₂ (LocalizedMonoidal L W ε) ≫ ofBifunctor.Forward.secondMap₃ (braidingNatIso L W ε))

Tactic:
apply natTrans₃_ext (L') (L') (L') W W W
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
inst_5 : BraidedCategory.{v_1, u_1} C
⊢ ∀ (X₁ X₂ X₃ : C),
    Eq (α :=
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (obj.{v_2, v_2, u_2, u_2}
          (obj
            (obj (bifunctorComp₁₂ (curriedTensor (LocalizedMonoidal L W ε)) (curriedTensor (LocalizedMonoidal L W ε)))
              (obj L' X₁))
            (obj L' X₂))
          (obj L' X₃))
        (obj.{v_2, v_2, u_2, u_2} (obj (obj (Hexagon.functor₂₃₁' (LocalizedMonoidal L W ε)) (obj L' X₁)) (obj L' X₂))
          (obj L' X₃)))
      (NatTrans.app
        (NatTrans.app
          (NatTrans.app
            (Iso.hom (curriedAssociatorNatIso (LocalizedMonoidal L W ε)) ≫
              ofBifunctor.Forward.firstMap₂ (braidingNatIso L W ε) ≫
                ofBifunctor.Forward.firstMap₃ (LocalizedMonoidal L W ε))
            (obj L' X₁))
          (obj L' X₂))
        (obj L' X₃))
      (NatTrans.app
        (NatTrans.app
          (NatTrans.app
            (ofBifunctor.Forward.secondMap₁ (braidingNatIso L W ε) ≫
              ofBifunctor.Forward.secondMap₂ (LocalizedMonoidal L W ε) ≫
                ofBifunctor.Forward.secondMap₃ (braidingNatIso L W ε))
            (obj L' X₁))
          (obj L' X₂))
        (obj L' X₃))

Tactic:
simpa using map_hexagon_forward _ _ _

Premises used: CategoryTheory.Localization.Monoidal.map_hexagon_forward
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
inst_5 : BraidedCategory.{v_1, u_1} C
refine_2 :
  ∀ (X₁ X₂ X₃ : C),
    Eq (α :=
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (obj.{v_2, v_2, u_2, u_2}
          (obj
            (obj (bifunctorComp₂₃ (curriedTensor (LocalizedMonoidal L W ε)) (curriedTensor (LocalizedMonoidal L W ε)))
              (obj L' X₁))
            (obj L' X₂))
          (obj L' X₃))
        (obj.{v_2, v_2, u_2, u_2} (obj (obj (Hexagon.functor₃₁₂ (LocalizedMonoidal L W ε)) (obj L' X₁)) (obj L' X₂))
          (obj L' X₃)))
      (NatTrans.app
        (NatTrans.app
          (NatTrans.app
            (Iso.inv (curriedAssociatorNatIso (LocalizedMonoidal L W ε)) ≫
              ofBifunctor.Reverse.firstMap₂ (braidingNatIso L W ε) ≫
                ofBifunctor.Reverse.firstMap₃ (LocalizedMonoidal L W ε))
            (obj L' X₁))
          (obj L' X₂))
        (obj L' X₃))
      (NatTrans.app
        (NatTrans.app
          (NatTrans.app
            (ofBifunctor.Reverse.secondMap₁ (braidingNatIso L W ε) ≫
              ofBifunctor.Reverse.secondMap₂ (LocalizedMonoidal L W ε) ≫
                ofBifunctor.Reverse.secondMap₃ (braidingNatIso L W ε))
            (obj L' X₁))
          (obj L' X₂))
        (obj L' X₃))
⊢ Eq (α :=
    Quiver.Hom (V :=
      LocalizedMonoidal L W ε ⥤
        LocalizedMonoidal L W ε ⥤ Functor.{v_2, v_2, u_2, u_2} (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε))
      (bifunctorComp₂₃ (curriedTensor (LocalizedMonoidal L W ε)) (curriedTensor (LocalizedMonoidal L W ε)))
      (Hexagon.functor₃₁₂ (LocalizedMonoidal L W ε)))
    (Iso.inv (curriedAssociatorNatIso (LocalizedMonoidal L W ε)) ≫
      ofBifunctor.Reverse.firstMap₂ (braidingNatIso L W ε) ≫ ofBifunctor.Reverse.firstMap₃ (LocalizedMonoidal L W ε))
    (ofBifunctor.Reverse.secondMap₁ (braidingNatIso L W ε) ≫
      ofBifunctor.Reverse.secondMap₂ (LocalizedMonoidal L W ε) ≫ ofBifunctor.Reverse.secondMap₃ (braidingNatIso L W ε))

Tactic:
apply natTrans₃_ext (L') (L') (L') W W W
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
inst_5 : BraidedCategory.{v_1, u_1} C
⊢ ∀ (X₁ X₂ X₃ : C),
    Eq (α :=
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (obj.{v_2, v_2, u_2, u_2}
          (obj
            (obj (bifunctorComp₂₃ (curriedTensor (LocalizedMonoidal L W ε)) (curriedTensor (LocalizedMonoidal L W ε)))
              (obj L' X₁))
            (obj L' X₂))
          (obj L' X₃))
        (obj.{v_2, v_2, u_2, u_2} (obj (obj (Hexagon.functor₃₁₂ (LocalizedMonoidal L W ε)) (obj L' X₁)) (obj L' X₂))
          (obj L' X₃)))
      (NatTrans.app
        (NatTrans.app
          (NatTrans.app
            (Iso.inv (curriedAssociatorNatIso (LocalizedMonoidal L W ε)) ≫
              ofBifunctor.Reverse.firstMap₂ (braidingNatIso L W ε) ≫
                ofBifunctor.Reverse.firstMap₃ (LocalizedMonoidal L W ε))
            (obj L' X₁))
          (obj L' X₂))
        (obj L' X₃))
      (NatTrans.app
        (NatTrans.app
          (NatTrans.app
            (ofBifunctor.Reverse.secondMap₁ (braidingNatIso L W ε) ≫
              ofBifunctor.Reverse.secondMap₂ (LocalizedMonoidal L W ε) ≫
                ofBifunctor.Reverse.secondMap₃ (braidingNatIso L W ε))
            (obj L' X₁))
          (obj L' X₂))
        (obj L' X₃))

Tactic:
simpa using map_hexagon_reverse _ _ _

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

Tactic:
braidingNatIso_hom_app L W ε X Y

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

Tactic:
simp [β_hom_app]

Premises used: CategoryTheory.Localization.Monoidal.β_hom_app
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
inst_5 : SymmetricCategory.{v_1, u_1} C
refine :
  ∀ (X Y : C),
    Eq (α :=
      Quiver.Hom (V := LocalizedMonoidal L W ε)
        (obj.{v_2, v_2, u_2, u_2} (obj (curriedTensor (LocalizedMonoidal L W ε)) (obj L' X)) (obj L' Y))
        (obj.{v_2, v_2, u_2, u_2}
          (obj
            (obj (flipFunctor (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε))
              (Functor.flip (curriedTensor (LocalizedMonoidal L W ε))))
            (obj L' X))
          (obj L' Y)))
      (NatTrans.app
        (NatTrans.app
          (Iso.hom (curriedBraidingNatIso (LocalizedMonoidal L W ε)) ≫
            Functor.map (flipFunctor (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε))
              (Iso.hom (curriedBraidingNatIso (LocalizedMonoidal L W ε))))
          (obj L' X))
        (obj L' Y))
      (NatTrans.app (NatTrans.app (𝟙 (curriedTensor (LocalizedMonoidal L W ε))) (obj L' X)) (obj L' Y))
⊢ SymmetricCategory.{v_2, u_2} (LocalizedMonoidal L W ε)

Tactic:
refine .ofCurried (natTrans₂_ext (L') (L') W W fun X Y ↦ ?_)
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Braided
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : W.IsMonoidal
inst_4 : L.IsLocalization W
unit : D
ε : L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≅ unit
inst_5 : SymmetricCategory.{v_1, u_1} C
X Y : C
⊢ Eq (α :=
    Quiver.Hom (V := LocalizedMonoidal L W ε)
      (obj.{v_2, v_2, u_2, u_2} (obj (curriedTensor (LocalizedMonoidal L W ε)) (obj L' X)) (obj L' Y))
      (obj.{v_2, v_2, u_2, u_2}
        (obj
          (obj (flipFunctor (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε))
            (Functor.flip (curriedTensor (LocalizedMonoidal L W ε))))
          (obj L' X))
        (obj L' Y)))
    (NatTrans.app
      (NatTrans.app
        (Iso.hom (curriedBraidingNatIso (LocalizedMonoidal L W ε)) ≫
          Functor.map (flipFunctor (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε) (LocalizedMonoidal L W ε))
            (Iso.hom (curriedBraidingNatIso (LocalizedMonoidal L W ε))))
        (obj L' X))
      (obj L' Y))
    (NatTrans.app (NatTrans.app (𝟙 (curriedTensor (LocalizedMonoidal L W ε))) (obj L' X)) (obj L' Y))

Tactic:
simp [-Functor.map_braiding, β_hom_app, ← Functor.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Localization.Monoidal.β_hom_app, CategoryTheory.Functor.map_braiding
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
X₁ X₂ : C
⊢ Eq (α := ((curriedTensorPre F).obj (L.obj X₁)).obj (L.obj X₂) ⟶ ((curriedTensorPost F).obj (L.obj X₁)).obj (L.obj X₂))
    (NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj X₁)) (L.obj X₂))
    (((Lifting.iso L W G F).hom.app X₁ ⊗ₘ (Lifting.iso L W G F).hom.app X₂) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂)) (μ G X₁ X₂)
        ((Lifting.iso L W G F).inv.app (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) ≫ F.map (δ L X₁ X₂)))

Tactic:
simp [curriedTensorPreIsoPost]

Premises used: CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
⊢ ((curriedTensorPre F).obj Y₁).map e₂.hom ≫
      NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) Y₁) (L.obj X₂) =
    NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) Y₁) Y₂ ≫
      ((curriedTensorPost F).obj Y₁).map e₂.hom

Tactic:
have h₁ := ((curriedTensorPreIsoPost L W F G).hom.app Y₁).naturality e₂.hom
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  ((curriedTensorPre F).obj Y₁).map e₂.hom ≫
      NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) Y₁) (L.obj X₂) =
    NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) Y₁) Y₂ ≫
      ((curriedTensorPost F).obj Y₁).map e₂.hom
⊢ ∀ (X : D),
    NatTrans.app ((curriedTensorPre F).map e₁.hom ≫ NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj X₁))
        X =
      NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) Y₁ ≫ (curriedTensorPost F).map e₁.hom) X

Tactic:
have h₂ := congr_app ((curriedTensorPreIsoPost L W F G).hom.naturality e₁.hom)
-- Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor
Goal:
C : Type u_1
D : Type u_2
E : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} E
inst_3 : MonoidalCategory.{v_1, u_1} C
inst_4 : MonoidalCategory.{v_2, u_2} D
inst_5 : MonoidalCategory.{v_3, u_3} E
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : L.Monoidal
F : Functor.{v_2, v_3, u_2, u_3} D E
G : Functor.{v_1, v_3, u_1, u_3} C E
inst_8 : G.Monoidal
inst_9 : W.ContainsIdentities
inst_10 : Lifting L W G F
X₁ X₂ : C
Y₁ Y₂ : D
e₁ : Y₁ ≅ L.obj X₁
e₂ : Y₂ ≅ L.obj X₂
h₁ :
  ((curriedTensorPre F).obj Y₁).map e₂.hom ≫
      NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) Y₁) (L.obj X₂) =
    NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) Y₁) Y₂ ≫
      ((curriedTensorPost F).obj Y₁).map e₂.hom
h₂ :
  ∀ (X : D),
    NatTrans.app ((curriedTensorPre F).map e₁.hom ≫ NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj X₁))
        X =
      NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) Y₁ ≫ (curriedTensorPost F).map e₁.hom) X
dsimp :
  Eq (α := tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj Y₁) (F.obj Y₂) ⟶ F.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) Y₁ Y₂))
    (NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) Y₁) Y₂)
    ((F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂)) (μ G X₁ X₂)
        ((Lifting.iso L W G F).inv.app (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) ≫
          F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv))))
⊢ Eq (α := ((curriedTensorPre F).obj Y₁).obj Y₂ ⟶ ((curriedTensorPost F).obj Y₁).obj Y₂)
    (NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) Y₁) Y₂)
    ((F.map e₁.hom ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ F.map e₂.hom ≫ (Lifting.iso L W G F).hom.app X₂) ≫
      CategoryStruct.comp (Y := G.obj (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂)) (μ G X₁ X₂)
        ((Lifting.iso L W G F).inv.app (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) ≫
          F.map (δ L X₁ X₂ ≫ (e₁.inv ⊗ₘ e₂.inv))))

Tactic:
dsimp at h₁ h₂ ⊢