-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.DayConvolution (hypothesis)
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
U : Functor.{v₁, v₂, u₁, u₂} C V
inst_4 : DayConvolutionUnit U
F : Functor.{v₁, v₂, u₁, u₂} C V
inst_5 :
  ∀ (v : V) (d : C),
    Limits.PreservesColimitsOfShape.{0, v₁, v₂, v₂, u₂, u₂}
      (CostructuredArrow (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst))) d) (tensorLeft v)
inst_6 : DayConvolution F U
x : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x) (tensorUnit.{v₂, u₂} V (𝒞 := inst_1)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (CategoryStruct.comp (Y :=
      tensorObj.{v₂, u₂} (𝒞 := inst_1) (F.obj x) ((F, U).2.obj (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) (F.obj x ◁ can)
      (CategoryStruct.comp (Y :=
        (tensor C ⋙ @DayConvolution.convolution _ _ _ _ inst_2 inst_3 F U _).obj (x, tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (NatTrans.app (DayConvolution.unit F U) (x, tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (NatTrans.app (Iso.hom (rightUnitor U F))
          (tensorObj.{v₁, u₁} (𝒞 := inst) x (tensorUnit.{v₁, u₁} C (𝒞 := inst))))))
    (Iso.hom (ρ_ (F.obj x)) ≫ F.map (Iso.inv (ρ_ x)))
have this : Eq.{v₂ + 1} (α :=
  (Opposite.unop (Opposite.op (F ⊠ fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1))))).obj
      (x, { as := PUnit.unit : Discrete PUnit.{1} }) ⟶
    (obj
          (obj (whiskeringLeft (C × Discrete PUnit.{1}) (C × C) V)
            (Functor.prod (𝟭 C) (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst)))))
          (obj (obj (whiskeringLeft (C × C) C V) (tensor C)) F)).obj
      (x, { as := PUnit.unit }))
  ((fun
        (t :
          (obj (whiskeringLeft (C × C) C V) (tensor C) ⋙
                obj (whiskeringLeft (C × Discrete PUnit.{1}) (C × C) V)
                    (Functor.prod (𝟭 C) (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ⋙
                  obj coyoneda (Opposite.op (F ⊠ fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1))))).obj
            F) ↦
      (t.app (x, { as := PUnit.unit }) :
        (Opposite.unop (Opposite.op (F ⊠ fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1))))).obj
            (x, { as := PUnit.unit : Discrete PUnit.{1} }) ⟶
          (obj
                (obj (whiskeringLeft (C × Discrete PUnit.{1}) (C × C) V)
                  (Functor.prod (𝟭 C) (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst)))))
                (obj (obj (whiskeringLeft (C × C) C V) (tensor C)) F)).obj
            (x, { as := PUnit.unit })))
    ((CorepresentableBy.homEquiv (corepresentableByRight U F) :
        (a : F ⊛ U ⟶ F) →
          ((whiskeringLeft (C × C) C V).obj (tensor C) ⋙
                (whiskeringLeft (C × Discrete PUnit.{1}) (C × C) V).obj ((𝟭 C).prod (fromPUnit (𝟙_ C))) ⋙
                  coyoneda.obj (Opposite.op (F ⊠ fromPUnit (𝟙_ V)))).obj
            F)
      ((Equiv.symm (CorepresentableBy.homEquiv (corepresentableByRight U F)) :
          (a :
              ((whiskeringLeft (C × C) C V).obj (tensor C) ⋙
                    (whiskeringLeft (C × Discrete PUnit.{1}) (C × C) V).obj ((𝟭 C).prod (fromPUnit (𝟙_ C))) ⋙
                      coyoneda.obj (Opposite.op (F ⊠ fromPUnit (𝟙_ V)))).obj
                F) →
            F ⊛ U ⟶ F)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (Iso.hom (Iso.symm (rightUnitorCorepresentingIso F))) F) :
            (a : (fun (X : Type (max u₁ v₂)) ↦ X) ((coyoneda.obj (Opposite.op F)).obj F)) →
              (fun (X : Type (max u₁ v₂)) ↦ X)
                (((whiskeringLeft (C × C) C V).obj (tensor C) ⋙
                      (whiskeringLeft (C × Discrete PUnit.{1}) (C × C) V).obj ((𝟭 C).prod (fromPUnit (𝟙_ C))) ⋙
                        coyoneda.obj (Opposite.op (F ⊠ fromPUnit (𝟙_ V)))).obj
                  F))
          (𝟙 (Opposite.unop (Opposite.op F)))))))
  ((fun
        (t :
          (obj (whiskeringLeft (C × C) C V) (tensor C) ⋙
                obj (whiskeringLeft (C × Discrete PUnit.{1}) (C × C) V)
                    (Functor.prod (𝟭 C) (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ⋙
                  obj coyoneda (Opposite.op (F ⊠ fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1))))).obj
            F) ↦
      (t.app (x, { as := PUnit.unit }) :
        (Opposite.unop (Opposite.op (F ⊠ fromPUnit (tensorUnit.{v₂, u₂} V (𝒞 := inst_1))))).obj
            (x, { as := PUnit.unit : Discrete PUnit.{1} }) ⟶
          (obj
                (obj (whiskeringLeft (C × Discrete PUnit.{1}) (C × C) V)
                  (Functor.prod (𝟭 C) (fromPUnit (tensorUnit.{v₁, u₁} C (𝒞 := inst)))))
                (obj (obj (whiskeringLeft (C × C) C V) (tensor C)) F)).obj
            (x, { as := PUnit.unit })))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (Iso.hom (Iso.symm (rightUnitorCorepresentingIso F))) F) :
        (a : (fun (X : Type (max u₁ v₂)) ↦ X) ((coyoneda.obj (Opposite.op F)).obj F)) →
          (fun (X : Type (max u₁ v₂)) ↦ X)
            (((whiskeringLeft (C × C) C V).obj (tensor C) ⋙
                  (whiskeringLeft (C × Discrete PUnit.{1}) (C × C) V).obj ((𝟭 C).prod (fromPUnit (𝟙_ C))) ⋙
                    coyoneda.obj (Opposite.op (F ⊠ fromPUnit (𝟙_ V)))).obj
              F))
      (𝟙 (Opposite.unop (Opposite.op F)))))
Tactic: have := congrArg (fun t ↦ t.app (x, .mk PUnit.unit)) <|
      (corepresentableByRight U F).homEquiv.rightInverse_symm <|
        ((rightUnitorCorepresentingIso F).symm.hom.app F) (𝟙 _)