-- 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₃))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (L.obj X₁) (L.obj X₂)))
        (F.obj (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₂))) ▷
        F.obj (L.obj X₃))
      (CategoryStruct.comp (Y :=
          tensorObj.{v_3, u_3} (𝒞 := inst_2) (G.obj (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂)) (G.obj X₃))
          (F.map (Iso.hom (μIso L X₁ X₂)) ≫ (Lifting.iso L W G F).hom.app (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ X₂) ⊗ₘ
            F.map (Iso.hom (Iso.refl (L.obj 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₃ ≫
                  (Iso.inv (μIso L X₁ X₂) ⊗ₘ Iso.inv (Iso.refl (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₃))) ≫
      CategoryStruct.comp (Y :=
        tensorObj.{v_3, u_3} (𝒞 := inst_2) (F.obj (L.obj X₁))
          (F.obj (tensorObj.{v_2, u_2} (𝒞 := inst_1) (L.obj X₂) (L.obj X₃))))
        (F.obj (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₃))))
        (CategoryStruct.comp (Y :=
          tensorObj.{v_3, u_3} (𝒞 := inst_2) (G.obj X₁) (G.obj (tensorObj.{v_1, u_1} (𝒞 := inst) X₂ X₃)))
          (F.map (Iso.hom (Iso.refl (L.obj X₁))) ≫ (Lifting.iso L W G F).hom.app X₁ ⊗ₘ
            F.map (Iso.hom (μIso L X₂ X₃)) ≫ (Lifting.iso L W G F).hom.app (tensorObj.{v_1, u_1} (𝒞 := inst) 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₃) ≫
                  (Iso.inv (Iso.refl (L.obj X₁)) ⊗ₘ Iso.inv (μIso L X₂ X₃)))))))
⊢ 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₃)))

Tactic:
rw [curriedTensorPreIsoPost_hom_app_app, curriedTensorPreIsoPost_hom_app_app,
      curriedTensorPreIsoPost_hom_app_app' L W F G (μIso L _ _) (Iso.refl _),
      curriedTensorPreIsoPost_hom_app_app' L W F G (Iso.refl _) (μIso L _ _)]

Premises used: CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app, CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app', CategoryTheory.Iso.refl, CategoryTheory.Functor.Monoidal.μIso