From 871aabc9197749b3afaac6d9a072892106204bca Mon Sep 17 00:00:00 2001
From: FM22 <artem.khovanov@gmail.com>
Date: Tue, 24 Dec 2024 00:45:45 +0000
Subject: [PATCH] switch to IsSquare

---
 .../RealClosedField/RingOrdering/Adjoin.lean  | 15 +++++------
 .../RealClosedField/RingOrdering/Basic.lean   | 27 +++++++++----------
 .../RealClosedField/RingOrdering/Defs.lean    | 16 ++++++++---
 3 files changed, 32 insertions(+), 26 deletions(-)

diff --git a/RealClosedField/RealClosedField/RingOrdering/Adjoin.lean b/RealClosedField/RealClosedField/RingOrdering/Adjoin.lean
index af994a7..de33794 100644
--- a/RealClosedField/RealClosedField/RingOrdering/Adjoin.lean
+++ b/RealClosedField/RealClosedField/RingOrdering/Adjoin.lean
@@ -14,7 +14,7 @@ variable {R : Type*} [CommRing R] (P : RingPreordering R) (a : R)
 
 namespace Subsemiring
 
-/-- An explicit form of the semiring generated by a preordering `P` and an element `a`. -/
+/-- An explicit form for the semiring generated by a preordering `P` and an element `a`. -/
 def ringPreordering_adjoin : Subsemiring R where
   carrier := {z : R | ∃ x ∈ P, ∃ y ∈ P, z = x + a * y}
   zero_mem' := ⟨0, by aesop, 0, by aesop, by simp⟩
@@ -36,8 +36,8 @@ lemma subset_ringPreordering_adjoin {x : R} (hx : x ∈ P) :
 lemma mem_ringPreordering_adjoin : a ∈ ringPreordering_adjoin P a :=
   ⟨0, by aesop, 1, by aesop, by simp⟩
 
-@[aesop safe 0 apply (rule_sets := [SetLike])]
-lemma square_mem_ringPreordering_adjoin (x : R) : x * x ∈ ringPreordering_adjoin P a :=
+@[aesop unsafe 50% apply (rule_sets := [SetLike])]
+lemma isSquare_mem_ringPreordering_adjoin {x : R} (hx : IsSquare x) : x ∈ ringPreordering_adjoin P a :=
   by simpa using subset_ringPreordering_adjoin a (by aesop)
 
 theorem closure_insert_eq_ringPreordering_adjoin :
@@ -49,10 +49,9 @@ end Subsemiring
 namespace RingPreordering
 
 variable {P a} in
-def adjoin (h : -1 ∉ Subsemiring.ringPreordering_adjoin P a) :
-    RingPreordering R where
+def adjoin (h : -1 ∉ Subsemiring.ringPreordering_adjoin P a) : RingPreordering R where
   __ := Subsemiring.ringPreordering_adjoin P a
-  square_mem' := by aesop
+  isSquare_mem' := by aesop
   minus_one_not_mem' := h
 
 variable {P a} in
@@ -74,7 +73,7 @@ lemma mem_adjoin (h : -1 ∉ Subsemiring.ringPreordering_adjoin P a) : a ∈ adj
 -/
 
 variable {P} in
-theorem not_mem_adjoin_or {x y : R} (h : - (x * y) ∈ P) :
+theorem not_mem_adjoin_or {x y : R} (h : -(x * y) ∈ P) :
     -1 ∉ Subsemiring.ringPreordering_adjoin P x ∨ -1 ∉ Subsemiring.ringPreordering_adjoin P y := by
   by_contra
   apply RingPreordering.minus_one_not_mem P
@@ -86,7 +85,7 @@ theorem not_mem_adjoin_or {x y : R} (h : - (x * y) ∈ P) :
 
 theorem not_mem_adjoin_or' :
     -1 ∉ Subsemiring.ringPreordering_adjoin P a ∨ -1 ∉ Subsemiring.ringPreordering_adjoin P (-a) :=
-  not_mem_adjoin_or (by aesop : - (a * (-a)) ∈ P)
+  not_mem_adjoin_or (by aesop : -(a * (-a)) ∈ P)
 
 theorem minus_one_not_mem_ringPreordering_adjoin
     (h : ∀ x y, x ∈ P → y ∈ P → x + (1 + y) * a + 1 ≠ 0) :
