-- 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 ⟶
      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)))
have rw : 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)))
  (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)))
  (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: rw [← this]