feat: port CategoryTheory.Bicategory.CoherenceTactic (#4610)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Jun 6, 2023 · 1c05bfa · 1c05bfa
1 parent c340d96
commit 1c05bfa
Show file tree

Hide file tree

Showing 11 changed files with 398 additions and 109 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2374,6 +2374,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/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/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/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