split(data/finsupp/order): Split off data.finsupp.basic (#11045)

This moves all order instances about `finsupp` from `data.finsupp.basic` and `data.finsupp.lattice` to a new file `data.finsupp.order`.

I'm crediting
* Johan for #1216, #1244
* Aaron Anderson for #3335

src/data/finsupp/antidiagonal.lean

@@ -3,7 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Yury Kudryashov
 -/
-import data.finsupp.basic
+import data.finsupp.order
 import data.multiset.antidiagonal
 
 /-!

src/data/finsupp/basic.lean

@@ -2697,159 +2697,6 @@ end multiset
 @[simp] lemma finsupp.to_multiset_to_finsupp (f : α →₀ ℕ) :
   f.to_multiset.to_finsupp = f :=
 finsupp.to_multiset.symm_apply_apply f
-
-/-! ### Declarations about order(ed) instances on `finsupp` -/
-
-namespace finsupp
-
-instance [preorder M] [has_zero M] : preorder (α →₀ M) :=
-{ le := λ f g, ∀ s, f s ≤ g s,
-  le_refl := λ f s, le_refl _,
-  le_trans := λ f g h Hfg Hgh s, le_trans (Hfg s) (Hgh s) }
-
-instance [partial_order M] [has_zero M] : partial_order (α →₀ M) :=
-{ le_antisymm := λ f g hfg hgf, ext $ λ s, le_antisymm (hfg s) (hgf s),
-  .. finsupp.preorder }
-
-instance [ordered_add_comm_monoid M] : ordered_add_comm_monoid (α →₀ M) :=
-{ add_le_add_left := λ a b h c s, add_le_add_left (h s) (c s),
-  .. finsupp.add_comm_monoid, .. finsupp.partial_order }
-
-instance [ordered_cancel_add_comm_monoid M] : ordered_cancel_add_comm_monoid (α →₀ M) :=
-{ add_le_add_left := λ a b h c s, add_le_add_left (h s) (c s),
-  le_of_add_le_add_left := λ a b c h s, le_of_add_le_add_left (h s),
-  add_left_cancel := λ a b c h, ext $ λ s, add_left_cancel (ext_iff.1 h s),
-  .. finsupp.add_comm_monoid, .. finsupp.partial_order }
-
-instance [ordered_add_comm_monoid M] [contravariant_class M M (+) (≤)] :
-  contravariant_class (α →₀ M) (α →₀ M) (+) (≤) :=
-⟨λ f g h H x, le_of_add_le_add_left $ H x⟩
-
-lemma le_def [preorder M] [has_zero M] {f g : α →₀ M} : f ≤ g ↔ ∀ x, f x ≤ g x := iff.rfl
-
-lemma le_iff' [canonically_ordered_add_monoid M] (f g : α →₀ M)
-  {t : finset α} (hf : f.support ⊆ t) :
-  f ≤ g ↔ ∀ s ∈ t, f s ≤ g s :=
-⟨λ h s hs, h s,
-λ h s, if H : s ∈ f.support then h s (hf H) else (not_mem_support_iff.1 H).symm ▸ zero_le (g s)⟩
-
-lemma le_iff [canonically_ordered_add_monoid M] (f g : α →₀ M) :
-  f ≤ g ↔ ∀ s ∈ f.support, f s ≤ g s :=
-le_iff' f g (subset.refl _)
-
-instance decidable_le [canonically_ordered_add_monoid M] [decidable_rel (@has_le.le M _)] :
-  decidable_rel (@has_le.le (α →₀ M) _) :=
-λ f g, decidable_of_iff _ (le_iff f g).symm
-
-@[simp] lemma single_le_iff [canonically_ordered_add_monoid M] {i : α} {x : M} {f : α →₀ M} :
-  single i x ≤ f ↔ x ≤ f i :=
-(le_iff' _ _ support_single_subset).trans $ by simp
-
-@[simp] lemma add_eq_zero_iff [canonically_ordered_add_monoid M] (f g : α →₀ M) :
-  f + g = 0 ↔ f = 0 ∧ g = 0 :=
-by simp [ext_iff, forall_and_distrib]
-
-/-- `finsupp.to_multiset` as an order isomorphism. -/
-def order_iso_multiset : (α →₀ ℕ) ≃o multiset α :=
-{ to_equiv := to_multiset.to_equiv,
-  map_rel_iff' := λ f g, by simp [multiset.le_iff_count, le_def] }
-
-@[simp] lemma coe_order_iso_multiset : ⇑(@order_iso_multiset α) = to_multiset := rfl
-
-@[simp] lemma coe_order_iso_multiset_symm :
-  ⇑(@order_iso_multiset α).symm = multiset.to_finsupp := rfl
-
-lemma to_multiset_strict_mono : strict_mono (@to_multiset α) :=
-order_iso_multiset.strict_mono
-
-lemma sum_id_lt_of_lt (m n : α →₀ ℕ) (h : m < n) :
-  m.sum (λ _, id) < n.sum (λ _, id) :=
-begin
-  rw [← card_to_multiset, ← card_to_multiset],
-  apply multiset.card_lt_of_lt,
-  exact to_multiset_strict_mono h
-end
-
-variable (α)
-
-/-- The order on `σ →₀ ℕ` is well-founded.-/
-lemma lt_wf : well_founded (@has_lt.lt (α →₀ ℕ) _) :=
-subrelation.wf (sum_id_lt_of_lt) $ inv_image.wf _ nat.lt_wf
-
-variable {α}
-
-/-! Declarations about subtraction on `finsupp` with codomain a `canonically_ordered_add_monoid`.
-
-Some of these lemmas are used to develop the partial derivative on `mv_polynomial`. -/
-section nat_sub
-section canonically_ordered_monoid
-
-instance [canonically_ordered_add_monoid M] : order_bot (α →₀ M) :=
-{ bot := 0,
-  bot_le := by simp [finsupp.le_def] }
-
-variables [canonically_ordered_add_monoid M] [has_sub M] [has_ordered_sub M]
-
-/-- This is called `tsub` for truncated subtraction, to distinguish it with subtraction in an
-additive group. -/
-instance tsub : has_sub (α →₀ M) :=
-⟨zip_with (λ m n, m - n) (tsub_self 0)⟩
-
-@[simp] lemma coe_tsub (g₁ g₂ : α →₀ M) : ⇑(g₁ - g₂) = g₁ - g₂ := rfl
-
-lemma tsub_apply (g₁ g₂ : α →₀ M) (a : α) : (g₁ - g₂) a = g₁ a - g₂ a := rfl
-
-instance : canonically_ordered_add_monoid (α →₀ M) :=
-{ le_iff_exists_add := begin
-      intros f g,
-      split,
-      { intro H, use g - f, ext x, symmetry, exact add_tsub_cancel_of_le (H x) },
-      { rintro ⟨g, rfl⟩ x, exact self_le_add_right (f x) (g x) }
-    end,
- ..finsupp.order_bot,
- ..(by apply_instance : ordered_add_comm_monoid (α →₀ M)) }
-
-instance : has_ordered_sub (α →₀ M) :=
-⟨λ n m k, forall_congr $ λ x, tsub_le_iff_right⟩
-
-@[simp] lemma single_tsub {a : α} {n₁ n₂ : M} : single a (n₁ - n₂) = single a n₁ - single a n₂ :=
-begin
-  ext f,
-  by_cases h : (a = f),
-  { rw [h, tsub_apply, single_eq_same, single_eq_same, single_eq_same] },
-  rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]
-end
-
-lemma support_tsub {f1 f2 : α →₀ M} : (f1 - f2).support ⊆ f1.support :=
-by simp only [subset_iff, tsub_eq_zero_iff_le, mem_support_iff, ne.def, coe_tsub, pi.sub_apply,
-    not_imp_not, zero_le, implies_true_iff] {contextual := tt}
-
-lemma subset_support_tsub {f1 f2 : α →₀ M} : f1.support \ f2.support ⊆ (f1 - f2).support :=
-by simp [subset_iff] {contextual := tt}
-
-end canonically_ordered_monoid
-
-/-! Some lemmas specifically about `ℕ`. -/
-
-lemma sub_single_one_add {a : α} {u u' : α →₀ ℕ} (h : u a ≠ 0) :
-  u - single a 1 + u' = u + u' - single a 1 :=
-tsub_add_eq_add_tsub $ single_le_iff.mpr $ nat.one_le_iff_ne_zero.mpr h
-
-lemma add_sub_single_one {a : α} {u u' : α →₀ ℕ} (h : u' a ≠ 0) :
-  u + (u' - single a 1) = u + u' - single a 1 :=
-(add_tsub_assoc_of_le (single_le_iff.mpr $ nat.one_le_iff_ne_zero.mpr h) _).symm
-
-end nat_sub
-
-end finsupp
-
-namespace multiset
-
-lemma to_finsuppstrict_mono : strict_mono (@to_finsupp α) :=
-finsupp.order_iso_multiset.symm.strict_mono
-
-end multiset
-
 section cast_finsupp
 variables [has_zero M] (f : α →₀ M)