chore(CategoryTheory): dsimp the apply lemmas in the monoidal structure on types (leanprover-community#37168)

Author: dagurtomas

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -158,8 +158,6 @@ lemma μIso_inv_freeMk {X Y : Type u} (z : X ⊗ Y) :
   erw [finsuppTensorFinsupp'_symm_single_eq_single_one_tmul]
 
 end FreeMonoidal
-
-set_option backward.isDefEq.respectTransparency false in
 open FreeMonoidal in
 /-- The free functor `Type u ⥤ ModuleCat R` is a monoidal functor. -/
 instance : (free R).Monoidal :=

Mathlib/CategoryTheory/Action/Monoidal.lean

@@ -266,6 +266,7 @@ theorem diagonalSuccIsoTensorTrivial_hom_hom_apply {n : ℕ} (f : Fin (n + 1) 
       leftRegularTensorIso_hom_hom, tensor_ρ, tensor_apply, ofMulAction_apply]
     <;> simp [ofMulAction_V, types_tensorObj_def, Fin.tail]
 
+attribute [local simp] types_tensorObj_def types_tensorUnit_def in
 set_option backward.isDefEq.respectTransparency false in
 @[simp]
 theorem diagonalSuccIsoTensorTrivial_inv_hom_apply {n : ℕ} (g : G) (f : Fin n → G) :

Mathlib/CategoryTheory/Monoidal/Functor/Types.lean

@@ -27,7 +27,7 @@ section
 variable (F : Type* → Type*) [Applicative F] [LawfulApplicative F]
 
 set_option backward.isDefEq.respectTransparency false in
-attribute [local simp] map_seq seq_map_assoc
+attribute [local simp] map_seq seq_map_assoc types_tensorObj_def types_tensorUnit_def
   LawfulApplicative.pure_seq LawfulApplicative.seq_assoc in
 /-- A lawful `Applicative` gives a category theory `LaxMonoidal` functor
 between categories of types. -/

Mathlib/CategoryTheory/Monoidal/Internal/Types/Basic.lean

@@ -44,6 +44,7 @@ noncomputable def functor : Mon (Type u) ⥤ MonCat.{u} where
       map_one' := congr_fun (IsMonHom.one_hom f.hom) PUnit.unit
       map_mul' x y := congr_fun (IsMonHom.mul_hom f.hom) (x, y) }
 
+attribute [local simp] types_tensorObj_def types_tensorUnit_def in
 /-- Converting a bundled monoid to a monoid object in `Type`.
 -/
 noncomputable def inverse : MonCat.{u} ⥤ Mon (Type u) where

Mathlib/CategoryTheory/Monoidal/Types/Basic.lean

@@ -33,88 +33,90 @@ theorem types_tensorObj_def {X Y : Type u} : X ⊗ Y = (X × Y) := rfl
 
 theorem types_tensorUnit_def : 𝟙_ (Type u) = PUnit := rfl
 
+attribute [local simp] types_tensorObj_def types_tensorUnit_def
+
 @[simp]
 theorem tensor_apply {W X Y Z : Type u} (f : W ⟶ X) (g : Y ⟶ Z) (p : W ⊗ Y) :
-    (f ⊗ₘ g) p = (f p.1, g p.2) :=
+    dsimp% (f ⊗ₘ g) p = (f p.1, g p.2) :=
   rfl
 
 @[simp]
 theorem whiskerLeft_apply (X : Type u) {Y Z : Type u} (f : Y ⟶ Z) (p : X ⊗ Y) :
-    (X ◁ f) p = (p.1, f p.2) :=
+    dsimp% (X ◁ f) p = (p.1, f p.2) :=
   rfl
 
 @[simp]
 theorem whiskerRight_apply {Y Z : Type u} (f : Y ⟶ Z) (X : Type u) (p : Y ⊗ X) :
-    (f ▷ X) p = (f p.1, p.2) :=
+    dsimp% (f ▷ X) p = (f p.1, p.2) :=
   rfl
 
 @[simp]
 theorem leftUnitor_hom_apply {X : Type u} {x : X} {p : PUnit} :
-    ((λ_ X).hom : 𝟙_ (Type u) ⊗ X → X) (p, x) = x :=
+    dsimp% (λ_ X).hom (p, x) = x :=
   rfl
 
 @[simp]
 theorem leftUnitor_inv_apply {X : Type u} {x : X} :
-    ((λ_ X).inv : X ⟶ 𝟙_ (Type u) ⊗ X) x = (PUnit.unit, x) :=
+    dsimp% (λ_ X).inv x = (PUnit.unit, x) :=
   rfl
 
 @[simp]
 theorem rightUnitor_hom_apply {X : Type u} {x : X} {p : PUnit} :
-    ((ρ_ X).hom : X ⊗ 𝟙_ (Type u) → X) (x, p) = x :=
+    dsimp% (ρ_ X).hom (x, p) = x :=
   rfl
 
 @[simp]
 theorem rightUnitor_inv_apply {X : Type u} {x : X} :
-    ((ρ_ X).inv : X ⟶ X ⊗ 𝟙_ (Type u)) x = (x, PUnit.unit) :=
+    dsimp% (ρ_ X).inv x = (x, PUnit.unit) :=
   rfl
 
 @[simp]
 theorem associator_hom_apply {X Y Z : Type u} {x : X} {y : Y} {z : Z} :
-    ((α_ X Y Z).hom : (X ⊗ Y) ⊗ Z → X ⊗ Y ⊗ Z) ((x, y), z) = (x, (y, z)) :=
+    dsimp% (α_ X Y Z).hom ((x, y), z) = (x, (y, z)) :=
   rfl
 
 @[simp]
 theorem associator_inv_apply {X Y Z : Type u} {x : X} {y : Y} {z : Z} :
-    ((α_ X Y Z).inv : X ⊗ Y ⊗ Z → (X ⊗ Y) ⊗ Z) (x, (y, z)) = ((x, y), z) :=
+    dsimp% (α_ X Y Z).inv (x, (y, z)) = ((x, y), z) :=
   rfl
 
 @[simp] theorem associator_hom_apply_1 {X Y Z : Type u} {x} :
-    (((α_ X Y Z).hom : (X ⊗ Y) ⊗ Z → X ⊗ Y ⊗ Z) x).1 = x.1.1 :=
+    dsimp% ((α_ X Y Z).hom x).1 = x.1.1 :=
   rfl
 
 @[simp] theorem associator_hom_apply_2_1 {X Y Z : Type u} {x} :
-    (((α_ X Y Z).hom : (X ⊗ Y) ⊗ Z → X ⊗ Y ⊗ Z) x).2.1 = x.1.2 :=
+    dsimp% ((α_ X Y Z).hom x).2.1 = x.1.2 :=
   rfl
 
 @[simp] theorem associator_hom_apply_2_2 {X Y Z : Type u} {x} :
-    (((α_ X Y Z).hom : (X ⊗ Y) ⊗ Z → X ⊗ Y ⊗ Z) x).2.2 = x.2 :=
+    dsimp% ((α_ X Y Z).hom x).2.2 = x.2 :=
   rfl
 
 @[simp] theorem associator_inv_apply_1_1 {X Y Z : Type u} {x} :
-    (((α_ X Y Z).inv : X ⊗ Y ⊗ Z → (X ⊗ Y) ⊗ Z) x).1.1 = x.1 :=
+    dsimp% ((α_ X Y Z).inv x).1.1 = x.1 :=
   rfl
 
 @[simp] theorem associator_inv_apply_1_2 {X Y Z : Type u} {x} :
-    (((α_ X Y Z).inv : X ⊗ Y ⊗ Z → (X ⊗ Y) ⊗ Z) x).1.2 = x.2.1 :=
+    dsimp% ((α_ X Y Z).inv x).1.2 = x.2.1 :=
   rfl
 
 @[simp] theorem associator_inv_apply_2 {X Y Z : Type u} {x} :
-    (((α_ X Y Z).inv : X ⊗ Y ⊗ Z → (X ⊗ Y) ⊗ Z) x).2 = x.2.2 :=
+    dsimp% ((α_ X Y Z).inv x).2 = x.2.2 :=
   rfl
 
 @[simp]
 theorem braiding_hom_apply {X Y : Type u} {x : X} {y : Y} :
-    ((β_ X Y).hom : X ⊗ Y → Y ⊗ X) (x, y) = (y, x) :=
+    dsimp% (β_ X Y).hom (x, y) = (y, x) :=
   rfl
 
 @[simp]
 theorem braiding_inv_apply {X Y : Type u} {x : X} {y : Y} :
-    ((β_ X Y).inv : Y ⊗ X → X ⊗ Y) (y, x) = (x, y) :=
+    dsimp% (β_ X Y).inv (y, x) = (x, y) :=
   rfl
 
 @[simp]
 theorem CartesianMonoidalCategory.lift_apply {X Y Z : Type u} {f : X ⟶ Y} {g : X ⟶ Z} {x : X} :
-    lift f g x = (f x, g x) :=
+    dsimp% lift f g x = (f x, g x) :=
   rfl
 
 -- We don't yet have an API for tensor products indexed by finite ordered types,

Mathlib/CategoryTheory/Monoidal/Types/Coyoneda.lean

@@ -20,6 +20,7 @@ namespace CategoryTheory
 
 open Opposite MonoidalCategory
 
+attribute [local simp] types_tensorObj_def types_tensorUnit_def in
 instance (C : Type u) [Category.{v} C] [MonoidalCategory C] :
     (coyoneda.obj (op (𝟙_ C))).LaxMonoidal :=
   Functor.LaxMonoidal.ofTensorHom

Mathlib/RepresentationTheory/Action.lean

@@ -156,9 +156,7 @@ lemma μ_comp_assoc : ((linearizeMap (α_ X Y Z).hom).comp
   -- after fixing the defeq problems in `Action` and in the monoidal category structure of `types`
   -- this line should close the goal so this is left as an indicator.
   with_reducible convert linearizeMap_single (α_ X Y Z).hom ((x, y), z) _
-  with_reducible simp only [Action.tensorObj_V, types_tensorObj_def, Action.associator_hom_hom]
-  with_reducible refine Prod.ext ?_ (Prod.ext ?_ ?_)
-  <;>  with_reducible simp
+  with_reducible simp
 
 variable (X) in
 lemma μ_leftUnitor : (lid k (linearize k G X)).toIntertwiningMap =