more fix

RealClosedField/RealClosedField/FormallyReal.lean

@@ -5,7 +5,6 @@ Authors: Artie Khovanov
 -/
 import RealClosedField.Mathlib.Algebra.Order.Ring.Cone
 import RealClosedField.Mathlib.Algebra.Ring.Semireal.Defs
-import Mathlib.Tactic.LinearCombination
 
 class IsFormallyReal (R : Type*) [AddCommMonoid R] [Mul R] : Prop where
   eq_zero_of_mul_self_add {a s : R} (hs : IsSumSq s) (h : a * a + s = 0) : a = 0

RealClosedField/RealClosedField/RingOrdering/Adjoin.lean

@@ -6,6 +6,10 @@ Authors: Florent Schaffhauser, Artie Khovanov
 import RealClosedField.RealClosedField.RingOrdering.Basic
 import Mathlib.Order.Zorn
 
+/- TODO : make this change in the actual location -/
+attribute [- aesop] mul_mem add_mem
+attribute [aesop unsafe 99% apply (rule_sets := [SetLike])] mul_mem add_mem
+
 /-!
 ## Adjoining an element to a preordering
 -/
@@ -20,25 +24,25 @@ def ringPreordering_adjoin : Subsemiring R where
   zero_mem' := ⟨0, by aesop, 0, by aesop, by simp⟩
   one_mem' := ⟨1, by aesop, 0, by aesop, by simp⟩
   add_mem' := fun ha hb => by
-    obtain ⟨x₁, hx₁, y₁, hy₁, eqw⟩ := ha
-    obtain ⟨x₂, hx₂, y₂, hy₂, eqz⟩ := hb
-    exact ⟨x₁ + x₂, by aesop, y₁ + y₂, by aesop, by linear_combination eqw + eqz⟩
-  mul_mem' := fun {w z} ⟨x₁, hx₁, y₁, hy₁, eqw⟩ ⟨x₂, hx₂, y₂, hy₂, eqz⟩ => by
+    rcases ha, hb with ⟨⟨x₁, hx₁, y₁, hy₁, rfl⟩, ⟨x₂, hx₂, y₂, hy₂, rfl⟩⟩
+    exact ⟨x₁ + x₂, by aesop, y₁ + y₂, by aesop, by linear_combination⟩
+  mul_mem' := fun ha hb => by
+    rcases ha, hb with ⟨⟨x₁, hx₁, y₁, hy₁, rfl⟩, ⟨x₂, hx₂, y₂, hy₂, rfl⟩⟩
     exact ⟨x₁ * x₂ + (a * a) * (y₁ * y₂), by aesop, x₁ * y₂ + y₁ * x₂, by aesop,
-      by linear_combination z * eqw + (a * y₁ + x₁) * eqz⟩
+      by linear_combination⟩
 
 variable {P} in
 @[aesop unsafe 70% apply (rule_sets := [SetLike])]
-lemma subset_ringPreordering_adjoin {x : R} (hx : x ∈ P) :
+lemma mem_ringPreordering_adjoin_of_mem {x : R} (hx : x ∈ P) :
     x ∈ ringPreordering_adjoin P a := ⟨x, by aesop, 0, by aesop, by simp⟩
 
-@[aesop safe 0 apply (rule_sets := [SetLike])]
+@[aesop safe apply (rule_sets := [SetLike])]
 lemma mem_ringPreordering_adjoin : a ∈ ringPreordering_adjoin P a :=
   ⟨0, by aesop, 1, by aesop, by simp⟩
 
 @[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)
+  by simpa using mem_ringPreordering_adjoin_of_mem a (by aesop)
 
 theorem closure_insert_eq_ringPreordering_adjoin :
     closure (insert a P) = ringPreordering_adjoin P a :=
@@ -57,7 +61,7 @@ def adjoin (h : -1 ∉ Subsemiring.ringPreordering_adjoin P a) : RingPreordering
 variable {P a} in
 @[aesop unsafe 70% apply (rule_sets := [SetLike])]
 lemma subset_adjoin' (h : -1 ∉ Subsemiring.ringPreordering_adjoin P a) {x : R} (hx : x ∈ P) :
-    x ∈ adjoin h := Subsemiring.subset_ringPreordering_adjoin a hx
+    x ∈ adjoin h := Subsemiring.mem_ringPreordering_adjoin_of_mem a hx
 
 variable {P a} in
 lemma subset_adjoin (h : -1 ∉ Subsemiring.ringPreordering_adjoin P a) : (P : Set R) ⊆ adjoin h :=

