chore(Algebra): Improve attribute generation (#20451)

artie2000 · artie2000 · commit f87a13504e7b · 2025-01-03T23:29:25.000Z
* Teach `to_additive` about `oneLE` -&gt; `nonneg` and `square` -&gt; `even`
* Make `simps` lemma generated for the `carrier` projection consistently `coe_*`
* Clarify some documentation

Moves:
* `\*_coe` -&gt; `coe_\*` where generated by `@[simps]`
  * `IsOpenMap.functor_obj_coe` -&gt; `IsOpenMap.coe_functor_obj`
  * `AlgebraicGeometry.Scheme.Hom.opensRange_coe` -&gt; `AlgebraicGeometry.Scheme.Hom.coe_opensRange`
diff --git a/Mathlib/Algebra/Group/Subsemigroup/Defs.lean b/Mathlib/Algebra/Group/Subsemigroup/Defs.lean
@@ -97,8 +97,8 @@ instance : SetLike (Subsemigroup M) M :=
 @[to_additive]
 instance : MulMemClass (Subsemigroup M) M where mul_mem := fun {_ _ _} => Subsemigroup.mul_mem' _
 
-initialize_simps_projections Subsemigroup (carrier → coe)
-initialize_simps_projections AddSubsemigroup (carrier → coe)
+initialize_simps_projections Subsemigroup (carrier → coe, as_prefix coe)
+initialize_simps_projections AddSubsemigroup (carrier → coe, as_prefix coe)
 
 @[to_additive (attr := simp)]
 theorem mem_carrier {s : Subsemigroup M} {x : M} : x ∈ s.carrier ↔ x ∈ s :=
diff --git a/Mathlib/Algebra/Order/Group/Cone.lean b/Mathlib/Algebra/Order/Group/Cone.lean
@@ -58,6 +58,9 @@ instance GroupCone.instGroupConeClass (G : Type*) [CommGroup G] :
   one_mem {C} := C.one_mem'
   eq_one_of_mem_of_inv_mem {C} := C.eq_one_of_mem_of_inv_mem'
 
+initialize_simps_projections GroupCone (carrier → coe, as_prefix coe)
+initialize_simps_projections AddGroupCone (carrier → coe, as_prefix coe)
+
 /-- Typeclass for maximal additive cones. -/
 class IsMaxCone {S G : Type*} [AddCommGroup G] [SetLike S G] (C : S) : Prop where
   mem_or_neg_mem (a : G) : a ∈ C ∨ -a ∈ C
@@ -74,19 +77,17 @@ namespace GroupCone
 variable {H : Type*} [OrderedCommGroup H] {a : H}
 
 variable (H) in
-/-- Construct a cone from the set of elements of
-a partially ordered abelian group that are at least 1. -/
-@[to_additive nonneg
-"Construct a cone from the set of non-negative elements of a partially ordered abelian group."]
+/-- The cone of elements that are at least 1. -/
+@[to_additive "The cone of non-negative elements."]
 def oneLE : GroupCone H where
   __ := Submonoid.oneLE H
   eq_one_of_mem_of_inv_mem' {a} := by simpa using ge_antisymm
 
-@[to_additive (attr := simp) nonneg_toAddSubmonoid]
+@[to_additive (attr := simp)]
 lemma oneLE_toSubmonoid : (oneLE H).toSubmonoid = .oneLE H := rfl
-@[to_additive (attr := simp) mem_nonneg]
+@[to_additive (attr := simp)]
 lemma mem_oneLE : a ∈ oneLE H ↔ 1 ≤ a := Iff.rfl
-@[to_additive (attr := simp, norm_cast) coe_nonneg]
+@[to_additive (attr := simp, norm_cast)]
 lemma coe_oneLE : oneLE H = {x : H | 1 ≤ x} := rfl
 
 @[to_additive nonneg.isMaxCone]
diff --git a/Mathlib/Algebra/Order/Monoid/Submonoid.lean b/Mathlib/Algebra/Order/Monoid/Submonoid.lean
@@ -91,16 +91,16 @@ section Preorder
 variable (M)
 variable [Monoid M] [Preorder M] [MulLeftMono M] {a : M}
 
-/-- The submonoid of elements greater than `1`. -/
-@[to_additive (attr := simps) nonneg "The submonoid of nonnegative elements."]
+/-- The submonoid of elements that are at least `1`. -/
+@[to_additive (attr := simps) "The submonoid of nonnegative elements."]
 def oneLE : Submonoid M where
   carrier := Set.Ici 1
   mul_mem' := one_le_mul
   one_mem' := le_rfl
 
 variable {M}
 
-@[to_additive (attr := simp) mem_nonneg] lemma mem_oneLE : a ∈ oneLE M ↔ 1 ≤ a := Iff.rfl
+@[to_additive (attr := simp)] lemma mem_oneLE : a ∈ oneLE M ↔ 1 ≤ a := Iff.rfl
 
 end Preorder
 end Submonoid
diff --git a/Mathlib/AlgebraicGeometry/Cover/Open.lean b/Mathlib/AlgebraicGeometry/Cover/Open.lean
@@ -210,7 +210,7 @@ lemma OpenCover.ext_elem {X : Scheme.{u}} {U : X.Opens} (f g : Γ(X, U)) (𝒰 :
   fapply TopCat.Sheaf.eq_of_locally_eq' X.sheaf
     (fun i ↦ (𝒰.map (𝒰.f i)).opensRange ⊓ U) _ (fun _ ↦ homOfLE inf_le_right)
   · intro x hx
-    simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_inf, Hom.opensRange_coe, Opens.coe_mk,
+    simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_inf, Hom.coe_opensRange, Opens.coe_mk,
       Set.mem_iUnion, Set.mem_inter_iff, Set.mem_range, SetLike.mem_coe, exists_and_right]
     refine ⟨?_, hx⟩
     simpa using ⟨_, 𝒰.covers x⟩
diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Separated.lean b/Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
@@ -126,7 +126,7 @@ lemma Scheme.Pullback.diagonalCoverDiagonalRange_eq_top_of_injective
   rw [← top_le_iff]
   rintro x -
   simp only [diagonalCoverDiagonalRange, openCoverOfBase_J, openCoverOfBase_obj,
-    openCoverOfLeftRight_J, Opens.iSup_mk, Opens.carrier_eq_coe, Hom.opensRange_coe, Opens.coe_mk,
+    openCoverOfLeftRight_J, Opens.iSup_mk, Opens.carrier_eq_coe, Hom.coe_opensRange, Opens.coe_mk,
     Set.mem_iUnion, Set.mem_range, Sigma.exists]
   have H : (pullback.fst f f).base x = (pullback.snd f f).base x :=
     hf (by rw [← Scheme.comp_base_apply, ← Scheme.comp_base_apply, pullback.condition])
@@ -147,7 +147,7 @@ lemma Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange :
     Set.range (pullback.diagonal f).base ⊆ diagonalCoverDiagonalRange f 𝒰 𝒱 := by
   rintro _ ⟨x, rfl⟩
   simp only [diagonalCoverDiagonalRange, openCoverOfBase_J, openCoverOfBase_obj,
-    openCoverOfLeftRight_J, Opens.iSup_mk, Opens.carrier_eq_coe, Hom.opensRange_coe, Opens.coe_mk,
+    openCoverOfLeftRight_J, Opens.iSup_mk, Opens.carrier_eq_coe, Hom.coe_opensRange, Opens.coe_mk,
     Set.mem_iUnion, Set.mem_range, Sigma.exists]
   let i := 𝒰.f (f.base x)
   obtain ⟨y : 𝒰.obj i, hy : (𝒰.map i).base y = f.base x⟩ := 𝒰.covers (f.base x)
diff --git a/Mathlib/AlgebraicGeometry/Noetherian.lean b/Mathlib/AlgebraicGeometry/Noetherian.lean
@@ -158,7 +158,7 @@ lemma isLocallyNoetherian_of_isOpenImmersion {Y : Scheme} (f : X ⟶ Y) [IsOpenI
   · suffices Scheme.Hom.opensRange f ⊓ V = V by
       rw [this]
     rw [← Opens.coe_inj]
-    rw [Opens.coe_inf, Scheme.Hom.opensRange_coe, IsOpenMap.functor_obj_coe,
+    rw [Opens.coe_inf, Scheme.Hom.coe_opensRange, IsOpenMap.coe_functor_obj,
       Set.inter_eq_right, Set.image_subset_iff, Set.preimage_range]
     exact Set.subset_univ _
 
diff --git a/Mathlib/AlgebraicGeometry/OpenImmersion.lean b/Mathlib/AlgebraicGeometry/OpenImmersion.lean
@@ -543,7 +543,7 @@ theorem range_pullback_to_base_of_left :
       Set.range f.base ∩ Set.range g.base := by
   rw [pullback.condition, Scheme.comp_base, TopCat.coe_comp, Set.range_comp,
     range_pullback_snd_of_left, Opens.carrier_eq_coe, Opens.map_obj, Opens.coe_mk,
-    Set.image_preimage_eq_inter_range, Opens.carrier_eq_coe, Scheme.Hom.opensRange_coe]
+    Set.image_preimage_eq_inter_range, Opens.carrier_eq_coe, Scheme.Hom.coe_opensRange]
 
 theorem range_pullback_to_base_of_right :
     Set.range (pullback.fst g f ≫ g).base =
diff --git a/Mathlib/AlgebraicGeometry/RationalMap.lean b/Mathlib/AlgebraicGeometry/RationalMap.lean
@@ -247,7 +247,7 @@ lemma equiv_of_fromSpecStalkOfMem_eq [IrreducibleSpace X]
       ((Set.image_subset_range _ _).trans_eq (Subtype.range_val)).trans inf_le_left,
       ((Set.image_subset_range _ _).trans_eq (Subtype.range_val)).trans inf_le_right, ?_⟩
     rw [← cancel_epi (Scheme.Hom.isoImage _ _).hom]
-    simp only [TopologicalSpace.Opens.carrier_eq_coe, IsOpenMap.functor_obj_coe,
+    simp only [TopologicalSpace.Opens.carrier_eq_coe, IsOpenMap.coe_functor_obj,
       TopologicalSpace.Opens.coe_inf, restrict_hom, ← Category.assoc] at e ⊢
     convert e using 2 <;> rw [← cancel_mono (Scheme.Opens.ι _)] <;> simp
   · rw [← f.fromSpecStalkOfMem_restrict hdense inf_le_left ⟨hxf, hxg⟩,
diff --git a/Mathlib/AlgebraicGeometry/Restrict.lean b/Mathlib/AlgebraicGeometry/Restrict.lean
@@ -233,7 +233,7 @@ theorem Scheme.homOfLE_apply {U V : X.Opens} (e : U ≤ V) (x : U) :
 
 theorem Scheme.ι_image_homOfLE_le_ι_image {U V : X.Opens} (e : U ≤ V) (W : Opens V) :
     U.ι ''ᵁ (X.homOfLE e ⁻¹ᵁ W) ≤ V.ι ''ᵁ W := by
-  simp only [← SetLike.coe_subset_coe, IsOpenMap.functor_obj_coe, Set.image_subset_iff,
+  simp only [← SetLike.coe_subset_coe, IsOpenMap.coe_functor_obj, Set.image_subset_iff,
     Scheme.homOfLE_base, Opens.map_coe, Opens.inclusion'_apply]
   rintro _ h
   exact ⟨_, h, rfl⟩
@@ -595,7 +595,7 @@ def morphismRestrictRestrict {X Y : Scheme.{u}} (f : X ⟶ Y) (U : Y.Opens) (V :
   refine Arrow.isoMk' _ _ ((Scheme.Opens.ι _).isoImage _ ≪≫ Scheme.isoOfEq _ ?_)
     ((Scheme.Opens.ι _).isoImage _) ?_
   · ext x
-    simp only [IsOpenMap.functor_obj_coe, Opens.coe_inclusion',
+    simp only [IsOpenMap.coe_functor_obj, Opens.coe_inclusion',
       Opens.map_coe, Set.mem_image, Set.mem_preimage, SetLike.mem_coe, morphismRestrict_base]
     constructor
     · rintro ⟨⟨a, h₁⟩, h₂, rfl⟩
diff --git a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean
@@ -156,7 +156,7 @@ instance comp {Z : PresheafedSpace C} (g : Y ⟶ Z) [hg : IsOpenImmersion g] :
     · exact c_iso' g ((opensFunctor f).obj U) (by ext; simp)
     · apply c_iso' f U
       ext1
-      dsimp only [Opens.map_coe, IsOpenMap.functor_obj_coe, comp_base, TopCat.coe_comp]
+      dsimp only [Opens.map_coe, IsOpenMap.coe_functor_obj, comp_base, TopCat.coe_comp]
       rw [Set.image_comp, Set.preimage_image_eq _ hg.base_open.injective]
 
 /-- For an open immersion `f : X ⟶ Y` and an open set `U ⊆ X`, we have the map `X(U) ⟶ Y(U)`. -/
diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
@@ -242,7 +242,7 @@ theorem ι_image_preimage_eq (i j : D.J) (U : Opens (D.U i).carrier) :
       (opensFunctor (D.f j i)).obj
         ((Opens.map (𝖣.t j i).base).obj ((Opens.map (𝖣.f i j).base).obj U)) := by
   ext1
-  dsimp only [Opens.map_coe, IsOpenMap.functor_obj_coe]
+  dsimp only [Opens.map_coe, IsOpenMap.coe_functor_obj]
   rw [← show _ = (𝖣.ι i).base from 𝖣.ι_gluedIso_inv (PresheafedSpace.forget _) i, ←
     show _ = (𝖣.ι j).base from 𝖣.ι_gluedIso_inv (PresheafedSpace.forget _) j]
   -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11224): change `rw` to `erw` on `coe_comp`
@@ -328,7 +328,7 @@ def ιInvAppπApp {i : D.J} (U : Opens (D.U i).carrier) (j) :
       D.opensImagePreimageMap i j U ≫ (D.f j k).c.app _ ≫ (D.V (j, k)).presheaf.map (eqToHom ?_)
     rw [Functor.op_obj]
     congr 1; ext1
-    dsimp only [Functor.op_obj, Opens.map_coe, unop_op, IsOpenMap.functor_obj_coe]
+    dsimp only [Functor.op_obj, Opens.map_coe, unop_op, IsOpenMap.coe_functor_obj]
     rw [Set.preimage_preimage]
     change (D.f j k ≫ 𝖣.ι j).base ⁻¹' _ = _
     -- Porting note: used to be `congr 3`
diff --git a/Mathlib/ModelTheory/Substructures.lean b/Mathlib/ModelTheory/Substructures.lean
@@ -106,7 +106,7 @@ instance instSetLike : SetLike (L.Substructure M) M :=
 def Simps.coe (S : L.Substructure M) : Set M :=
   S
 
-initialize_simps_projections Substructure (carrier → coe)
+initialize_simps_projections Substructure (carrier → coe, as_prefix coe)
 
 @[simp]
 theorem mem_carrier {s : L.Substructure M} {x : M} : x ∈ s.carrier ↔ x ∈ s :=
diff --git a/Mathlib/Order/UpperLower/Basic.lean b/Mathlib/Order/UpperLower/Basic.lean
@@ -429,7 +429,7 @@ instance : SetLike (UpperSet α) α where
 /-- See Note [custom simps projection]. -/
 def Simps.coe (s : UpperSet α) : Set α := s
 
-initialize_simps_projections UpperSet (carrier → coe)
+initialize_simps_projections UpperSet (carrier → coe, as_prefix coe)
 
 @[ext]
 theorem ext {s t : UpperSet α} : (s : Set α) = t → s = t :=
@@ -455,7 +455,7 @@ instance : SetLike (LowerSet α) α where
 /-- See Note [custom simps projection]. -/
 def Simps.coe (s : LowerSet α) : Set α := s
 
-initialize_simps_projections LowerSet (carrier → coe)
+initialize_simps_projections LowerSet (carrier → coe, as_prefix coe)
 
 @[ext]
 theorem ext {s t : LowerSet α} : (s : Set α) = t → s = t :=
diff --git a/Mathlib/Tactic/ToAdditive/Frontend.lean b/Mathlib/Tactic/ToAdditive/Frontend.lean
@@ -977,6 +977,7 @@ def nameDict : String → List String
   | "multipliable"=> ["summable"]
   | "gpfree"      => ["apfree"]
   | "quantale"    => ["add", "Quantale"]
+  | "square"      => ["even"]
   | x             => [x]
 
 /--
@@ -1007,8 +1008,10 @@ def fixAbbreviation : List String → List String
   | "Comm" :: "Add" :: s              => "AddComm" :: fixAbbreviation s
   | "Zero" :: "LE" :: s               => "Nonneg" :: fixAbbreviation s
   | "zero" :: "_" :: "le" :: s        => "nonneg" :: fixAbbreviation s
+  | "zero" :: "LE" :: s               => "nonneg" :: fixAbbreviation s
   | "Zero" :: "LT" :: s               => "Pos" :: fixAbbreviation s
   | "zero" :: "_" :: "lt" :: s        => "pos" :: fixAbbreviation s
+  | "zero" :: "LT" :: s               => "pos" :: fixAbbreviation s
   | "LE" :: "Zero" :: s               => "Nonpos" :: fixAbbreviation s
   | "le" :: "_" :: "zero" :: s        => "nonpos" :: fixAbbreviation s
   | "LT" :: "Zero" :: s               => "Neg" :: fixAbbreviation s
@@ -1025,9 +1028,8 @@ def fixAbbreviation : List String → List String
   | "Add" :: "Indicator" :: s         => "Indicator" :: fixAbbreviation s
   | "add" :: "Indicator" :: s         => "indicator" :: fixAbbreviation s
   | "add" :: "_" :: "indicator" :: s  => "indicator" :: fixAbbreviation s
-  | "is" :: "Square" :: s             => "even" :: fixAbbreviation s
-  | "Is" :: "Square" :: s             => "Even" :: fixAbbreviation s
-  | "square" :: "In" :: s             => "evenIn" :: fixAbbreviation s
+  | "is" :: "Even" :: s             => "even" :: fixAbbreviation s
+  | "Is" :: "Even" :: s             => "Even" :: fixAbbreviation s
   -- "Regular" is well-used in mathlib with various meanings (e.g. in
   -- measure theory) and a direct translation
   -- "regular" --> ["add", "Regular"] in `nameDict` above seems error-prone.
diff --git a/Mathlib/Topology/Category/TopCat/Opens.lean b/Mathlib/Topology/Category/TopCat/Opens.lean
@@ -409,7 +409,7 @@ lemma set_range_inclusion' {X : TopCat} (U : Opens X) :
 theorem functor_map_eq_inf {X : TopCat} (U V : Opens X) :
     U.isOpenEmbedding.isOpenMap.functor.obj ((Opens.map U.inclusion').obj V) = V ⊓ U := by
   ext1
-  simp only [IsOpenMap.functor_obj_coe, map_coe, coe_inf,
+  simp only [IsOpenMap.coe_functor_obj, map_coe, coe_inf,
     Set.image_preimage_eq_inter_range, set_range_inclusion' U]
 
 theorem map_functor_eq' {X U : TopCat} (f : U ⟶ X) (hf : IsOpenEmbedding f) (V) :
diff --git a/Mathlib/Topology/Sets/Closeds.lean b/Mathlib/Topology/Sets/Closeds.lean
@@ -274,7 +274,7 @@ theorem isClopen (s : Clopens α) : IsClopen (s : Set α) :=
 /-- See Note [custom simps projection]. -/
 def Simps.coe (s : Clopens α) : Set α := s
 
-initialize_simps_projections Clopens (carrier → coe)
+initialize_simps_projections Clopens (carrier → coe, as_prefix coe)
 
 /-- Reinterpret a clopen as an open. -/
 @[simps]
diff --git a/Mathlib/Topology/Sets/Compacts.lean b/Mathlib/Topology/Sets/Compacts.lean
@@ -45,7 +45,7 @@ instance : SetLike (Compacts α) α where
 /-- See Note [custom simps projection]. -/
 def Simps.coe (s : Compacts α) : Set α := s
 
-initialize_simps_projections Compacts (carrier → coe)
+initialize_simps_projections Compacts (carrier → coe, as_prefix coe)
 
 protected theorem isCompact (s : Compacts α) : IsCompact (s : Set α) :=
   s.isCompact'
@@ -197,7 +197,7 @@ instance : SetLike (NonemptyCompacts α) α where
 /-- See Note [custom simps projection]. -/
 def Simps.coe (s : NonemptyCompacts α) : Set α := s
 
-initialize_simps_projections NonemptyCompacts (carrier → coe)
+initialize_simps_projections NonemptyCompacts (carrier → coe, as_prefix coe)
 
 protected theorem isCompact (s : NonemptyCompacts α) : IsCompact (s : Set α) :=
   s.isCompact'
@@ -288,7 +288,7 @@ instance : SetLike (PositiveCompacts α) α where
 /-- See Note [custom simps projection]. -/
 def Simps.coe (s : PositiveCompacts α) : Set α := s
 
-initialize_simps_projections PositiveCompacts (carrier → coe)
+initialize_simps_projections PositiveCompacts (carrier → coe, as_prefix coe)
 
 protected theorem isCompact (s : PositiveCompacts α) : IsCompact (s : Set α) :=
   s.isCompact'
@@ -417,7 +417,7 @@ instance : SetLike (CompactOpens α) α where
 /-- See Note [custom simps projection]. -/
 def Simps.coe (s : CompactOpens α) : Set α := s
 
-initialize_simps_projections CompactOpens (carrier → coe)
+initialize_simps_projections CompactOpens (carrier → coe, as_prefix coe)
 
 protected theorem isCompact (s : CompactOpens α) : IsCompact (s : Set α) :=
   s.isCompact'
diff --git a/Mathlib/Topology/Sets/Opens.lean b/Mathlib/Topology/Sets/Opens.lean
@@ -118,7 +118,7 @@ protected theorem isOpen (U : Opens α) : IsOpen (U : Set α) :=
 /-- See Note [custom simps projection]. -/
 def Simps.coe (U : Opens α) : Set α := U
 
-initialize_simps_projections Opens (carrier → coe)
+initialize_simps_projections Opens (carrier → coe, as_prefix coe)
 
 /-- The interior of a set, as an element of `Opens`. -/
 @[simps]
diff --git a/Mathlib/Topology/Sets/Order.lean b/Mathlib/Topology/Sets/Order.lean
@@ -36,7 +36,7 @@ instance : SetLike (ClopenUpperSet α) α where
 /-- See Note [custom simps projection]. -/
 def Simps.coe (s : ClopenUpperSet α) : Set α := s
 
-initialize_simps_projections ClopenUpperSet (carrier → coe)
+initialize_simps_projections ClopenUpperSet (carrier → coe, as_prefix coe)
 
 theorem upper (s : ClopenUpperSet α) : IsUpperSet (s : Set α) :=
   s.upper'
