-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Monoidal.Functor (goal)
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₃))))
    (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₃)))))))
have 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₁ ▷ (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: monoidal_simps