-- 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 : MonoidalLeftAction.{v_1, u_1, v_2, u_2} C D
c₁ c₂ c₃ c₄ : C
d₁ d₂ : D
f : c₁ ⟶ c₂
g : c₃ ⟶ c₄
h : d₁ ⟶ d₂
rw :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₂
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₄ d₂))
    (f ⊙ₗₘ g ⊙ₗₘ h) ((Iso.inv (αₗ c₁ c₃ d₁) ≫ ((f ⊗ₘ g) ⊙ₗₘ h)) ≫ Iso.hom (αₗ c₂ c₄ d₂))
rw₁ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₂
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₄ d₂))
    (f ⊙ₗₘ g ⊙ₗₘ h) (Iso.inv (αₗ c₁ c₃ d₁) ≫ ((f ⊗ₘ g) ⊙ₗₘ h) ≫ Iso.hom (αₗ c₂ c₄ d₂))
rw₂ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₂
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₄ d₂))
    (Iso.inv (αₗ c₁ c₃ d₁) ≫ ((f ⊗ₘ g) ⊙ₗₘ h) ≫ Iso.hom (αₗ c₂ c₄ d₂)) (f ⊙ₗₘ g ⊙ₗₘ h)
rw₃ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₃)
        d₁ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₂
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₄ d₂))
    (((f ⊗ₘ g) ⊙ₗₘ h) ≫ Iso.hom (αₗ c₂ c₄ d₂)) (Iso.hom (αₗ c₁ c₃ d₁) ≫ (f ⊙ₗₘ g ⊙ₗₘ h))
rw₄ rw₅ :
  Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₃)
        d₁ ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₂
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₄ d₂))
    (Iso.hom (αₗ c₁ c₃ d₁) ≫ (f ⊙ₗₘ g ⊙ₗₘ h)) (Iso.hom (αₗ c₁ c₃ d₁) ≫ (f ⊙ₗₘ g ⊙ₗₘ h))
⊢ Eq (α :=
    @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₁
        (@actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _ c₃ d₁) ⟶
      @actionObj.{v_1, u_1, v_2, u_2} _ _ inst inst_1 toMonoidalCategoryStruct _
        (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₄) d₂)
    ((f ⊙ₗₘ g ⊙ₗₘ h) ≫ Iso.inv (αₗ c₂ c₄ d₂)) (Iso.inv (αₗ c₁ c₃ d₁) ≫ ((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.MonoidalLeftAction.actionAssocIso_hom_naturality, Eq.comm