awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
e : L ⋙ F ≅ G := Lifting.iso L W G F
refine_1 :
  Eq (α := curriedTensorPrePre F ⟶ curriedTensorPostPost' F)
    (LaxMonoidal.ofBifunctor.firstMap (Iso.hom (curriedTensorPreIsoPost L W F G)))
    (LaxMonoidal.ofBifunctor.secondMap (Iso.hom (curriedTensorPreIsoPost L W F G)))
refine_2 :
  Eq (α := F ⋙ tensorUnitLeft E ⟶ F) (LaxMonoidal.ofBifunctor.leftMapₗ F)
    (CategoryStruct.comp (Y := (curriedTensorPre F).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
      (LaxMonoidal.ofBifunctor.topMapₗ
        (Iso.hom
          (Iso.trans (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (εIso G)
            (e.symm.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≪≫ F.mapIso (Iso.symm (εIso L))))))
      (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) ≫
        LaxMonoidal.ofBifunctor.bottomMapₗ F))
refine_3 :
  Eq (α := F ⋙ tensorUnitRight E ⟶ F) (LaxMonoidal.ofBifunctor.leftMapᵣ F)
    (CategoryStruct.comp (Y := (curriedTensorPre F).flip.obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
      (LaxMonoidal.ofBifunctor.topMapᵣ
        (Iso.hom
          (Iso.trans (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (εIso G)
            (e.symm.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≪≫ F.mapIso (Iso.symm (εIso L))))))
      (CategoryStruct.comp (Y :=
        (obj (flipFunctor D D E) (curriedTensorPost F)).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
        (NatTrans.app (map (flipFunctor D D E) (Iso.hom (curriedTensorPreIsoPost L W F G)))
          (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
        (LaxMonoidal.ofBifunctor.bottomMapᵣ F)))
⊢ F.CoreMonoidal

Tactic:
refine Functor.CoreMonoidal.ofBifunctor
    (εIso G ≪≫ e.symm.app _ ≪≫ F.mapIso (εIso L).symm) (curriedTensorPreIsoPost L W F G) ?_ ?_ ?_

Premises used: CategoryTheory.Functor.Monoidal.εIso, CategoryTheory.Iso.trans, CategoryTheory.Functor.CoreMonoidal.ofBifunctor, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Functor.mapIso, 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
e : L ⋙ F ≅ G := Lifting.iso L W G F
⊢ Eq (α := curriedTensorPrePre F ⟶ curriedTensorPostPost' F)
    (LaxMonoidal.ofBifunctor.firstMap (Iso.hom (curriedTensorPreIsoPost L W F G)))
    (LaxMonoidal.ofBifunctor.secondMap (Iso.hom (curriedTensorPreIsoPost L W F G)))

Tactic:
natTrans₃_ext L L L W W W (fun X₁ X₂ X₃ ↦ ?_)

Premises used: CategoryTheory.Localization.natTrans₃_ext
-- 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
e : L ⋙ F ≅ G := Lifting.iso L W G F
refine_1 :
  ∀ (X₁ X₂ X₃ : C),
    Eq (α :=
      (((curriedTensorPrePre F).obj (L.obj X₁)).obj (L.obj X₂)).obj (L.obj X₃) ⟶
        (((curriedTensorPostPost' F).obj (L.obj X₁)).obj (L.obj X₂)).obj (L.obj X₃))
      (NatTrans.app
        (NatTrans.app
          (NatTrans.app (LaxMonoidal.ofBifunctor.firstMap (Iso.hom (curriedTensorPreIsoPost L W F G))) (L.obj X₁))
          (L.obj X₂))
        (L.obj X₃))
      (NatTrans.app
        (NatTrans.app
          (NatTrans.app (LaxMonoidal.ofBifunctor.secondMap (Iso.hom (curriedTensorPreIsoPost L W F G))) (L.obj X₁))
          (L.obj X₂))
        (L.obj X₃))
⊢ Eq (α := curriedTensorPrePre F ⟶ curriedTensorPostPost' F)
    (LaxMonoidal.ofBifunctor.firstMap (Iso.hom (curriedTensorPreIsoPost L W F G)))
    (LaxMonoidal.ofBifunctor.secondMap (Iso.hom (curriedTensorPreIsoPost L W F G)))

Tactic:
refine natTrans₃_ext L L L W W W (fun X₁ X₂ X₃ ↦ ?_)

Premises used: CategoryTheory.Localization.natTrans₃_ext
-- 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
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₁ X₂ X₃ : C
refine_1 :
  Eq (α :=
    tensorObj.{v_3, u_3} (𝒞 := inst_2) (tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (L.obj X₁)) (F.obj (L.obj X₂)))
        (F.obj (L.obj X₃)) ⟶
      F.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (L.obj X₁) (tensorObj.{v_2, u_2} (𝒞 := inst_1) (L.obj X₂) (L.obj X₃))))
    (NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj X₁)) (L.obj X₂) ▷ F.obj (L.obj X₃) ≫
      NatTrans.app
          (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G))
            (tensorObj.{v_2, u_2} (𝒞 := inst_1) (L.obj X₁) (L.obj X₂)))
          (L.obj X₃) ≫
        F.map (Iso.hom (α_ (L.obj X₁) (L.obj X₂) (L.obj X₃))))
    (Iso.hom (α_ (F.obj (L.obj X₁)) (F.obj (L.obj X₂)) (F.obj (L.obj X₃))) ≫
      F.obj (L.obj X₁) ◁ NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj X₂)) (L.obj X₃) ≫
        NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj X₁))
          (tensorObj.{v_2, u_2} (𝒞 := inst_1) (L.obj X₂) (L.obj X₃)))
⊢ Eq (α :=
    (((curriedTensorPrePre F).obj (L.obj X₁)).obj (L.obj X₂)).obj (L.obj X₃) ⟶
      (((curriedTensorPostPost' F).obj (L.obj X₁)).obj (L.obj X₂)).obj (L.obj X₃))
    (NatTrans.app
      (NatTrans.app
        (NatTrans.app (LaxMonoidal.ofBifunctor.firstMap (Iso.hom (curriedTensorPreIsoPost L W F G))) (L.obj X₁))
        (L.obj X₂))
      (L.obj X₃))
    (NatTrans.app
      (NatTrans.app
        (NatTrans.app (LaxMonoidal.ofBifunctor.secondMap (Iso.hom (curriedTensorPreIsoPost L W F G))) (L.obj X₁))
        (L.obj X₂))
      (L.obj X₃))

Tactic:
dsimp [e]
-- 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
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₁ X₂ X₃ : C
⊢ Eq (α :=
    tensorObj.{v_3, u_3} (𝒞 := inst_2) (tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (L.obj X₁)) (F.obj (L.obj X₂)))
        (F.obj (L.obj X₃)) ⟶
      F.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (L.obj X₁) (tensorObj.{v_2, u_2} (𝒞 := inst_1) (L.obj X₂) (L.obj X₃))))
    (((Lifting.iso L W G F).hom.app X₁ ▷ F.obj (L.obj X₂) ≫ G.obj X₁ ◁ (Lifting.iso L W G F).hom.app X₂ ≫ μ G X₁ X₂) ▷
        F.obj (L.obj X₃) ≫
      G.obj (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) ◁ (Lifting.iso L W G F).hom.app X₃ ≫
        CategoryStruct.comp (Y := G.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) X₃))
          (μ G (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) X₃)
          ((Lifting.iso L W G F).inv.app
              (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) X₃) ≫
            F.map (δ L (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) X₃) ≫
              F.map (δ L X₁ X₂ ▷ L.obj X₃) ≫ F.map (Iso.hom (α_ (L.obj X₁) (L.obj X₂) (L.obj X₃)))))
    (Iso.hom (α_ (F.obj (L.obj X₁)) (F.obj (L.obj X₂)) (F.obj (L.obj X₃))) ≫
      F.obj (L.obj X₁) ◁
          ((Lifting.iso L W G F).hom.app X₂ ▷ F.obj (L.obj X₃) ≫ G.obj X₂ ◁ (Lifting.iso L W G F).hom.app X₃) ≫
        Iso.inv (α_ (F.obj (L.obj X₁)) (G.obj X₂) (G.obj X₃)) ≫
          (Lifting.iso L W G F).hom.app X₁ ▷ G.obj X₂ ▷ G.obj X₃ ≫
            Iso.hom (α_ (G.obj X₁) (G.obj X₂) (G.obj X₃)) ≫
              CategoryStruct.comp (Y :=
                tensorObj.{v_3, u_3} (𝒞 := inst_2) (G.obj X₁) (G.obj (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃)))
                (G.obj X₁ ◁ μ G X₂ X₃)
                (CategoryStruct.comp (Y :=
                  G.obj (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃)))
                  (μ G X₁ (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃))
                  ((Lifting.iso L W G F).inv.app
                      (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃)) ≫
                    F.map (δ L X₁ (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃)) ≫ F.map (L.obj X₁ ◁ δ L X₂ X₃))))

