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
F : C ⥤ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ
inst_3 : F.Monoidal
c₁ c₂ c₃ : C
d : D
⊢ Eq.{v_2 + 1} (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃)).unmop.obj d ⟶
      (tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c₁)
              (tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c₂) (F.obj c₃))).unmop.obj
        d)
    ((fun
          (t :
            F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃) ⟶
              tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c₁)
                (tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c₂) (F.obj c₃))) ↦
        t.unmop.app d)
      (Functor.OplaxMonoidal.δ F (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃ ≫
        Functor.OplaxMonoidal.δ F c₁ c₂ ▷ F.obj c₃ ≫ Iso.hom (α_ (F.obj c₁) (F.obj c₂) (F.obj c₃))))
    ((fun
          (t :
            F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃) ⟶
              tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c₁)
                (tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c₂) (F.obj c₃))) ↦
        t.unmop.app d)
      (F.map (Iso.hom (α_ c₁ c₂ c₃)) ≫
        Functor.OplaxMonoidal.δ F c₁ (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃) ≫
          F.obj c₁ ◁ Functor.OplaxMonoidal.δ F c₂ c₃))

Tactic:
have e := congrArg (fun t ↦ t.unmop.app d) <|
      Functor.OplaxMonoidal.associativity F c₁ c₂ 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
c₁ c₂ c₃ : C
d : D
e :
  Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃)).unmop.obj d ⟶
      (F.obj c₁).unmop.obj ((F.obj c₂).unmop.obj ((F.obj c₃).unmop.obj d)))
    (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃)) d ≫
      NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c₁ c₂)) ((F.obj c₃).unmop.obj d) ≫
        𝟙 ((F.obj c₁).unmop.obj ((F.obj c₂).unmop.obj ((F.obj c₃).unmop.obj d))))
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (α_ c₁ c₂ c₃)))) d ≫
      NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c₁ (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃))) d ≫
        (F.obj c₁).unmop.map (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c₂ c₃)) d))
⊢ Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃)).unmop.obj d ⟶
      (F.obj c₁).unmop.obj ((F.obj c₂).unmop.obj ((F.obj c₃).unmop.obj d)))
    (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃)) d ≫
      NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c₁ c₂)) ((F.obj c₃).unmop.obj d))
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (α_ c₁ c₂ c₃)))) d ≫
      NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c₁ (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃))) d ≫
        (F.obj c₁).unmop.map (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c₂ c₃)) d))

Tactic:
simp only [Category.comp_id] at e

Premises used: CategoryTheory.Category.comp_id
-- 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
d : D
e :
  Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃)).unmop.obj d ⟶
      (F.obj c₁).unmop.obj ((F.obj c₂).unmop.obj ((F.obj c₃).unmop.obj d)))
    (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃)) d ≫
      NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c₁ c₂)) ((F.obj c₃).unmop.obj d))
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (α_ c₁ c₂ c₃)))) d ≫
      NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c₁ (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃))) d ≫
        (F.obj c₁).unmop.map (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c₂ c₃)) d))
⊢ Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃)).unmop.obj d ⟶
      (F.obj c₁).unmop.obj ((F.obj c₂).unmop.obj ((F.obj c₃).unmop.obj d)))
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (α_ c₁ c₂ c₃)))) d ≫
      Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F c₁ (tensorObj.{v_1, u_1} (𝒞 := inst) c₂ c₃))) d)) ≫
        (F.obj c₁).unmop.map (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F c₂ c₃)) d))))
    (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F (tensorObj.{v_1, u_1} (𝒞 := inst) c₁ c₂) c₃)) d)) ≫
      Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F c₁ c₂)) ((F.obj c₃).unmop.obj d))))

Tactic:
simp [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 : C
d : D
⊢ Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c)).unmop.obj d ⟶
      (tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory)
              ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := MonoidalOpposite.monoidalOppositeCategory))
              (F.obj c)).unmop.obj
        d)
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (λ_ c)))) d ≫
      (fun
            (t :
              F.obj c ⟶
                tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory)
                  ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := MonoidalOpposite.monoidalOppositeCategory))
                  (F.obj c)) ↦
          t.unmop.app d)
        (Iso.inv (λ_ (F.obj c))))
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (λ_ c)))) d ≫
      (fun
            (t :
              F.obj c ⟶
                tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory)
                  ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := MonoidalOpposite.monoidalOppositeCategory))
                  (F.obj c)) ↦
          t.unmop.app d)
        (CategoryStruct.comp (Y := F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c))
          (F.map (Iso.inv (λ_ c)))
          (Functor.OplaxMonoidal.δ F (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c ≫ Functor.OplaxMonoidal.η F ▷ F.obj c)))

