revert _root_ additions

Author: justus-springer

Mathlib/CategoryTheory/Abelian/SerreClass/Localization.lean

@@ -242,13 +242,13 @@ lemma preservesEpimorphisms : L.PreservesEpimorphisms where
 set_option backward.isDefEq.respectTransparency false in
 lemma mono_iff {X Y : D} (f : X ⟶ Y) :
     Mono f ↔ ∃ (X' Y' : C) (f' : X' ⟶ Y') (_ : Mono f'),
-      _root_.Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f) := by
+      Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f) := by
   have := preservesMonomorphisms L P
   have := Localization.essSurj_mapArrow L P.isoModSerre
   refine ⟨fun _ ↦ ?_, ?_⟩
   · suffices ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (_ : Mono (L.map f)),
       ∃ (X' Y' : C) (f' : X' ⟶ Y') (_ : Mono f'),
-          _root_.Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f)) by
+          Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f)) by
         let e := L.mapArrow.objObjPreimageIso (Arrow.mk f)
         obtain ⟨X', Y', f', _, ⟨e'⟩⟩ := this _
           (((MorphismProperty.monomorphisms D).arrow_iso_iff e).2 (.infer_property f))
@@ -266,13 +266,13 @@ lemma mono_iff {X Y : D} (f : X ⟶ Y) :
 set_option backward.isDefEq.respectTransparency false in
 lemma epi_iff {X Y : D} (f : X ⟶ Y) :
     Epi f ↔ ∃ (X' Y' : C) (f' : X' ⟶ Y') (_ : Epi f'),
-      _root_.Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f) := by
+      Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk f) := by
   have := preservesEpimorphisms L P
   have := Localization.essSurj_mapArrow L P.isoModSerre
   refine ⟨fun _ ↦ ?_, ?_⟩
   · suffices ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (_ : Epi (L.map f)),
       ∃ (X' Y' : C) (f' : X' ⟶ Y') (_ : Epi f'),
