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:
]

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₁ ⊗ₘ (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))