fix

leanprover-community · Jan 6, 2022 · 12223bd · 12223bd
1 parent 45b945c
commit 12223bd
Show file tree

Hide file tree

Showing 4 changed files with 3 additions and 16 deletions.
diff --git a/src/algebraic_geometry/properties.lean b/src/algebraic_geometry/properties.lean
@@ -123,8 +123,6 @@ begin
     ((as_iso $ to_Spec_Γ R).CommRing_iso_to_ring_equiv.injective)
 end
 
-local attribute [elementwise] category_theory.is_iso.hom_inv_id
-
 lemma basic_open_eq_of_affine {R : CommRing} (f : R) :
   RingedSpace.basic_open (Spec.to_SheafedSpace.obj (op R)) ((Spec_Γ_identity.app R).inv f) =
     prime_spectrum.basic_open f :=

diff --git a/src/category_theory/limits/concrete_category.lean b/src/category_theory/limits/concrete_category.lean
@@ -7,7 +7,7 @@ import category_theory.limits.preserves.basic
 import category_theory.limits.types
 import category_theory.limits.shapes.wide_pullbacks
 import category_theory.limits.shapes.multiequalizer
-import tactic.elementwise
+import category_theory.concrete_category.elementwise
 
 /-!
 # Facts about (co)limits of functors into concrete categories
@@ -19,8 +19,6 @@ open category_theory
 
 namespace category_theory.limits
 
-attribute [elementwise] cone.w limit.lift_π limit.w cocone.w colimit.ι_desc colimit.w
-
 local attribute [instance] concrete_category.has_coe_to_fun concrete_category.has_coe_to_sort
 
 section limits

diff --git a/src/category_theory/limits/shapes/concrete_category.lean b/src/category_theory/limits/shapes/concrete_category.lean
@@ -5,7 +5,7 @@ Authors: Scott Morrison
 -/
 import category_theory.limits.shapes.kernels
 import category_theory.concrete_category.basic
-import tactic.elementwise
+import category_theory.concrete_category.elementwise
 
 /-!
 # Facts about limits of functors into concrete categories
@@ -18,10 +18,3 @@ while comparing categorical limits with existing constructions in concrete categ
 universes u
 
 open category_theory
-
-
-namespace category_theory.limits
-
-attribute [elementwise] kernel.condition cokernel.condition
-
-end category_theory.limits
diff --git a/src/topology/gluing.lean b/src/topology/gluing.lean
@@ -5,7 +5,7 @@ Authors: Andrew Yang
 -/
 import topology.category.Top
 import category_theory.glue_data
-import data.sym.sym2
+import category_theory.concrete_category.elementwise
 
 /-!
 # Gluing Topological spaces
@@ -202,8 +202,6 @@ end
 instance ι_mono (i : D.J) : mono (𝖣 .ι i) :=
 (Top.mono_iff_injective _).mpr (D.ι_injective _)
 
-local attribute [elementwise] is_iso.hom_inv_id is_iso.inv_hom_id
-
 lemma image_inter (i j : D.J) :
   set.range (𝖣 .ι i) ∩ set.range (𝖣 .ι j) = set.range (D.f i j ≫ 𝖣 .ι _) :=
 begin