Tactic:
have e := (F.map (λ_ c).hom).unmop.app d ≫=
      (congrArg (fun t ↦ t.unmop.app d) <|
        Functor.OplaxMonoidal.left_unitality 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
c : C
d : D
e :
  Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c)).unmop.obj d ⟶
      (F.obj c).unmop.obj d)
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (λ_ c)))) d ≫ 𝟙 ((F.obj c).unmop.obj d))
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (λ_ c)))) d ≫
      CategoryStruct.comp (Y :=
        (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c)).unmop.obj d)
        (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.inv (λ_ c)))) d)
        (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c)) d ≫
          NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.η F)) ((F.obj c).unmop.obj d)))
⊢ Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c)).unmop.obj d ⟶
      (F.obj c).unmop.obj d)
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (λ_ c)))) d)
    (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c)) d ≫
      NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.η F)) ((F.obj c).unmop.obj d))

Tactic:
simp only [Category.comp_id, ← NatTrans.comp_app_assoc, ← unmop_comp,
      ← F.map_comp_assoc, Iso.hom_inv_id, Functor.map_id, Category.id_comp] at e

Premises used: CategoryTheory.NatTrans.comp_app_assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.unmop_comp, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp
-- 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
d : D
e :
  Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c)).unmop.obj d ⟶
      (F.obj c).unmop.obj d)
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (λ_ c)))) d)
    (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c)) d ≫
      NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.η F)) ((F.obj c).unmop.obj d))
⊢ Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c)).unmop.obj d ⟶
      (F.obj c).unmop.obj d)
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (λ_ c)))) d)
    (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F (tensorUnit.{v_1, u_1} C (𝒞 := inst)) c)) d)) ≫
      Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.εIso F)) ((F.obj c).unmop.obj d))))

Tactic:
simp [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 : C
d : D
⊢ Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c (tensorUnit.{v_1, u_1} C (𝒞 := inst)))).unmop.obj d ⟶
      (tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c)
              ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := MonoidalOpposite.monoidalOppositeCategory))).unmop.obj
        d)
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (ρ_ c)))) d ≫
      (fun
            (t :
              F.obj c ⟶
                tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c)
                  ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := MonoidalOpposite.monoidalOppositeCategory))) ↦
          t.unmop.app d)
        (Iso.inv (ρ_ (F.obj c))))
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (ρ_ c)))) d ≫
      (fun
            (t :
              F.obj c ⟶
                tensorObj (𝒞 := MonoidalOpposite.monoidalOppositeCategory) (F.obj c)
                  ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)ᴹᵒᵖ) (𝒞 := MonoidalOpposite.monoidalOppositeCategory))) ↦
          t.unmop.app d)
        (CategoryStruct.comp (Y := F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
          (F.map (Iso.inv (ρ_ c)))
          (Functor.OplaxMonoidal.δ F c (tensorUnit.{v_1, u_1} C (𝒞 := inst)) ≫ F.obj c ◁ Functor.OplaxMonoidal.η F)))

Tactic:
have e := (F.map (ρ_ c).hom).unmop.app d ≫=
      (congrArg (fun t ↦ t.unmop.app d) <|
        Functor.OplaxMonoidal.right_unitality 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
c : C
d : D
e :
  Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c (tensorUnit.{v_1, u_1} C (𝒞 := inst)))).unmop.obj d ⟶
      (F.obj c).unmop.obj d)
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (ρ_ c)))) d ≫ 𝟙 ((F.obj c).unmop.obj d))
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (ρ_ c)))) d ≫
      CategoryStruct.comp (Y :=
        (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c (tensorUnit.{v_1, u_1} C (𝒞 := inst)))).unmop.obj d)
        (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.inv (ρ_ c)))) d)
        (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c (tensorUnit.{v_1, u_1} C (𝒞 := inst)))) d ≫
          (F.obj c).unmop.map (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.η F)) d)))
