-- 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₃))))
    (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₃)))
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₃))))
  (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₃)))))))
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 _ _)]