Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C✝ : Type u₁
inst✝¹³ : Category.{v₁, u₁} C✝
V✝ : Type u₂
inst✝¹² : Category.{v₂, u₂} V✝
inst✝¹¹ : MonoidalCategory C✝
inst✝¹⁰ : MonoidalCategory V✝
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory V
D : Type u₃
inst✝⁵ : Category.{v₃, u₃} D
inst✝⁴ : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
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)
inst✝¹ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
this : MonoidalCategoryStruct D := mkMonoidalCategoryStruct C V D
d₁ d₂ d₃ : D
x₁ x₂ x₃ : C
⊢ (DayConvolution.unit ((ι C V D).obj d₁) ((ι C V D).obj d₂)).app (x₁, x₂) ▷ ((ι C V D).obj d₃).obj x₃ ≫
      (DayConvolution.unit ((ι C V D).obj (d₁ ⊗ d₂)) ((ι C V D).obj d₃)).app (x₁ ⊗ x₂, x₃) ≫
        ((ι C V D).map (α_ d₁ d₂ d₃).hom).app ((x₁ ⊗ x₂) ⊗ x₃) =
    (α_ (((ι C V D).obj d₁).obj x₁) (((ι C V D).obj d₂, (ι C V D).obj d₃).1.obj (x₂, x₃).1)
          (((ι C V D).obj d₂, (ι C V D).obj d₃).2.obj (x₂, x₃).2)).hom ≫
      ((ι C V D).obj d₁).obj x₁ ◁ (DayConvolution.unit ((ι C V D).obj d₂) ((ι C V D).obj d₃)).app (x₂, x₃) ≫
        (DayConvolution.unit ((ι C V D).obj d₁) ((ι C V D).obj (d₂ ⊗ d₃))).app (x₁, x₂ ⊗ x₃) ≫
          ((ι C V D).obj (d₁ ⊗ d₂ ⊗ d₃)).map (α_ (x₁, x₂ ⊗ x₃).1 x₂ x₃).inv

Tactic:
simp only [externalProductBifunctor_obj_obj, Functor.comp_obj, tensor_obj, associator,
        Functor.FullyFaithful.preimageIso_hom, Functor.FullyFaithful.map_preimage]

Goal state after:
C✝ : Type u₁
inst✝¹³ : Category.{v₁, u₁} C✝
V✝ : Type u₂
inst✝¹² : Category.{v₂, u₂} V✝
inst✝¹¹ : MonoidalCategory C✝
inst✝¹⁰ : MonoidalCategory V✝
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory V
D : Type u₃
inst✝⁵ : Category.{v₃, u₃} D
inst✝⁴ : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
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)
inst✝¹ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
this : MonoidalCategoryStruct D := mkMonoidalCategoryStruct C V D
d₁ d₂ d₃ : D
x₁ x₂ x₃ : C
⊢ (DayConvolution.unit ((ι C V D).obj d₁) ((ι C V D).obj d₂)).app (x₁, x₂) ▷ ((ι C V D).obj d₃).obj x₃ ≫
      (DayConvolution.unit ((ι C V D).obj (d₁ ⊗ d₂)) ((ι C V D).obj d₃)).app (x₁ ⊗ x₂, x₃) ≫
        (DayConvolution.associator ((ι C V D).obj d₁) ((ι C V D).obj d₂) ((ι C V D).obj d₃)).hom.app ((x₁ ⊗ x₂) ⊗ x₃) =
    (α_ (((ι C V D).obj d₁).obj x₁) (((ι C V D).obj d₂).obj x₂) (((ι C V D).obj d₃).obj x₃)).hom ≫
      ((ι C V D).obj d₁).obj x₁ ◁ (DayConvolution.unit ((ι C V D).obj d₂) ((ι C V D).obj d₃)).app (x₂, x₃) ≫
        (DayConvolution.unit ((ι C V D).obj d₁) ((ι C V D).obj (d₂ ⊗ d₃))).app (x₁, x₂ ⊗ x₃) ≫
          ((ι C V D).obj (d₁ ⊗ d₂ ⊗ d₃)).map (α_ x₁ x₂ x₃).inv