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

Tactic:
simp only [comp_obj, μIso_hom, Iso.refl_hom, map_id, Category.id_comp, μIso_inv, Iso.refl_inv,
      MonoidalCategory.whiskerLeft_id, Category.comp_id, map_comp, Category.assoc,
      ← comp_whiskerRight_assoc, map_δ_μ_assoc, Iso.inv_hom_id_app, id_whiskerRight,
      whisker_exchange_assoc, ← MonoidalCategory.whiskerLeft_comp_assoc, whiskerRight_tensor]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.whiskerRight_tensor, CategoryTheory.Functor.Monoidal.map_δ_μ_assoc, CategoryTheory.Category.comp_id, CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.id_whiskerRight, CategoryTheory.Functor.Monoidal.μIso_hom, CategoryTheory.Iso.refl_inv, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc, CategoryTheory.MonoidalCategory.whiskerLeft_id, CategoryTheory.Functor.Monoidal.μIso_inv, CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.refl_hom, CategoryTheory.Category.id_comp