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
U : C ⥤ V
inst✝² : DayConvolutionUnit U
F : C ⥤ V
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝ : DayConvolution F U
x : C
this :
  ((corepresentableByRight U F).homEquiv
          ((corepresentableByRight U F).homEquiv.symm
            ((ConcreteCategory.hom ((rightUnitorCorepresentingIso F).symm.hom.app F))
              (𝟙 (Opposite.unop (Opposite.op F)))))).app
      (x, { as := PUnit.unit }) =
    ((ConcreteCategory.hom ((rightUnitorCorepresentingIso F).symm.hom.app F)) (𝟙 (Opposite.unop (Opposite.op F)))).app
      (x, { as := PUnit.unit })
⊢ F.obj x ◁ can ≫ (DayConvolution.unit F U).app (x, 𝟙_ C) ≫ (rightUnitor U F).hom.app (x ⊗ 𝟙_ C) =
    (ρ_ (F.obj x)).hom ≫ F.map (ρ_ x).inv

Tactic:
dsimp [rightUnitor, Coyoneda.fullyFaithful, corepresentableByRight,
    rightUnitorCorepresentingIso, Functor.CorepresentableBy.ofIso,
    Functor.corepresentableByEquiv] at this ⊢

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
U : C ⥤ V
inst✝² : DayConvolutionUnit U
F : C ⥤ V
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝ : DayConvolution F U
x : C
this :
  (𝟙 (F.obj x) ▷ 𝟙_ V ≫ F.obj x ◁ can) ≫
      (DayConvolution.unit F U).app (x, 𝟙_ C) ≫
        ((F ⊛ U).descOfIsLeftKanExtension (DayConvolution.unit F U) F
              ((F ⊠ U).descOfIsLeftKanExtension (extensionUnitRight U (φ U) F) (tensor C ⋙ F)
                ((prod.rightUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv.symm
                  ((ConcreteCategory.hom
                      (𝟙
                        (prod.rightInverseUnitor C ⋙ F ⊠ fromPUnit (𝟙_ V) ⟶
                          prod.rightInverseUnitor C ⋙ (𝟭 C).prod (fromPUnit (𝟙_ C)) ⋙ tensor C ⋙ F)))
                    (((NatIso.ofComponents (fun x ↦ (ρ_ (F.obj x)).symm) ⋯).inv ≫ 𝟙 F) ≫
                      ((whiskeringLeft C C V).map (NatIso.ofComponents (fun x ↦ ρ_ x) ⋯).inv).app F))))).app
          (x ⊗ 𝟙_ C) =
    ((prod.rightUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv.symm
          ((ConcreteCategory.hom
              (𝟙
                (prod.rightInverseUnitor C ⋙ F ⊠ fromPUnit (𝟙_ V) ⟶
                  prod.rightInverseUnitor C ⋙ (𝟭 C).prod (fromPUnit (𝟙_ C)) ⋙ tensor C ⋙ F)))
            (((NatIso.ofComponents (fun x ↦ (ρ_ (F.obj x)).symm) ⋯).inv ≫ 𝟙 F) ≫
              ((whiskeringLeft C C V).map (NatIso.ofComponents (fun x ↦ ρ_ x) ⋯).inv).app F))).app
      (x, { as := PUnit.unit })
⊢ F.obj x ◁ can ≫
      (DayConvolution.unit F U).app (x, 𝟙_ C) ≫
        ((F ⊛ U).descOfIsLeftKanExtension (DayConvolution.unit F U) F
              ((F ⊠ U).descOfIsLeftKanExtension (extensionUnitRight U (φ U) F) (tensor C ⋙ F)
                ((prod.rightUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv.symm
                  ((ConcreteCategory.hom
                      (𝟙
                        (prod.rightInverseUnitor C ⋙ F ⊠ fromPUnit (𝟙_ V) ⟶
                          prod.rightInverseUnitor C ⋙ (𝟭 C).prod (fromPUnit (𝟙_ C)) ⋙ tensor C ⋙ F)))
                    (((NatIso.ofComponents (fun x ↦ (ρ_ (F.obj x)).symm) ⋯).inv ≫ 𝟙 F) ≫
                      ((whiskeringLeft C C V).map (NatIso.ofComponents (fun x ↦ ρ_ x) ⋯).inv).app F))))).app
          (x ⊗ 𝟙_ C) =
    (ρ_ (F.obj x)).hom ≫ F.map (ρ_ x).inv