-- 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 : MonoidalRightAction.{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}
          (tensorObj (𝒞 := Functor.category)
            (tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) c₁)
              (Functor.obj (curriedAction C D) c₂))
            (Functor.obj (curriedAction C D) c₃))
          d ⟶
        Functor.obj.{v_2, v_2, u_2, u_2}
          (Functor.obj (curriedAction C D)
            (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃)))
          d)
      (NatTrans.app
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂))
            (Functor.obj (curriedAction C D) c₃))
          ({ app := fun (x : D) ↦ Iso.inv (αᵣ x c₁ c₂), naturality := ⋯ } ▷ Functor.obj (curriedAction C D) c₃)
          ({ app := fun (x : D) ↦ Iso.inv (αᵣ x (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃), naturality := ⋯ } ≫
            Functor.map (curriedAction C D) (Iso.hom (α_ c₁ c₂ c₃))))
        d)
      (NatTrans.app
        (Iso.hom
            (α_ (Functor.obj (curriedAction C D) c₁) (Functor.obj (curriedAction C D) c₂)
              (Functor.obj (curriedAction C D) c₃)) ≫
          CategoryStruct.comp (Y :=
            tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) c₁)
              (Functor.obj (curriedAction C D) (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃)))
            (Functor.obj (curriedAction C D) c₁ ◁ { app := fun (x : D) ↦ Iso.inv (αᵣ x c₂ c₃), naturality := ⋯ })
            { app := fun (x : D) ↦ Iso.inv (αᵣ x c₁ (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃)), naturality := ⋯ })
        d)
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v_2, v_2, u_2, u_2} D D)
      (tensorObj (𝒞 := Functor.category)
        (tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) c₁) (Functor.obj (curriedAction C D) c₂))
        (Functor.obj (curriedAction C D) c₃))
      (Functor.obj (curriedAction C D) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃))))
    (CategoryStruct.comp (Y :=
      tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂))
        (Functor.obj (curriedAction C D) c₃))
      ({ app := fun (x : D) ↦ Iso.inv (αᵣ x c₁ c₂), naturality := ⋯ } ▷ Functor.obj (curriedAction C D) c₃)
      ({ app := fun (x : D) ↦ Iso.inv (αᵣ x (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃), naturality := ⋯ } ≫
        Functor.map (curriedAction C D) (Iso.hom (α_ c₁ c₂ c₃))))
    (Iso.hom
        (α_ (Functor.obj (curriedAction C D) c₁) (Functor.obj (curriedAction C D) c₂)
          (Functor.obj (curriedAction C D) c₃)) ≫
      CategoryStruct.comp (Y :=
        tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) c₁)
          (Functor.obj (curriedAction C D) (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃)))
        (Functor.obj (curriedAction C D) c₁ ◁ { app := fun (x : D) ↦ Iso.inv (αᵣ x c₂ c₃), naturality := ⋯ })
        { app := fun (x : D) ↦ Iso.inv (αᵣ x c₁ (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃)), naturality := ⋯ })

Tactic:
ext d