-          _root_.Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f)) by
+          Nonempty (Arrow.mk (L.map f') ≅ Arrow.mk (L.map f)) by
         let e := L.mapArrow.objObjPreimageIso (Arrow.mk f)
         obtain ⟨X', Y', f', _, ⟨e'⟩⟩ := this _
           (((MorphismProperty.epimorphisms D).arrow_iso_iff e).2 (.infer_property f))

Mathlib/CategoryTheory/Limits/Final.lean

@@ -1178,7 +1178,7 @@ theorem initial_ι {C : Type u₁} [Category.{v₁} C] (P : ObjectProperty C)
     (h : ∀ d, ¬ P d → IsConnected (CostructuredArrow P.ι d)) :
     P.ι.Initial := .mk <| fun d => by
   by_cases hd : P d
-  · have : _root_.Nonempty (CostructuredArrow P.ι d) := ⟨⟨d, hd⟩, ⟨⟨⟩⟩, 𝟙 _⟩
+  · have : Nonempty (CostructuredArrow P.ι d) := ⟨⟨d, hd⟩, ⟨⟨⟩⟩, 𝟙 _⟩
     refine zigzag_isConnected fun ⟨c₁, ⟨⟨⟩⟩, g₁⟩ ⟨c₂, ⟨⟨⟩⟩, g₂⟩ =>
       Zigzag.trans (j₂ := ⟨⟨d, hd⟩, ⟨⟨⟩⟩, 𝟙 _⟩) (.of_hom ?_) (.of_inv ?_)
     · exact CostructuredArrow.homMk (InducedCategory.homMk g₁)

Mathlib/CategoryTheory/ObjectProperty/Basic.lean

@@ -157,10 +157,10 @@ lemma prop_inverseImage_iff (P : ObjectProperty D) (F : C ⥤ D) (X : C) :
 
 /-- The essential image of a property of objects by a functor. -/
 def map (P : ObjectProperty C) (F : C ⥤ D) : ObjectProperty D :=
-  fun Y ↦ ∃ (X : C), P X ∧ _root_.Nonempty (F.obj X ≅ Y)
+  fun Y ↦ ∃ (X : C), P X ∧ Nonempty (F.obj X ≅ Y)
 
 lemma prop_map_iff (P : ObjectProperty C) (F : C ⥤ D) (Y : D) :
-    P.map F Y ↔ ∃ (X : C), P X ∧ _root_.Nonempty (F.obj X ≅ Y) := Iff.rfl
+    P.map F Y ↔ ∃ (X : C), P X ∧ Nonempty (F.obj X ≅ Y) := Iff.rfl
 
 lemma prop_map_obj (P : ObjectProperty C) (F : C ⥤ D) {X : C} (hX : P X) :
     P.map F (F.obj X) :=

Mathlib/CategoryTheory/ObjectProperty/ClosedUnderIsomorphisms.lean

@@ -46,10 +46,10 @@ lemma prop_iff_of_isIso [IsClosedUnderIsomorphisms P] {X Y : C} (f : X ⟶ Y) [I
   prop_iff_of_iso P (asIso f)
 
 /-- The closure by isomorphisms of a predicate on objects in a category. -/
-def isoClosure : ObjectProperty C := fun X => ∃ (Y : C) (_ : P Y), _root_.Nonempty (X ≅ Y)
+def isoClosure : ObjectProperty C := fun X => ∃ (Y : C) (_ : P Y), Nonempty (X ≅ Y)
 
 lemma prop_isoClosure_iff (X : C) :
-    isoClosure P X ↔ ∃ (Y : C) (_ : P Y), _root_.Nonempty (X ≅ Y) := by rfl
+    isoClosure P X ↔ ∃ (Y : C) (_ : P Y), Nonempty (X ≅ Y) := by rfl
 
 variable {P} in
 lemma prop_isoClosure {X Y : C} (h : P X) (e : X ⟶ Y) [IsIso e] : isoClosure P Y :=

Mathlib/CategoryTheory/ObjectProperty/ColimitsClosure.lean

@@ -75,7 +75,7 @@ lemma colimitsClosure_eq_self [P.IsClosedUnderIsomorphisms]
   le_antisymm (colimitsClosure_le (le_refl P)) (P.le_colimitsClosure J)
 
 @[simp]
-lemma colimitsClosure_bot [∀ (a : α), _root_.Nonempty (J a)] :
+lemma colimitsClosure_bot [∀ (a : α), Nonempty (J a)] :
     colimitsClosure (⊥ : ObjectProperty C) J = ⊥ :=
   colimitsClosure_eq_self _ _
 

Mathlib/CategoryTheory/ObjectProperty/ColimitsOfShape.lean

@@ -71,7 +71,7 @@ lemma strictColimitsOfShape_monotone {Q : ObjectProperty C} (h : P ≤ Q) :
   exact ⟨F, fun j ↦ h _ (hF j)⟩
 
 @[simp]
-lemma strictColimitsOfShape_bot [_root_.Nonempty J] :
+lemma strictColimitsOfShape_bot [Nonempty J] :
     strictColimitsOfShape (⊥ : ObjectProperty C) J = ⊥ := by
   rw [eq_bot_iff]
   rintro _ ⟨_, h⟩
@@ -133,7 +133,7 @@ end ColimitOfShape
 /-- The property of objects that are the point of a colimit cocone for a
 functor `F : J ⥤ C` where all objects `F.obj j` satisfy `P`. -/
 def colimitsOfShape : ObjectProperty C :=
-  fun X ↦ _root_.Nonempty (P.ColimitOfShape J X)
+  fun X ↦ Nonempty (P.ColimitOfShape J X)
 
 variable {P J} in
 lemma ColimitOfShape.colimitsOfShape {X : C} (h : P.ColimitOfShape J X) :
@@ -146,7 +146,7 @@ lemma strictColimitsOfShape_le_colimitsOfShape :
   exact ⟨.colimit F hF⟩
 
 @[simp]
-lemma colimitsOfShape_bot [_root_.Nonempty J] : colimitsOfShape (⊥ : ObjectProperty C) J = ⊥ := by
+lemma colimitsOfShape_bot [Nonempty J] : colimitsOfShape (⊥ : ObjectProperty C) J = ⊥ := by
   rw [eq_bot_iff]
   rintro X ⟨⟨_, h⟩⟩
   exact h (Classical.arbitrary J)
@@ -204,7 +204,7 @@ lemma IsClosedUnderColimitsOfShape.mk' [P.IsClosedUnderIsomorphisms]
     rw [← isoClosure_strictColimitsOfShape]
     exact monotone_isoClosure h
 
-instance [_root_.Nonempty J] : IsClosedUnderColimitsOfShape (⊥ : ObjectProperty C) J where
+instance [Nonempty J] : IsClosedUnderColimitsOfShape (⊥ : ObjectProperty C) J where
   colimitsOfShape_le := by rw [colimitsOfShape_bot]
 
 instance : IsClosedUnderColimitsOfShape (⊤ : ObjectProperty C) J where

Mathlib/CategoryTheory/ObjectProperty/Ind.lean

@@ -83,8 +83,8 @@ lemma ind_iff_exists (H : P ≤ isFinitelyPresentable.{w} C)
     exact ⟨_, u, pres.ι.app j, hcomp, h j⟩
   · let incl : P.FullSubcategory ⥤ (isFinitelyPresentable.{w} C).FullSubcategory :=
       ObjectProperty.ιOfLE H
-    have H (d : CostructuredArrow (isFinitelyPresentable.{w} C).ι X) : ∃ c, _root_.Nonempty
-        (d ⟶ (CostructuredArrow.pre incl (isFinitelyPresentable.{w} C).ι X).obj c) := by
+    have H (d : CostructuredArrow (isFinitelyPresentable.{w} C).ι X) : ∃ c,
+        Nonempty (d ⟶ (CostructuredArrow.pre incl (isFinitelyPresentable.{w} C).ι X).obj c) := by
       obtain ⟨W, u, v, huv, hW⟩ := hfac d.hom
       exact ⟨CostructuredArrow.mk (Y := FullSubcategory.mk _ hW) v,
         ⟨CostructuredArrow.homMk ⟨u⟩ huv⟩⟩

Mathlib/CategoryTheory/ObjectProperty/LimitsClosure.lean

@@ -73,7 +73,7 @@ lemma limitsClosure_eq_self [P.IsClosedUnderIsomorphisms]
   le_antisymm (limitsClosure_le (le_refl P)) (P.le_limitsClosure J)
 
 @[simp]
-lemma limitsClosure_bot [∀ (a : α), _root_.Nonempty (J a)] :
+lemma limitsClosure_bot [∀ (a : α), Nonempty (J a)] :
     limitsClosure (⊥ : ObjectProperty C) J = ⊥ :=
   limitsClosure_eq_self _ _
 

Mathlib/CategoryTheory/ObjectProperty/LimitsOfShape.lean

@@ -64,7 +64,7 @@ lemma strictLimitsOfShape_monotone {Q : ObjectProperty C} (h : P ≤ Q) :
   exact ⟨F, fun j ↦ h _ (hF j)⟩
 
 @[simp]
-lemma strictLimitsOfShape_bot [_root_.Nonempty J] :
+lemma strictLimitsOfShape_bot [Nonempty J] :
     strictLimitsOfShape (⊥ : ObjectProperty C) J = ⊥ := by
   rw [eq_bot_iff]
   rintro _ ⟨_, h⟩
@@ -125,7 +125,7 @@ end LimitOfShape
 /-- The property of objects that are the point of a limit cone for a
 functor `F : J ⥤ C` where all objects `F.obj j` satisfy `P`. -/
 def limitsOfShape : ObjectProperty C :=
-  fun X ↦ _root_.Nonempty (P.LimitOfShape J X)
+  fun X ↦ Nonempty (P.LimitOfShape J X)
 
 variable {P J} in
 lemma LimitOfShape.limitsOfShape {X : C} (h : P.LimitOfShape J X) :
@@ -138,7 +138,7 @@ lemma strictLimitsOfShape_le_limitsOfShape :
   exact ⟨.limit F hF⟩
 
 @[simp]
-lemma limitsOfShape_bot [_root_.Nonempty J] : limitsOfShape (⊥ : ObjectProperty C) J = ⊥ := by
+lemma limitsOfShape_bot [Nonempty J] : limitsOfShape (⊥ : ObjectProperty C) J = ⊥ := by
   rw [eq_bot_iff]
   rintro X ⟨⟨_, h⟩⟩
   exact h (Classical.arbitrary J)
@@ -201,7 +201,7 @@ lemma IsClosedUnderLimitsOfShape.mk' [P.IsClosedUnderIsomorphisms]
     rw [← isoClosure_strictLimitsOfShape]
     exact monotone_isoClosure h
 
-instance [_root_.Nonempty J] : IsClosedUnderLimitsOfShape (⊥ : ObjectProperty C) J where
+instance [Nonempty J] : IsClosedUnderLimitsOfShape (⊥ : ObjectProperty C) J where
   limitsOfShape_le := by rw [limitsOfShape_bot]
 
 instance : IsClosedUnderLimitsOfShape (⊤ : ObjectProperty C) J where

Mathlib/CategoryTheory/ObjectProperty/Retract.lean

@@ -86,10 +86,10 @@ lemma of_biproduct [HasZeroMorphisms C] {J : Type*} (F : J → C) [HasBiproduct
 end IsStableUnderRetracts
 
 /-- The closure by retracts of a predicate on objects in a category. -/
-def retractClosure : ObjectProperty C := fun X => ∃ (Y : C) (_ : P Y), _root_.Nonempty (Retract X Y)
+def retractClosure : ObjectProperty C := fun X => ∃ (Y : C) (_ : P Y), Nonempty (Retract X Y)
 
 lemma prop_retractClosure_iff (X : C) :
-    retractClosure P X ↔ ∃ (Y : C) (_ : P Y), _root_.Nonempty (Retract X Y) := by rfl
+    retractClosure P X ↔ ∃ (Y : C) (_ : P Y), Nonempty (Retract X Y) := by rfl
 
 variable {P} in
 lemma prop_retractClosure {X Y : C} (h : P Y) (r : Retract X Y) : retractClosure P X :=