improve proofs

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

@@ -101,17 +101,22 @@ instance RingConeClass.instRingConeClass_of_isMaxCone {S R : Type*}
   eq_zero_of_mem_of_neg_mem := eq_zero_of_mem_of_neg_mem (S := S)
 
 open Classical in
-/-- A maximal cone over a commutative ring `R` is an ordering on `R`. -/
-instance RingConeClass.instRingOrderingClass_of_isMaxCone {S R : Type*} [Nontrivial R]
+instance RingConeClass.instRingPreorderingClass_of_isMaxCone {S R : Type*} [Nontrivial R]
     [CommRing R] [SetLike S R] [RingConeClass S R] :
-    RingOrderingClass {x : S // IsMaxCone x} (R := R) where
+    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
     | 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
-  mem_or_neg_mem P x := @mem_or_neg_mem S _ _ _ _ P.2 x
+
+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
 
 /- TODO : decide whether to keep this cursed subtype instance, or whether to change to a def. -/

RealClosedField/RealClosedField/RingOrdering/Adjoin.lean

@@ -6,7 +6,6 @@ Authors: Florent Schaffhauser, Artie Khovanov
 import RealClosedField.RealClosedField.RingOrdering.Basic
 
 import Mathlib.Order.Zorn
-import Mathlib.Tactic.Polyrith
 
 /-
 ## Adjoining an element to a preordering
@@ -21,13 +20,11 @@ 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⟩
   one_mem' := ⟨1, by aesop, 0, by aesop, by simp⟩
-  add_mem' := by
-    intro a b ha hb
+  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' := by
-    intro a b ha hb
+  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⟩
@@ -46,13 +43,8 @@ lemma square_mem_ringPreordering_adjoin (x : R) : x * x ∈ ringPreordering_adjo
   by simpa using subset_ringPreordering_adjoin a (by aesop)
 
 theorem closure_insert_eq_ringPreordering_adjoin :
-    closure (insert a P) = ringPreordering_adjoin P a := by
-  refine closure_eq_of_le (fun x hx => ?_)
-                          (fun _ hz => ?_)
-  · rcases hx with ⟨_, _⟩ | h
-    · exact mem_ringPreordering_adjoin P a
-    · exact subset_ringPreordering_adjoin a h
-  · obtain ⟨_, _, _, _, rfl⟩ := hz; aesop
+    closure (insert a P) = ringPreordering_adjoin P a :=
+  closure_eq_of_le (fun _ => by aesop) (fun _ ⟨_, _, _, _, _⟩ => by aesop)
 
 end Subsemiring
 
@@ -67,18 +59,17 @@ def adjoin (h : -1 ∉ Subsemiring.ringPreordering_adjoin P a) :
 
 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
+lemma subset_adjoin' (h : -1 ∉ Subsemiring.ringPreordering_adjoin P a) {x : R} (hx : x ∈ P) :
+    x ∈ adjoin h := Subsemiring.subset_ringPreordering_adjoin a hx
 
 variable {P a} in
-lemma subset_adjoin (h : -1 ∉ Subsemiring.ringPreordering_adjoin P a) :
-    (P : Set R) ⊆ adjoin h := fun _ => by aesop
+lemma subset_adjoin (h : -1 ∉ Subsemiring.ringPreordering_adjoin P a) : (P : Set R) ⊆ adjoin h :=
+  fun _ => by aesop
 
 variable {P a} in
 @[aesop safe 0 apply (rule_sets := [SetLike])]
-lemma mem_adjoin (h : -1 ∉ Subsemiring.ringPreordering_adjoin P a) :
-    a ∈ adjoin h := Subsemiring.mem_ringPreordering_adjoin P a
+lemma mem_adjoin (h : -1 ∉ Subsemiring.ringPreordering_adjoin P a) : a ∈ adjoin h :=
+  Subsemiring.mem_ringPreordering_adjoin P a
 
 /-
 ## Sufficient conditions for adjoining an element
@@ -89,40 +80,33 @@ theorem minus_one_not_mem_or {x y : R} (h : - (x * y) ∈ P) :
     -1 ∉ Subsemiring.ringPreordering_adjoin P x ∨ -1 ∉ Subsemiring.ringPreordering_adjoin P y := by
   by_contra
   apply minus_one_not_mem P
-  have hx : -1 ∈ Subsemiring.ringPreordering_adjoin P x := by aesop
-  have hy : -1 ∈ Subsemiring.ringPreordering_adjoin P y := by aesop
-  rcases hx with ⟨s₁, hs₁, s₂, hs₂, eqx⟩
-  rcases hy with ⟨t₁, ht₁, t₂, ht₂, eqy⟩
-  rw [(by linear_combination (t₁ + 1) * eqx - 1 * x * s₂ * eqy :
-    -1 = (-(x * y)) * s₂ * t₂ + s₁ + t₁ + (s₁ * t₁))]
+  have ⟨s₁, hs₁, s₂, hs₂, eqx⟩ : -1 ∈ Subsemiring.ringPreordering_adjoin P x := by aesop
+  have ⟨t₁, ht₁, t₂, ht₂, eqy⟩ : -1 ∈ Subsemiring.ringPreordering_adjoin P y := by aesop
+  rw [show -1 = (-(x * y)) * s₂ * t₂ + s₁ + t₁ + (s₁ * t₁) by
+    linear_combination (t₁ + 1) * eqx - 1 * x * s₂ * eqy]
   aesop (config := { enableSimp := false })
 
 theorem minus_one_not_mem_or' :
-    -1 ∉ Subsemiring.ringPreordering_adjoin P a ∨ -1 ∉ Subsemiring.ringPreordering_adjoin P (-a)
-    := RingPreordering.minus_one_not_mem_or (by aesop : - (a * (-a)) ∈ P)
+    -1 ∉ Subsemiring.ringPreordering_adjoin P a ∨ -1 ∉ Subsemiring.ringPreordering_adjoin P (-a) :=
+  RingPreordering.minus_one_not_mem_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) :
     -1 ∉ Subsemiring.ringPreordering_adjoin P a := fun contr => by
