shake and lint

leanprover-community · Jul 3, 2024 · 75127a2 · 75127a2
1 parent 747ac14
commit 75127a2
Show file tree

Hide file tree

Showing 6 changed files with 6 additions and 6 deletions.
diff --git a/Mathlib/Algebra/Order/Group/DenselyOrdered.lean b/Mathlib/Algebra/Order/Group/DenselyOrdered.lean
@@ -3,9 +3,9 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 -/
-import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 import Mathlib.Algebra.Order.Group.Unbundled.Basic
 import Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
+import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
 
 #align_import algebra.order.group.densely_ordered from "leanprover-community/mathlib"@"4e87c8477c6c38b753f050bc9664b94ee859896c"
 

diff --git a/Mathlib/Algebra/Order/Interval/Set/Instances.lean b/Mathlib/Algebra/Order/Interval/Set/Instances.lean
@@ -249,7 +249,7 @@ variable [StrictOrderedSemiring α]
 
 namespace Set.Ioc
 
-instance one [Nontrivial α] : One (Ioc (0 : α) 1) where one := ⟨1, ⟨zero_lt_one, le_refl 1⟩⟩
+instance one : One (Ioc (0 : α) 1) where one := ⟨1, ⟨zero_lt_one, le_refl 1⟩⟩
 #align set.Ioc.has_one Set.Ioc.one
 
 @[simp, norm_cast]

diff --git a/Mathlib/Algebra/Order/Interval/Set/Monoid.lean b/Mathlib/Algebra/Order/Interval/Set/Monoid.lean
@@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov, Patrick Massot
 -/
 import Mathlib.Algebra.Group.Basic
-import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 import Mathlib.Data.Set.Function
 import Mathlib.Order.Interval.Set.Basic
+import Mathlib.Algebra.Order.Monoid.Defs
+import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
 
 #align_import data.set.intervals.monoid from "leanprover-community/mathlib"@"aba57d4d3dae35460225919dcd82fe91355162f9"
 

diff --git a/Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean b/Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean
@@ -5,6 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 -/
 import Mathlib.Algebra.Order.Monoid.Defs
 import Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
+import Mathlib.Algebra.NeZero
 
 #align_import algebra.order.monoid.canonical.defs from "leanprover-community/mathlib"@"e8638a0fcaf73e4500469f368ef9494e495099b3"
 

diff --git a/Mathlib/Algebra/Order/Monoid/Unbundled/ExistsOfLE.lean b/Mathlib/Algebra/Order/Monoid/Unbundled/ExistsOfLE.lean
@@ -3,9 +3,7 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl
 -/
-import Mathlib.Algebra.NeZero
 import Mathlib.Algebra.Order.Monoid.Unbundled.Basic
-import Mathlib.Order.BoundedOrder
 import Mathlib.Order.MinMax
 
 #align_import algebra.order.monoid.canonical.defs from "leanprover-community/mathlib"@"e8638a0fcaf73e4500469f368ef9494e495099b3"

diff --git a/Mathlib/Algebra/Order/Positive/Ring.lean b/Mathlib/Algebra/Order/Positive/Ring.lean
@@ -119,7 +119,7 @@ instance : Semigroup { x : R // 0 < x } :=
 instance : Distrib { x : R // 0 < x } :=
   Subtype.coe_injective.distrib _ coe_add val_mul
 
-instance [Nontrivial R] : One { x : R // 0 < x } :=
+instance : One { x : R // 0 < x } :=
   ⟨⟨1, one_pos⟩⟩
 
 @[simp]