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