-  have : -1 * (1 + a) ∈ Subsemiring.ringPreordering_adjoin P a :=
+  have ⟨x, hx, y, hy, eqn⟩ : -1 * (1 + a) ∈ Subsemiring.ringPreordering_adjoin P a :=
     by aesop (config := { enableSimp := false })
-  obtain ⟨x, hx, y, hy, eqn⟩ := this
-  exact h _ _ hx hy (by linear_combination -(1 * eqn) : x + (1 + y) * a + 1 = 0)
+  exact h _ _ hx hy (show x + (1 + y) * a + 1 = 0 by linear_combination -(1 * eqn))
 
 /--
 If `F` is a field, `P` is a preordering on `F`, and `a` is an element of `P` such that `-a ∉ P`,
 then `-1` is not of the form `x + a * y` with `x` and `y` in `P`.
 -/
 theorem minus_one_not_mem_adjoin_linear
     {S F : Type*} [Field F] [SetLike S F] [RingPreorderingClass S F] {P : S} {a : F}
-    (ha : -a ∉ P) : -1 ∉ Subsemiring.ringPreordering_adjoin P a := fun h => by
-  rcases h with ⟨x, hx, y, hy, eqn⟩
-  apply ha
+    (ha : -a ∉ P) : -1 ∉ Subsemiring.ringPreordering_adjoin P a := fun ⟨x, hx, y, hy, eqn⟩ =>
+  ha <| by
   have : y ≠ 0 := fun _ => by simpa [*] using minus_one_not_mem P
-  rw [show -a = x * y⁻¹ + y⁻¹ by
-    field_simp
-    rw [neg_eq_iff_eq_neg.mp eqn]
-    ring]
+  rw [show -a = x * y⁻¹ + y⁻¹ by field_simp; linear_combination eqn]
   aesop
 
 /-
