awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)

Tactic:
simpa [-associator_actionHom] using
      (IsIso.inv_eq_inv.mpr <| associator_actionHom c₁ c₂ c₃ d).symm =≫
        (α_ c₁ c₂ c₃).hom ⊵ₗ d

Premises used: Iff.mpr, CategoryTheory.IsIso.inv_eq_inv, CategoryTheory.MonoidalCategory.MonoidalLeftAction.associator_actionHom, CategoryTheory.MonoidalCategoryStruct.associator, Eq.symm, CategoryTheory.Iso.hom
-- 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
x : C
h :
  Eq (α :=
    Quiver.Hom (V := Functor.{v_2, v_2, u_2, u_2} D D) (unmop (Functor.obj (curriedActionMop C D) x))
      (unmop
        (tensorObj (𝒞 := monoidalOppositeCategory)
          ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := monoidalOppositeCategory))
          (Functor.obj (curriedActionMop C D) x))))
    (Quiver.Hom.unmop (Iso.inv (λ_ (Functor.obj (curriedActionMop C D) x))))
    (Quiver.Hom.unmop
      (CategoryStruct.comp (Y :=
        Functor.obj (curriedActionMop C D) (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x))
        (Functor.map (curriedActionMop C D) (Iso.inv (λ_ x)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := monoidalOppositeCategory)
            (Functor.obj (curriedActionMop C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
            (Functor.obj (curriedActionMop C D) x))
          (Quiver.Hom.mop
            { app := fun (x_1 : D) ↦ Iso.hom (αₗ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x x_1), naturality := ⋯ })
          (Quiver.Hom.mop (Iso.hom (actionUnitNatIso C D)) ▷ Functor.obj (curriedActionMop C D) x))))
⊢ Eq (α :=
    Quiver.Hom (V := (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (Functor.obj (curriedActionMop C D) x)
      (tensorObj (𝒞 := monoidalOppositeCategory)
        ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := monoidalOppositeCategory))
        (Functor.obj (curriedActionMop C D) x)))
    (Iso.inv (λ_ (Functor.obj (curriedActionMop C D) x)))
    (CategoryStruct.comp (Y :=
      Functor.obj (curriedActionMop C D) (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x))
      (Functor.map (curriedActionMop C D) (Iso.inv (λ_ x)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := monoidalOppositeCategory)
          (Functor.obj (curriedActionMop C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
          (Functor.obj (curriedActionMop C D) x))
        (Quiver.Hom.mop
          { app := fun (x_1 : D) ↦ Iso.hom (αₗ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x x_1), naturality := ⋯ })
        (Quiver.Hom.mop (Iso.hom (actionUnitNatIso C D)) ▷ Functor.obj (curriedActionMop C D) x)))

Tactic:
apply MonoidalOpposite.hom_ext

Premises used: CategoryTheory.MonoidalOpposite.hom_ext
-- 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
x : C
h :
  ∀ (t : D),
    Eq.{v_2 + 1} (α :=
      Functor.obj.{v_2, v_2, u_2, u_2} (unmop (Functor.obj (curriedActionMop C D) x)) t ⟶
        Functor.obj.{v_2, v_2, u_2, u_2}
          (unmop
            (tensorObj (𝒞 := monoidalOppositeCategory)
              ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := monoidalOppositeCategory))
              (Functor.obj (curriedActionMop C D) x)))
          t)
      (NatTrans.app (Quiver.Hom.unmop (Iso.inv (λ_ (Functor.obj (curriedActionMop C D) x)))) t)
      (NatTrans.app
        (Quiver.Hom.unmop
          (CategoryStruct.comp (Y :=
            Functor.obj (curriedActionMop C D)
              (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x))
            (Functor.map (curriedActionMop C D) (Iso.inv (λ_ x)))
            (CategoryStruct.comp (Y :=
              tensorObj (𝒞 := monoidalOppositeCategory)
                (Functor.obj (curriedActionMop C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
                (Functor.obj (curriedActionMop C D) x))
              (Quiver.Hom.mop
                { app := fun (x_1 : D) ↦ Iso.hom (αₗ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x x_1), naturality := ⋯ })
              (Quiver.Hom.mop (Iso.hom (actionUnitNatIso C D)) ▷ Functor.obj (curriedActionMop C D) x))))
        t)
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v_2, v_2, u_2, u_2} D D) (unmop (Functor.obj (curriedActionMop C D) x))
      (unmop
        (tensorObj (𝒞 := monoidalOppositeCategory)
          ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := monoidalOppositeCategory))
          (Functor.obj (curriedActionMop C D) x))))
    (Quiver.Hom.unmop (Iso.inv (λ_ (Functor.obj (curriedActionMop C D) x))))
    (Quiver.Hom.unmop
      (CategoryStruct.comp (Y :=
        Functor.obj (curriedActionMop C D) (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x))
        (Functor.map (curriedActionMop C D) (Iso.inv (λ_ x)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := monoidalOppositeCategory)
            (Functor.obj (curriedActionMop C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
            (Functor.obj (curriedActionMop C D) x))
          (Quiver.Hom.mop
            { app := fun (x_1 : D) ↦ Iso.hom (αₗ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x x_1), naturality := ⋯ })
          (Quiver.Hom.mop (Iso.hom (actionUnitNatIso C D)) ▷ Functor.obj (curriedActionMop C D) x))))

Tactic:
ext t
-- 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
x : C
t : D
⊢ Eq.{v_2 + 1} (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (unmop (Functor.obj (curriedActionMop C D) x)) t ⟶
      Functor.obj.{v_2, v_2, u_2, u_2}
        (unmop
          (tensorObj (𝒞 := monoidalOppositeCategory)
            ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := monoidalOppositeCategory))
            (Functor.obj (curriedActionMop C D) x)))
        t)
    (NatTrans.app (Quiver.Hom.unmop (Iso.inv (λ_ (Functor.obj (curriedActionMop C D) x)))) t)
    (NatTrans.app
      (Quiver.Hom.unmop
        (CategoryStruct.comp (Y :=
          Functor.obj (curriedActionMop C D) (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x))
          (Functor.map (curriedActionMop C D) (Iso.inv (λ_ x)))
          (CategoryStruct.comp (Y :=
            tensorObj (𝒞 := monoidalOppositeCategory)
              (Functor.obj (curriedActionMop C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
              (Functor.obj (curriedActionMop C D) x))
            (Quiver.Hom.mop
              { app := fun (x_1 : D) ↦ Iso.hom (αₗ (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x x_1), naturality := ⋯ })
            (Quiver.Hom.mop (Iso.hom (actionUnitNatIso C D)) ▷ Functor.obj (curriedActionMop C D) x))))
      t)

Tactic:
simpa [-leftUnitor_actionHom] using
      (λ_ x).inv ⊵ₗ t ≫= leftUnitor_actionHom x t

Premises used: CategoryTheory.MonoidalCategoryStruct.leftUnitor, CategoryTheory.MonoidalCategory.MonoidalLeftAction.leftUnitor_actionHom, CategoryTheory.Iso.inv
-- 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
x : C
h :
  Eq (α :=
    Quiver.Hom (V := Functor.{v_2, v_2, u_2, u_2} D D) (unmop (Functor.obj (curriedActionMop C D) x))
      (unmop
        (tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) x)
          ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := monoidalOppositeCategory)))))
    (Quiver.Hom.unmop (Iso.inv (ρ_ (Functor.obj (curriedActionMop C D) x))))
    (Quiver.Hom.unmop
      (CategoryStruct.comp (Y :=
        Functor.obj (curriedActionMop C D) (tensorObj.{v_1, u_1} (𝒞 := inst) x (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (Functor.map (curriedActionMop C D) (Iso.inv (ρ_ x)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) x)
            (Functor.obj (curriedActionMop C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
          (Quiver.Hom.mop
            { app := fun (x_1 : D) ↦ Iso.hom (αₗ x (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x_1), naturality := ⋯ })
          (Functor.obj (curriedActionMop C D) x ◁ Quiver.Hom.mop (Iso.hom (actionUnitNatIso C D))))))
⊢ Eq (α :=
    Quiver.Hom (V := (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (Functor.obj (curriedActionMop C D) x)
      (tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) x)
        ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := monoidalOppositeCategory))))
    (Iso.inv (ρ_ (Functor.obj (curriedActionMop C D) x)))
    (CategoryStruct.comp (Y :=
      Functor.obj (curriedActionMop C D) (tensorObj.{v_1, u_1} (𝒞 := inst) x (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
      (Functor.map (curriedActionMop C D) (Iso.inv (ρ_ x)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) x)
          (Functor.obj (curriedActionMop C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (Quiver.Hom.mop
          { app := fun (x_1 : D) ↦ Iso.hom (αₗ x (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x_1), naturality := ⋯ })
        (Functor.obj (curriedActionMop C D) x ◁ Quiver.Hom.mop (Iso.hom (actionUnitNatIso C D)))))

Tactic:
apply MonoidalOpposite.hom_ext

Premises used: CategoryTheory.MonoidalOpposite.hom_ext
-- 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
x : C
h :
  ∀ (t : D),
    Eq.{v_2 + 1} (α :=
      Functor.obj.{v_2, v_2, u_2, u_2} (unmop (Functor.obj (curriedActionMop C D) x)) t ⟶
        Functor.obj.{v_2, v_2, u_2, u_2}
          (unmop
            (tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) x)
              ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := monoidalOppositeCategory))))
          t)
      (NatTrans.app (Quiver.Hom.unmop (Iso.inv (ρ_ (Functor.obj (curriedActionMop C D) x)))) t)
      (NatTrans.app
        (Quiver.Hom.unmop
          (CategoryStruct.comp (Y :=
            Functor.obj (curriedActionMop C D)
              (tensorObj.{v_1, u_1} (𝒞 := inst) x (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
            (Functor.map (curriedActionMop C D) (Iso.inv (ρ_ x)))
            (CategoryStruct.comp (Y :=
              tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) x)
                (Functor.obj (curriedActionMop C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
              (Quiver.Hom.mop
                { app := fun (x_1 : D) ↦ Iso.hom (αₗ x (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x_1), naturality := ⋯ })
              (Functor.obj (curriedActionMop C D) x ◁ Quiver.Hom.mop (Iso.hom (actionUnitNatIso C D))))))
        t)
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v_2, v_2, u_2, u_2} D D) (unmop (Functor.obj (curriedActionMop C D) x))
      (unmop
        (tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) x)
          ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := monoidalOppositeCategory)))))
    (Quiver.Hom.unmop (Iso.inv (ρ_ (Functor.obj (curriedActionMop C D) x))))
    (Quiver.Hom.unmop
      (CategoryStruct.comp (Y :=
        Functor.obj (curriedActionMop C D) (tensorObj.{v_1, u_1} (𝒞 := inst) x (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (Functor.map (curriedActionMop C D) (Iso.inv (ρ_ x)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) x)
            (Functor.obj (curriedActionMop C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
          (Quiver.Hom.mop
            { app := fun (x_1 : D) ↦ Iso.hom (αₗ x (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x_1), naturality := ⋯ })
          (Functor.obj (curriedActionMop C D) x ◁ Quiver.Hom.mop (Iso.hom (actionUnitNatIso C D))))))

Tactic:
ext t
-- 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
x : C
t : D
⊢ Eq.{v_2 + 1} (α :=
    Functor.obj.{v_2, v_2, u_2, u_2} (unmop (Functor.obj (curriedActionMop C D) x)) t ⟶
      Functor.obj.{v_2, v_2, u_2, u_2}
        (unmop
          (tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) x)
            ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := monoidalOppositeCategory))))
        t)
    (NatTrans.app (Quiver.Hom.unmop (Iso.inv (ρ_ (Functor.obj (curriedActionMop C D) x)))) t)
    (NatTrans.app
      (Quiver.Hom.unmop
        (CategoryStruct.comp (Y :=
          Functor.obj (curriedActionMop C D) (tensorObj.{v_1, u_1} (𝒞 := inst) x (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
          (Functor.map (curriedActionMop C D) (Iso.inv (ρ_ x)))
          (CategoryStruct.comp (Y :=
            tensorObj (𝒞 := monoidalOppositeCategory) (Functor.obj (curriedActionMop C D) x)
              (Functor.obj (curriedActionMop C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
            (Quiver.Hom.mop
              { app := fun (x_1 : D) ↦ Iso.hom (αₗ x (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x_1), naturality := ⋯ })
            (Functor.obj (curriedActionMop C D) x ◁ Quiver.Hom.mop (Iso.hom (actionUnitNatIso C D))))))
      t)

Tactic:
simpa [-rightUnitor_actionHom] using
      (ρ_ x).inv ⊵ₗ t ≫= rightUnitor_actionHom x t

Premises used: CategoryTheory.MonoidalCategoryStruct.rightUnitor, CategoryTheory.MonoidalCategory.MonoidalLeftAction.rightUnitor_actionHom, CategoryTheory.Iso.inv
-- 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
F : C ⥤ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ
inst_3 : F.Monoidal
c₁ c₁' c₂ c₂' : C
c₃ c₃' : D
f : c₁ ⟶ c₁'
g : c₂ ⟶ c₂'
h : c₃ ⟶ c₃'
⊢ Eq.{v_2 + 1} (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂)).unmop.obj c₃ ⟶
      (tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c₁') (F.obj c₂')).unmop.obj c₃)
    ((fun
          (t :
            F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) ⟶
              tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c₁') (F.obj c₂')) ↦
        t.unmop.app c₃)
      (Functor.OplaxMonoidal.δ F c₁ c₂ ≫ (F.map f ⊗ₘ F.map g)))
    ((fun
          (t :
            F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) ⟶
              tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c₁') (F.obj c₂')) ↦
        t.unmop.app c₃)
      (F.map (f ⊗ₘ g) ≫ Functor.OplaxMonoidal.δ F c₁' c₂'))

Tactic:
have e := congrArg (fun t ↦ t.unmop.app c₃) <|
      Functor.OplaxMonoidal.δ_natural F f g
-- 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
F : C ⥤ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ
inst_3 : F.Monoidal
c₁ c₁' c₂ c₂' : C
c₃ c₃' : D
f : c₁ ⟶ c₁'
g : c₂ ⟶ c₂'
h : c₃ ⟶ c₃'
e :
  Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂)).unmop.obj c₃ ⟶ (F.obj c₁').unmop.obj ((F.obj c₂').unmop.obj c₃))
    (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c₁ c₂)) c₃ ≫
      (F.map f).unmop.app ((F.obj c₂).unmop.obj c₃) ≫ (F.obj c₁').unmop.map ((F.map g).unmop.app c₃))
    (NatTrans.app (Quiver.Hom.unmop (F.map (f ⊗ₘ g))) c₃ ≫
      NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c₁' c₂')) c₃)
