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) (tensorRight v)
inst✝ : DayConvolution U F
y : C
this :
  (can ▷ F.obj y ≫ U.obj (𝟙_ C) ◁ 𝟙 (F.obj y)) ≫
      (DayConvolution.unit U F).app (𝟙_ C, y) ≫
        ((U ⊛ F).descOfIsLeftKanExtension (DayConvolution.unit U F) F
              ((U ⊠ F).descOfIsLeftKanExtension (extensionUnitLeft U (φ U) F) (tensor C ⋙ F)
                ((prod.leftUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv.symm
                  ((ConcreteCategory.hom
                      (𝟙
                        (prod.leftInverseUnitor C ⋙ fromPUnit (𝟙_ V) ⊠ F ⟶
                          prod.leftInverseUnitor C ⋙ (fromPUnit (𝟙_ C)).prod (𝟭 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
          (𝟙_ C ⊗ y) =
    ((prod.leftUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv.symm
          ((ConcreteCategory.hom
              (𝟙
                (prod.leftInverseUnitor C ⋙ fromPUnit (𝟙_ V) ⊠ F ⟶
                  prod.leftInverseUnitor C ⋙ (fromPUnit (𝟙_ C)).prod (𝟭 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
      ({ as := PUnit.unit }, y)
⊢ can ▷ F.obj y ≫
      (DayConvolution.unit U F).app (𝟙_ C, y) ≫
        ((U ⊛ F).descOfIsLeftKanExtension (DayConvolution.unit U F) F
              ((U ⊠ F).descOfIsLeftKanExtension (extensionUnitLeft U (φ U) F) (tensor C ⋙ F)
                ((prod.leftUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv.symm
                  ((ConcreteCategory.hom
                      (𝟙
                        (prod.leftInverseUnitor C ⋙ fromPUnit (𝟙_ V) ⊠ F ⟶
                          prod.leftInverseUnitor C ⋙ (fromPUnit (𝟙_ C)).prod (𝟭 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
          (𝟙_ C ⊗ y) =
    (λ_ (F.obj y)).hom ≫ F.map (λ_ y).inv

Tactic:
simp only [whiskerLeft_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) (tensorRight v)
inst✝ : DayConvolution U F
y : C
this :
  can ▷ F.obj y ≫
      (DayConvolution.unit U F).app (𝟙_ C, y) ≫
        ((U ⊛ F).descOfIsLeftKanExtension (DayConvolution.unit U F) F
              ((U ⊠ F).descOfIsLeftKanExtension (extensionUnitLeft U (φ U) F) (tensor C ⋙ F)
                ((prod.leftUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv.symm
                  ((ConcreteCategory.hom
                      (𝟙
                        (prod.leftInverseUnitor C ⋙ fromPUnit (𝟙_ V) ⊠ F ⟶
                          prod.leftInverseUnitor C ⋙ (fromPUnit (𝟙_ C)).prod (𝟭 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
          (𝟙_ C ⊗ y) =
    ((prod.leftUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv.symm
          ((ConcreteCategory.hom
              (𝟙
                (prod.leftInverseUnitor C ⋙ fromPUnit (𝟙_ V) ⊠ F ⟶
                  prod.leftInverseUnitor C ⋙ (fromPUnit (𝟙_ C)).prod (𝟭 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
      ({ as := PUnit.unit }, y)
⊢ can ▷ F.obj y ≫
      (DayConvolution.unit U F).app (𝟙_ C, y) ≫
        ((U ⊛ F).descOfIsLeftKanExtension (DayConvolution.unit U F) F
              ((U ⊠ F).descOfIsLeftKanExtension (extensionUnitLeft U (φ U) F) (tensor C ⋙ F)
                ((prod.leftUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv.symm
                  ((ConcreteCategory.hom
                      (𝟙
                        (prod.leftInverseUnitor C ⋙ fromPUnit (𝟙_ V) ⊠ F ⟶
                          prod.leftInverseUnitor C ⋙ (fromPUnit (𝟙_ C)).prod (𝟭 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
          (𝟙_ C ⊗ y) =
    (λ_ (F.obj y)).hom ≫ F.map (λ_ y).inv