Tactic:
simp [← whisker_exchange_assoc, tensor_whiskerLeft_symm, -tensor_whiskerLeft,
      ← LaxMonoidal.associativity_assoc G, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.LaxMonoidal.associativity_assoc, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.MonoidalCategory.tensor_whiskerLeft, CategoryTheory.MonoidalCategory.tensor_whiskerLeft_symm
-- 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
e : L ⋙ F ≅ G := Lifting.iso L W G F
⊢ Eq (α := F ⋙ tensorUnitLeft E ⟶ F) (LaxMonoidal.ofBifunctor.leftMapₗ F)
    (CategoryStruct.comp (Y := (curriedTensorPre F).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
      (LaxMonoidal.ofBifunctor.topMapₗ
        (Iso.hom
          (Iso.trans (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (εIso G)
            (e.symm.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≪≫ F.mapIso (Iso.symm (εIso L))))))
      (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) ≫
        LaxMonoidal.ofBifunctor.bottomMapₗ F))

Tactic:
natTrans_ext L W (fun X₂ ↦ ?_)

Premises used: CategoryTheory.Localization.natTrans_ext
-- 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
e : L ⋙ F ≅ G := Lifting.iso L W G F
refine_2 :
  ∀ (X₂ : C),
    Eq (α := (F ⋙ tensorUnitLeft E).obj (L.obj X₂) ⟶ F.obj (L.obj X₂))
      (NatTrans.app (LaxMonoidal.ofBifunctor.leftMapₗ F) (L.obj X₂))
      (NatTrans.app
        (CategoryStruct.comp (Y := (curriedTensorPre F).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
          (LaxMonoidal.ofBifunctor.topMapₗ
            (Iso.hom
              (Iso.trans (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (εIso G)
                (e.symm.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≪≫ F.mapIso (Iso.symm (εIso L))))))
          (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) ≫
            LaxMonoidal.ofBifunctor.bottomMapₗ F))
        (L.obj X₂))
⊢ Eq (α := F ⋙ tensorUnitLeft E ⟶ F) (LaxMonoidal.ofBifunctor.leftMapₗ F)
    (CategoryStruct.comp (Y := (curriedTensorPre F).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
      (LaxMonoidal.ofBifunctor.topMapₗ
        (Iso.hom
          (Iso.trans (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (εIso G)
            (e.symm.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≪≫ F.mapIso (Iso.symm (εIso L))))))
      (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) ≫
        LaxMonoidal.ofBifunctor.bottomMapₗ F))

Tactic:
refine natTrans_ext L W (fun X₂ ↦ ?_)

Premises used: CategoryTheory.Localization.natTrans_ext
-- 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
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₂ : C
⊢ Eq (α :=
    ((curriedTensorPre F).obj (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)))).obj (L.obj X₂) ⟶
      ((curriedTensorPost F).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1))).obj (L.obj X₂))
    (NatTrans.app
      ((curriedTensorPre F).map (Iso.inv (εIso L)) ≫
        NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
      (L.obj X₂))
    (NatTrans.app
      (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
        (curriedTensorPost F).map (Iso.inv (εIso L)))
      (L.obj X₂))

Tactic:
have := NatTrans.congr_app ((curriedTensorPreIsoPost L W F G).hom.naturality (εIso L).inv)
      (L.obj X₂)
-- 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
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₂ : C
this :
  Eq (α :=
    ((curriedTensorPre F).obj (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)))).obj (L.obj X₂) ⟶
      ((curriedTensorPost F).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1))).obj (L.obj X₂))
    (NatTrans.app
      ((curriedTensorPre F).map (Iso.inv (εIso L)) ≫
        NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
      (L.obj X₂))
    (NatTrans.app
      (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) ≫
        (curriedTensorPost F).map (Iso.inv (εIso L)))
      (L.obj X₂))