diff --git a/RealClosedField/RealClosedField/RingOrdering/Basic.lean b/RealClosedField/RealClosedField/RingOrdering/Basic.lean
index db98951..1b30796 100644
--- a/RealClosedField/RealClosedField/RingOrdering/Basic.lean
+++ b/RealClosedField/RealClosedField/RingOrdering/Basic.lean
@@ -49,9 +49,9 @@ theorem Field.inv_mem {F : Type*} [Field F] {P : RingPreordering F} {a : F} (ha
   rw [show a⁻¹ = a * (a⁻¹ * a⁻¹) by field_simp]
   aesop
 
-/- TODO : decide whether to rewrite RingPreordering stuff to use IsSquare -/
-/- TODO : decide whether/how to improve IsSquare automation -/
-theorem mem_of_isSumSq {x : R} (hx : IsSumSq x) : x ∈ P := sorry
+theorem mem_of_isSumSq {x : R} (hx : IsSumSq x) : x ∈ P := by
+  rcases IsSumSq.exists_sum hx with ⟨_, _, _, _, rfl⟩
+  exact sum_mem (by aesop)
 
 section mk'
 variable {R : Type*} [CommRing R] {P : Set R} {add} {mul} {sq} {minus}
@@ -66,7 +66,7 @@ def mk' {R : Type*} [CommRing R] (P : Set R)
   carrier := P
   add_mem' {x y} := by simpa using add
   mul_mem' {x y} := by simpa using mul
-  square_mem' x := by simpa using sq x
+  isSquare_mem' hx := by rcases hx with ⟨y, hy⟩; aesop /- TODO : automate? -/
   minus_one_not_mem' := by simpa using minus
   zero_mem' := by simpa using sq 0
   one_mem' := by simpa using sq 1
@@ -122,7 +122,7 @@ theorem support_eq_bot {F : Type*} [Field F] (P : RingPreordering F) :
   refine AddSubgroup.ext (fun x => Iff.intro (fun h => ?_) (fun h => by aesop))
   by_contra hz
   apply RingPreordering.minus_one_not_mem P
-  rw [show -1 = -x * (x)⁻¹ by field_simp [show x ≠ 0 by simp_all]]
+  rw [show -1 = -x * x⁻¹ by field_simp [show x ≠ 0 by simp_all]]
   aesop (erase simp neg_mul)
 
 /-!
@@ -186,7 +186,7 @@ variable {P₁ P₂ : RingPreordering R}
 
 instance : Min (RingPreordering R) where
   min P₁ P₂ := { min P₁.toSubsemiring P₂.toSubsemiring with
-                  square_mem' := by aesop
+                  isSquare_mem' := by aesop
                   minus_one_not_mem' := by aesop }
 
 @[simp]
@@ -208,7 +208,7 @@ variable {S : Set (RingPreordering R)} {hS : S.Nonempty}
 variable (hS) in
 def sInf {S : Set (RingPreordering R)} (hS : S.Nonempty) : RingPreordering R where
   __ := InfSet.sInf (RingPreordering.toSubsemiring '' S)
-  square_mem' x := by aesop (add simp Submonoid.mem_iInf)
+  isSquare_mem' x := by aesop (add simp Submonoid.mem_iInf)
   minus_one_not_mem' := by aesop (add simp Submonoid.mem_iInf,
                                       unsafe forward (Set.Nonempty.some_mem hS))
 
@@ -244,7 +244,7 @@ variable {S : Set (RingPreordering R)} {hS : S.Nonempty} {hSd : DirectedOn (· 
 variable (hS) (hSd) in
 def sSup : RingPreordering R where
   __ := SupSet.sSup (toSubsemiring '' S)
-  square_mem' x := by
+  isSquare_mem' x := by
     have : DirectedOn (· ≤ ·) (toSubsemiring '' S) := directedOn_image.mpr hSd
     aesop (add simp Subsemiring.mem_sSup_of_directedOn,
                unsafe forward (Set.Nonempty.some_mem hS))
@@ -288,7 +288,7 @@ variable [IsSemireal R]
 
 instance : Bot (RingPreordering R) where
   bot := { Subsemiring.sumSqIn R with
-            square_mem' := by aesop
+            isSquare_mem' := by aesop
             minus_one_not_mem' := by simpa using IsSemireal.not_isSumSq_neg_one }
 
 @[simp] lemma bot_toSubsemiring : (⊥ : RingPreordering R).toSubsemiring = .sumSqIn R := rfl
@@ -309,7 +309,7 @@ variable {A B C : Type*} [CommRing A] [CommRing B] [CommRing C]
 /-- The preimage of a preordering along a ring homomorphism is a preordering. -/
 def comap (f : A →+* B) (P : RingPreordering B) : RingPreordering A where
   __ := P.toSubsemiring.comap f
-  square_mem' x := by aesop
+  isSquare_mem' := by aesop (add unsafe apply IsSquare.map) /- TODO : automate? -/
   minus_one_not_mem' := by aesop
 
 @[simp]
@@ -360,8 +360,9 @@ instance comap.instIsPrimeOrdering (P : RingPreordering B) [IsPrimeOrdering P] (
 def map {f : A →+* B} {P : RingPreordering A} (hf : Function.Surjective f)
     (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P) : RingPreordering B where
   __ := P.toSubsemiring.map f
-  square_mem' x := by
-    obtain ⟨x', rfl⟩ := hf x
+  isSquare_mem' hx := by
+    rcases hx with ⟨y, rfl⟩
+    rcases hf y with ⟨y', rfl⟩ /- TODO : generalise? ie Surjective f → IsSquare x → ∃ y, f y = x ∧ IsSquare y -/
     aesop
   minus_one_not_mem' := fun ⟨x', hx', _⟩ => by
     have : -(x' + 1) + x' ∈ P := add_mem (hsupp (show f (x' + 1) = 0 by simp_all)).2 hx'
@@ -436,5 +437,3 @@ instance map.instIsPrimeOrdering {f : A →+* B} {P : RingPreordering A} [IsPrim
   infer_instance
 
 end RingPreordering
-
-/- TODO : look into changing aesop mul_mem tag to unsafe -/
diff --git a/RealClosedField/RealClosedField/RingOrdering/Defs.lean b/RealClosedField/RealClosedField/RingOrdering/Defs.lean
index 94802b7..490aef1 100644
--- a/RealClosedField/RealClosedField/RingOrdering/Defs.lean
+++ b/RealClosedField/RealClosedField/RingOrdering/Defs.lean
@@ -6,6 +6,7 @@ Authors: Florent Schaffhauser, Artie Khovanov
 
 import Mathlib.Algebra.Ring.Subsemiring.Basic
 import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.Algebra.Group.Even
 
 /-!
 ## Preorderings
@@ -17,7 +18,7 @@ variable (R : Type*) [CommRing R]
 but not containing `-1`. -/
 @[ext]
 structure RingPreordering extends Subsemiring R where
-  square_mem' (x : R) : x * x ∈ carrier
+  isSquare_mem' {x : R} (hx : IsSquare x) : x ∈ carrier
   minus_one_not_mem' : -1 ∉ carrier
 
 namespace RingPreordering
@@ -36,9 +37,16 @@ instance : SubsemiringClass (RingPreordering R) R where
 
 variable {R}
 
+/- TODO : make this change in the actual location -/
+attribute [- aesop] mul_mem add_mem
+attribute [aesop unsafe 90% apply (rule_sets := [SetLike])] mul_mem add_mem
+
+@[aesop unsafe 50% apply (rule_sets := [SetLike])]
+protected theorem isSquare_mem (P : RingPreordering R) {x : R} (hx : IsSquare x) : x ∈ P :=
+  RingPreordering.isSquare_mem' _ hx
+
 @[aesop safe 0 apply (rule_sets := [SetLike])]
-protected theorem square_mem (P : RingPreordering R) (x : R) : x * x ∈ P :=
-  RingPreordering.square_mem' _ _
+protected theorem mul_self_mem (P : RingPreordering R) (x : R) : x * x ∈ P := by aesop
 
 @[aesop unsafe 20% forward (rule_sets := [SetLike])]
 protected theorem minus_one_not_mem (P : RingPreordering R) : -1 ∉ P :=
@@ -71,7 +79,7 @@ protected def copy : RingPreordering R where
   add_mem' ha hb := by aesop
   one_mem' := by aesop
   mul_mem' ha hb := by aesop
-  square_mem' := by aesop
+  isSquare_mem' := by aesop
   minus_one_not_mem' := by aesop
 
 @[simp]