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 :
  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 ≫
                      ((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 ≫
              ((whiskeringLeft C C V).map (NatIso.ofComponents (fun x ↦ ρ_ x) ⋯).inv).app F))).app
      (x, { as := PUnit.unit })
⊢ ((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 ≫
              ((whiskeringLeft C C V).map (NatIso.ofComponents (fun x ↦ ρ_ x) ⋯).inv).app F))).app
      (x, { as := PUnit.unit }) =
    (ρ_ (F.obj x)).hom ≫ F.map (ρ_ x).inv

Tactic:
simp [prod.rightUnitorEquivalence, Equivalence.congrLeft, Equivalence.fullyFaithfulFunctor,
    Functor.FullyFaithful.homEquiv]

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 ◁ 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 ≫
                      ((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 ≫
              ((whiskeringLeft C C V).map (NatIso.ofComponents (fun x ↦ ρ_ x) ⋯).inv).app F))).app
      (x, { as := PUnit.unit })
⊢ ((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 ≫
            ((whiskeringLeft C C V).map (NatIso.ofComponents (fun x ↦ ρ_ x) ⋯).inv).app F)).app
      x =
    (ρ_ (F.obj x)).hom ≫ F.map (ρ_ x).inv