-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Action.End (goal)
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
⊢ Eq (α :=
    Quiver.Hom (V := (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 (curriedActionMop C D)
        (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃))))
    (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₃))))
    (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 := ⋯ }))
have apply : 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 := sorry } ▷
        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 := sorry } ≫
        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 := sorry })
        (Quiver.Hom.mop
          { app := fun (x : D) ↦ Iso.inv (αₗ c₁ (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃) x), naturality := sorry })))
Tactic: apply (mopEquiv (D ⥤ D)).fullyFaithfulInverse.map_injective