⊢ Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c (tensorUnit.{v_1, u_1} C (𝒞 := inst)))).unmop.obj d ⟶
      (F.obj c).unmop.obj d)
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (ρ_ c)))) d)
    (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c (tensorUnit.{v_1, u_1} C (𝒞 := inst)))) d ≫
      (F.obj c).unmop.map (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.η F)) d))

Tactic:
simp only [Category.comp_id, ← NatTrans.comp_app_assoc, ← unmop_comp,
      ← F.map_comp_assoc, Iso.hom_inv_id, Functor.map_id, Category.id_comp] at e

Premises used: CategoryTheory.NatTrans.comp_app_assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.unmop_comp, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.Category.id_comp
-- 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
d : D
e :
  Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c (tensorUnit.{v_1, u_1} C (𝒞 := inst)))).unmop.obj d ⟶
      (F.obj c).unmop.obj d)
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (ρ_ c)))) d)
    (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.δ F c (tensorUnit.{v_1, u_1} C (𝒞 := inst)))) d ≫
      (F.obj c).unmop.map (NatTrans.app (Quiver.Hom.unmop (Functor.OplaxMonoidal.η F)) d))
⊢ Eq (α :=
    (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) c (tensorUnit.{v_1, u_1} C (𝒞 := inst)))).unmop.obj d ⟶
      (F.obj c).unmop.obj d)
    (NatTrans.app (Quiver.Hom.unmop (F.map (Iso.hom (ρ_ c)))) d)
    (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.μIso F c (tensorUnit.{v_1, u_1} C (𝒞 := inst)))) d)) ≫
      (F.obj c).unmop.map (Iso.hom (Iso.symm (Iso.app (Iso.unmop (Functor.Monoidal.εIso F)) d))))

Tactic:
simp [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
inst_3 : MonoidalRightAction.{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}
        (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)

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

Premises used: Iff.mpr, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_associator, CategoryTheory.IsIso.inv_eq_inv, 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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : C
w :
  ∀ (t : D),
    Eq.{v_2 + 1} (α :=
      Functor.obj.{v_2, v_2, u_2, u_2} (Functor.obj (curriedAction C D) x) t ⟶
        Functor.obj.{v_2, v_2, u_2, u_2}
          (tensorObj (𝒞 := Functor.category) ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)) (𝒞 := Functor.category))
            (Functor.obj (curriedAction C D) x))
          t)
      (NatTrans.app (Iso.inv (λ_ (Functor.obj (curriedAction C D) x))) t)
      (NatTrans.app
        (CategoryStruct.comp (Y :=
          Functor.obj (curriedAction C D) (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x))
          (Functor.map (curriedAction C D) (Iso.inv (λ_ x)))
          (CategoryStruct.comp (Y :=
            tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
              (Functor.obj (curriedAction C D) x))
            { app := fun (x_1 : D) ↦ Iso.hom (αᵣ x_1 (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x), naturality := ⋯ }
            (Iso.hom (actionUnitNatIso C D) ▷ Functor.obj (curriedAction C D) x)))
        t)
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v_2, v_2, u_2, u_2} D D) (Functor.obj (curriedAction C D) x)
      (tensorObj (𝒞 := Functor.category) ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)) (𝒞 := Functor.category))
        (Functor.obj (curriedAction C D) x)))
    (Iso.inv (λ_ (Functor.obj (curriedAction C D) x)))
    (CategoryStruct.comp (Y :=
      Functor.obj (curriedAction C D) (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x))
      (Functor.map (curriedAction C D) (Iso.inv (λ_ x)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
          (Functor.obj (curriedAction C D) x))
        { app := fun (x_1 : D) ↦ Iso.hom (αᵣ x_1 (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x), naturality := ⋯ }
        (Iso.hom (actionUnitNatIso C D) ▷ Functor.obj (curriedAction 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 : MonoidalRightAction.{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} (Functor.obj (curriedAction C D) x) t ⟶
      Functor.obj.{v_2, v_2, u_2, u_2}
        (tensorObj (𝒞 := Functor.category) ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)) (𝒞 := Functor.category))
          (Functor.obj (curriedAction C D) x))
        t)
    (NatTrans.app (Iso.inv (λ_ (Functor.obj (curriedAction C D) x))) t)
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        Functor.obj (curriedAction C D) (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x))
        (Functor.map (curriedAction C D) (Iso.inv (λ_ x)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst)))
            (Functor.obj (curriedAction C D) x))
          { app := fun (x_1 : D) ↦ Iso.hom (αᵣ x_1 (tensorUnit.{v_1, u_1} C (𝒞 := inst)) x), naturality := ⋯ }
          (Iso.hom (actionUnitNatIso C D) ▷ Functor.obj (curriedAction C D) x)))
      t)