⊢ Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂)).unmop.obj c₃ ⟶ (F.obj c₁').unmop.obj ((F.obj c₂').unmop.obj c₃'))
    (CategoryStruct.comp (Y := (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c₁' c₂')).unmop.obj c₃')
      (CategoryStruct.comp (Y :=
        (fun (c : C) (d : D) ↦ (F.obj c).unmop.obj d) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁' c₂') c₃)
        ((fun {c c' : C} (f : c ⟶ c') (d : D) ↦ (F.map f).unmop.app d) (f ⊗ₘ g) c₃)
        ((fun (c : C) (x x_1 : D) (f : x ⟶ x_1) ↦ (F.obj c).unmop.map f) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁' c₂') c₃
          c₃' h))
      (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F c₁' c₂')) c₃'))))
    (CategoryStruct.comp (Y := (F.obj c₁).unmop.obj ((F.obj c₂).unmop.obj c₃))
      (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F c₁ c₂)) c₃)))
      (CategoryStruct.comp (Y := (fun (c : C) (d : D) ↦ (F.obj c).unmop.obj d) c₁' ((F.obj c₂).unmop.obj c₃))
        ((fun {c c' : C} (f : c ⟶ c') (d : D) ↦ (F.map f).unmop.app d) f ((F.obj c₂).unmop.obj c₃))
        ((fun (c : C) (x x_1 : D) (f : x ⟶ x_1) ↦ (F.obj c).unmop.map f) c₁' ((F.obj c₂).unmop.obj c₃)
          ((F.obj c₂').unmop.obj c₃')
          (CategoryStruct.comp (Y := (fun (c : C) (d : D) ↦ (F.obj c).unmop.obj d) c₂' c₃)
            ((fun {c c' : C} (f : c ⟶ c') (d : D) ↦ (F.map f).unmop.app d) g c₃)
            ((fun (c : C) (x x_1 : D) (f : x ⟶ x_1) ↦ (F.obj c).unmop.map f) c₂' c₃ c₃' h)))))

Tactic:
simp [reassoc_of% e]
-- 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
F : C ⥤ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ
inst_3 : F.Monoidal
c x y : C
f : x ⟶ y
d : D
⊢ Eq.{v_2 + 1} (α :=
    (tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c) (F.obj x)).unmop.obj d ⟶
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c y)).unmop.obj d)
    ((fun
          (t :
            tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c) (F.obj x) ⟶
              F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c y)) ↦
        t.unmop.app d)
      (F.obj c ◁ F.map f ≫ Functor.LaxMonoidal.μ F c y))
    ((fun
          (t :
            tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c) (F.obj x) ⟶
              F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c y)) ↦
        t.unmop.app d)
      (Functor.LaxMonoidal.μ F c x ≫ F.map (c ◁ f)))