RealClosedField/RealClosedField/RingOrdering/Basic.lean

@@ -12,7 +12,7 @@ import RealClosedField.RealClosedField.RingOrdering.Defs
 
 /- 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
+attribute [aesop unsafe 99% apply (rule_sets := [SetLike])] mul_mem add_mem
 
 variable {R : Type*} [CommRing R] {P : RingPreordering R}
 
@@ -369,6 +369,7 @@ def map {f : A →+* B} {P : RingPreordering A} (hf : Function.Surjective f)
   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 -/
+    simp_all
     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'
@@ -399,7 +400,7 @@ instance map.instIsOrdering {f : A →+* B} {P : RingPreordering A} [IsOrdering
 theorem AddSubgroup.mem_map_support {f : A →+* B} {P : RingPreordering A}
     {hf : Function.Surjective f} {hsupp : (RingHom.ker f : Set A) ⊆ support P} {x : B} :
     x ∈ support (map hf hsupp) ↔ ∃ y ∈ support P, f y = x := by
-  refine Iff.intro (fun ⟨⟨a, ⟨ha₁, ha₂⟩⟩, ⟨b, ⟨hb₁, hb₂⟩⟩⟩ => ?_) (by aesop)
+  refine Iff.intro (fun ⟨⟨a, ⟨ha₁, ha₂⟩⟩, ⟨b, ⟨hb₁, hb₂⟩⟩⟩ => ?_) (by aesop?)
   have : -(a + b) + b ∈ P := by exact add_mem (hsupp (show f (a + b) = 0 by simp_all)).2 hb₁
   aesop
 

RealClosedField/RealClosedField/RingOrdering/Defs.lean

@@ -39,7 +39,7 @@ 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
+attribute [aesop unsafe 99% 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 :=

RealClosedField/RealClosedField/Semireal/Field.lean

@@ -7,29 +7,29 @@ import RealClosedField.RealClosedField.FormallyReal
 import RealClosedField.RealClosedField.RingOrdering.Order
 import RealClosedField.RealClosedField.RingOrdering.Adjoin
 
-variable (S F : Type*) [Field F] [SetLike S F] [RingPreorderingClass S F]
+variable (F : Type*) [Field F]
 
-instance RingPreorderingClass.instRingConeClass : RingConeClass S F where
+instance : RingConeClass (RingPreordering F) F where
   eq_zero_of_mem_of_neg_mem {P} {a} ha hna := by
     by_contra h
     have : a⁻¹ * -a ∈ P := by aesop (config := { enableSimp := False })
-    exact minus_one_not_mem P (by aesop)
+    aesop
 
-instance RingPreorderingClass.instIsMaxCone (O : S) [RingPreordering.IsOrdering O] : IsMaxCone O
-    where
+/- TODO : decide whether to unify these -/
+instance (O : RingPreordering F) [RingPreordering.IsOrdering O] : IsMaxCone O where
   mem_or_neg_mem' := RingPreordering.mem_or_neg_mem O
 
-open Classical in
 instance IsSemireal.instIsFormallyReal [IsSemireal F] : IsFormallyReal F where
-  eq_zero_of_sum_of_squares_eq_zero {ι} {I} {x} {i} hx hi := by
+  eq_zero_of_mul_self_add {a} {s} hs h := by
     by_contra
-    exact add_one_ne_zero_of_isSumSq (IsSumSq.mul (IsSumSq.sum_mul_self _) (IsSumSq.mul_self _))
-      (show 1 + (∑ j ∈ I.erase i, x j * x j) * ((x i)⁻¹ * (x i)⁻¹) = 0 by field_simp [hx])
+    exact add_one_ne_zero_of_isSumSq (by aesop) (show 1 + s * (a⁻¹ * a⁻¹) = 0 by field_simp [h])
+
+variable [IsSemireal F]
 
 open Classical RingPreordering in
 noncomputable def LinearOrderedField.mkOfIsSemireal [IsSemireal F] : LinearOrderedField F where
-  __ := have := (choose_spec <| exists_le_isPrimeOrdering <| sumSqIn F).2
-        LinearOrderedRing.mkOfCone (choose <| exists_le_isPrimeOrdering <| sumSqIn F)
+  __ := have := (choose_spec <| exists_le_isPrimeOrdering (⊥ : RingPreordering F)).2
+        LinearOrderedRing.mkOfCone (choose <| exists_le_isPrimeOrdering ⊥)
   __ := ‹Field F›
 
 theorem ArtinSchreier_basic :