improve proofs, fix instance trouble

RealClosedField/Mathlib/Algebra/Order/Ring/Cone.lean

@@ -60,7 +60,7 @@ def nonneg : RingCone T where
 @[simp, norm_cast] lemma coe_nonneg : nonneg T = {x : T | 0 ≤ x} := rfl
 
 instance nonneg.isMaxCone {T : Type*} [LinearOrderedRing T] : IsMaxCone (nonneg T) where
-  mem_or_neg_mem := mem_or_neg_mem (C := AddGroupCone.nonneg T)
+  mem_or_neg_mem' := mem_or_neg_mem <| AddGroupCone.nonneg T
 
 end RingCone
 
@@ -79,12 +79,11 @@ due to non-customisable field: `lt`. -/
 Warning: using this def as a constructor in an instance can lead to diamonds
 due to non-customisable fields: `lt`, `decidableLT`, `decidableEq`, `compare`. -/
 @[reducible] def LinearOrderedRing.mkOfCone
-    [IsDomain R] [IsMaxCone C]
-    (dec : DecidablePred (· ∈ C)) : LinearOrderedRing R where
+    [IsDomain R] [IsMaxCone C] [DecidablePred (· ∈ C)] : LinearOrderedRing R where
   __ := OrderedRing.mkOfCone C
   __ := OrderedRing.toStrictOrderedRing R
