Module: Mathlib.CategoryTheory.Localization.Monoidal.Functor

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₁ X₂ X₃ : C
⊢ ((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₃) ≫
      μ G X₁ X₂ ▷ F.obj (L.obj X₃) ≫
        (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂) ▷ F.obj (L.obj X₃) ≫
          F.map (δ L X₁ X₂) ▷ F.obj (L.obj X₃) ≫
            ((F.map (μIso L X₁ X₂).hom ≫ (Lifting.iso L W G F).hom.app (X₁ ⊗ X₂)) ▷ F.obj (L.obj X₃) ≫
                G.obj (X₁ ⊗ X₂) ◁ (F.map (Iso.refl (L.obj X₃)).hom ≫ (Lifting.iso L W G F).hom.app X₃)) ≫
              μ G (X₁ ⊗ X₂) X₃ ≫
                (Lifting.iso L W G F).inv.app ((X₁ ⊗ X₂) ⊗ X₃) ≫
                  F.map
                      (δ L (X₁ ⊗ X₂) X₃ ≫
                        (μIso L X₁ X₂).inv ▷ L.obj X₃ ≫ (L.obj X₁ ⊗ L.obj X₂) ◁ (Iso.refl (L.obj X₃)).inv) ≫
                    F.map (α_ (L.obj X₁) (L.obj X₂) (L.obj X₃)).hom =
    (α_ (F.obj (L.obj X₁)) (F.obj (L.obj X₂)) (F.obj (L.obj X₃))).hom ≫
      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₃) ≫
        F.obj (L.obj X₁) ◁ μ G X₂ X₃ ≫
          F.obj (L.obj X₁) ◁ (Lifting.iso L W G F).inv.app (X₂ ⊗ X₃) ≫
            F.obj (L.obj X₁) ◁ F.map (δ L X₂ X₃) ≫
              ((F.map (Iso.refl (L.obj X₁)).hom ≫ (Lifting.iso L W G F).hom.app X₁) ▷ F.obj (L.obj X₂ ⊗ L.obj X₃) ≫
                  G.obj X₁ ◁ (F.map (μIso L X₂ X₃).hom ≫ (Lifting.iso L W G F).hom.app (X₂ ⊗ X₃))) ≫
                μ G X₁ (X₂ ⊗ X₃) ≫
                  (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂ ⊗ X₃) ≫
                    F.map
                      (δ L X₁ (X₂ ⊗ X₃) ≫ (Iso.refl (L.obj X₁)).inv ▷ L.obj (X₂ ⊗ X₃) ≫ L.obj X₁ ◁ (μIso L X₂ X₃).inv)

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]

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory D
inst✝⁵ : MonoidalCategory E
L : C ⥤ D
W : MorphismProperty C
inst✝⁴ : L.IsLocalization W
inst✝³ : L.Monoidal
F : D ⥤ E
G : C ⥤ E
inst✝² : G.Monoidal
inst✝¹ : W.ContainsIdentities
inst✝ : Lifting L W G F
e : L ⋙ F ≅ G := Lifting.iso L W G F
X₁ X₂ X₃ : C
⊢ ((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 (X₁ ⊗ X₂) ◁ (Lifting.iso L W G F).hom.app X₃ ≫
        μ G (X₁ ⊗ X₂) X₃ ≫
          (Lifting.iso L W G F).inv.app ((X₁ ⊗ X₂) ⊗ X₃) ≫
            F.map (δ L (X₁ ⊗ X₂) X₃) ≫ F.map (δ L X₁ X₂ ▷ L.obj X₃) ≫ F.map (α_ (L.obj X₁) (L.obj X₂) (L.obj X₃)).hom =
    (α_ (F.obj (L.obj X₁)) (F.obj (L.obj X₂)) (F.obj (L.obj X₃))).hom ≫
      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₃) ≫
        (α_ (F.obj (L.obj X₁)) (G.obj X₂) (G.obj X₃)).inv ≫
          (Lifting.iso L W G F).hom.app X₁ ▷ G.obj X₂ ▷ G.obj X₃ ≫
            (α_ (G.obj X₁) (G.obj X₂) (G.obj X₃)).hom ≫
              G.obj X₁ ◁ μ G X₂ X₃ ≫
                μ G X₁ (X₂ ⊗ X₃) ≫
                  (Lifting.iso L W G F).inv.app (X₁ ⊗ X₂ ⊗ X₃) ≫ F.map (δ L X₁ (X₂ ⊗ X₃)) ≫ F.map (L.obj X₁ ◁ δ L X₂ X₃)