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) ▷ 𝟙_ 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

Tactic:
simp only [MonoidalCategory.whiskerRight_id, Category.id_comp, Iso.hom_inv_id,
    Category.comp_id] 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 ◁ 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 })
⊢ 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