@@ -141,22 +125,25 @@ theorem exists_lt (hp : a ∉ P) (hn : -a ∉ P) :
   · exact ⟨Q, lt_of_le_of_ne le <| Ne.symm (ne_of_mem_of_not_mem' p_mem hp)⟩
   · exact ⟨Q, lt_of_le_of_ne le <| Ne.symm (ne_of_mem_of_not_mem' n_mem hn)⟩
 
-variable {P} in
 /- A preordering on `R` that is maximal with respect to inclusion is a prime ordering. -/
-theorem isPrimeOrdering_of_maximal
-    (max : Maximal Set.univ (RingPreorderingClass.toRingPreordering P)) :
-    IsPrimeOrdering P := isPrimeOrdering_iff.mpr (fun a b h => by
+theorem isPrimeOrdering_of_maximal {O : RingPreordering R} (max : IsMax O) :
+    IsPrimeOrdering O := isPrimeOrdering_iff.mpr (fun a b h => by
   cases RingPreordering.minus_one_not_mem_or h with
-  | inl h => exact Or.inl <| Maximal.le_of_ge max trivial (subset_adjoin h) (mem_adjoin h)
-  | inr h => exact Or.inr <| Maximal.le_of_ge max trivial (subset_adjoin h) (mem_adjoin h))
+  | inl h => exact Or.inl <| max (subset_adjoin h) (mem_adjoin h)
+  | inr h => exact Or.inr <| max (subset_adjoin h) (mem_adjoin h))
 
 /- Every preordering on `R` extends to a prime ordering. -/
 theorem exists_le_isPrimeOrdering :
-    ∃ Q : RingPreordering R, (P : Set R) ⊆ Q ∧ IsPrimeOrdering Q := by
-  suffices ∃ Q, RingPreorderingClass.toRingPreordering P ≤ Q ∧ Maximal (fun x => x ∈ Set.univ) Q by
-    obtain ⟨Q, hQ⟩ := this
-    exact ⟨Q, by aesop, isPrimeOrdering_of_maximal hQ.2⟩
-  apply zorn_le_nonempty₀
-  · intro c _ hc P' hP'
-    simp_all [← bddAbove_def, nonempty_chain_bddAbove c hc (Set.nonempty_of_mem hP')]
-  · trivial
+    ∃ O : RingPreordering R, (P : Set R) ⊆ O ∧ IsPrimeOrdering O := by
+  have ⟨O, le, hO⟩ : ∃ O, RingPreorderingClass.toRingPreordering P ≤ O ∧ IsMax O := by
+    refine zorn_le_nonempty_Ici₀ _ (fun _ _ hc _ hQ => ?_) _ (by trivial)
+    simp_all [← bddAbove_def, nonempty_chain_bddAbove _ hc (Set.nonempty_of_mem hQ)]
+  exact ⟨O, by aesop, isPrimeOrdering_of_maximal hO⟩
+
+/- A prime ordering on `R` is maximal among preorderings iff it is maximal among prime orderings. -/
+theorem maximal_isPrimeOrdering_iff_maximal {O : RingPreordering R} [IsPrimeOrdering O] :
+    IsMax O ↔ Maximal IsPrimeOrdering O := by
+  refine Iff.intro (fun h => ?_) (fun hO P le₁ => ?_)
+  · exact Maximal.mono (by simpa using h) (fun _ _ => trivial) (inferInstance)
+  · rcases exists_le_isPrimeOrdering P with ⟨Q, le₂, hQ⟩
+    aesop (add safe forward le_trans, safe forward Maximal.eq_of_ge)

RealClosedField/RealClosedField/RingOrdering/Basic.lean

@@ -9,6 +9,7 @@ import Mathlib.Tactic.Ring
 import Mathlib.Algebra.CharP.Defs
 import Mathlib.RingTheory.Ideal.Basic
 import Mathlib.Tactic.FieldSimp
+import Mathlib.Tactic.Polyrith
 
 /-
 ## Definitions
@@ -83,13 +84,13 @@ lemma neg_mul_mem_of_neg_mem {x y : R} (hx : -x ∈ P) (hy : y ∈ P) : -(x * y)
 
 @[aesop safe apply (rule_sets := [SetLike])]
 theorem inv_mem {a : Rˣ} (ha : ↑a ∈ P) : ↑a⁻¹ ∈ P := by
-  rw [(by simp : (↑a⁻¹ : R) = a * (a⁻¹ * a⁻¹))]
+  rw [show (↑a⁻¹ : R) = a * (a⁻¹ * a⁻¹) by simp]
   aesop (config := { enableSimp := false })
 
 @[aesop safe apply (rule_sets := [SetLike])]
 theorem Field.inv_mem {S F : Type*} [Field F] [SetLike S F] [RingPreorderingClass S F]
     {P : S} {a : F} (ha : a ∈ P) : a⁻¹ ∈ P := by
-  rw [(by field_simp : a⁻¹ = a * (a⁻¹ * a⁻¹))]
+  rw [show a⁻¹ = a * (a⁻¹ * a⁻¹) by field_simp]
   aesop
 
 /- Construct a preordering from a minimal set of axioms. -/
@@ -108,21 +109,17 @@ def mk' {R : Type*} [CommRing R] (P : Set R)
   one_mem' := by simpa using sq 1
 
 theorem nonempty_chain_bddAbove {R : Type*} [CommRing R]
-    (c : Set (RingPreordering R)) (hcc : IsChain (· ≤ ·) c) (hc : c.Nonempty) : BddAbove c := by
-  rw [bddAbove_def]
-  let Q := mk (sSup (toSubsemiring '' c))
+    (c : Set (RingPreordering R)) (hcc : IsChain (· ≤ ·) c) (hc : c.Nonempty) : BddAbove c :=
+  ⟨mk (sSup (toSubsemiring '' c))
     (fun x => CompleteLattice.le_sSup _ hc.some.toSubsemiring (by aesop (add hc.some_mem safe))
               (by simpa using (hc.some.square_mem' x)))
     (by
       have a : ∀ x ∈ (toSubsemiring '' c), -1 ∉ x := fun P' hP' => by
         obtain ⟨P, _, rfl⟩ := (by aesop : ∃ x ∈ c, x.toSubsemiring = P')
         simpa using P.minus_one_not_mem'
-      aesop (add (Subsemiring.coe_sSup_of_directedOn (by simp [hc])
-        (IsChain.directedOn (IsChain.image _ _ _ (by aesop) hcc))) norm))
-  refine ⟨Q, fun P _ => ?_⟩
-  have : P.toSubsemiring ≤ Q.toSubsemiring :=
-    CompleteLattice.le_sSup (toSubsemiring '' c) _ (by aesop)
-  aesop
+      simp_all [Subsemiring.coe_sSup_of_directedOn (by simp [hc])
+        (IsChain.directedOn (IsChain.image _ _ _ (by aesop) hcc))]),
+  fun _ _ => by simpa using CompleteLattice.le_sSup (toSubsemiring '' c) _ (by aesop)⟩
 
 end RingPreordering
 
@@ -152,24 +149,33 @@ namespace RingPreordering
 
 variable (P) in
 class HasIdealSupport : Prop where
-  smul_mem_support (x : R) {a : R} (ha : a ∈ AddSubgroup.preordering_support P) :
+  smul_mem_support' (x : R) {a : R} (ha : a ∈ AddSubgroup.preordering_support P) :
     x * a ∈ AddSubgroup.preordering_support P
 
-theorem HasIdealSupport.smul_mem [RingPreordering.HasIdealSupport P]
+namespace HasIdealSupport
+
+variable (P) in
+/-- Technical lemma to get P as explicit argument -/
+lemma smul_mem_support [RingPreordering.HasIdealSupport P] :
+    ∀ (x : R) {a : R}, a ∈ AddSubgroup.preordering_support P →
+      x * a ∈ AddSubgroup.preordering_support P :=
+  HasIdealSupport.smul_mem_support' (P := P)
+
+theorem smul_mem [RingPreordering.HasIdealSupport P]
   (x : R) {a : R} (h₁a : a ∈ P) (h₂a : -a ∈ P) : x * a ∈ P := by
-  have := RingPreordering.HasIdealSupport.smul_mem_support (P := P)
+  have := smul_mem_support P
   simp_all
 
-theorem HasIdealSupport.neg_smul_mem [RingPreordering.HasIdealSupport P]
+theorem neg_smul_mem [RingPreordering.HasIdealSupport P]
   (x : R) {a : R} (h₁a : a ∈ P) (h₂a : -a ∈ P) : -(x * a) ∈ P := by
-  have := RingPreordering.HasIdealSupport.smul_mem_support (P := P)
+  have := smul_mem_support P
   simp_all
 
-theorem HasIdealSupport.hasIdealSupport
+theorem hasIdealSupport
     (h : ∀ x a : R, a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P) : HasIdealSupport P where
-  smul_mem_support := by simp_all
+  smul_mem_support' := by simp_all
 
-end RingPreordering
+end RingPreordering.HasIdealSupport
 
 namespace Ideal
 
@@ -182,7 +188,7 @@ the set of elements `x` in `R` such that both `x` and `-x` lie in `P`.
 -/
 def preordering_support : Ideal R where
   __ := AddSubgroup.preordering_support P
-  smul_mem' := by simpa using RingPreordering.HasIdealSupport.smul_mem_support (P := P)
+  smul_mem' := by simpa using RingPreordering.HasIdealSupport.smul_mem_support P
 
 @[simp] lemma mem_support : x ∈ preordering_support P ↔ x ∈ P ∧ -x ∈ P := Iff.rfl
 @[simp, norm_cast] lemma coe_support : preordering_support P = {x : R | x ∈ P ∧ -x ∈ P} := rfl
@@ -196,9 +202,7 @@ theorem RingPreordering.hasIdealSupport_of_isUnit_2 (isUnit_2 : IsUnit (2 : R))
   let y := (1 + x) * half
   let z := (1 - x) * half
   have mem : (y * y) * a + (z * z) * (-a) ∈ P ∧ (y * y) * (-a) + (z * z) * a ∈ P := by aesop
-  have : x = x * (half * (half * 2) * 2) := by simp [h2]
-  have : x = y * y - z * z := by simp only [y, z]; ring_nf at this ⊢; assumption
-  rw [this]
+  rw [show x = y * y - z * z by linear_combination (-(2 * x * half) - 1 * x) * h2]
   ring_nf at mem ⊢
   assumption
 
@@ -233,12 +237,10 @@ lemma mem_of_not_neg_mem (x : R) (h : -x ∉ P) : x ∈ P := by
   simp_all
 
 instance hasIdealSupport : HasIdealSupport P where
-  smul_mem_support x a ha := by
-    cases mem_or_neg_mem (P := P) x with
+  smul_mem_support' x a ha := by
+    cases mem_or_neg_mem P x with
     | inl => aesop
-    | inr hx =>
-        rw [AddSubgroup.mem_support] at *
-        exact ⟨by simpa using mul_mem hx ha.2, by simpa using mul_mem hx ha.1⟩
+    | inr hx => simpa using ⟨by simpa using mul_mem hx ha.2, by simpa using mul_mem hx ha.1⟩
 
 end IsOrdering
 
@@ -271,16 +273,14 @@ theorem isPrimeOrdering_iff :
     have : a ∈ Ideal.preordering_support P ∨ b ∈ Ideal.preordering_support P :=
       Ideal.IsPrime.mem_or_mem inferInstance (by simp_all)
     simp_all
-  · constructor
-    · aesop
-    · intro x y hxy
-      by_contra h₂
-      cases (by aesop : x ∈ P ∨ -x ∈ P) with
-      | inl =>  have := h (-x) y (by aesop)
-                have := h (-x) (-y) (by aesop)
-                aesop
-      | inr =>  have := h x y (by aesop)
-                have := h x (-y) (by aesop)
-                aesop
+  · 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)
+              simp_all
+    | inr =>  have := h x y (by simp_all)
+              have := h x (-y) (by simp_all)
+              simp_all
 
 end RingPreordering

RealClosedField/RealClosedField/Semireal.Field.lean

@@ -4,18 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Artie Khovanov
 -/
 import RealClosedField.RealClosedField.FormallyReal
-import RealClosedField.RealClosedField.RingOrdering.Field
+import RealClosedField.RealClosedField.RingOrdering.Adjoin
 
-variable (F S : Type*) [Field F] [SetLike S F]
+/- TODO: prove prime orderings with support {0} are maximal ring cones, and deduce field case -/
 
-instance RingPreorderingClass.instRingConeClass [RingPreorderingClass S F] : RingConeClass S F where
+variable (S F : Type*) [Field F] [SetLike S F] [RingPreorderingClass S F]
+
+instance RingPreorderingClass.instRingConeClass : RingConeClass S 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)
 
-instance RingOrderingClass.instIsMaxCone [RingOrderingClass S F] (O : S) : IsMaxCone O where
-  mem_or_neg_mem := mem_or_neg_mem O
+instance RingPreorderingClass.instIsMaxCone (O : S) [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
@@ -24,9 +27,16 @@ instance IsSemireal.instIsFormallyReal [IsSemireal F] : IsFormallyReal F where
     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
+
 noncomputable def LinearOrderedField.mkOfIsSemireal [IsSemireal F] : LinearOrderedField F where
   __ := LinearOrderedRing.mkOfCone
-          (Classical.choose <| RingPreordering.exists_le_ordering <| RingPreordering.sumSqIn F)
+          (Classical.choose <|
+            RingPreordering.exists_le_isPrimeOrdering <| RingPreordering.sumSqIn F)
           (Classical.decPred _)
   __ := ‹Field F›
 
@@ -37,5 +47,6 @@ theorem ArtinSchreier_basic :
   refine Iff.intro (fun h => ?_) (fun h => ?_)
   · rcases Classical.choice h with ⟨inst, extend⟩
     have : ExistsAddOfLE F := AddGroup.existsAddOfLE F
-    exact LinearOrderedSemiring.instIsSemireal F
+    have := LinearOrderedSemiring.instIsSemireal F
+    infer_instance
   · exact Nonempty.intro ⟨LinearOrderedField.mkOfIsSemireal F, by aesop⟩