minor changes

artie2000 · Jan 7, 2025 · 652511a · 652511a
1 parent fc38474
commit 652511a
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/RealClosedField/RealClosedField/RingOrdering/Basic.lean b/RealClosedField/RealClosedField/RingOrdering/Basic.lean
@@ -317,7 +317,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
-  isSquare_mem' := by aesop (add unsafe apply IsSquare.map) /- TODO : automate? -/
+  isSquare_mem' := by aesop (add unsafe apply IsSquare.map) /- TODO : automate -/
   minus_one_not_mem' := by aesop
 
 @[simp]
@@ -371,7 +371,6 @@ 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'

diff --git a/RealClosedField/RealClosedField/Semireal/Field.lean b/RealClosedField/RealClosedField/Semireal/Field.lean
@@ -7,7 +7,7 @@ import RealClosedField.RealClosedField.FormallyReal
 import RealClosedField.RealClosedField.RingOrdering.Order
 import RealClosedField.RealClosedField.RingOrdering.Adjoin
 
-variable (F : Type*) [Field F]
+variable {F : Type*} [Field F]
 
 instance : RingConeClass (RingPreordering F) F where
   eq_zero_of_mem_of_neg_mem {P} {a} ha hna := by
@@ -26,6 +26,7 @@ instance IsSemireal.instIsFormallyReal [IsSemireal F] : IsFormallyReal F where
 
 variable [IsSemireal F]
 
+variable (F) in
 open Classical RingPreordering in
 noncomputable def LinearOrderedField.mkOfIsSemireal [IsSemireal F] : LinearOrderedField F where
   __ := have := (choose_spec <| exists_le_isPrimeOrdering (⊥ : RingPreordering F)).2