finsupp.lean

/-
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

Type of functions with finite support.

Functions with finite support provide the basis for the following concrete instances:

 * ℕ →₀ α: Polynomials (where α is a ring)
 * (σ →₀ ℕ) →₀ α: Multivariate Polynomials (again α is a ring, and σ are variable names)
 * α →₀ ℕ: Multisets
 * α →₀ ℤ: Abelian groups freely generated by α
 * β →₀ α: Linear combinations over β where α is the scalar ring

Most of the theory assumes that the range is a commutative monoid. This gives us the big sum
operator as a powerful way to construct `finsupp` elements.

A general advice is to not use α →₀ β directly, as the type class setup might not be fitting.
The best is to define a copy and select the instances best suited.

-/
import data.finset data.set.finite algebra.big_operators algebra.module

noncomputable theory
open_locale classical

open finset

variables {α : Type*} {β : Type*} {γ : Type*} {δ : Type*} {ι : Type*}
  {α₁ : Type*} {α₂ : Type*} {β₁ : Type*} {β₂ : Type*}

/-- `finsupp α β`, denoted `α →₀ β`, is the type of functions `f : α → β` such that
  `f x = 0` for all but finitely many `x`. -/
structure finsupp (α : Type*) (β : Type*) [has_zero β] :=
(support            : finset α)
(to_fun             : α → β)
(mem_support_to_fun : ∀a, a ∈ support ↔ to_fun a ≠ 0)

infixr ` →₀ `:25 := finsupp

namespace finsupp

section basic
variable [has_zero β]

instance : has_coe_to_fun (α →₀ β) := ⟨λ_, α → β, finsupp.to_fun⟩

instance : has_zero (α →₀ β) := ⟨⟨∅, (λ_, 0), λ _, ⟨false.elim, λ H, H rfl⟩⟩⟩

@[simp] lemma zero_apply {a : α} : (0 : α →₀ β) a = 0 := rfl

@[simp] lemma support_zero : (0 : α →₀ β).support = ∅ := rfl

instance : inhabited (α →₀ β) := ⟨0⟩

@[simp] lemma mem_support_iff {f : α →₀ β} : ∀{a:α}, a ∈ f.support ↔ f a ≠ 0 :=
f.mem_support_to_fun

lemma not_mem_support_iff {f : α →₀ β} {a} : a ∉ f.support ↔ f a = 0 :=
not_iff_comm.1 mem_support_iff.symm

@[ext]
lemma ext : ∀{f g : α →₀ β}, (∀a, f a = g a) → f = g
| ⟨s, f, hf⟩ ⟨t, g, hg⟩ h :=
  begin
    have : f = g, { funext a, exact h a },
    subst this,
    have : s = t, { ext a, exact (hf a).trans (hg a).symm },
    subst this
  end

lemma ext_iff {f g : α →₀ β} : f = g ↔ (∀a:α, f a = g a) :=
⟨by rintros rfl a; refl, ext⟩

@[simp] lemma support_eq_empty {f : α →₀ β} : f.support = ∅ ↔ f = 0 :=
⟨assume h, ext $ assume a, by_contradiction $ λ H, (finset.ext.1 h a).1 $
  mem_support_iff.2 H, by rintro rfl; refl⟩

instance finsupp.decidable_eq [decidable_eq α] [decidable_eq β] : decidable_eq (α →₀ β) :=
assume f g, decidable_of_iff (f.support = g.support ∧ (∀a∈f.support, f a = g a))
  ⟨assume ⟨h₁, h₂⟩, ext $ assume a,
      if h : a ∈ f.support then h₂ a h else
        have hf : f a = 0, by rwa [mem_support_iff, not_not] at h,
        have hg : g a = 0, by rwa [h₁, mem_support_iff, not_not] at h,
        by rw [hf, hg],
    by rintro rfl; exact ⟨rfl, λ _ _, rfl⟩⟩

lemma finite_supp (f : α →₀ β) : set.finite {a | f a ≠ 0} :=
⟨fintype.of_finset f.support (λ _, mem_support_iff)⟩

lemma support_subset_iff {s : set α} {f : α →₀ β} :
  ↑f.support ⊆ s ↔ (∀a∉s, f a = 0) :=
by simp only [set.subset_def, mem_coe, mem_support_iff];
   exact forall_congr (assume a, @not_imp_comm _ _ (classical.dec _) (classical.dec _))

def equiv_fun_on_fintype [fintype α] : (α →₀ β) ≃ (α → β) :=
⟨λf a, f a, λf, mk (finset.univ.filter $ λa, f a ≠ 0) f (by simp),
  begin intro f, ext a, refl end,
  begin intro f, ext a, refl end⟩

end basic

