-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
V : Type u₂
inst_1 : Category.{v₂, u₂} V
inst_2 : MonoidalCategory.{v₁, u₁} C
inst_3 : MonoidalCategory.{v₂, u₂} V
inst_4 : MonoidalClosed.{v₂, u₂} V
F G_1 H G : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 : DayConvolution F G
ℌ : DayConvolutionInternalHom F (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _) H
c c' c'' : C
f : c' ⟶ c''
this :
  Eq (α :=
    G.obj c ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c'))
        ((tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (c'', c)))
    (CategoryStruct.comp (Y :=
        Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c')) (tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj c'') (G.obj c)))
        (MonoidalClosed.curry (F.map f ▷ G.obj c))
        (Functor.map (ihom (F.obj c')) (NatTrans.app (DayConvolution.unit F G) (c'', c))) :
      G.obj c ⟶
        Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c'))
          ((tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (c'', c)))
    (MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c', c)) ≫
        Functor.map (ihom (F.obj c')) ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).map (f ▷ c)) :
      G.obj c ⟶
        Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c'))
          ((tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (c'', c)))
⊢ Eq (α :=
    G.obj c ⟶
      ((((dayConvolutionInternalHomDiagramFunctor F).obj (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _)).obj
                c).obj
            (op c')).obj
        c'')
    ((fun (c' : C) ↦
          (MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c', c)) :
            G.obj c ⟶
              Functor.obj.{v₂, v₂, u₂, u₂} (ihom (unop (F.op.obj (op c'))))
                ((tensorRight c ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj c')))
        c' ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _)).obj
                c).obj
            (op c')).map
        f)
    ((fun (c' : C) ↦
          (MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c', c)) :
            G.obj c ⟶
              Functor.obj.{v₂, v₂, u₂, u₂} (ihom (unop (F.op.obj (op c'))))
                ((tensorRight c ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj c')))
        c'' ≫
      ((((dayConvolutionInternalHomDiagramFunctor F).obj (@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _)).obj
                c).map
            f.op).app
        c'')
have dsimp : Eq (α :=
  G.obj c ⟶
    Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c'))
      ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (tensorObj.{v₁, u₁} (𝒞 := inst) c'' c)))
  (MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c', c)) ≫
      Functor.map (ihom (F.obj c')) ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).map (f ▷ c)) :
    G.obj c ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c'))
        ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (tensorObj.{v₁, u₁} (𝒞 := inst) c'' c)))
  (CategoryStruct.comp (Y :=
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c''))
        ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (tensorObj.{v₁, u₁} (𝒞 := inst) c'' c)))
      (MonoidalClosed.curry (NatTrans.app (DayConvolution.unit F G) (c'', c)))
      (NatTrans.app (MonoidalClosed.pre (F.map f))
        ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (tensorObj.{v₁, u₁} (𝒞 := inst) c'' c))) :
    G.obj c ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (ihom (F.obj c'))
        ((@DayConvolution.convolution _ _ _ _ inst_2 inst_3 F G _).obj (tensorObj.{v₁, u₁} (𝒞 := inst) c'' c)))
Tactic: dsimp