refine_2 :
  Eq (α :=
    tensorObj.{v_3, u_3} (𝒞 := inst_2) (tensorUnit.{v_3, u_3} E (𝒞 := inst_2)) (F.obj (L.obj X₂)) ⟶ F.obj (L.obj X₂))
    (Iso.hom (λ_ (F.obj (L.obj X₂))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1))) (F.obj (L.obj X₂)))
      (CategoryStruct.comp (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (ε G)
          ((Lifting.iso L W G F).inv.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≫ F.map (η L)) ▷
        F.obj (L.obj X₂))
      (NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
          (L.obj X₂) ≫
        F.map (Iso.hom (λ_ (L.obj X₂)))))
⊢ Eq (α := (F ⋙ tensorUnitLeft E).obj (L.obj X₂) ⟶ F.obj (L.obj X₂))
    (NatTrans.app (LaxMonoidal.ofBifunctor.leftMapₗ F) (L.obj X₂))
    (NatTrans.app
      (CategoryStruct.comp (Y := (curriedTensorPre F).obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
        (LaxMonoidal.ofBifunctor.topMapₗ
          (Iso.hom
            (Iso.trans (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (εIso G)
              (e.symm.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≪≫ F.mapIso (Iso.symm (εIso L))))))
        (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) ≫
          LaxMonoidal.ofBifunctor.bottomMapₗ F))
      (L.obj X₂))

Tactic:
dsimp [e] at this ⊢
-- 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
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₂ : C
this :
  Eq (α :=
    tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)))) (F.obj (L.obj X₂)) ⟶
      F.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) (L.obj X₂)))
    (F.map (η L) ▷ F.obj (L.obj X₂) ≫
      NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
        (L.obj X₂))
    (NatTrans.app
        (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (L.obj X₂) ≫
      F.map (η L ▷ L.obj X₂))
refine_2 :
  Eq (α :=
    tensorObj.{v_3, u_3} (𝒞 := inst_2) (tensorUnit.{v_3, u_3} E (𝒞 := inst_2)) (F.obj (L.obj X₂)) ⟶ F.obj (L.obj X₂))
    (Iso.hom (λ_ (F.obj (L.obj X₂))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_3, u_3} (𝒞 := inst_2) (G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (F.obj (L.obj X₂)))
      (ε G ▷ F.obj (L.obj X₂))
      ((Lifting.iso L W G F).inv.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ▷ F.obj (L.obj X₂) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1))) (F.obj (L.obj X₂)))
          (F.map (η L) ▷ F.obj (L.obj X₂))
          (NatTrans.app
              (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
              (L.obj X₂) ≫
            F.map (Iso.hom (λ_ (L.obj X₂))))))
