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✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct 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) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : D
x✝³ : X₁✝ ⟶ Y₁✝
x✝² : X₂✝ ⟶ Y₂✝
x✝¹ : Y₁✝ ⟶ Z₁✝
x✝ : Y₂✝ ⟶ Z₂✝
⊢ (corepresentableBy ((ι C V D).obj X₁✝) ((ι C V D).obj X₂✝)).homEquiv
      (map ((ι C V D).map x✝³) ((ι C V D).map x✝²) ≫ map ((ι C V D).map x✝¹) ((ι C V D).map x✝)) =
    (corepresentableBy ((ι C V D).obj X₁✝) ((ι C V D).obj X₂✝)).homEquiv
      (map ((ι C V D).map x✝³ ≫ (ι C V D).map x✝¹) ((ι C V D).map x✝² ≫ (ι C V D).map x✝))

Tactic:
ext ⟨_, _⟩

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✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct 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) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : D
x✝³ : X₁✝ ⟶ Y₁✝
x✝² : X₂✝ ⟶ Y₂✝
x✝¹ : Y₁✝ ⟶ Z₁✝
x✝ : Y₂✝ ⟶ Z₂✝
fst✝ snd✝ : C
⊢ ((corepresentableBy ((ι C V D).obj X₁✝) ((ι C V D).obj X₂✝)).homEquiv
          (map ((ι C V D).map x✝³) ((ι C V D).map x✝²) ≫ map ((ι C V D).map x✝¹) ((ι C V D).map x✝))).app
      (fst✝, snd✝) =
    ((corepresentableBy ((ι C V D).obj X₁✝) ((ι C V D).obj X₂✝)).homEquiv
          (map ((ι C V D).map x✝³ ≫ (ι C V D).map x✝¹) ((ι C V D).map x✝² ≫ (ι C V D).map x✝))).app
      (fst✝, snd✝)