-- Module: Mathlib.CategoryTheory.Monoidal.Action.End
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} D
inst_3 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c₁ c₂ c₃ : C
w :
  ∀ (d : D),
    Eq.{v_2 + 1} (α :=
      Functor.obj.{v_2, v_2, u_2, u_2}
          (Functor.obj (Equivalence.inverse (mopEquiv (Functor.{v_2, v_2, u_2, u_2} D D)))
            (tensorObj (𝒞 := monoidalOppositeCategory)
              (tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) c₁)
                (Functor.obj (curriedActionMop C D) c₂))
              (Functor.obj (curriedActionMop C D) c₃)))
          d ⟶
        Functor.obj.{v_2, v_2, u_2, u_2}
          (Functor.obj (Equivalence.inverse (mopEquiv (Functor.{v_2, v_2, u_2, u_2} D D)))
            (Functor.obj (curriedActionMop C D)
              (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃))))
          d)
      (NatTrans.app
        (Functor.map (Equivalence.inverse (mopEquiv (Functor.{v_2, v_2, u_2, u_2} D D)))
          (CategoryStruct.comp (Y :=
            tensorObj (𝒞 := monoidalOppositeCategory)
              (Functor.obj (curriedActionMop C D) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂))
              (Functor.obj (curriedActionMop C D) c₃))
            (Quiver.Hom.mop { app := fun (x : D) ↦ Iso.inv (αₗ c₁ c₂ x), naturality := ⋯ } ▷
              Functor.obj (curriedActionMop C D) c₃)
            (Quiver.Hom.mop
                { app := fun (x : D) ↦ Iso.inv (αₗ (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃ x), naturality := ⋯ } ≫
              Functor.map (curriedActionMop C D) (Iso.hom (α_ c₁ c₂ c₃)))))
        d)
      (NatTrans.app
        (Functor.map (Equivalence.inverse (mopEquiv (Functor.{v_2, v_2, u_2, u_2} D D)))
          (Iso.hom
              (α_ (Functor.obj (curriedActionMop C D) c₁) (Functor.obj (curriedActionMop C D) c₂)
                (Functor.obj (curriedActionMop C D) c₃)) ≫
            CategoryStruct.comp (Y :=
              tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) c₁)
                (Functor.obj (curriedActionMop C D) (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃)))
              (Functor.obj (curriedActionMop C D) c₁ ◁
                Quiver.Hom.mop { app := fun (x : D) ↦ Iso.inv (αₗ c₂ c₃ x), naturality := ⋯ })
              (Quiver.Hom.mop
                { app := fun (x : D) ↦ Iso.inv (αₗ c₁ (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃) x), naturality := ⋯ })))
        d)
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v_2, v_2, u_2, u_2} D D)
      (Functor.obj (Equivalence.inverse (mopEquiv (Functor.{v_2, v_2, u_2, u_2} D D)))
        (tensorObj (𝒞 := monoidalOppositeCategory)
          (tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) c₁)
            (Functor.obj (curriedActionMop C D) c₂))
          (Functor.obj (curriedActionMop C D) c₃)))
      (Functor.obj (Equivalence.inverse (mopEquiv (Functor.{v_2, v_2, u_2, u_2} D D)))
        (Functor.obj (curriedActionMop C D)
          (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃)))))
    (Functor.map (Equivalence.inverse (mopEquiv (Functor.{v_2, v_2, u_2, u_2} D D)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := monoidalOppositeCategory)
          (Functor.obj (curriedActionMop C D) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂))
          (Functor.obj (curriedActionMop C D) c₃))
        (Quiver.Hom.mop { app := fun (x : D) ↦ Iso.inv (αₗ c₁ c₂ x), naturality := ⋯ } ▷
          Functor.obj (curriedActionMop C D) c₃)
        (Quiver.Hom.mop
            { app := fun (x : D) ↦ Iso.inv (αₗ (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃ x), naturality := ⋯ } ≫
          Functor.map (curriedActionMop C D) (Iso.hom (α_ c₁ c₂ c₃)))))
    (Functor.map (Equivalence.inverse (mopEquiv (Functor.{v_2, v_2, u_2, u_2} D D)))
      (Iso.hom
          (α_ (Functor.obj (curriedActionMop C D) c₁) (Functor.obj (curriedActionMop C D) c₂)
            (Functor.obj (curriedActionMop C D) c₃)) ≫
        CategoryStruct.comp (Y :=
          tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) c₁)
            (Functor.obj (curriedActionMop C D) (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃)))
          (Functor.obj (curriedActionMop C D) c₁ ◁
            Quiver.Hom.mop { app := fun (x : D) ↦ Iso.inv (αₗ c₂ c₃ x), naturality := ⋯ })
          (Quiver.Hom.mop
            { app := fun (x : D) ↦ Iso.inv (αₗ c₁ (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃) x), naturality := ⋯ })))

Tactic:
ext d