⊢ Eq (α :=
    tensorObj.{v_3, u_3} (𝒞 := inst_2) (tensorUnit.{v_3, u_3} E (𝒞 := inst_2)) (F.obj (L.obj X₂)) ⟶ F.obj (L.obj X₂))
    (Iso.hom (λ_ (F.obj (L.obj X₂))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1))) (F.obj (L.obj X₂)))
      (CategoryStruct.comp (Y := G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (ε G)
          ((Lifting.iso L W G F).inv.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≫ F.map (η L)) ▷
        F.obj (L.obj X₂))
      (NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
          (L.obj X₂) ≫
        F.map (Iso.hom (λ_ (L.obj X₂)))))

Tactic:
monoidal_simps
-- 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
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₂ : C
this :
  Eq (α :=
    tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst)))) (F.obj (L.obj X₂)) ⟶
      F.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)) (L.obj X₂)))
    (F.map (η L) ▷ F.obj (L.obj X₂) ≫
      NatTrans.app (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
        (L.obj X₂))
    (NatTrans.app
        (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (L.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (L.obj X₂) ≫
      F.map (η L ▷ L.obj X₂))
⊢ Eq (α :=
    tensorObj.{v_3, u_3} (𝒞 := inst_2) (tensorUnit.{v_3, u_3} E (𝒞 := inst_2)) (F.obj (L.obj X₂)) ⟶ F.obj (L.obj X₂))
    (Iso.hom (λ_ (F.obj (L.obj X₂))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_3, u_3} (𝒞 := inst_2) (G.obj (tensorUnit.{v_1, u_1} C (𝒞 := inst))) (F.obj (L.obj X₂)))
      (ε G ▷ F.obj (L.obj X₂))
      ((Lifting.iso L W G F).inv.app (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ▷ F.obj (L.obj X₂) ≫
        CategoryStruct.comp (Y :=
          tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (tensorUnit.{v_2, u_2} D (𝒞 := inst_1))) (F.obj (L.obj X₂)))
          (F.map (η L) ▷ F.obj (L.obj X₂))
          (NatTrans.app
              (NatTrans.app (Iso.hom (curriedTensorPreIsoPost L W F G)) (tensorUnit.{v_2, u_2} D (𝒞 := inst_1)))
              (L.obj X₂) ≫
            F.map (Iso.hom (λ_ (L.obj X₂))))))

Tactic:
simp [reassoc_of% this, curriedTensorPreIsoPost_hom_app_app, ← comp_whiskerRight_assoc,
      -comp_whiskerRight, tensorHom_def, ← whisker_exchange_assoc, ← map_comp]

Premises used: CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app, CategoryTheory.MonoidalCategory.comp_whiskerRight, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc, CategoryTheory.Functor.map_comp