section single
variables [has_zero β] {a a' : α} {b : β}

/-- `single a b` is the finitely supported function which has
  value `b` at `a` and zero otherwise. -/
def single (a : α) (b : β) : α →₀ β :=
⟨if b = 0 then ∅ else finset.singleton a, λ a', if a = a' then b else 0, λ a', begin
  by_cases hb : b = 0; by_cases a = a';
    simp only [hb, h, if_pos, if_false, mem_singleton],
  { exact ⟨false.elim, λ H, H rfl⟩ },
  { exact ⟨false.elim, λ H, H rfl⟩ },
  { exact ⟨λ _, hb, λ _, rfl⟩ },
  { exact ⟨λ H _, h H.symm, λ H, (H rfl).elim⟩ }
end⟩

lemma single_apply : (single a b : α →₀ β) a' = if a = a' then b else 0 := rfl

@[simp] lemma single_eq_same : (single a b : α →₀ β) a = b := if_pos rfl

@[simp] lemma single_eq_of_ne (h : a ≠ a') : (single a b : α →₀ β) a' = 0 := if_neg h

@[simp] lemma single_zero : (single a 0 : α →₀ β) = 0 :=
ext $ assume a',
begin
  by_cases h : a = a',
  { rw [h, single_eq_same, zero_apply] },
  { rw [single_eq_of_ne h, zero_apply] }
end

lemma support_single_ne_zero (hb : b ≠ 0) : (single a b).support = {a} :=
if_neg hb

lemma support_single_subset : (single a b).support ⊆ {a} :=
show ite _ _ _ ⊆ _, by split_ifs; [exact empty_subset _, exact subset.refl _]

lemma injective_single (a : α) : function.injective (single a : β → α →₀ β) :=
assume b₁ b₂ eq,
have (single a b₁ : α →₀ β) a = (single a b₂ : α →₀ β) a, by rw eq,
by rwa [single_eq_same, single_eq_same] at this

lemma single_eq_single_iff (a₁ a₂ : α) (b₁ b₂ : β) :
  single a₁ b₁ = single a₂ b₂ ↔ ((a₁ = a₂ ∧ b₁ = b₂) ∨ (b₁ = 0 ∧ b₂ = 0)) :=
begin
  split,
  { assume eq,
    by_cases a₁ = a₂,
    { refine or.inl ⟨h, _⟩,
      rwa [h, (injective_single a₂).eq_iff] at eq },
    { rw [finsupp.ext_iff] at eq,
      have h₁ := eq a₁,
      have h₂ := eq a₂,
      simp only [single_eq_same, single_eq_of_ne h, single_eq_of_ne (ne.symm h)] at h₁ h₂,
      exact or.inr ⟨h₁, h₂.symm⟩ } },
  { rintros (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩),
    { refl },
    { rw [single_zero, single_zero] } }
end

lemma single_right_inj (h : b ≠ 0) :
  single a b = single a' b ↔ a = a' :=
⟨λ H, by simpa [h, single_eq_single_iff] using H, λ H, by rw [H]⟩

lemma single_eq_zero : single a b = 0 ↔ b = 0 :=
⟨λ h, by { rw ext_iff at h, simpa only [finsupp.single_eq_same, finsupp.zero_apply] using h a },
λ h, by rw [h, single_zero]⟩

lemma single_swap {α β : Type*} [has_zero β] (a₁ a₂ : α) (b : β) :
  (single a₁ b : α → β) a₂ = (single a₂ b : α → β) a₁ :=
by simp [single_apply]; ac_refl

lemma unique_single [unique α] (x : α →₀ β) : x = single (default α) (x (default α)) :=
by ext i; simp [unique.eq_default i]

@[simp] lemma unique_single_eq_iff [unique α] {b' : β} :
  single a b = single a' b' ↔ b = b' :=
begin
  rw [single_eq_single_iff],
  split,
  { rintros (⟨_, rfl⟩ | ⟨rfl, rfl⟩); refl },
  { intro h, left, exact ⟨subsingleton.elim _ _, h⟩ }
end

end single

section on_finset
variables [has_zero β]

/-- `on_finset s f hf` is the finsupp function representing `f` restricted to the set `s`.
The function needs to be 0 outside of `s`. Use this when the set needs filtered anyway, otherwise
often better set representation is available. -/
def on_finset (s : finset α) (f : α → β) (hf : ∀a, f a ≠ 0 → a ∈ s) : α →₀ β :=
⟨s.filter (λa, f a ≠ 0), f,
  assume a, classical.by_cases
    (assume h : f a = 0, by rw mem_filter; exact ⟨and.right, λ H, (H h).elim⟩)
    (assume h : f a ≠ 0, by rw mem_filter; simp only [iff_true_intro h, hf a h, true_and])⟩

@[simp] lemma on_finset_apply {s : finset α} {f : α → β} {hf a} :
  (on_finset s f hf : α →₀ β) a = f a :=
rfl

@[simp] lemma support_on_finset_subset {s : finset α} {f : α → β} {hf} :
  (on_finset s f hf).support ⊆ s := filter_subset _

end on_finset

section map_range
variables [has_zero β₁] [has_zero β₂]

/-- The composition of `f : β₁ → β₂` and `g : α →₀ β₁` is
  `map_range f hf g : α →₀ β₂`, well defined when `f 0 = 0`. -/
def map_range (f : β₁ → β₂) (hf : f 0 = 0) (g : α →₀ β₁) : α →₀ β₂ :=
on_finset g.support (f ∘ g) $
  assume a, by rw [mem_support_iff, not_imp_not]; exact λ H, (congr_arg f H).trans hf

@[simp] lemma map_range_apply {f : β₁ → β₂} {hf : f 0 = 0} {g : α →₀ β₁} {a : α} :
  map_range f hf g a = f (g a) :=
rfl

@[simp] lemma map_range_zero {f : β₁ → β₂} {hf : f 0 = 0} : map_range f hf (0 : α →₀ β₁) = 0 :=
finsupp.ext $ λ a, by simp [hf]

lemma support_map_range {f : β₁ → β₂} {hf : f 0 = 0} {g : α →₀ β₁} :
  (map_range f hf g).support ⊆ g.support :=
support_on_finset_subset

@[simp] lemma map_range_single {f : β₁ → β₂} {hf : f 0 = 0} {a : α} {b : β₁} :
  map_range f hf (single a b) = single a (f b) :=
finsupp.ext $ λ a', show f (ite _ _ _) = ite _ _ _, by split_ifs; [refl, exact hf]

end map_range

section emb_domain
variables [has_zero β]

/-- Given `f : α₁ ↪ α₂` and `v : α₁ →₀ β`, `emb_domain f v : α₂ →₀ β` is the finitely supported
function whose value at `f a : α₂` is `v a`. For a `b : α₂` outside the range of `f` it is zero. -/
def emb_domain (f : α₁ ↪ α₂) (v : α₁ →₀ β) : α₂ →₀ β :=
begin
  refine ⟨v.support.map f, λa₂,
    if h : a₂ ∈ v.support.map f then v (v.support.choose (λa₁, f a₁ = a₂) _) else 0, _⟩,
  { rcases finset.mem_map.1 h with ⟨a, ha, rfl⟩,
    exact exists_unique.intro a ⟨ha, rfl⟩ (assume b ⟨_, hb⟩, f.inj hb) },
  { assume a₂,
    split_ifs,
    { simp [h],
      rw [← finsupp.not_mem_support_iff, not_not],
      apply finset.choose_mem },
    { simp [h] } }
end

lemma support_emb_domain (f : α₁ ↪ α₂) (v : α₁ →₀ β) :
  (emb_domain f v).support = v.support.map f :=
rfl

lemma emb_domain_zero (f : α₁ ↪ α₂) : (emb_domain f 0 : α₂ →₀ β) = 0 :=
rfl

lemma emb_domain_apply (f : α₁ ↪ α₂) (v : α₁ →₀ β) (a : α₁) :
  emb_domain f v (f a) = v a :=
begin
  change dite _ _ _ = _,
  split_ifs; rw [finset.mem_map' f] at h,
  { refine congr_arg (v : α₁ → β) (f.inj' _),
    exact finset.choose_property (λa₁, f a₁ = f a) _ _ },
  { exact (finsupp.not_mem_support_iff.1 h).symm }
end

lemma emb_domain_notin_range (f : α₁ ↪ α₂) (v : α₁ →₀ β) (a : α₂) (h : a ∉ set.range f) :
  emb_domain f v a = 0 :=
begin
  refine dif_neg (mt (assume h, _) h),
  rcases finset.mem_map.1 h with ⟨a, h, rfl⟩,
  exact set.mem_range_self a
end

lemma emb_domain_inj {f : α₁ ↪ α₂} {l₁ l₂ : α₁ →₀ β} :
  emb_domain f l₁ = emb_domain f l₂ ↔ l₁ = l₂ :=
⟨λ h, finsupp.ext $ λ a, by simpa [emb_domain_apply] using finsupp.ext_iff.1 h (f a),
  λ h, by rw h⟩

lemma emb_domain_map_range
  {β₁ β₂ : Type*} [has_zero β₁] [has_zero β₂]
  (f : α₁ ↪ α₂) (g : β₁ → β₂) (p : α₁ →₀ β₁) (hg : g 0 = 0) :
  emb_domain f (map_range g hg p) = map_range g hg (emb_domain f p) :=
begin
  ext a,
  by_cases a ∈ set.range f,
  { rcases h with ⟨a', rfl⟩,
    rw [map_range_apply, emb_domain_apply, emb_domain_apply, map_range_apply] },
  { rw [map_range_apply, emb_domain_notin_range, emb_domain_notin_range, ← hg]; assumption }
end

lemma single_of_emb_domain_single
  (l : α₁ →₀ β) (f : α₁ ↪ α₂) (a : α₂) (b : β) (hb : b ≠ 0)
  (h : l.emb_domain f = finsupp.single a b) :
  ∃ x, l = finsupp.single x b ∧ f x = a :=
begin
  have h_map_support : finset.map f (l.support) = finset.singleton a,
    by rw [←finsupp.support_emb_domain, h, finsupp.support_single_ne_zero hb]; refl,
  have ha : a ∈ finset.map f (l.support),
    by simp [h_map_support],
  rcases finset.mem_map.1 ha with ⟨c, hc₁, hc₂⟩,
  use c,
  split,
  { ext d,
    rw [← finsupp.emb_domain_apply f l, h],
    by_cases h_cases : c = d,
    { simp [h_cases.symm, hc₂] },
    { rw [finsupp.single_apply, finsupp.single_apply, if_neg, if_neg h_cases],
      by_contra hfd,
      exact h_cases (f.inj (hc₂.trans hfd)) } },
  { exact hc₂ }
end

end emb_domain

section zip_with
variables [has_zero β] [has_zero β₁] [has_zero β₂]

/-- `zip_with f hf g₁ g₂` is the finitely supported function satisfying
  `zip_with f hf g₁ g₂ a = f (g₁ a) (g₂ a)`, and well defined when `f 0 0 = 0`. -/
def zip_with (f : β₁ → β₂ → β) (hf : f 0 0 = 0) (g₁ : α →₀ β₁) (g₂ : α →₀ β₂) : (α →₀ β) :=
on_finset (g₁.support ∪ g₂.support) (λa, f (g₁ a) (g₂ a)) $ λ a H, begin
  simp only [mem_union, mem_support_iff, ne], rw [← not_and_distrib],
  rintro ⟨h₁, h₂⟩, rw [h₁, h₂] at H, exact H hf
end

@[simp] lemma zip_with_apply
  {f : β₁ → β₂ → β} {hf : f 0 0 = 0} {g₁ : α →₀ β₁} {g₂ : α →₀ β₂} {a : α} :
  zip_with f hf g₁ g₂ a = f (g₁ a) (g₂ a) := rfl

lemma support_zip_with {f : β₁ → β₂ → β} {hf : f 0 0 = 0} {g₁ : α →₀ β₁} {g₂ : α →₀ β₂} :
  (zip_with f hf g₁ g₂).support ⊆ g₁.support ∪ g₂.support :=
support_on_finset_subset

end zip_with

section erase

def erase [has_zero β] (a : α) (f : α →₀ β) : α →₀ β :=
⟨f.support.erase a, (λa', if a' = a then 0 else f a'),
  assume a', by rw [mem_erase, mem_support_iff]; split_ifs;
    [exact ⟨λ H _, H.1 h, λ H, (H rfl).elim⟩,
    exact and_iff_right h]⟩

@[simp] lemma support_erase [has_zero β] {a : α} {f : α →₀ β} :
  (f.erase a).support = f.support.erase a :=
rfl

@[simp] lemma erase_same [has_zero β] {a : α} {f : α →₀ β} : (f.erase a) a = 0 :=
if_pos rfl

@[simp] lemma erase_ne [has_zero β] {a a' : α} {f : α →₀ β} (h : a' ≠ a) : (f.erase a) a' = f a' :=
if_neg h

end erase

-- [to_additive sum] for finsupp.prod doesn't work, the equation lemmas are not generated
/-- `sum f g` is the sum of `g a (f a)` over the support of `f`. -/
def sum [has_zero β] [add_comm_monoid γ] (f : α →₀ β) (g : α → β → γ) : γ :=
f.support.sum (λa, g a (f a))

/-- `prod f g` is the product of `g a (f a)` over the support of `f`. -/
@[to_additive]
def prod [has_zero β] [comm_monoid γ] (f : α →₀ β) (g : α → β → γ) : γ :=
f.support.prod (λa, g a (f a))

@[to_additive]
lemma prod_map_range_index [has_zero β₁] [has_zero β₂] [comm_monoid γ]
  {f : β₁ → β₂} {hf : f 0 = 0} {g : α →₀ β₁} {h : α → β₂ → γ} (h0 : ∀a, h a 0 = 1) :
  (map_range f hf g).prod h = g.prod (λa b, h a (f b)) :=
finset.prod_subset support_map_range $ λ _ _ H,
by rw [not_mem_support_iff.1 H, h0]

@[to_additive]
lemma prod_zero_index [add_comm_monoid β] [comm_monoid γ] {h : α → β → γ} :
  (0 : α →₀ β).prod h = 1 := rfl

section nat_sub
instance nat_sub : has_sub (α →₀ ℕ) := ⟨zip_with (λ m n, m - n) (nat.sub_zero 0)⟩

@[simp] lemma nat_sub_apply {g₁ g₂ : α →₀ ℕ} {a : α} :
  (g₁ - g₂) a = g₁ a - g₂ a := rfl

end nat_sub

section add_monoid
variables [add_monoid β]

@[to_additive]
lemma prod_single_index [comm_monoid γ] {a : α} {b : β} {h : α → β → γ} (h_zero : h a 0 = 1) :
  (single a b).prod h = h a b :=
begin
  by_cases h : b = 0,
  { simp only [h, h_zero, single_zero]; refl },
  { simp only [finsupp.prod, support_single_ne_zero h, insert_empty_eq_singleton,
      prod_singleton, single_eq_same] }
end

instance : has_add (α →₀ β) := ⟨zip_with (+) (add_zero 0)⟩

@[simp] lemma add_apply {g₁ g₂ : α →₀ β} {a : α} : (g₁ + g₂) a = g₁ a + g₂ a :=
rfl

lemma support_add {g₁ g₂ : α →₀ β} : (g₁ + g₂).support ⊆ g₁.support ∪ g₂.support :=
support_zip_with

lemma support_add_eq {g₁ g₂ : α →₀ β} (h : disjoint g₁.support g₂.support) :
  (g₁ + g₂).support = g₁.support ∪ g₂.support :=
le_antisymm support_zip_with $ assume a ha,
(finset.mem_union.1 ha).elim
  (assume ha, have a ∉ g₂.support, from disjoint_left.1 h ha,
    by simp only [mem_support_iff, not_not] at *;
    simpa only [add_apply, this, add_zero])
  (assume ha, have a ∉ g₁.support, from disjoint_right.1 h ha,
    by simp only [mem_support_iff, not_not] at *;
    simpa only [add_apply, this, zero_add])

@[simp] lemma single_add {a : α} {b₁ b₂ : β} : single a (b₁ + b₂) = single a b₁ + single a b₂ :=
ext $ assume a',
begin
  by_cases h : a = a',
  { rw [h, add_apply, single_eq_same, single_eq_same, single_eq_same] },
  { rw [add_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, zero_add] }
end

instance : add_monoid (α →₀ β) :=
{ add_monoid .
  zero      := 0,
  add       := (+),
  add_assoc := assume ⟨s, f, hf⟩ ⟨t, g, hg⟩ ⟨u, h, hh⟩, ext $ assume a, add_assoc _ _ _,
  zero_add  := assume ⟨s, f, hf⟩, ext $ assume a, zero_add _,
  add_zero  := assume ⟨s, f, hf⟩, ext $ assume a, add_zero _ }

instance (a : α) : is_add_monoid_hom (λ g : α →₀ β, g a) :=
{ map_add := λ _ _, add_apply, map_zero := zero_apply }

lemma single_add_erase {a : α} {f : α →₀ β} : single a (f a) + f.erase a = f :=
ext $ λ a',
if h : a = a' then by subst h; simp only [add_apply, single_eq_same, erase_same, add_zero]
else by simp only [add_apply, single_eq_of_ne h, zero_add, erase_ne (ne.symm h)]

lemma erase_add_single {a : α} {f : α →₀ β} : f.erase a + single a (f a) = f :=
ext $ λ a',
if h : a = a' then by subst h; simp only [add_apply, single_eq_same, erase_same, zero_add]
else by simp only [add_apply, single_eq_of_ne h, add_zero, erase_ne (ne.symm h)]

@[elab_as_eliminator]
protected theorem induction {p : (α →₀ β) → Prop} (f : α →₀ β)
  (h0 : p 0) (ha : ∀a b (f : α →₀ β), a ∉ f.support → b ≠ 0 → p f → p (single a b + f)) :
  p f :=
suffices ∀s (f : α →₀ β), f.support = s → p f, from this _ _ rfl,
assume s, finset.induction_on s (λ f hf, by rwa [support_eq_empty.1 hf]) $
assume a s has ih f hf,
suffices p (single a (f a) + f.erase a), by rwa [single_add_erase] at this,
begin
  apply ha,
  { rw [support_erase, mem_erase], exact λ H, H.1 rfl },
  { rw [← mem_support_iff, hf], exact mem_insert_self _ _ },
  { apply ih _ _,
    rw [support_erase, hf, finset.erase_insert has] }
end

lemma induction₂ {p : (α →₀ β) → Prop} (f : α →₀ β)
  (h0 : p 0) (ha : ∀a b (f : α →₀ β), a ∉ f.support → b ≠ 0 → p f → p (f + single a b)) :
  p f :=
suffices ∀s (f : α →₀ β), f.support = s → p f, from this _ _ rfl,
assume s, finset.induction_on s (λ f hf, by rwa [support_eq_empty.1 hf]) $
assume a s has ih f hf,
suffices p (f.erase a + single a (f a)), by rwa [erase_add_single] at this,
begin
  apply ha,
  { rw [support_erase, mem_erase], exact λ H, H.1 rfl },
  { rw [← mem_support_iff, hf], exact mem_insert_self _ _ },
  { apply ih _ _,
    rw [support_erase, hf, finset.erase_insert has] }
end

lemma map_range_add [add_monoid β₁] [add_monoid β₂]
  {f : β₁ → β₂} {hf : f 0 = 0} (hf' : ∀ x y, f (x + y) = f x + f y) (v₁ v₂ : α →₀ β₁) :
  map_range f hf (v₁ + v₂) = map_range f hf v₁ + map_range f hf v₂ :=
finsupp.ext $ λ a, by simp [hf']

end add_monoid

instance [add_comm_monoid β] : add_comm_monoid (α →₀ β) :=
{ add_comm := assume ⟨s, f, _⟩ ⟨t, g, _⟩, ext $ assume a, add_comm _ _,
  .. finsupp.add_monoid }

instance [add_group β] : add_group (α →₀ β) :=
{ neg          := map_range (has_neg.neg) neg_zero,
  add_left_neg := assume ⟨s, f, _⟩, ext $ assume x, add_left_neg _,
  .. finsupp.add_monoid }

lemma single_multiset_sum [add_comm_monoid β] (s : multiset β) (a : α) :
  single a s.sum = (s.map (single a)).sum :=
multiset.induction_on s single_zero $ λ a s ih,
by rw [multiset.sum_cons, single_add, ih, multiset.map_cons, multiset.sum_cons]

lemma single_finset_sum [add_comm_monoid β] (s : finset γ) (f : γ → β) (a : α) :
  single a (s.sum f) = s.sum (λb, single a (f b)) :=
begin
  transitivity,
  apply single_multiset_sum,
  rw [multiset.map_map],
  refl
end

lemma single_sum [has_zero γ] [add_comm_monoid β] (s : δ →₀ γ) (f : δ → γ → β) (a : α) :
  single a (s.sum f) = s.sum (λd c, single a (f d c)) :=
single_finset_sum _ _ _


@[to_additive]
lemma prod_neg_index [add_group β] [comm_monoid γ]
  {g : α →₀ β} {h : α → β → γ} (h0 : ∀a, h a 0 = 1) :
  (-g).prod h = g.prod (λa b, h a (- b)) :=
prod_map_range_index h0

@[simp] lemma neg_apply [add_group β] {g : α →₀ β} {a : α} : (- g) a = - g a := rfl

@[simp] lemma sub_apply [add_group β] {g₁ g₂ : α →₀ β} {a : α} : (g₁ - g₂) a = g₁ a - g₂ a := rfl

@[simp] lemma support_neg [add_group β] {f : α →₀ β} : support (-f) = support f :=
finset.subset.antisymm
  support_map_range
  (calc support f = support (- (- f)) : congr_arg support (neg_neg _).symm
     ... ⊆ support (- f) : support_map_range)

instance [add_comm_group β] : add_comm_group (α →₀ β) :=
{ add_comm := add_comm, ..finsupp.add_group }

@[simp] lemma sum_apply [has_zero β₁] [add_comm_monoid β]
  {f : α₁ →₀ β₁} {g : α₁ → β₁ → α →₀ β} {a₂ : α} :
  (f.sum g) a₂ = f.sum (λa₁ b, g a₁ b a₂) :=
(f.support.sum_hom (λf : α →₀ β, f a₂)).symm

lemma support_sum [has_zero β₁] [add_comm_monoid β]
  {f : α₁ →₀ β₁} {g : α₁ → β₁ → (α →₀ β)} :
  (f.sum g).support ⊆ f.support.bind (λa, (g a (f a)).support) :=
have ∀a₁ : α, f.sum (λ (a : α₁) (b : β₁), (g a b) a₁) ≠ 0 →
    (∃ (a : α₁), f a ≠ 0 ∧ ¬ (g a (f a)) a₁ = 0),
  from assume a₁ h,
  let ⟨a, ha, ne⟩ := finset.exists_ne_zero_of_sum_ne_zero h in
  ⟨a, mem_support_iff.mp ha, ne⟩,
by simpa only [finset.subset_iff, mem_support_iff, finset.mem_bind, sum_apply, exists_prop] using this

@[simp] lemma sum_zero [add_comm_monoid β] [add_comm_monoid γ] {f : α →₀ β} :
  f.sum (λa b, (0 : γ)) = 0 :=
finset.sum_const_zero

@[simp] lemma sum_add  [add_comm_monoid β] [add_comm_monoid γ] {f : α →₀ β}
  {h₁ h₂ : α → β → γ} :
  f.sum (λa b, h₁ a b + h₂ a b) = f.sum h₁ + f.sum h₂ :=
finset.sum_add_distrib

@[simp] lemma sum_neg [add_comm_monoid β] [add_comm_group γ] {f : α →₀ β}
  {h : α → β → γ} : f.sum (λa b, - h a b) = - f.sum h :=
f.support.sum_hom (@has_neg.neg γ _)

@[simp] lemma sum_sub [add_comm_monoid β] [add_comm_group γ] {f : α →₀ β}
  {h₁ h₂ : α → β → γ} :
  f.sum (λa b, h₁ a b - h₂ a b) = f.sum h₁ - f.sum h₂ :=
by rw [sub_eq_add_neg, ←sum_neg, ←sum_add]; refl

@[simp] lemma sum_single [add_comm_monoid β] (f : α →₀ β) :
  f.sum single = f :=
have ∀a:α, f.sum (λa' b, ite (a' = a) b 0) =
    ({a} : finset α).sum (λa', ite (a' = a) (f a') 0),
begin
  intro a,
  by_cases h : a ∈ f.support,
  { have : (finset.singleton a : finset α) ⊆ f.support,
      { simpa only [finset.subset_iff, mem_singleton, forall_eq] },
    refine (finset.sum_subset this (λ _ _ H, _)).symm,
    exact if_neg (mt mem_singleton.2 H) },
  { transitivity (f.support.sum (λa, (0 : β))),
    { refine (finset.sum_congr rfl $ λ a' ha', if_neg _),
      rintro rfl, exact h ha' },
    { rw [sum_const_zero, insert_empty_eq_singleton, sum_singleton,
        if_pos rfl, not_mem_support_iff.1 h] } }
end,
ext $ assume a, by simp only [sum_apply, single_apply, this,
  insert_empty_eq_singleton, sum_singleton, if_pos]

@[to_additive]
lemma prod_add_index [add_comm_monoid β] [comm_monoid γ] {f g : α →₀ β}
  {h : α → β → γ} (h_zero : ∀a, h a 0 = 1) (h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
  (f + g).prod h = f.prod h * g.prod h :=
have f_eq : (f.support ∪ g.support).prod (λa, h a (f a)) = f.prod h,
  from (finset.prod_subset (finset.subset_union_left _ _) $
    by intros _ _ H; rw [not_mem_support_iff.1 H, h_zero]).symm,
have g_eq : (f.support ∪ g.support).prod (λa, h a (g a)) = g.prod h,
  from (finset.prod_subset (finset.subset_union_right _ _) $
    by intros _ _ H; rw [not_mem_support_iff.1 H, h_zero]).symm,
calc (f + g).support.prod (λa, h a ((f + g) a)) =
      (f.support ∪ g.support).prod (λa, h a ((f + g) a)) :
    finset.prod_subset support_add $
      by intros _ _ H; rw [not_mem_support_iff.1 H, h_zero]
  ... = (f.support ∪ g.support).prod (λa, h a (f a)) *
      (f.support ∪ g.support).prod (λa, h a (g a)) :
    by simp only [add_apply, h_add, finset.prod_mul_distrib]
  ... = _ : by rw [f_eq, g_eq]

lemma sum_sub_index [add_comm_group β] [add_comm_group γ] {f g : α →₀ β}
  {h : α → β → γ} (h_sub : ∀a b₁ b₂, h a (b₁ - b₂) = h a b₁ - h a b₂) :
  (f - g).sum h = f.sum h - g.sum h :=
have h_zero : ∀a, h a 0 = 0,
  from assume a,
  have h a (0 - 0) = h a 0 - h a 0, from h_sub a 0 0,
  by simpa only [sub_self] using this,
have h_neg : ∀a b, h a (- b) = - h a b,
  from assume a b,
  have h a (0 - b) = h a 0 - h a b, from h_sub a 0 b,
  by simpa only [h_zero, zero_sub] using this,
have h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ + h a b₂,
  from assume a b₁ b₂,
  have h a (b₁ - (- b₂)) = h a b₁ - h a (- b₂), from h_sub a b₁ (-b₂),
  by simpa only [h_neg, sub_neg_eq_add] using this,
calc (f - g).sum h = (f + - g).sum h : rfl
  ... = f.sum h + - g.sum h : by simp only [sum_add_index h_zero h_add, sum_neg_index h_zero, h_neg, sum_neg]
  ... = f.sum h - g.sum h : rfl

@[to_additive]
lemma prod_finset_sum_index [add_comm_monoid β] [comm_monoid γ]
  {s : finset ι} {g : ι → α →₀ β}
  {h : α → β → γ} (h_zero : ∀a, h a 0 = 1) (h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
  s.prod (λi, (g i).prod h) = (s.sum g).prod h :=
finset.induction_on s rfl $ λ a s has ih,
by rw [prod_insert has, ih, sum_insert has, prod_add_index h_zero h_add]

@[to_additive]
lemma prod_sum_index
  [add_comm_monoid β₁] [add_comm_monoid β] [comm_monoid γ]
  {f : α₁ →₀ β₁} {g : α₁ → β₁ → α →₀ β}
  {h : α → β → γ} (h_zero : ∀a, h a 0 = 1) (h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
  (f.sum g).prod h = f.prod (λa b, (g a b).prod h) :=
(prod_finset_sum_index h_zero h_add).symm

lemma multiset_sum_sum_index
  [add_comm_monoid β] [add_comm_monoid γ]
  (f : multiset (α →₀ β)) (h : α → β → γ)
  (h₀ : ∀a, h a 0 = 0) (h₁ : ∀ (a : α) (b₁ b₂ : β), h a (b₁ + b₂) = h a b₁ + h a b₂) :
  (f.sum.sum h) = (f.map $ λg:α →₀ β, g.sum h).sum :=
multiset.induction_on f rfl $ assume a s ih,
by rw [multiset.sum_cons, multiset.map_cons, multiset.sum_cons, sum_add_index h₀ h₁, ih]

lemma multiset_map_sum [has_zero β] {f : α →₀ β} {m : γ → δ} {h : α → β → multiset γ} :
  multiset.map m (f.sum h) = f.sum (λa b, (h a b).map m) :=
(f.support.sum_hom _).symm

lemma multiset_sum_sum [has_zero β] [add_comm_monoid γ] {f : α →₀ β} {h : α → β → multiset γ} :
  multiset.sum (f.sum h) = f.sum (λa b, multiset.sum (h a b)) :=
(f.support.sum_hom multiset.sum).symm

section map_range
variables
  [add_comm_monoid β₁] [add_comm_monoid β₂]
  (f : β₁ → β₂) [hf : is_add_monoid_hom f]

instance is_add_monoid_hom_map_range :
  is_add_monoid_hom (map_range f hf.map_zero : (α →₀ β₁) → (α →₀ β₂)) :=
{ map_zero := map_range_zero, map_add := λ a b, map_range_add hf.map_add _ _ }

lemma map_range_multiset_sum (m : multiset (α →₀ β₁)) :
  map_range f hf.map_zero m.sum = (m.map $ λx, map_range f hf.map_zero x).sum :=
(m.sum_hom (map_range f hf.map_zero)).symm

lemma map_range_finset_sum {ι : Type*} (s : finset ι) (g : ι → (α →₀ β₁))  :
  map_range f hf.map_zero (s.sum g) = s.sum (λx, map_range f hf.map_zero (g x)) :=
by rw [finset.sum.equations._eqn_1, map_range_multiset_sum, multiset.map_map]; refl

end map_range

section map_domain
variables [add_comm_monoid β] {v v₁ v₂ : α →₀ β}

/-- Given `f : α₁ → α₂` and `v : α₁ →₀ β`, `map_domain f v : α₂ →₀ β`
  is the finitely supported function whose value at `a : α₂` is the sum
  of `v x` over all `x` such that `f x = a`. -/
def map_domain (f : α₁ → α₂) (v : α₁ →₀ β) : α₂ →₀ β :=
v.sum $ λa, single (f a)

lemma map_domain_apply {f : α₁ → α₂} (hf : function.injective f) (x : α₁ →₀ β) (a : α₁) :
  map_domain f x (f a) = x a :=
begin
  rw [map_domain, sum_apply, sum, finset.sum_eq_single a, single_eq_same],
  { assume b _ hba, exact single_eq_of_ne (hf.ne hba) },
  { simp only [(∉), (≠), not_not, mem_support_iff],
    assume h,
    rw [h, single_zero],
    refl }
end

lemma map_domain_notin_range {f : α₁ → α₂} (x : α₁ →₀ β) (a : α₂) (h : a ∉ set.range f) :
  map_domain f x a = 0 :=
begin
  rw [map_domain, sum_apply, sum],
  exact finset.sum_eq_zero
    (assume a' h', single_eq_of_ne $ assume eq, h $ eq ▸ set.mem_range_self _)
end

lemma map_domain_id : map_domain id v = v := sum_single _

lemma map_domain_comp {f : α → α₁} {g : α₁ → α₂} :
  map_domain (g ∘ f) v = map_domain g (map_domain f v) :=
begin
  refine ((sum_sum_index _ _).trans _).symm,
  { intros, exact single_zero },
  { intros, exact single_add },
  refine sum_congr rfl (λ _ _, sum_single_index _),
  { exact single_zero }
end

lemma map_domain_single {f : α → α₁} {a : α} {b : β} : map_domain f (single a b) = single (f a) b :=
sum_single_index single_zero

@[simp] lemma map_domain_zero {f : α → α₂} : map_domain f 0 = (0 : α₂ →₀ β) :=
sum_zero_index

lemma map_domain_congr {f g : α → α₂} (h : ∀x∈v.support, f x = g x) :
  v.map_domain f = v.map_domain g :=
finset.sum_congr rfl $ λ _ H, by simp only [h _ H]

lemma map_domain_add {f : α → α₂} : map_domain f (v₁ + v₂) = map_domain f v₁ + map_domain f v₂ :=
sum_add_index (λ _, single_zero) (λ _ _ _, single_add)

lemma map_domain_finset_sum {f : α → α₂} {s : finset ι} {v : ι → α →₀ β} :
  map_domain f (s.sum v) = s.sum (λi, map_domain f (v i)) :=
eq.symm $ sum_finset_sum_index (λ _, single_zero) (λ _ _ _, single_add)

lemma map_domain_sum [has_zero β₁] {f : α → α₂} {s : α →₀ β₁} {v : α → β₁ → α →₀ β} :
  map_domain f (s.sum v) = s.sum (λa b, map_domain f (v a b)) :=
eq.symm $ sum_finset_sum_index (λ _, single_zero) (λ _ _ _, single_add)

lemma map_domain_support {f : α → α₂} {s : α →₀ β} :
  (s.map_domain f).support ⊆ s.support.image f :=
finset.subset.trans support_sum $
  finset.subset.trans (finset.bind_mono $ assume a ha, support_single_subset) $
  by rw [finset.bind_singleton]; exact subset.refl _

@[to_additive]
lemma prod_map_domain_index [comm_monoid γ] {f : α → α₂} {s : α →₀ β}
  {h : α₂ → β → γ} (h_zero : ∀a, h a 0 = 1) (h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
  (s.map_domain f).prod h = s.prod (λa b, h (f a) b) :=
(prod_sum_index h_zero h_add).trans $ prod_congr rfl $ λ _ _, prod_single_index (h_zero _)

lemma emb_domain_eq_map_domain (f : α₁ ↪ α₂) (v : α₁ →₀ β) :
  emb_domain f v = map_domain f v :=
begin
  ext a,
  by_cases a ∈ set.range f,
  { rcases h with ⟨a, rfl⟩,
    rw [map_domain_apply (function.embedding.inj' _), emb_domain_apply] },
  { rw [map_domain_notin_range, emb_domain_notin_range]; assumption }
end

lemma injective_map_domain {f : α₁ → α₂} (hf : function.injective f) :
  function.injective (map_domain f : (α₁ →₀ β) → (α₂ →₀ β)) :=
begin
  assume v₁ v₂ eq, ext a,
  have : map_domain f v₁ (f a) = map_domain f v₂ (f a), { rw eq },
  rwa [map_domain_apply hf, map_domain_apply hf] at this,
end

end map_domain

section comap_domain

noncomputable def comap_domain {α₁ α₂ γ : Type*} [has_zero γ]
  (f : α₁ → α₂) (l : α₂ →₀ γ) (hf : set.inj_on f (f ⁻¹' l.support.to_set)) : α₁ →₀ γ :=
{ support := l.support.preimage hf,
  to_fun := (λ a, l (f a)),
  mem_support_to_fun :=
    begin
      intros a,
      simp only [finset.mem_def.symm, finset.mem_preimage],
      exact l.mem_support_to_fun (f a),
    end }

lemma comap_domain_apply {α₁ α₂ γ : Type*} [has_zero γ]
  (f : α₁ → α₂) (l : α₂ →₀ γ) (hf : set.inj_on f (f ⁻¹' l.support.to_set)) (a : α₁) :
  comap_domain f l hf a = l (f a) :=
begin
  unfold_coes,
  unfold comap_domain,
  simp,
  refl
end

lemma sum_comap_domain {α₁ α₂ β γ : Type*} [has_zero β] [add_comm_monoid γ]
  (f : α₁ → α₂) (l : α₂ →₀ β) (g : α₂ → β → γ) (hf : set.bij_on f (f ⁻¹' l.support.to_set) l.support.to_set):
  (comap_domain f l (set.inj_on_of_bij_on hf)).sum (g ∘ f) = l.sum g :=
begin
  unfold sum,
  haveI := classical.dec_eq α₂,
  simp only [comap_domain, comap_domain_apply, finset.sum_preimage f _ _ (λ (x : α₂), g x (l x))],
end

lemma eq_zero_of_comap_domain_eq_zero {α₁ α₂ γ : Type*} [add_comm_monoid γ]
  (f : α₁ → α₂) (l : α₂ →₀ γ) (hf : set.bij_on f (f ⁻¹' l.support.to_set) l.support.to_set) :
   comap_domain f l (set.inj_on_of_bij_on hf) = 0 → l = 0 :=
begin
  rw [← support_eq_empty, ← support_eq_empty, comap_domain],
  simp only [finset.ext, finset.not_mem_empty, iff_false, mem_preimage],
  assume h a ha,
  cases hf.2.2 ha with b hb,
  exact h b (hb.2.symm ▸ ha)
end

lemma map_domain_comap_domain {α₁ α₂ γ : Type*} [add_comm_monoid γ]
  (f : α₁ → α₂) (l : α₂ →₀ γ)
  (hf : function.injective f) (hl : ↑l.support ⊆ set.range f):
  map_domain f (comap_domain f l (set.inj_on_of_injective _ hf)) = l :=
begin
  ext a,
  haveI := classical.dec (a ∈ set.range f),
  by_cases h_cases: a ∈ set.range f,
  { rcases set.mem_range.1 h_cases with ⟨b, hb⟩,
    rw [hb.symm, map_domain_apply hf, comap_domain_apply] },
  { rw map_domain_notin_range _ _ h_cases,
    by_contra h_contr,
    apply h_cases (hl (finset.mem_coe.2 (mem_support_iff.2 (λ h, h_contr h.symm)))) }
end

end comap_domain

/-- The product of `f g : α →₀ β` is the finitely supported function
  whose value at `a` is the sum of `f x * g y` over all pairs `x, y`
  such that `x + y = a`. (Think of the product of multivariate
  polynomials where `α` is the monoid of monomial exponents.) -/
instance [has_add α] [semiring β] : has_mul (α →₀ β) :=
⟨λf g, f.sum $ λa₁ b₁, g.sum $ λa₂ b₂, single (a₁ + a₂) (b₁ * b₂)⟩

lemma mul_def [has_add α] [semiring β] {f g : α →₀ β} :
  f * g = (f.sum $ λa₁ b₁, g.sum $ λa₂ b₂, single (a₁ + a₂) (b₁ * b₂)) := rfl

lemma support_mul [has_add α] [semiring β] (a b : α →₀ β) :
  (a * b).support ⊆ a.support.bind (λa₁, b.support.bind $ λa₂, {a₁ + a₂}) :=
subset.trans support_sum $ bind_mono $ assume a₁ _,
  subset.trans support_sum $ bind_mono $ assume a₂ _, support_single_subset

/-- The unit of the multiplication is `single 0 1`, i.e. the function
  that is 1 at 0 and zero elsewhere. -/
instance [has_zero α] [has_zero β] [has_one β] : has_one (α →₀ β) :=
⟨single 0 1⟩

lemma one_def [has_zero α] [has_zero β] [has_one β] : 1 = (single 0 1 : α →₀ β) := rfl

section filter
section has_zero
variables [has_zero β] (p : α → Prop) (f : α →₀ β)

/-- `filter p f` is the function which is `f a` if `p a` is true and 0 otherwise. -/
def filter (p : α → Prop) (f : α →₀ β) : α →₀ β :=
on_finset f.support (λa, if p a then f a else 0) $ λ a H,
mem_support_iff.2 $ λ h, by rw [h, if_t_t] at H; exact H rfl

@[simp] lemma filter_apply_pos {a : α} (h : p a) : f.filter p a = f a :=
if_pos h

@[simp] lemma filter_apply_neg {a : α} (h : ¬ p a) : f.filter p a = 0 :=
if_neg h

@[simp] lemma support_filter : (f.filter p).support = f.support.filter p :=
finset.ext.mpr $ assume a, if H : p a
then by simp only [mem_support_iff, filter_apply_pos _ _ H, mem_filter, H, and_true]
else by simp only [mem_support_iff, filter_apply_neg _ _ H, mem_filter, H, and_false, ne.def, ne_self_iff_false]

lemma filter_zero : (0 : α →₀ β).filter p = 0 :=
by rw [← support_eq_empty, support_filter, support_zero, finset.filter_empty]

@[simp] lemma filter_single_of_pos
  {a : α} {b : β} (h : p a) : (single a b).filter p = single a b :=
finsupp.ext $ λ x, begin
  by_cases h' : p x; simp [h'],
  rw single_eq_of_ne, rintro rfl, exact h' h
end

@[simp] lemma filter_single_of_neg
  {a : α} {b : β} (h : ¬ p a) : (single a b).filter p = 0 :=
finsupp.ext $ λ x, begin
  by_cases h' : p x; simp [h'],
  rw single_eq_of_ne, rintro rfl, exact h h'
end

end has_zero

lemma filter_pos_add_filter_neg [add_monoid β] (f : α →₀ β) (p : α → Prop) :
  f.filter p + f.filter (λa, ¬ p a) = f :=
finsupp.ext $ assume a, if H : p a
then by simp only [add_apply, filter_apply_pos, filter_apply_neg, H, not_not, add_zero]
else by simp only [add_apply, filter_apply_pos, filter_apply_neg, H, not_false_iff, zero_add]

end filter

section frange
variables [has_zero β]

def frange (f : α →₀ β) : finset β :=
finset.image f f.support

theorem mem_frange {f : α →₀ β} {y : β} :
  y ∈ f.frange ↔ y ≠ 0 ∧ ∃ x, f x = y :=
finset.mem_image.trans
⟨λ ⟨x, hx1, hx2⟩, ⟨hx2 ▸ mem_support_iff.1 hx1, x, hx2⟩,
λ ⟨hy, x, hx⟩, ⟨x, mem_support_iff.2 (hx.symm ▸ hy), hx⟩⟩

theorem zero_not_mem_frange {f : α →₀ β} : (0:β) ∉ f.frange :=
λ H, (mem_frange.1 H).1 rfl

theorem frange_single {x : α} {y : β} : frange (single x y) ⊆ {y} :=
λ r hr, let ⟨t, ht1, ht2⟩ := mem_frange.1 hr in ht2 ▸
(by rw single_apply at ht2 ⊢; split_ifs at ht2 ⊢; [exact finset.mem_singleton_self _, cc])

end frange

section subtype_domain

variables {α' : Type*} [has_zero δ] {p : α → Prop}

section zero
variables [has_zero β] {v v' : α' →₀ β}

/-- `subtype_domain p f` is the restriction of the finitely supported function
  `f` to the subtype `p`. -/
def subtype_domain (p : α → Prop) (f : α →₀ β) : (subtype p →₀ β) :=
⟨f.support.subtype p, f ∘ subtype.val, λ a, by simp only [mem_subtype, mem_support_iff]⟩

@[simp] lemma support_subtype_domain {f : α →₀ β} :
  (subtype_domain p f).support = f.support.subtype p :=
rfl

@[simp] lemma subtype_domain_apply {a : subtype p} {v : α →₀ β} :
  (subtype_domain p v) a = v (a.val) :=
rfl

@[simp] lemma subtype_domain_zero : subtype_domain p (0 : α →₀ β) = 0 :=
rfl

@[to_additive]
lemma prod_subtype_domain_index [comm_monoid γ] {v : α →₀ β}
  {h : α → β → γ} (hp : ∀x∈v.support, p x) :
  (v.subtype_domain p).prod (λa b, h a.1 b) = v.prod h :=
prod_bij (λp _, p.val)
  (λ _, mem_subtype.1)
  (λ _ _, rfl)
  (λ _ _ _ _, subtype.eq)
  (λ b hb, ⟨⟨b, hp b hb⟩, mem_subtype.2 hb, rfl⟩)

end zero

section monoid
variables [add_monoid β] {v v' : α' →₀ β}

@[simp] lemma subtype_domain_add {v v' : α →₀ β} :
  (v + v').subtype_domain p = v.subtype_domain p + v'.subtype_domain p :=
ext $ λ _, rfl

instance subtype_domain.is_add_monoid_hom :
  is_add_monoid_hom (subtype_domain p : (α →₀ β) → subtype p →₀ β) :=
{ map_add := λ _ _, subtype_domain_add, map_zero := subtype_domain_zero }

@[simp] lemma filter_add {v v' : α →₀ β} :
  (v + v').filter p = v.filter p + v'.filter p :=
ext $ λ a, by by_cases p a; simp [h]

instance filter.is_add_monoid_hom (p : α → Prop) :
  is_add_monoid_hom (filter p : (α →₀ β) → (α →₀ β)) :=
{ map_zero := filter_zero p, map_add := λ x y, filter_add }

end monoid

section comm_monoid
variables [add_comm_monoid β]

lemma subtype_domain_sum {s : finset γ} {h : γ → α →₀ β} :
  (s.sum h).subtype_domain p = s.sum (λc, (h c).subtype_domain p) :=
eq.symm (s.sum_hom _)

lemma subtype_domain_finsupp_sum {s : γ →₀ δ} {h : γ → δ → α →₀ β} :
  (s.sum h).subtype_domain p = s.sum (λc d, (h c d).subtype_domain p) :=
subtype_domain_sum

lemma filter_sum (s : finset γ) (f : γ → α →₀ β) :
  (s.sum f).filter p = s.sum (λa, filter p (f a)) :=
(s.sum_hom (filter p)).symm

end comm_monoid

section group
variables [add_group β] {v v' : α' →₀ β}

@[simp] lemma subtype_domain_neg {v : α →₀ β} :
  (- v).subtype_domain p = - v.subtype_domain p :=
ext $ λ _, rfl

@[simp] lemma subtype_domain_sub {v v' : α →₀ β} :
  (v - v').subtype_domain p = v.subtype_domain p - v'.subtype_domain p :=
ext $ λ _, rfl

end group

end subtype_domain

section multiset

def to_multiset (f : α →₀ ℕ) : multiset α :=
f.sum (λa n, add_monoid.smul n {a})

lemma to_multiset_zero : (0 : α →₀ ℕ).to_multiset = 0 :=
rfl

lemma to_multiset_add (m n : α →₀ ℕ) :
  (m + n).to_multiset = m.to_multiset + n.to_multiset :=
sum_add_index (assume a, add_monoid.zero_smul _) (assume a b₁ b₂, add_monoid.add_smul _ _ _)

lemma to_multiset_single (a : α) (n : ℕ) : to_multiset (single a n) = add_monoid.smul n {a} :=
by rw [to_multiset, sum_single_index]; apply add_monoid.zero_smul

instance is_add_monoid_hom.to_multiset : is_add_monoid_hom (to_multiset : _ → multiset α) :=
{ map_zero := to_multiset_zero, map_add := to_multiset_add }

lemma card_to_multiset (f : α →₀ ℕ) : f.to_multiset.card = f.sum (λa, id) :=
begin
  refine f.induction _ _,
  { rw [to_multiset_zero, multiset.card_zero, sum_zero_index] },
  { assume a n f _ _ ih,
    rw [to_multiset_add, multiset.card_add, ih, sum_add_index, to_multiset_single,
      sum_single_index, multiset.card_smul, multiset.singleton_eq_singleton,
      multiset.card_singleton, mul_one]; intros; refl }
end

lemma to_multiset_map (f : α →₀ ℕ) (g : α → β) :
  f.to_multiset.map g = (f.map_domain g).to_multiset :=
begin
  refine f.induction _ _,
  { rw [to_multiset_zero, multiset.map_zero, map_domain_zero, to_multiset_zero] },
  { assume a n f _ _ ih,
    rw [to_multiset_add, multiset.map_add, ih, map_domain_add, map_domain_single,
      to_multiset_single, to_multiset_add, to_multiset_single,
      is_add_monoid_hom.map_smul (multiset.map g)],
    refl }
end

lemma prod_to_multiset [comm_monoid α] (f : α →₀ ℕ) :
  f.to_multiset.prod = f.prod (λa n, a ^ n) :=
begin
  refine f.induction _ _,
  { rw [to_multiset_zero, multiset.prod_zero, finsupp.prod_zero_index] },
  { assume a n f _ _ ih,
    rw [to_multiset_add, multiset.prod_add, ih, to_multiset_single, finsupp.prod_add_index,
      finsupp.prod_single_index, multiset.prod_smul, multiset.singleton_eq_singleton,
      multiset.prod_singleton],
    { exact pow_zero a },
    { exact pow_zero },
    { exact pow_add  } }
end

lemma to_finset_to_multiset (f : α →₀ ℕ) : f.to_multiset.to_finset = f.support :=
begin
  refine f.induction _ _,
  { rw [to_multiset_zero, multiset.to_finset_zero, support_zero] },
  { assume a n f ha hn ih,
    rw [to_multiset_add, multiset.to_finset_add, ih, to_multiset_single, support_add_eq,
      support_single_ne_zero hn, multiset.to_finset_smul _ _ hn,
      multiset.singleton_eq_singleton, multiset.to_finset_cons, multiset.to_finset_zero],
    refl,
    refine disjoint_mono support_single_subset (subset.refl _) _,
    rwa [finset.singleton_eq_singleton, finset.singleton_disjoint] }
end

@[simp] lemma count_to_multiset (f : α →₀ ℕ) (a : α) :
  f.to_multiset.count a = f a :=
calc f.to_multiset.count a = f.sum (λx n, (add_monoid.smul n {x} : multiset α).count a) :
    (f.support.sum_hom $ multiset.count a).symm
  ... = f.sum (λx n, n * ({x} : multiset α).count a) : by simp only [multiset.count_smul]
  ... = f.sum (λx n, n * (x :: 0 : multiset α).count a) : rfl
  ... = f a * (a :: 0 : multiset α).count a : sum_eq_single _
    (λ a' _ H, by simp only [multiset.count_cons_of_ne (ne.symm H), multiset.count_zero, mul_zero])
    (λ H, by simp only [not_mem_support_iff.1 H, zero_mul])
  ... = f a : by simp only [multiset.count_singleton, mul_one]

def of_multiset (m : multiset α) : α →₀ ℕ :=
on_finset m.to_finset (λa, m.count a) $ λ a H, multiset.mem_to_finset.2 $
by_contradiction (mt multiset.count_eq_zero.2 H)

@[simp] lemma of_multiset_apply (m : multiset α) (a : α) :
  of_multiset m a = m.count a :=
rfl

def equiv_multiset : (α →₀ ℕ) ≃ (multiset α) :=
⟨ to_multiset, of_multiset,
assume f, finsupp.ext $ λ a, by rw [of_multiset_apply, count_to_multiset],
assume m, multiset.ext.2 $ λ a, by rw [count_to_multiset, of_multiset_apply] ⟩

lemma mem_support_multiset_sum [add_comm_monoid β]
  {s : multiset (α →₀ β)} (a : α) :
  a ∈ s.sum.support → ∃f∈s, a ∈ (f : α →₀ β).support :=
multiset.induction_on s false.elim
  begin
    assume f s ih ha,
    by_cases a ∈ f.support,
    { exact ⟨f, multiset.mem_cons_self _ _, h⟩ },
    { simp only [multiset.sum_cons, mem_support_iff, add_apply,
        not_mem_support_iff.1 h, zero_add] at ha,
      rcases ih (mem_support_iff.2 ha) with ⟨f', h₀, h₁⟩,
      exact ⟨f', multiset.mem_cons_of_mem h₀, h₁⟩ }
  end

lemma mem_support_finset_sum [add_comm_monoid β]
  {s : finset γ} {h : γ → α →₀ β} (a : α) (ha : a ∈ (s.sum h).support) : ∃c∈s, a ∈ (h c).support :=
let ⟨f, hf, hfa⟩ := mem_support_multiset_sum a ha in
let ⟨c, hc, eq⟩ := multiset.mem_map.1 hf in
⟨c, hc, eq.symm ▸ hfa⟩

lemma mem_support_single [has_zero β] (a a' : α) (b : β) :
  a ∈ (single a' b).support ↔ a = a' ∧ b ≠ 0 :=
⟨λ H : (a ∈ ite _ _ _), if h : b = 0
  then by rw if_pos h at H; exact H.elim
  else ⟨by rw if_neg h at H; exact mem_singleton.1 H, h⟩,
λ ⟨h1, h2⟩, show a ∈ ite _ _ _, by rw [if_neg h2]; exact mem_singleton.2 h1⟩

end multiset

section curry_uncurry

protected def curry [add_comm_monoid γ]
  (f : (α × β) →₀ γ) : α →₀ (β →₀ γ) :=
f.sum $ λp c, single p.1 (single p.2 c)

lemma sum_curry_index
  [add_comm_monoid γ] [add_comm_monoid δ]
  (f : (α × β) →₀ γ) (g : α → β → γ → δ)
  (hg₀ : ∀ a b, g a b 0 = 0) (hg₁ : ∀a b c₀ c₁, g a b (c₀ + c₁) = g a b c₀ + g a b c₁) :
  f.curry.sum (λa f, f.sum (g a)) = f.sum (λp c, g p.1 p.2 c) :=
begin
  rw [finsupp.curry],
  transitivity,
  { exact sum_sum_index (assume a, sum_zero_index)
      (assume a b₀ b₁, sum_add_index (assume a, hg₀ _ _) (assume c d₀ d₁, hg₁ _ _ _ _)) },
  congr, funext p c,
  transitivity,
  { exact sum_single_index sum_zero_index },
  exact sum_single_index (hg₀ _ _)
end

protected def uncurry [add_comm_monoid γ] (f : α →₀ (β →₀ γ)) : (α × β) →₀ γ :=
f.sum $ λa g, g.sum $ λb c, single (a, b) c

def finsupp_prod_equiv [add_comm_monoid γ] : ((α × β) →₀ γ) ≃ (α →₀ (β →₀ γ)) :=
by refine ⟨finsupp.curry, finsupp.uncurry, λ f, _, λ f, _⟩; simp only [
  finsupp.curry, finsupp.uncurry, sum_sum_index, sum_zero_index, sum_add_index,
  sum_single_index, single_zero, single_add, eq_self_iff_true, forall_true_iff,
  forall_3_true_iff, prod.mk.eta, (single_sum _ _ _).symm, sum_single]

lemma filter_curry [add_comm_monoid β] (f : α₁ × α₂ →₀ β) (p : α₁ → Prop) :
  (f.filter (λa:α₁×α₂, p a.1)).curry = f.curry.filter p :=
begin
  rw [finsupp.curry, finsupp.curry, finsupp.sum, finsupp.sum,
    @filter_sum _ (α₂ →₀ β) _ p _ f.support _],
  rw [support_filter, sum_filter],
  refine finset.sum_congr rfl _,
  rintros ⟨a₁, a₂⟩ ha,
  dsimp only,
  split_ifs,
  { rw [filter_apply_pos, filter_single_of_pos]; exact h },
  { rwa [filter_single_of_neg] }
end

lemma support_curry [add_comm_monoid β] (f : α₁ × α₂ →₀ β) :
  f.curry.support ⊆ f.support.image prod.fst :=
begin
  rw ← finset.bind_singleton,
  refine finset.subset.trans support_sum _,
  refine finset.bind_mono (assume a _, support_single_subset)
end

end curry_uncurry

section
variables [add_monoid α] [semiring β]

-- TODO: the simplifier unfolds 0 in the instance proof!
private lemma zero_mul (f : α →₀ β) : 0 * f = 0 := by simp only [mul_def, sum_zero_index]
private lemma mul_zero (f : α →₀ β) : f * 0 = 0 := by simp only [mul_def, sum_zero_index, sum_zero]
private lemma left_distrib (a b c : α →₀ β) : a * (b + c) = a * b + a * c :=
by simp only [mul_def, sum_add_index, mul_add, _root_.mul_zero, single_zero, single_add,
  eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_add]
private lemma right_distrib (a b c : α →₀ β) : (a + b) * c = a * c + b * c :=
by simp only [mul_def, sum_add_index, add_mul, _root_.mul_zero, _root_.zero_mul, single_zero, single_add,
  eq_self_iff_true, forall_true_iff, forall_3_true_iff, sum_zero, sum_add]

instance : semiring (α →₀ β) :=
{ one       := 1,
  mul       := (*),
  one_mul   := assume f, by simp only [mul_def, one_def, sum_single_index, _root_.zero_mul, single_zero, sum_zero,
    zero_add, one_mul, sum_single],
  mul_one   := assume f, by simp only [mul_def, one_def, sum_single_index, _root_.mul_zero, single_zero, sum_zero,
    add_zero, mul_one, sum_single],
  zero_mul  := zero_mul,
  mul_zero  := mul_zero,
  mul_assoc := assume f g h, by simp only [mul_def, sum_sum_index, sum_zero_index, sum_add_index, sum_single_index,
    single_zero, single_add, eq_self_iff_true, forall_true_iff, forall_3_true_iff,
    add_mul, mul_add, add_assoc, mul_assoc, _root_.zero_mul, _root_.mul_zero, sum_zero, sum_add],
  left_distrib  := left_distrib,
  right_distrib := right_distrib,
  .. finsupp.add_comm_monoid }

end

instance [add_comm_monoid α] [comm_semiring β] : comm_semiring (α →₀ β) :=
{ mul_comm := assume f g,
  begin
    simp only [mul_def, finsupp.sum, mul_comm],
    rw [finset.sum_comm],
    simp only [add_comm]
  end,
  .. finsupp.semiring }

instance [add_monoid α] [ring β] : ring (α →₀ β) :=
{ neg := has_neg.neg,
  add_left_neg := add_left_neg,
  .. finsupp.semiring }

instance [add_comm_monoid α] [comm_ring β] : comm_ring (α →₀ β) :=
{ mul_comm := mul_comm, .. finsupp.ring}

lemma single_mul_single [has_add α] [semiring β] {a₁ a₂ : α} {b₁ b₂ : β}:
  single a₁ b₁ * single a₂ b₂ = single (a₁ + a₂) (b₁ * b₂) :=
(sum_single_index (by simp only [_root_.zero_mul, single_zero, sum_zero])).trans
  (sum_single_index (by rw [_root_.mul_zero, single_zero]))

lemma prod_single [add_comm_monoid α] [comm_semiring β]
  {s : finset ι} {a : ι → α} {b : ι → β} :
  s.prod (λi, single (a i) (b i)) = single (s.sum a) (s.prod b) :=
finset.induction_on s rfl $ λ a s has ih, by rw [prod_insert has, ih,
  single_mul_single, sum_insert has, prod_insert has]

section

instance [semiring γ] [add_comm_monoid β] [semimodule γ β] : has_scalar γ (α →₀ β) := ⟨λa v, v.map_range ((•) a) (smul_zero _)⟩

variables (α β)

@[simp] lemma smul_apply' {R:semiring γ} [add_comm_monoid β] [semimodule γ β] {a : α} {b : γ} {v : α →₀ β} :
  (b • v) a = b • (v a) := rfl

instance [semiring γ] [add_comm_monoid β] [semimodule γ β] : semimodule γ (α →₀ β) :=
{ smul      := (•),
  smul_add  := λ a x y, finsupp.ext $ λ _, smul_add _ _ _,
  add_smul  := λ a x y, finsupp.ext $ λ _, add_smul _ _ _,
  one_smul  := λ x, finsupp.ext $ λ _, one_smul _ _,
  mul_smul  := λ r s x, finsupp.ext $ λ _, mul_smul _ _ _,
  zero_smul := λ x, finsupp.ext $ λ _, zero_smul _ _,
  smul_zero := λ x, finsupp.ext $ λ _, smul_zero _ }

instance [ring γ] [add_comm_group β] [module γ β] : module γ (α →₀ β) :=
{ ..finsupp.semimodule α β }

instance [discrete_field γ] [add_comm_group β] [vector_space γ β] : vector_space γ (α →₀ β) :=
{ ..finsupp.module α β }

variables {α β}
lemma support_smul {R:semiring γ} [add_comm_monoid β] [semimodule γ β] {b : γ} {g : α →₀ β} :
  (b • g).support ⊆ g.support :=
λ a, by simp; exact mt (λ h, h.symm ▸ smul_zero _)

section
variables {α' : Type*} [has_zero δ] {p : α → Prop}

@[simp] lemma filter_smul {R : semiring γ} [add_comm_monoid β] [semimodule γ β]
  {b : γ} {v : α →₀ β} : (b • v).filter p = b • v.filter p :=
ext $ λ a, by by_cases p a; simp [h]
end

lemma map_domain_smul {α'} {R : semiring γ} [add_comm_monoid β] [semimodule γ β]
   {f : α → α'} (b : γ) (v : α →₀ β) : map_domain f (b • v) = b • map_domain f v :=
begin
  change map_domain f (map_range _ _ _) = map_range _ _ _,
  apply finsupp.induction v, {simp},
  intros a b v' hv₁ hv₂ IH,
  rw [map_range_add, map_domain_add, IH, map_domain_add, map_range_add,
    map_range_single, map_domain_single, map_domain_single, map_range_single];
  apply smul_add
end

@[simp] lemma smul_single {R : semiring γ} [add_comm_monoid β] [semimodule γ β]
  (c : γ) (a : α) (b : β) : c • finsupp.single a b = finsupp.single a (c • b) :=
ext $ λ a', by by_cases a = a'; [{subst h, simp}, simp [h]]

end

@[simp] lemma smul_apply [ring β] {a : α} {b : β} {v : α →₀ β} :
  (b • v) a = b • (v a) := rfl

lemma sum_smul_index [ring β] [add_comm_monoid γ] {g : α →₀ β} {b : β} {h : α → β → γ}
  (h0 : ∀i, h i 0 = 0) : (b • g).sum h = g.sum (λi a, h i (b * a)) :=
finsupp.sum_map_range_index h0

section
variables [semiring β] [semiring γ]

lemma sum_mul (b : γ) (s : α →₀ β) {f : α → β → γ} :
  (s.sum f) * b = s.sum (λ a c, (f a (s a)) * b) :=
by simp only [finsupp.sum, finset.sum_mul]

lemma mul_sum (b : γ) (s : α →₀ β) {f : α → β → γ} :
  b * (s.sum f) = s.sum (λ a c, b * (f a (s a))) :=
by simp only [finsupp.sum, finset.mul_sum]

protected lemma eq_zero_of_zero_eq_one
  (zero_eq_one : (0 : β) = 1) (l : α →₀ β) : l = 0 :=
  by ext i; simp [eq_zero_of_zero_eq_one β zero_eq_one (l i)]

end

def restrict_support_equiv [add_comm_monoid β] (s : set α) :
  {f : α →₀ β // ↑f.support ⊆ s } ≃ (s →₀ β):=
begin
  refine ⟨λf, subtype_domain (λx, x ∈ s) f.1, λ f, ⟨f.map_domain subtype.val, _⟩, _, _⟩,
  { refine set.subset.trans (finset.coe_subset.2 map_domain_support) _,
    rw [finset.coe_image, set.image_subset_iff],
    exact assume x hx, x.2 },
  { rintros ⟨f, hf⟩,
    apply subtype.eq,
    ext a,
    dsimp only,
    refine classical.by_cases (assume h : a ∈ set.range (subtype.val : s → α), _) (assume h, _),
    { rcases h with ⟨x, rfl⟩,
      rw [map_domain_apply subtype.val_injective, subtype_domain_apply] },
    { convert map_domain_notin_range _ _ h,
      rw [← not_mem_support_iff],
      refine mt _ h,
      exact assume ha, ⟨⟨a, hf ha⟩, rfl⟩ } },
  { assume f,
    ext ⟨a, ha⟩,
    dsimp only,
    rw [subtype_domain_apply, map_domain_apply subtype.val_injective] }
end

protected def dom_congr [add_comm_monoid β] (e : α₁ ≃ α₂) : (α₁ →₀ β) ≃ (α₂ →₀ β) :=
⟨map_domain e, map_domain e.symm,
  begin
    assume v,
    simp only [map_domain_comp.symm, (∘), equiv.symm_apply_apply],
    exact map_domain_id
  end,
  begin
    assume v,
    simp only [map_domain_comp.symm, (∘), equiv.apply_symm_apply],
    exact map_domain_id
  end⟩

section sigma

variables {αs : ι → Type*} [has_zero β] (l : (Σ i, αs i) →₀ β)

noncomputable def split (i : ι) : αs i →₀ β :=
l.comap_domain (sigma.mk i) (λ x1 x2 _ _ hx, heq_iff_eq.1 (sigma.mk.inj hx).2)

lemma split_apply (i : ι) (x : αs i) : split l i x = l ⟨i, x⟩ :=
begin
 dunfold split,
 rw comap_domain_apply
end

def split_support : finset ι := l.support.image sigma.fst

lemma mem_split_support_iff_nonzero (i : ι) :
  i ∈ split_support l ↔ split l i ≠ 0 :=
begin
  classical,
  rw [split_support, mem_image, ne.def, ← support_eq_empty, ← ne.def,
    ← finset.nonempty_iff_ne_empty, split, comap_domain, finset.nonempty],
  simp
end

noncomputable def split_comp [has_zero γ] (g : Π i, (αs i →₀ β) → γ)
  (hg : ∀ i x, x = 0 ↔ g i x = 0) : ι →₀ γ :=
{ support := split_support l,
  to_fun := λ i, g i (split l i),
  mem_support_to_fun :=
  begin
    intros i,
    rw mem_split_support_iff_nonzero,
    haveI := classical.dec,
    rwa not_iff_not,
    exact hg _ _,
  end }

lemma sigma_support : l.support = l.split_support.sigma (λ i, (l.split i).support) :=
by simp [finset.ext, split_support, split, comap_domain]; tauto

lemma sigma_sum [add_comm_monoid γ] (f : (Σ (i : ι), αs i) → β → γ) :
  l.sum f = (split_support l).sum (λ (i : ι), (split l i).sum (λ (a : αs i) b, f ⟨i, a⟩ b)) :=
by simp [sum, sigma_support, sum_sigma,split_apply]

end sigma

end finsupp

namespace multiset

def to_finsupp (s : multiset α) : α →₀ ℕ :=
{ support := s.to_finset,
  to_fun := λ a, s.count a,
  mem_support_to_fun := λ a,
  begin
    rw mem_to_finset,
    convert not_iff_not_of_iff (count_eq_zero.symm),
    rw not_not
  end }

@[simp] lemma to_finsupp_support (s : multiset α) :
  s.to_finsupp.support = s.to_finset := rfl

@[simp] lemma to_finsupp_apply (s : multiset α) (a : α) :
  s.to_finsupp a = s.count a := rfl

@[simp] lemma to_finsupp_zero :
  to_finsupp (0 : multiset α) = 0 :=
finsupp.ext $ λ a, count_zero a

@[simp] lemma to_finsupp_add (s t : multiset α) :
  to_finsupp (s + t) = to_finsupp s + to_finsupp t :=
finsupp.ext $ λ a, count_add a s t

lemma to_finsupp_singleton (a : α) :
  to_finsupp {a} = finsupp.single a 1 :=
finsupp.ext $ λ b,
if h : a = b then by simp [finsupp.single_apply, h] else
begin
  rw [to_finsupp_apply, finsupp.single_apply, if_neg h, count_eq_zero,
      singleton_eq_singleton, mem_singleton],
  rintro rfl, exact h rfl
end

namespace to_finsupp

instance : is_add_monoid_hom (to_finsupp : multiset α → α →₀ ℕ) :=
{ map_zero := to_finsupp_zero,
  map_add  := to_finsupp_add }

end to_finsupp

@[simp] lemma to_finsupp_to_multiset (s : multiset α) :
  s.to_finsupp.to_multiset = s :=
ext.2 $ λ a, by rw [finsupp.count_to_multiset, to_finsupp_apply]

end multiset

namespace finsupp
variables {σ : Type*}

instance [preorder α] [has_zero α] : preorder (σ →₀ α) :=
{ 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 α] [has_zero α] : partial_order (σ →₀ α) :=
{ le_antisymm := λ f g hfg hgf, finsupp.ext $ λ s, le_antisymm (hfg s) (hgf s),
  .. finsupp.preorder }

instance [ordered_cancel_comm_monoid α] :
  add_left_cancel_semigroup (σ →₀ α) :=
{ add_left_cancel := λ a b c h, finsupp.ext $ λ s,
  by { rw finsupp.ext_iff at h, exact add_left_cancel (h s) },
  .. finsupp.add_monoid }

instance [ordered_cancel_comm_monoid α] :
  add_right_cancel_semigroup (σ →₀ α) :=
{ add_right_cancel := λ a b c h, finsupp.ext $ λ s,
  by { rw finsupp.ext_iff at h, exact add_right_cancel (h s) },
  .. finsupp.add_monoid }

instance [ordered_cancel_comm_monoid α] :
  ordered_cancel_comm_monoid (σ →₀ α) :=
{ 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),
  .. finsupp.add_comm_monoid, .. finsupp.partial_order,
  .. finsupp.add_left_cancel_semigroup, .. finsupp.add_right_cancel_semigroup }

lemma le_iff [canonically_ordered_monoid α] (f g : σ →₀ α) :
  f ≤ g ↔ ∀ s ∈ f.support, f s ≤ g s :=
⟨λ h s hs, h s,
λ h s, if H : s ∈ f.support then h s H else (not_mem_support_iff.1 H).symm ▸ zero_le (g s)⟩

@[simp] lemma add_eq_zero_iff [canonically_ordered_monoid α] (f g : σ →₀ α) :
  f + g = 0 ↔ f = 0 ∧ g = 0 :=
begin
  split,
  { assume h,
    split,
    all_goals
    { ext s,
      suffices H : f s + g s = 0,
      { rw add_eq_zero_iff at H, cases H, assumption },
      show (f + g) s = 0,
      rw h, refl } },
  { rintro ⟨rfl, rfl⟩, simp }
end

attribute [simp] to_multiset_zero to_multiset_add

@[simp] lemma to_multiset_to_finsupp (f : σ →₀ ℕ) :
  f.to_multiset.to_finsupp = f :=
ext $ λ s, by rw [multiset.to_finsupp_apply, count_to_multiset]

lemma to_multiset_strict_mono : strict_mono (@to_multiset σ) :=
λ m n h,
begin
  rw lt_iff_le_and_ne at h ⊢, cases h with h₁ h₂,
  split,
  { rw multiset.le_iff_count, intro s, erw [count_to_multiset m s, count_to_multiset], exact h₁ s },
  { intro H, apply h₂, replace H := congr_arg multiset.to_finsupp H, simpa using H }
end

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

instance decidable_le : decidable_rel (@has_le.le (σ →₀ ℕ) _) :=
λ m n, by rw le_iff; apply_instance

variable {σ}

def antidiagonal (f : σ →₀ ℕ) : ((σ →₀ ℕ) × (σ →₀ ℕ)) →₀ ℕ :=
(f.to_multiset.antidiagonal.map (prod.map multiset.to_finsupp multiset.to_finsupp)).to_finsupp

lemma mem_antidiagonal_support {f : σ →₀ ℕ} {p : (σ →₀ ℕ) × (σ →₀ ℕ)} :
  p ∈ (antidiagonal f).support ↔ p.1 + p.2 = f :=
begin
  erw [multiset.mem_to_finset, multiset.mem_map],
  split,
  { rintros ⟨⟨a, b⟩, h, rfl⟩,
    rw multiset.mem_antidiagonal at h,
    simpa using congr_arg multiset.to_finsupp h },
  { intro h,
    refine ⟨⟨p.1.to_multiset, p.2.to_multiset⟩, _, _⟩,
    { simpa using congr_arg to_multiset h },
    { rw [prod.map, to_multiset_to_finsupp, to_multiset_to_finsupp, prod.mk.eta] } }
end

@[simp] lemma antidiagonal_zero : antidiagonal (0 : σ →₀ ℕ) = single (0,0) 1 :=
by rw [← multiset.to_finsupp_singleton]; refl

lemma swap_mem_antidiagonal_support {n : σ →₀ ℕ} {f} (hf : f ∈ (antidiagonal n).support) :
  f.swap ∈ (antidiagonal n).support :=
by simpa [mem_antidiagonal_support, add_comm] using hf

end finsupp