fix

leanprover-community · Dec 29, 2024 · afc6403 · afc6403
1 parent 9b7f4d6
commit afc6403
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 8 deletions.
diff --git a/Mathlib/Algebra/GeomSum.lean b/Mathlib/Algebra/GeomSum.lean
@@ -298,7 +298,8 @@ lemma geom_sum_of_lt_one {x : α} [LinearOrderedSemifield α] [CanonicallyOrdere
     ∑ i ∈ Finset.range n, x ^ i = (1 - x ^ n) / (1 - x) :=
   eq_div_of_mul_eq (tsub_pos_of_lt h).ne' (geom_sum_mul_of_le_one h.le n)
 
-theorem geom_sum_lt {x : α} [CanonicallyLinearOrderedSemifield α] [Sub α] [OrderedSub α]
+theorem geom_sum_lt {x : α} [LinearOrderedSemifield α] [CanonicallyOrderedAdd α]
+    [Sub α] [OrderedSub α]
     (h0 : x ≠ 0) (h1 : x < 1) (n : ℕ) : ∑ i ∈ range n, x ^ i < (1 - x)⁻¹ := by
   rw [← zero_lt_iff] at h0
   rw [geom_sum_of_lt_one h1, div_lt_iff₀, inv_mul_cancel₀, tsub_lt_self_iff]

diff --git a/Mathlib/Algebra/Order/Field/Canonical.lean b/Mathlib/Algebra/Order/Field/Canonical.lean
@@ -14,10 +14,8 @@ import Mathlib.Algebra.Order.Ring.Canonical
 
 variable {α : Type*} [LinearOrderedSemifield α] [CanonicallyOrderedAdd α]
 
--- See note [reducible non-instances]
-/-- Construct a `LinearOrderedCommGroupWithZero` from a canonically ordered
-`LinearOrderedSemifield`. -/
-abbrev CanonicallyOrderedAdd.toLinearOrderedCommGroupWithZero :
+-- See note [lower instance priority]
+instance (priority := 100) LinearOrderedSemifield.toLinearOrderedCommGroupWithZero :
     LinearOrderedCommGroupWithZero α :=
   { ‹LinearOrderedSemifield α› with
     mul_le_mul_left := fun _ _ h _ ↦ mul_le_mul_of_nonneg_left h <| zero_le _ }

diff --git a/Mathlib/Algebra/Order/Nonneg/Field.lean b/Mathlib/Algebra/Order/Nonneg/Field.lean
@@ -103,6 +103,6 @@ end LinearOrderedSemifield
 
 instance linearOrderedCommGroupWithZero [LinearOrderedField α] :
     LinearOrderedCommGroupWithZero { x : α // 0 ≤ x } :=
-  CanonicallyOrderedAdd.toLinearOrderedCommGroupWithZero
+  LinearOrderedSemifield.toLinearOrderedCommGroupWithZero
 
 end Nonneg
diff --git a/Mathlib/Data/ENat/Basic.lean b/Mathlib/Data/ENat/Basic.lean
@@ -457,8 +457,8 @@ protected def _root_.MonoidWithZeroHom.ENatMap {S : Type*} [MulZeroOneClass S] [
 
 /-- A version of `ENat.map` for `RingHom`s. -/
 @[simps (config := .asFn)]
-protected def _root_.RingHom.ENatMap {S : Type*} [CanonicallyOrderedCommSemiring S] [DecidableEq S]
-    [Nontrivial S] (f : ℕ →+* S) (hf : Function.Injective f) : ℕ∞ →+* WithTop S :=
+protected def _root_.RingHom.ENatMap {S : Type*} [OrderedCommSemiring S] [CanonicallyOrderedAdd S]
+    [DecidableEq S] [Nontrivial S] (f : ℕ →+* S) (hf : Function.Injective f) : ℕ∞ →+* WithTop S :=
   {MonoidWithZeroHom.ENatMap f.toMonoidWithZeroHom hf, f.toAddMonoidHom.ENatMap with}
 
 end ENat