chore: move some aliases earlier (#11122)

leanprover-community · Mar 28, 2024 · d1a1aa1 · d1a1aa1
1 parent f09ccf6
commit d1a1aa1
Show file tree

Hide file tree

Showing 5 changed files with 11 additions and 10 deletions.
diff --git a/Mathlib/Algebra/GroupPower/Order.lean b/Mathlib/Algebra/GroupPower/Order.lean
@@ -451,9 +451,6 @@ theorem pow_bit0_nonneg (a : R) (n : ℕ) : 0 ≤ a ^ bit0 n := by
   exact mul_self_nonneg _
 #align pow_bit0_nonneg pow_bit0_nonneg
 
-alias pow_two_nonneg := sq_nonneg
-#align pow_two_nonneg pow_two_nonneg
-
 theorem pow_bit0_pos {a : R} (h : a ≠ 0) (n : ℕ) : 0 < a ^ bit0 n :=
   (pow_bit0_nonneg a n).lt_of_ne (pow_ne_zero _ h).symm
 #align pow_bit0_pos pow_bit0_pos

diff --git a/Mathlib/Algebra/Order/Ring/Defs.lean b/Mathlib/Algebra/Order/Ring/Defs.lean
@@ -1212,6 +1212,10 @@ lemma sq_nonneg (a : α) : 0 ≤ a ^ 2 := by
     b ^ 2 + a * b = (a + b) * b := by rw [add_comm, sq, add_mul]
     _ = a * (a + b) := by simp [← hab]
     _ = a ^ 2 + a * b := by rw [sq, mul_add]
+#align sq_nonneg sq_nonneg
+
+alias pow_two_nonneg := sq_nonneg
+#align pow_two_nonneg pow_two_nonneg
 
 lemma mul_self_nonneg (a : α) : 0 ≤ a * a := by simpa only [sq] using sq_nonneg a
 

diff --git a/Mathlib/Data/Tree.lean b/Mathlib/Data/Tree.lean
@@ -3,11 +3,11 @@ Copyright (c) 2019 mathlib community. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Wojciech Nawrocki
 -/
-import Std.Data.RBMap.Basic
 import Mathlib.Data.Num.Basic
-import Mathlib.Order.Basic
 import Mathlib.Init.Data.Ordering.Basic
+import Mathlib.Init.Order.LinearOrder
 import Mathlib.Util.CompileInductive
+import Std.Data.RBMap.Basic
 
 #align_import data.tree from "leanprover-community/mathlib"@"ed989ff568099019c6533a4d94b27d852a5710d8"
 

diff --git a/Mathlib/Init/Order/Defs.lean b/Mathlib/Init/Order/Defs.lean
@@ -45,6 +45,11 @@ theorem le_refl : ∀ a : α, a ≤ a :=
   Preorder.le_refl
 #align le_refl le_refl
 
+/-- A version of `le_refl` where the argument is implicit -/
+theorem le_rfl {a : α} : a ≤ a :=
+  le_refl a
+#align le_rfl le_rfl
+
 /-- The relation `≤` on a preorder is transitive. -/
 @[trans]
 theorem le_trans : ∀ {a b c : α}, a ≤ b → b ≤ c → a ≤ c :=

diff --git a/Mathlib/Order/Basic.lean b/Mathlib/Order/Basic.lean
@@ -163,11 +163,6 @@ section
 
 variable [Preorder α] {a b c : α}
 
-/-- A version of `le_refl` where the argument is implicit -/
-theorem le_rfl : a ≤ a :=
-  le_refl a
-#align le_rfl le_rfl
-
 @[simp]
 theorem lt_self_iff_false (x : α) : x < x ↔ False :=
   ⟨lt_irrefl x, False.elim⟩