Tactic:
simpa [-actionHom_leftUnitor] using
      t ⊴ᵣ (λ_ x).inv ≫= actionHom_leftUnitor x t

Premises used: CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_leftUnitor, CategoryTheory.MonoidalCategoryStruct.leftUnitor, 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 : MonoidalRightAction.{v_1, u_1, v_2, u_2} C D
x : C
w :
  ∀ (t : D),
    Eq.{v_2 + 1} (α :=
      Functor.obj.{v_2, v_2, u_2, u_2} (Functor.obj (curriedAction C D) x) t ⟶
        Functor.obj.{v_2, v_2, u_2, u_2}
          (tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) x)
            ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)) (𝒞 := Functor.category)))
          t)
      (NatTrans.app (Iso.inv (ρ_ (Functor.obj (curriedAction C D) x))) t)
      (NatTrans.app
        (CategoryStruct.comp (Y :=
          Functor.obj (curriedAction C D) (tensorObj.{v_1, u_1} (𝒞 := inst) x (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
          (Functor.map (curriedAction C D) (Iso.inv (ρ_ x)))
          (CategoryStruct.comp (Y :=
            tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) x)
              (Functor.obj (curriedAction C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
            { app := fun (x_1 : D) ↦ Iso.hom (αᵣ x_1 x (tensorUnit.{v_1, u_1} C (𝒞 := inst))), naturality := ⋯ }
            (Functor.obj (curriedAction C D) x ◁ Iso.hom (actionUnitNatIso C D))))
        t)
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v_2, v_2, u_2, u_2} D D) (Functor.obj (curriedAction C D) x)
      (tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) x)
        ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)) (𝒞 := Functor.category))))
    (Iso.inv (ρ_ (Functor.obj (curriedAction C D) x)))
    (CategoryStruct.comp (Y :=
      Functor.obj (curriedAction C D) (tensorObj.{v_1, u_1} (𝒞 := inst) x (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
      (Functor.map (curriedAction C D) (Iso.inv (ρ_ x)))
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) x)
          (Functor.obj (curriedAction C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        { app := fun (x_1 : D) ↦ Iso.hom (αᵣ x_1 x (tensorUnit.{v_1, u_1} C (𝒞 := inst))), naturality := ⋯ }
        (Functor.obj (curriedAction C D) x ◁ 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 : MonoidalRightAction.{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} (Functor.obj (curriedAction C D) x) t ⟶
      Functor.obj.{v_2, v_2, u_2, u_2}
        (tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) x)
          ((𝟙_ (Functor.{v_2, v_2, u_2, u_2} D D)) (𝒞 := Functor.category)))
        t)
    (NatTrans.app (Iso.inv (ρ_ (Functor.obj (curriedAction C D) x))) t)
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        Functor.obj (curriedAction C D) (tensorObj.{v_1, u_1} (𝒞 := inst) x (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
        (Functor.map (curriedAction C D) (Iso.inv (ρ_ x)))
        (CategoryStruct.comp (Y :=
          tensorObj (𝒞 := Functor.category) (Functor.obj (curriedAction C D) x)
            (Functor.obj (curriedAction C D) (tensorUnit.{v_1, u_1} C (𝒞 := inst))))
          { app := fun (x_1 : D) ↦ Iso.hom (αᵣ x_1 x (tensorUnit.{v_1, u_1} C (𝒞 := inst))), naturality := ⋯ }
          (Functor.obj (curriedAction C D) x ◁ Iso.hom (actionUnitNatIso C D))))
      t)

Tactic:
simpa [-actionHom_rightUnitor] using
      t ⊴ᵣ (ρ_ x).inv ≫= actionHom_rightUnitor x t

Premises used: CategoryTheory.MonoidalCategoryStruct.rightUnitor, CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_rightUnitor, CategoryTheory.Iso.inv