-- Module: Mathlib.CategoryTheory.Monoidal.Action.Basic
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
d₁ d₂ : D
c₁ c₂ c₃ c₄ : C
f : d₁ ⟶ d₂
g : c₁ ⟶ c₂
h : c₃ ⟶ c₄
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂ c₂) c₄)
    ((f ⊙ᵣₘ g) ⊙ᵣₘ h) ((Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h)) ≫ Iso.hom (αᵣ d₂ c₂ c₄))
rw₁ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂ c₂) c₄)
    ((f ⊙ᵣₘ g) ⊙ᵣₘ h) (Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h) ≫ Iso.hom (αᵣ d₂ c₂ c₄))
rw₂ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂ c₂) c₄)
    (Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h) ≫ Iso.hom (αᵣ d₂ c₂ c₄)) ((f ⊙ᵣₘ g) ⊙ᵣₘ h)
rw₃ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁
        (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₃) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂ c₂) c₄)
    ((f ⊙ᵣₘ g ⊗ₘ h) ≫ Iso.hom (αᵣ d₂ c₂ c₄)) (Iso.hom (αᵣ d₁ c₁ c₃) ≫ ((f ⊙ᵣₘ g) ⊙ᵣₘ h))
rw₄ rw₅ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁
        (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₃) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂ c₂) c₄)
    (Iso.hom (αᵣ d₁ c₁ c₃) ≫ ((f ⊙ᵣₘ g) ⊙ᵣₘ h)) (Iso.hom (αᵣ d₁ c₁ c₃) ≫ ((f ⊙ᵣₘ g) ⊙ᵣₘ h))
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₁ c₁) c₃ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ d₂
        (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₄))
    (((f ⊙ᵣₘ g) ⊙ᵣₘ h) ≫ Iso.inv (αᵣ d₂ c₂ c₄)) (Iso.inv (αᵣ d₁ c₁ c₃) ≫ (f ⊙ᵣₘ g ⊗ₘ h))

Tactic:
rw [Iso.comp_inv_eq, Category.assoc, Eq.comm, Iso.inv_comp_eq, actionAssocIso_hom_naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.comp_inv_eq, CategoryTheory.Iso.inv_comp_eq, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocIso_hom_naturality, Eq.comm