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₁ ⊗ₘ (Lifting.iso L W G F).hom.app X₂) ≫
          μ G X₁ X₂ ≫ (Lifting.iso L W G F).inv.app (X₁ ⊗ 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.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 ⊗ₘ (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₂ ⊗ₘ (Lifting.iso L W G F).hom.app X₃) ≫
            μ G X₂ X₃ ≫ (Lifting.iso L W G F).inv.app (X₂ ⊗ X₃) ≫ F.map (δ L X₂ X₃)) ≫
        (F.map (Iso.refl (L.obj X₁)).hom ≫ (Lifting.iso L W G F).hom.app 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 ⊗ₘ (μIso L X₂ X₃).inv))

Tactic:
monoidal_simps

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