Tactic:
have e := congrArg (fun t ↦ t.unmop.app d) <|
      Functor.LaxMonoidal.μ_natural_right F c f
-- 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
F : C ⥤ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ
inst_3 : F.Monoidal
c x y : C
f : x ⟶ y
d : D
e :
  Eq (α := (F.obj c).unmop.obj ((F.obj x).unmop.obj d) ⟶ (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c y)).unmop.obj d)
    ((F.obj c).unmop.map ((F.map f).unmop.app d) ≫ NatTrans.app (Quiver.Hom.unmop (Functor.LaxMonoidal.μ F c y)) d)
    (NatTrans.app (Quiver.Hom.unmop (Functor.LaxMonoidal.μ F c x)) d ≫
      NatTrans.app (Quiver.Hom.unmop (F.map (c ◁ f))) d)
⊢ Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c x)).unmop.obj d ⟶
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c y)).unmop.obj d)
    (NatTrans.app (Quiver.Hom.unmop (F.map (c ◁ f))) d)
    (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F c x)) d)) ≫
      (F.obj c).unmop.map ((F.map f).unmop.app d) ≫
        Iso.inv (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F c y)) d)))

Tactic:
simp [e, ← NatTrans.comp_app, ← unmop_comp]

Premises used: CategoryTheory.unmop_comp, CategoryTheory.NatTrans.comp_app
-- 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
F : C ⥤ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ
inst_3 : F.Monoidal
x y c : C
f : x ⟶ y
d : D
⊢ Eq.{v_2 + 1} (α :=
    (tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj x) (F.obj c)).unmop.obj d ⟶
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) y c)).unmop.obj d)
    ((fun
          (t :
            tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj x) (F.obj c) ⟶
              F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) y c)) ↦
        t.unmop.app d)
      (F.map f ▷ F.obj c ≫ Functor.LaxMonoidal.μ F y c))
    ((fun
          (t :
            tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj x) (F.obj c) ⟶
              F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) y c)) ↦
        t.unmop.app d)
      (Functor.LaxMonoidal.μ F x c ≫ F.map (f ▷ c)))

