chore: Do not import algebra in Data.Finset.Lattice (#13243)

Move the `OrderBot Nat` instance to a new file `Order.Nat` and the `LinearOrderedSemiring` lemmas from `Data.Finset.Lattice` to a new file `Algebra.Order.Ring.Finset`. I credit Eric for leanprover-community/mathlib3#12912.

Author: YaelDillies

Archive/Wiedijk100Theorems/AscendingDescendingSequences.lean

@@ -155,15 +155,9 @@ theorem erdos_szekeres {r s n : ℕ} {f : Fin n → α} (hn : r * s < n) (hf : I
       constructor <;>
         · apply le_max'
           rw [mem_image]
-          refine ⟨{i}, by solve_by_elim, card_singleton i⟩
-    refine ⟨?_, ?_⟩
+          exact ⟨{i}, by solve_by_elim, card_singleton i⟩
     -- Need to get `a_i ≤ r`, here phrased as: there is some `a < r` with `a+1 = a_i`.
-    · refine ⟨(ab i).1 - 1, ?_, Nat.succ_pred_eq_of_pos z.1⟩
-      rw [tsub_lt_iff_right z.1]
-      apply Nat.lt_succ_of_le q.1
-    · refine ⟨(ab i).2 - 1, ?_, Nat.succ_pred_eq_of_pos z.2⟩
-      rw [tsub_lt_iff_right z.2]
-      apply Nat.lt_succ_of_le q.2
+    exact ⟨⟨(ab i).1 - 1, by omega⟩, (ab i).2 - 1, by omega⟩
   -- To get our contradiction, it suffices to prove `n ≤ r * s`
   apply not_le_of_lt hn
   -- Which follows from considering the cardinalities of the subset above, since `ab` is injective.

Mathlib.lean

@@ -547,6 +547,7 @@ import Mathlib.Algebra.Order.Ring.Cast
 import Mathlib.Algebra.Order.Ring.CharZero
 import Mathlib.Algebra.Order.Ring.Cone
 import Mathlib.Algebra.Order.Ring.Defs
+import Mathlib.Algebra.Order.Ring.Finset
 import Mathlib.Algebra.Order.Ring.InjSurj
 import Mathlib.Algebra.Order.Ring.Int
 import Mathlib.Algebra.Order.Ring.Nat
@@ -3310,6 +3311,7 @@ import Mathlib.Order.Monotone.Extension
 import Mathlib.Order.Monotone.Monovary
 import Mathlib.Order.Monotone.Odd
 import Mathlib.Order.Monotone.Union
+import Mathlib.Order.Nat
 import Mathlib.Order.Notation
 import Mathlib.Order.OmegaCompletePartialOrder
 import Mathlib.Order.OrdContinuous

Mathlib/Algebra/BigOperators/Basic.lean

@@ -1534,7 +1534,7 @@ theorem prod_range_succ' (f : ℕ → β) :
 @[to_additive]
 theorem eventually_constant_prod {u : ℕ → β} {N : ℕ} (hu : ∀ n ≥ N, u n = 1) {n : ℕ} (hn : N ≤ n) :
     (∏ k ∈ range n, u k) = ∏ k ∈ range N, u k := by
-  obtain ⟨m, rfl : n = N + m⟩ := le_iff_exists_add.mp hn
+  obtain ⟨m, rfl : n = N + m⟩ := Nat.exists_eq_add_of_le hn
   clear hn
   induction' m with m hm
   · simp
@@ -2180,7 +2180,7 @@ theorem card_biUnion_le [DecidableEq β] {s : Finset α} {t : α → Finset β}
     calc
       ((insert a s).biUnion t).card ≤ (t a).card + (s.biUnion t).card := by
         { rw [biUnion_insert]; exact Finset.card_union_le _ _ }
-      _ ≤ ∑ a ∈ insert a s, card (t a) := by rw [sum_insert has]; exact add_le_add_left ih _
+      _ ≤ ∑ a ∈ insert a s, card (t a) := by rw [sum_insert has]; exact Nat.add_le_add_left ih _
 #align finset.card_bUnion_le Finset.card_biUnion_le
 
 theorem card_eq_sum_card_fiberwise [DecidableEq β] {f : α → β} {s : Finset α} {t : Finset β}
@@ -2576,7 +2576,7 @@ theorem nat_abs_sum_le {ι : Type*} (s : Finset ι) (f : ι → ℤ) :
     induction' s using Finset.induction_on with i s his IH
     · simp only [Finset.sum_empty, Int.natAbs_zero, le_refl]
     · simp only [his, Finset.sum_insert, not_false_iff]
-      exact (Int.natAbs_add_le _ _).trans (add_le_add le_rfl IH)
+      exact (Int.natAbs_add_le _ _).trans (Nat.add_le_add_left IH _)
 #align nat_abs_sum_le nat_abs_sum_le
 
 /-! ### `Additive`, `Multiplicative` -/

Mathlib/Algebra/BigOperators/Fin.lean

@@ -330,7 +330,7 @@ def finFunctionFinEquiv {m n : ℕ} : (Fin n → Fin m) ≃ Fin (m ^ n) :=
       cases m
       · exact isEmptyElim (f <| Fin.last _)
       simp_rw [Fin.sum_univ_castSucc, Fin.coe_castSucc, Fin.val_last]
-      refine (add_lt_add_of_lt_of_le (ih _) <| mul_le_mul_right' (Fin.is_le _) _).trans_eq ?_
+      refine (Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _ (Fin.is_le _)).trans_eq ?_
       rw [← one_add_mul (_ : ℕ), add_comm, pow_succ']⟩)
     (fun a b => ⟨a / m ^ (b : ℕ) % m, by
       cases' n with n
@@ -385,7 +385,7 @@ def finPiFinEquiv {m : ℕ} {n : Fin m → ℕ} : (∀ i : Fin m, Fin (n i)) ≃
       intro n nn f fn
       cases nn
       · exact isEmptyElim fn
-      refine (add_lt_add_of_lt_of_le (ih _) <| mul_le_mul_right' (Fin.is_le _) _).trans_eq ?_
+      refine (Nat.add_lt_add_of_lt_of_le (ih _) <| Nat.mul_le_mul_right _ (Fin.is_le _)).trans_eq ?_
       rw [← one_add_mul (_ : ℕ), mul_comm, add_comm]⟩)
     (fun a b => ⟨(a / ∏ j : Fin b, n (Fin.castLE b.is_lt.le j)) % n b, by
       cases m

Mathlib/Algebra/Order/Group/Nat.lean

@@ -45,15 +45,6 @@ instance instOrderedSub : OrderedSub ℕ := by
   · simp
   · simp only [sub_succ, pred_le_iff, ih, succ_add, add_succ]
 
-/-!
-### Extra instances to short-circuit type class resolution
-
-These also prevent non-computable instances being used to construct these instances non-computably.
--/
-
-instance instOrderBot : OrderBot ℕ := by infer_instance
-#align nat.order_bot Nat.instOrderBot
-
 /-! ### Miscellaneous lemmas -/
 
 theorem _root_.NeZero.one_le {n : ℕ} [NeZero n] : 1 ≤ n := one_le_iff_ne_zero.mpr (NeZero.ne n)

Mathlib/Algebra/Order/Ring/Finset.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2022 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import Mathlib.Algebra.Order.Ring.Defs
+import Mathlib.Data.Finset.Lattice
+
+/-!
+# Algebraic properties of finitary supremum
+-/
+
+namespace Finset
+variable {ι R : Type*} [LinearOrderedSemiring R] {a b : ι → R}
+
+theorem sup_mul_le_mul_sup_of_nonneg [OrderBot R] (s : Finset ι) (ha : ∀ i ∈ s, 0 ≤ a i)
+    (hb : ∀ i ∈ s, 0 ≤ b i) : s.sup (a * b) ≤ s.sup a * s.sup b :=
+  Finset.sup_le fun _i hi ↦
+    mul_le_mul (le_sup hi) (le_sup hi) (hb _ hi) ((ha _ hi).trans <| le_sup hi)
+#align finset.sup_mul_le_mul_sup_of_nonneg Finset.sup_mul_le_mul_sup_of_nonneg
+
+theorem mul_inf_le_inf_mul_of_nonneg [OrderTop R] (s : Finset ι) (ha : ∀ i ∈ s, 0 ≤ a i)
+    (hb : ∀ i ∈ s, 0 ≤ b i) : s.inf a * s.inf b ≤ s.inf (a * b) :=
+  Finset.le_inf fun i hi ↦ mul_le_mul (inf_le hi) (inf_le hi) (Finset.le_inf hb) (ha i hi)
+#align finset.mul_inf_le_inf_mul_of_nonneg Finset.mul_inf_le_inf_mul_of_nonneg
+
+theorem sup'_mul_le_mul_sup'_of_nonneg (s : Finset ι) (H : s.Nonempty) (ha : ∀ i ∈ s, 0 ≤ a i)
+    (hb : ∀ i ∈ s, 0 ≤ b i) : s.sup' H (a * b) ≤ s.sup' H a * s.sup' H b :=
+  (sup'_le _ _) fun _i hi ↦
+    mul_le_mul (le_sup' _ hi) (le_sup' _ hi) (hb _ hi) ((ha _ hi).trans <| le_sup' _ hi)
+#align finset.sup'_mul_le_mul_sup'_of_nonneg Finset.sup'_mul_le_mul_sup'_of_nonneg
+
+theorem inf'_mul_le_mul_inf'_of_nonneg (s : Finset ι) (H : s.Nonempty) (ha : ∀ i ∈ s, 0 ≤ a i)
+    (hb : ∀ i ∈ s, 0 ≤ b i) : s.inf' H a * s.inf' H b ≤ s.inf' H (a * b) :=
+  (le_inf' _ _) fun _i hi ↦ mul_le_mul (inf'_le _ hi) (inf'_le _ hi) (le_inf' _ _ hb) (ha _ hi)
+#align finset.inf'_mul_le_mul_inf'_of_nonneg Finset.inf'_mul_le_mul_inf'_of_nonneg
+
+end Finset

Mathlib/Analysis/Normed/Field/Basic.lean

@@ -5,6 +5,7 @@ Authors: Patrick Massot, Johannes Hölzl
 -/
 import Mathlib.Algebra.Algebra.NonUnitalSubalgebra
 import Mathlib.Algebra.Algebra.Subalgebra.Basic
+import Mathlib.Algebra.Order.Ring.Finset
 import Mathlib.Analysis.Normed.Group.Basic
 import Mathlib.GroupTheory.OrderOfElement
 import Mathlib.Topology.Instances.NNReal

Mathlib/Combinatorics/Additive/FreimanHom.lean

@@ -354,7 +354,7 @@ assuming there is no wrap-around. -/
 lemma isAddFreimanIso_Iio (hm : m ≠ 0) (hkmn : m * k ≤ n) :
     IsAddFreimanIso m (Iio (k : Fin (n + 1))) (Iio k) val := by
   obtain _ | k := k
-  · simp [← bot_eq_zero]; simp [← _root_.bot_eq_zero, -bot_eq_zero']
+  · simp [← bot_eq_zero]; simp [← _root_.bot_eq_zero, -Nat.bot_eq_zero, -bot_eq_zero']
   have hkmn' : m * k ≤ n := (Nat.mul_le_mul_left _ k.le_succ).trans hkmn
   convert isAddFreimanIso_Iic hm hkmn' using 1 <;> ext x
   · simp [lt_iff_val_lt_val, le_iff_val_le_val, -val_fin_le, -val_fin_lt, Nat.mod_eq_of_lt,

Mathlib/Combinatorics/Hall/Finite.lean

@@ -143,9 +143,9 @@ theorem hall_cond_of_compl {ι : Type u} {t : ι → Finset α} {s : Finset ι}
     intro x hx hc _
     exact absurd hx hc
   have : s'.card = (s ∪ s'.image fun z => z.1).card - s.card := by
-    simp [disj, card_image_of_injective _ Subtype.coe_injective]
+    simp [disj, card_image_of_injective _ Subtype.coe_injective, Nat.add_sub_cancel_left]
   rw [this, hus]
-  refine (tsub_le_tsub_right (ht _) _).trans ?_
+  refine (Nat.sub_le_sub_right (ht _) _).trans ?_
   rw [← card_sdiff]
   · refine (card_le_card ?_).trans le_rfl
     intro t

Mathlib/Combinatorics/SetFamily/Shatter.lean

@@ -120,7 +120,7 @@ lemma card_le_card_shatterer (𝒜 : Finset (Finset α)) : 𝒜.card ≤ 𝒜.sh
       mem_shatterer]
     exact fun s _ ↦ aux (fun t ht ↦ (mem_filter.1 ht).2)
   rw [← card_memberSubfamily_add_card_nonMemberSubfamily a]
-  refine (add_le_add ih₁ ih₀).trans ?_
+  refine (Nat.add_le_add ih₁ ih₀).trans ?_
   rw [← card_union_add_card_inter, ← hℬ, ← card_union_of_disjoint]
   swap
   · simp only [ℬ, disjoint_left, mem_union, mem_shatterer, mem_image, not_exists, not_and]