-  le_total a b := by simpa using mem_or_neg_mem (b - a)
-  decidableLE a b := dec _
+  le_total a b := by simpa using mem_or_neg_mem C (b - a)
+  decidableLE a b := _
 
 instance RingConeClass.instSetLike_of_isMaxCone {S R : Type*}
     [CommRing R] [SetLike S R] [RingConeClass S R] : SetLike {x : S // IsMaxCone x} R
@@ -105,18 +104,18 @@ instance RingConeClass.instRingPreorderingClass_of_isMaxCone {S R : Type*} [Nont
     [CommRing R] [SetLike S R] [RingConeClass S R] :
     RingPreorderingClass {x : S // IsMaxCone x} (R := R) where
   __ := RingConeClass.toSubsemiringClass
-  square_mem P x := by
-    cases @mem_or_neg_mem S _ _ _ _ P.2 x with
+  square_mem C x := by
+    obtain ⟨C, hC⟩ := C
+    cases mem_or_neg_mem C x with
     | inl hx  => aesop
-    | inr hnx => have : -x * -x ∈ P := by aesop (config := { enableSimp := false })
-                 simpa
-  minus_one_not_mem P h := one_ne_zero <| eq_zero_of_mem_of_neg_mem (one_mem ↑P) h
+    | inr hnx => simpa using (show -x * -x ∈ C by aesop (config := { enableSimp := false }))
+  minus_one_not_mem C h := one_ne_zero <| eq_zero_of_mem_of_neg_mem (one_mem C) h
 
 open Classical in
 /-- A maximal cone over a commutative ring `R` is an ordering on `R`. -/
 instance RingConeClass.instIsOrdering_of_isMaxCone {S R : Type*} [Nontrivial R]
     [CommRing R] [SetLike S R] [RingConeClass S R] (C : {x : S // IsMaxCone x}) :
     RingPreordering.IsOrdering C where
-  mem_or_neg_mem' x := @mem_or_neg_mem S _ _ _ _ C.2 x
+  mem_or_neg_mem' x := by obtain ⟨C, hC⟩ := C; exact mem_or_neg_mem C x
 
 /- TODO : decide whether to keep this cursed subtype instance, or whether to change to a def. -/

RealClosedField/RealClosedField/RingOrdering/Adjoin.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Florent Schaffhauser, Artie Khovanov
 -/
 import RealClosedField.RealClosedField.RingOrdering.Basic
-
 import Mathlib.Order.Zorn
 
 /-
@@ -21,13 +20,12 @@ 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₁, rfl⟩ := ha
-    obtain ⟨x₂, hx₂, y₂, hy₂, rfl⟩ := hb
-    exact ⟨x₁ + x₂, by aesop, y₁ + y₂, by aesop, by ring⟩
-  mul_mem' := fun ha hb => by
-    obtain ⟨x₁, hx₁, y₁, hy₁, rfl⟩ := ha
-    obtain ⟨x₂, hx₂, y₂, hy₂, rfl⟩ := hb
-    exact ⟨x₁ * x₂ + (a * a) * (y₁ * y₂), by aesop, x₁ * y₂ + y₁ * x₂, by aesop, by ring⟩
+    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
+    exact ⟨x₁ * x₂ + (a * a) * (y₁ * y₂), by aesop, x₁ * y₂ + y₁ * x₂, by aesop,
+      by linear_combination z * eqw + (a * y₁ + x₁) * eqz⟩
 
 variable {P} in
 @[aesop unsafe 70% apply (rule_sets := [SetLike])]

RealClosedField/RealClosedField/RingOrdering/Basic.lean

@@ -276,11 +276,11 @@ theorem isPrimeOrdering_iff :
   · refine ⟨by aesop, fun {x y} hxy => ?_⟩
     by_contra h₂
     cases (by aesop : x ∈ P ∨ -x ∈ P) with
-    | inl =>  have := h (-x) y (by simp_all)
-              have := h (-x) (-y) (by simp_all)
+    | inl =>  have := h (-x) y
+              have := h (-x) (-y)
               simp_all
-    | inr =>  have := h x y (by simp_all)
-              have := h x (-y) (by simp_all)
+    | inr =>  have := h x y
+              have := h x (-y)
               simp_all
 
 end RingPreordering

RealClosedField/RealClosedField/Semireal.Field.lean

@@ -22,35 +22,24 @@ instance RingPreorderingClass.instRingConeClass : RingConeClass S F where
 
 instance RingPreorderingClass.instIsMaxCone (O : S) [RingPreordering.IsOrdering O] : IsMaxCone O
     where
-  mem_or_neg_mem := RingPreordering.mem_or_neg_mem O
+  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
     by_contra
-    refine add_one_ne_zero_of_isSumSq (IsSumSq.mul (IsSumSq.sum_mul_self _) (IsSumSq.mul_self _))
-      (by field_simp [hx] : 1 + (∑ j ∈ I.erase i, x j * x j) * ((x i)⁻¹ * (x i)⁻¹) = 0)
-
-instance IsSemireal.inst_choose_isPrimeOrdering [IsSemireal F] :
-    RingPreordering.IsPrimeOrdering <| Classical.choose <|
-      RingPreordering.exists_le_isPrimeOrdering <| RingPreordering.sumSqIn F :=
-  (Classical.choose_spec <|
-    RingPreordering.exists_le_isPrimeOrdering <| RingPreordering.sumSqIn F).2
+    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])
 
+open Classical RingPreordering in
 noncomputable def LinearOrderedField.mkOfIsSemireal [IsSemireal F] : LinearOrderedField F where
-  __ := LinearOrderedRing.mkOfCone
-          (Classical.choose <|
-            RingPreordering.exists_le_isPrimeOrdering <| RingPreordering.sumSqIn F)
-          (Classical.decPred _)
+  __ := have := (choose_spec <| exists_le_isPrimeOrdering <| sumSqIn F).2
+        LinearOrderedRing.mkOfCone (choose <| exists_le_isPrimeOrdering <| sumSqIn F)
   __ := ‹Field F›
 
-set_option diagnostics true
-
 theorem ArtinSchreier_basic :
     Nonempty ({S : LinearOrderedField F // S.toField = ‹Field F›}) ↔ IsSemireal F := by
   refine Iff.intro (fun h => ?_) (fun h => ?_)
-  · rcases Classical.choice h with ⟨inst, extend⟩
-    have : ExistsAddOfLE F := AddGroup.existsAddOfLE F
-    have := LinearOrderedSemiring.instIsSemireal F
+  · rcases Classical.choice h with ⟨inst, rfl⟩
     infer_instance
-  · exact Nonempty.intro ⟨LinearOrderedField.mkOfIsSemireal F, by aesop⟩
+  · exact Nonempty.intro ⟨LinearOrderedField.mkOfIsSemireal F, rfl⟩