Tactic:
have e := congrArg (fun t ↦ t.unmop.app d) <|
      Functor.LaxMonoidal.μ_natural_left F f c
-- 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
F : C ⥤ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ
inst_3 : F.Monoidal
x y c : C
f : x ⟶ y
d : D
e :
  Eq (α := (F.obj x).unmop.obj ((F.obj c).unmop.obj d) ⟶ (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) y c)).unmop.obj d)
    ((F.map f).unmop.app ((F.obj c).unmop.obj d) ≫ NatTrans.app (Quiver.Hom.unmop (Functor.LaxMonoidal.μ F y c)) d)
    (NatTrans.app (Quiver.Hom.unmop (Functor.LaxMonoidal.μ F x c)) d ≫
      NatTrans.app (Quiver.Hom.unmop (F.map (f ▷ c))) d)
⊢ Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) x c)).unmop.obj d ⟶
      (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) y c)).unmop.obj d)
    (NatTrans.app (Quiver.Hom.unmop (F.map (f ▷ c))) d)
    (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F x c)) d)) ≫
      (F.map f).unmop.app ((F.obj c).unmop.obj d) ≫
        Iso.inv (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F y c)) d)))

Tactic:
simp [e, ← NatTrans.comp_app, ← unmop_comp]

Premises used: CategoryTheory.unmop_comp, CategoryTheory.NatTrans.comp_app