Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided

Goal state before:
pp: C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ V
inst✝¹² : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝¹¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H (F ⊛ G)
inst✝⁵ : DayConvolution H F
inst✝⁴ : DayConvolution (H ⊛ F) G
inst✝³ : DayConvolution H G
inst✝² : DayConvolution F (H ⊛ G)
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution (F ⊛ H) G
x y z : C
⊢ F.obj x ◁ (β_ (G.obj y) (H.obj z)).hom ≫
      (α_ (F.obj x) (H.obj z) (G.obj y)).inv ≫
        ((β_ (F.obj x) (H.obj z)).hom ≫ (unit H F).app (z, x)) ▷ G.obj y ≫
          (unit (H ⊛ F) G).app (z ⊗ x, y) ≫
            ((H ⊛ F) ⊛ G).map ((β_ z x).hom ▷ y) ≫
              ((H ⊛ F) ⊛ G).map (α_ x z y).hom ≫ ((H ⊛ F) ⊛ G).map (x ◁ (β_ z y).hom) =
    F.obj x ◁ ((β_ (G.obj y) (H.obj z)).hom ≫ (unit H G).app (z, y) ≫ (H ⊛ G).map (β_ z y).hom) ≫
      (unit F (H ⊛ G)).app (x, y ⊗ z) ≫
        (associator F H G).inv.app (x ⊗ y ⊗ z) ≫ (map (braiding F H).hom (𝟙 G)).app (x ⊗ y ⊗ z)

Tactic:
simp only [comp_whiskerRight, ← Functor.map_comp, Category.assoc, Functor.comp_obj, tensor_obj,
    whiskerLeft_comp, whiskerLeft_comp_unit_app_assoc, NatTrans.naturality_assoc,
    NatTrans.naturality, associator_inv_unit_unit_assoc, externalProductBifunctor_obj_obj,
    unit_app_map_app_assoc, NatTrans.id_app, tensorHom_id]

Goal state after:
C : Type u₁
inst✝¹⁸ : Category.{v₁, u₁} C
V : Type u₂
inst✝¹⁷ : Category.{v₂, u₂} V
inst✝¹⁶ : MonoidalCategory C
inst✝¹⁵ : BraidedCategory C
inst✝¹⁴ : MonoidalCategory V
inst✝¹³ : BraidedCategory V
F G : C ⥤ V
inst✝¹² : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝¹¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
H : C ⥤ V
inst✝¹⁰ : DayConvolution F G
inst✝⁹ : DayConvolution G H
inst✝⁸ : DayConvolution F (G ⊛ H)
inst✝⁷ : DayConvolution (F ⊛ G) H
inst✝⁶ : DayConvolution H (F ⊛ G)
inst✝⁵ : DayConvolution H F
inst✝⁴ : DayConvolution (H ⊛ F) G
inst✝³ : DayConvolution H G
inst✝² : DayConvolution F (H ⊛ G)
inst✝¹ : DayConvolution F H
inst✝ : DayConvolution (F ⊛ H) G
x y z : C
⊢ F.obj x ◁ (β_ (G.obj y) (H.obj z)).hom ≫
      (α_ (F.obj x) (H.obj z) (G.obj y)).inv ≫
        (β_ (F.obj x) (H.obj z)).hom ▷ G.obj y ≫
          (unit H F).app (z, x) ▷ G.obj y ≫
            (unit (H ⊛ F) G).app (z ⊗ x, y) ≫ ((H ⊛ F) ⊛ G).map ((β_ z x).hom ▷ y ≫ (α_ x z y).hom ≫ x ◁ (β_ z y).hom) =
    F.obj x ◁ (β_ (G.obj y) (H.obj z)).hom ≫
      (α_ (F.obj x) (H.obj z) (G.obj y)).inv ≫
        (unit F H).app (x, z) ▷ G.obj y ≫
          (braiding F H).hom.app (x ⊗ z) ▷ G.obj y ≫
            (unit (H ⊛ F) G).app (x ⊗ z, y) ≫ ((H ⊛ F) ⊛ G).map ((α_ x z y).hom ≫ x ◁ (β_ z y).hom)