chore(Data/Fin/Basic): avoid importing lattices

Author: SnirBroshi

Mathlib/Data/Fin/Basic.lean

@@ -6,7 +6,8 @@ Authors: Robert Y. Lewis, Keeley Hoek
 module
 
 public import Mathlib.Data.Int.DivMod
-public import Mathlib.Order.Lattice
+public import Mathlib.Data.Nat.Init
+public import Mathlib.Logic.Equiv.Defs
 public import Mathlib.Tactic.Common
 public import Batteries.Data.Fin.Basic
 public import Mathlib.Tactic.Attr.Core
@@ -28,7 +29,7 @@ This file expands on the development in the core library.
 @[expose] public section
 
 
-assert_not_exists Monoid Finset
+assert_not_exists Monoid Finset Preorder
 
 open Fin Nat Function
 
@@ -420,18 +421,18 @@ lemma natCast_lt_natCast (han : a ≤ n) (hbn : b ≤ n) : (a : Fin (n + 1)) < b
   rw [← Nat.lt_succ_iff] at han hbn; simp [lt_def, Nat.mod_eq_of_lt, han, hbn]
 
 lemma natCast_mono (hbn : b ≤ n) (hab : a ≤ b) : (a : Fin (n + 1)) ≤ b :=
-  (natCast_le_natCast (hab.trans hbn) hbn).2 hab
+  (natCast_le_natCast (Nat.le_trans hab hbn) hbn).2 hab
 
 lemma natCast_strictMono (hbn : b ≤ n) (hab : a < b) : (a : Fin (n + 1)) < b :=
-  (natCast_lt_natCast (hab.le.trans hbn) hbn).2 hab
+  (natCast_lt_natCast (Nat.le_trans (Nat.le_of_lt hab) hbn) hbn).2 hab
 
 @[simp]
 lemma castLE_natCast {m n : ℕ} [NeZero m] (h : m ≤ n) (a : ℕ) :
-    haveI : NeZero n := ⟨Nat.pos_iff_ne_zero.mp (lt_of_lt_of_le m.pos_of_neZero h)⟩
+    haveI : NeZero n := ⟨Nat.pos_iff_ne_zero.mp (Nat.lt_of_lt_of_le m.pos_of_neZero h)⟩
     Fin.castLE h (a.cast : Fin m) = (a % m : ℕ) := by
   ext
   simp only [val_castLE, val_natCast]
-  rw [Nat.mod_eq_of_lt (a := a % m) (lt_of_lt_of_le (Nat.mod_lt _ m.pos_of_neZero) h)]
+  rw [Nat.mod_eq_of_lt (a := a % m) (Nat.lt_of_lt_of_le (Nat.mod_lt _ m.pos_of_neZero) h)]
 
 end OfNatCoe
 
@@ -481,7 +482,7 @@ theorem liftFun_iff_succ {α : Type*} (r : α → α → Prop) [IsTrans α r] {f
     · simp at h
     · intro j ihj hij
       rw [← le_castSucc_iff] at hij
-      obtain hij | hij := (le_def.1 hij).eq_or_lt
+      obtain hij | hij := Nat.eq_or_lt_of_le <| le_def.1 hij
       · obtain rfl := Fin.ext hij
         exact H _
       · exact _root_.trans (ihj hij) (H j)
@@ -508,7 +509,7 @@ theorem add_one_le_of_lt {n : ℕ} {a b : Fin (n + 1)} (h : a < b) : a + 1 ≤ b
 theorem exists_eq_add_of_le {n : ℕ} {a b : Fin n} (h : a ≤ b) : ∃ k ≤ b, b = a + k := by
   obtain ⟨k, hk⟩ : ∃ k : ℕ, (b : ℕ) = a + k := Nat.exists_eq_add_of_le h
   have hkb : k ≤ b := by lia
-  refine ⟨⟨k, hkb.trans_lt b.is_lt⟩, hkb, ?_⟩
+  refine ⟨⟨k, Nat.lt_of_le_of_lt hkb b.is_lt⟩, hkb, ?_⟩
   simp [Fin.ext_iff, Fin.val_add, ← hk, Nat.mod_eq_of_lt b.is_lt]
 
 theorem exists_eq_add_of_lt {n : ℕ} {a b : Fin (n + 1)} (h : a < b) :
@@ -517,7 +518,7 @@ theorem exists_eq_add_of_lt {n : ℕ} {a b : Fin (n + 1)} (h : a < b) :
   · lia
   obtain ⟨k, hk⟩ : ∃ k : ℕ, (b : ℕ) = a + k + 1 := Nat.exists_eq_add_of_lt h
   have hkb : k < b := by lia
-  refine ⟨⟨k, hkb.trans b.is_lt⟩, hkb, by fin_omega, ?_⟩
+  refine ⟨⟨k, Nat.lt_trans hkb b.is_lt⟩, hkb, by fin_omega, ?_⟩
   simp [Fin.ext_iff, Fin.val_add, ← hk, Nat.mod_eq_of_lt b.is_lt]
 
 lemma pos_of_ne_zero {n : ℕ} {a : Fin (n + 1)} (h : a ≠ 0) : 0 < a :=