leanprover-community · joelriou · Jun 2, 2023 · Jun 2, 2023 · Jun 2, 2023 · Jun 2, 2023
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2399,6 +2399,7 @@ import Mathlib.Tactic.Cache
 import Mathlib.Tactic.CancelDenoms
 import Mathlib.Tactic.Cases
 import Mathlib.Tactic.CasesM
+import Mathlib.Tactic.CategoryTheory.BicategoryCoherence
 import Mathlib.Tactic.CategoryTheory.Coherence
 import Mathlib.Tactic.CategoryTheory.Elementwise
 import Mathlib.Tactic.CategoryTheory.Reassoc

diff --git a/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean b/Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
@@ -67,6 +67,8 @@ end
 
 namespace Free
 
+open MonoidalCategory
+
 variable [CommRing R]
 
 attribute [local ext] TensorProduct.ext
@@ -214,6 +216,8 @@ instance : IsIso (@LaxMonoidal.ε _ _ _ _ _ _ (free R).obj _ _) := by
 
 end Free
 
+open MonoidalCategory
+
 variable [CommRing R]
 
 /-- The free functor `Type u ⥤ ModuleCat R`, as a monoidal functor. -/

diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean
@@ -62,6 +62,8 @@ theorem ihom_map_apply {M N P : ModuleCat.{u} R} (f : N ⟶ P) (g : ModuleCat.of
 set_option linter.uppercaseLean3 false in
 #align Module.ihom_map_apply ModuleCat.ihom_map_apply
 
+open MonoidalCategory
+
 -- porting note: `CoeFun` was replaced by `FunLike`
 -- I can't seem to express the function coercion here without writing `@FunLike.coe`.
 @[simp]

diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean
@@ -18,7 +18,7 @@ import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
 
 universe v w x u
 
-open CategoryTheory
+open CategoryTheory MonoidalCategory
 
 namespace ModuleCat
 

diff --git a/Mathlib/CategoryTheory/Limits/Yoneda.lean b/Mathlib/CategoryTheory/Limits/Yoneda.lean
@@ -20,13 +20,7 @@ We calculate the colimit of `Y ↦ (X ⟶ Y)`, which is just `PUnit`.
 We also show the (co)yoneda embeddings preserve limits and jointly reflect them.
 -/
 
--- import Mathlib.Tactic.AssertExists -- Porting note: see end of file
-
-open Opposite
-
-open CategoryTheory
-
-open CategoryTheory.Limits
+open Opposite CategoryTheory Limits
 
 universe w v u
 

diff --git a/Mathlib/CategoryTheory/Monoidal/Braided.lean b/Mathlib/CategoryTheory/Monoidal/Braided.lean
@@ -32,7 +32,7 @@ just requiring a property.
 -/
 
 
-open CategoryTheory
+open CategoryTheory MonoidalCategory
 
 universe v v₁ v₂ v₃ u u₁ u₂ u₃
 

diff --git a/Mathlib/CategoryTheory/Monoidal/Category.lean b/Mathlib/CategoryTheory/Monoidal/Category.lean
@@ -137,42 +137,13 @@ class MonoidalCategory (C : Type u) [𝒞 : Category.{v} C] where
     aesop_cat
 #align category_theory.monoidal_category CategoryTheory.MonoidalCategory
 
--- Porting Note: `restate_axiom` doesn't seem to be necessary in Lean 4
--- restate_axiom MonoidalCategory.tensor_id'
-
 attribute [simp] MonoidalCategory.tensor_id
-
--- Porting Note: same as above
--- restate_axiom MonoidalCategory.tensor_comp'
-
 attribute [reassoc] MonoidalCategory.tensor_comp
-
--- This would be redundant in the simp set.
 attribute [simp] MonoidalCategory.tensor_comp
-
--- Porting Note: same as above
--- restate_axiom MonoidalCategory.associator_naturality'
-
 attribute [reassoc] MonoidalCategory.associator_naturality
-
--- Porting Note: same as above
--- restate_axiom MonoidalCategory.leftUnitor_naturality'
-
 attribute [reassoc] MonoidalCategory.leftUnitor_naturality
-
--- Porting Note: same as above
--- restate_axiom MonoidalCategory.rightUnitor_naturality'
-
 attribute [reassoc] MonoidalCategory.rightUnitor_naturality
-
--- Porting Note: same as above
--- restate_axiom MonoidalCategory.pentagon'
-
--- Porting Note: same as above
--- restate_axiom MonoidalCategory.triangle'
-
 attribute [reassoc] MonoidalCategory.pentagon
-
 attribute [reassoc (attr := simp)] MonoidalCategory.triangle
 
 -- Porting Note: This is here to make `tensorUnit` explicitly depend on `C`, which was done in
@@ -182,31 +153,30 @@ open CategoryTheory.MonoidalCategory in
 abbrev MonoidalCategory.tensorUnit (C : Type u) [Category.{v} C] [MonoidalCategory C] : C :=
   tensorUnit' (C := C)
 
-open MonoidalCategory
+namespace MonoidalCategory
 
--- mathport name: tensor_obj
 /-- Notation for `tensorObj`, the tensor product of objects in a monoidal category -/
-infixr:70 " ⊗ " => tensorObj
+scoped infixr:70 " ⊗ " => tensorObj
 
--- mathport name: tensor_hom
 /-- Notation for `tensorHom`, the tensor product of morphisms in a monoidal category -/
-infixr:70 " ⊗ " => tensorHom
+scoped infixr:70 " ⊗ " => tensorHom
 
--- mathport name: «expr𝟙_»
 /-- Notation for `tensorUnit`, the two-sided identity of `⊗` -/
-notation "𝟙_" => tensorUnit
+scoped notation "𝟙_" => tensorUnit
 
--- mathport name: exprα_
 /-- Notation for the monoidal `associator`: `(X ⊗ Y) ⊗ Z) ≃ X ⊗ (Y ⊗ Z)` -/
-notation "α_" => associator
+scoped notation "α_" => associator
 
--- mathport name: «exprλ_»
 /-- Notation for the `leftUnitor`: `𝟙_C ⊗ X ≃ X` -/
-notation "λ_" => leftUnitor
+scoped notation "λ_" => leftUnitor
 
--- mathport name: exprρ_
 /-- Notation for the `rightUnitor`: `X ⊗ 𝟙_C ≃ X` -/
-notation "ρ_" => rightUnitor
+scoped notation "ρ_" => rightUnitor
+
+end MonoidalCategory
+
+open scoped MonoidalCategory
+open MonoidalCategory
 
 variable (C : Type u) [𝒞 : Category.{v} C] [MonoidalCategory C]
 
@@ -220,7 +190,6 @@ def tensorIso {C : Type u} {X Y X' Y' : C} [Category.{v} C] [MonoidalCategory.{v
   inv_hom_id := by rw [← tensor_comp, Iso.inv_hom_id, Iso.inv_hom_id, ← tensor_id]
 #align category_theory.tensor_iso CategoryTheory.tensorIso
 
--- mathport name: tensor_iso
 /-- Notation for `tensorIso`, the tensor product of isomorphisms -/
 infixr:70 " ⊗ " => tensorIso
 

diff --git a/Mathlib/CategoryTheory/Monoidal/Discrete.lean b/Mathlib/CategoryTheory/Monoidal/Discrete.lean
@@ -22,9 +22,7 @@ Multiplicative morphisms induced monoidal functors.
 
 universe u
 
-open CategoryTheory
-
-open CategoryTheory.Discrete
+open CategoryTheory Discrete MonoidalCategory
 
 variable (M : Type u) [Monoid M]
 

diff --git a/Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
@@ -63,7 +63,7 @@ rigid category, monoidal category
 -/
 
 
-open CategoryTheory
+open CategoryTheory MonoidalCategory
 
 universe v v₁ v₂ v₃ u u₁ u₂ u₃
 

diff --git a/Mathlib/CategoryTheory/Monoidal/Rigid/OfEquivalence.lean b/Mathlib/CategoryTheory/Monoidal/Rigid/OfEquivalence.lean
@@ -19,6 +19,8 @@ noncomputable section
 
 namespace CategoryTheory
 
+open MonoidalCategory
+
 variable {C D : Type _} [Category C] [Category D] [MonoidalCategory C] [MonoidalCategory D]
 
 variable (F : MonoidalFunctor C D)

diff --git a/Mathlib/CategoryTheory/Monoidal/Types/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Types/Basic.lean
@@ -18,9 +18,7 @@ import Mathlib.Logic.Equiv.Fin
 -/
 
 
-open CategoryTheory
-
-open CategoryTheory.Limits
+open CategoryTheory Limits MonoidalCategory
 
 open Tactic
 

diff --git a/Mathlib/CategoryTheory/Monoidal/Types/Symmetric.lean b/Mathlib/CategoryTheory/Monoidal/Types/Symmetric.lean
@@ -22,6 +22,8 @@ universe v u
 
 namespace CategoryTheory
 
+open MonoidalCategory
+
 instance typesSymmetric : SymmetricCategory.{u} (Type u) :=
   symmetricOfChosenFiniteProducts Types.terminalLimitCone Types.binaryProductLimitCone
 #align category_theory.types_symmetric CategoryTheory.typesSymmetric

diff --git a/Mathlib/RepresentationTheory/Action.lean b/Mathlib/RepresentationTheory/Action.lean
@@ -471,6 +471,8 @@ end Abelian
 
 section Monoidal
 
+open MonoidalCategory
+
 variable [MonoidalCategory V]
 
 instance : MonoidalCategory (Action V G) :=
@@ -882,8 +884,8 @@ def diagonalOneIsoLeftRegular (G : Type u) [Monoid G] : diagonal G 1 ≅ leftReg
 set_option linter.uppercaseLean3 false in
 #align Action.diagonal_one_iso_left_regular Action.diagonalOneIsoLeftRegular
 
-/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
-/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
+open MonoidalCategory
+
 /-- Given `X : Action (Type u) (Mon.of G)` for `G` a group, then `G × X` (with `G` acting as left
 multiplication on the first factor and by `X.ρ` on the second) is isomorphic as a `G`-set to
 `G × X` (with `G` acting as left multiplication on the first factor and trivially on the second).
@@ -923,7 +925,6 @@ noncomputable def leftRegularTensorIso (G : Type u) [Group G] (X : Action (Type
 set_option linter.uppercaseLean3 false in
 #align Action.left_regular_tensor_iso Action.leftRegularTensorIso
 
-/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
 /-- The natural isomorphism of `G`-sets `Gⁿ⁺¹ ≅ G × Gⁿ`, where `G` acts by left multiplication on
 each factor. -/
 @[simps!]

diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean
@@ -10,6 +10,7 @@ import Mathlib.Tactic.Cache
 import Mathlib.Tactic.CancelDenoms
 import Mathlib.Tactic.Cases
 import Mathlib.Tactic.CasesM
+import Mathlib.Tactic.CategoryTheory.BicategoryCoherence
 import Mathlib.Tactic.CategoryTheory.Coherence
 import Mathlib.Tactic.CategoryTheory.Elementwise
 import Mathlib.Tactic.CategoryTheory.Reassoc