refactor(data/finsupp/antidiagonal): Make antidiagonal a finset (#7595)

Pursuant to discussion [here](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/antidiagonals.20having.20multiplicity) 

Refactoring so that `finsupp.antidiagonal` and `multiset.antidiagonal` are finsets.

~~Still TO DO: `multiset.antidiagonal`~~

src/data/finsupp/antidiagonal.lean

@@ -24,23 +24,28 @@ variables {α : Type*}
 /-- The `finsupp` counterpart of `multiset.antidiagonal`: the antidiagonal of
 `s : α →₀ ℕ` consists of all pairs `(t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ)` such that `t₁ + t₂ = s`.
 The finitely supported function `antidiagonal s` is equal to the multiplicities of these pairs. -/
-def antidiagonal (f : α →₀ ℕ) : ((α →₀ ℕ) × (α →₀ ℕ)) →₀ ℕ :=
+def antidiagonal' (f : α →₀ ℕ) : ((α →₀ ℕ) × (α →₀ ℕ)) →₀ ℕ :=
 (f.to_multiset.antidiagonal.map (prod.map multiset.to_finsupp multiset.to_finsupp)).to_finsupp
 
-@[simp] lemma mem_antidiagonal_support {f : α →₀ ℕ} {p : (α →₀ ℕ) × (α →₀ ℕ)} :
-  p ∈ (antidiagonal f).support ↔ p.1 + p.2 = f :=
+/-- The antidiagonal of `s : α →₀ ℕ` is the finset of all pairs `(t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ)`
+such that `t₁ + t₂ = s`. -/
+def antidiagonal (f : α →₀ ℕ) : finset ((α →₀ ℕ) × (α →₀ ℕ)) :=
+f.antidiagonal'.support
+
+@[simp] lemma mem_antidiagonal {f : α →₀ ℕ} {p : (α →₀ ℕ) × (α →₀ ℕ)} :
+  p ∈ antidiagonal f ↔ p.1 + p.2 = f :=
 begin
   rcases p with ⟨p₁, p₂⟩,
-  simp [antidiagonal, ← and.assoc, ← finsupp.to_multiset.apply_eq_iff_eq]
+  simp [antidiagonal, antidiagonal', ← and.assoc, ← finsupp.to_multiset.apply_eq_iff_eq]
 end
 
-lemma swap_mem_antidiagonal_support {n : α →₀ ℕ} {f : (α →₀ ℕ) × (α →₀ ℕ)} :
-  f.swap ∈ (antidiagonal n).support ↔ f ∈ (antidiagonal n).support :=
-by simp only [mem_antidiagonal_support, add_comm, prod.swap]
+lemma swap_mem_antidiagonal {n : α →₀ ℕ} {f : (α →₀ ℕ) × (α →₀ ℕ)} :
+  f.swap ∈ antidiagonal n ↔ f ∈ antidiagonal n :=
+by simp only [mem_antidiagonal, add_comm, prod.swap]
 
-lemma antidiagonal_support_filter_fst_eq (f g : α →₀ ℕ)
+lemma antidiagonal_filter_fst_eq (f g : α →₀ ℕ)
   [D : Π (p : (α →₀ ℕ) × (α →₀ ℕ)), decidable (p.1 = g)] :
-  (antidiagonal f).support.filter (λ p, p.1 = g) = if g ≤ f then {(g, f - g)} else ∅ :=
+  (antidiagonal f).filter (λ p, p.1 = g) = if g ≤ f then {(g, f - g)} else ∅ :=
 begin
   ext ⟨a, b⟩,
   suffices : a = g → (a + b = f ↔ g ≤ f ∧ b = f - g),
@@ -50,9 +55,9 @@ begin
   { rintro ⟨h, rfl⟩, exact nat_add_sub_of_le h }
 end
 
-lemma antidiagonal_support_filter_snd_eq (f g : α →₀ ℕ)
+lemma antidiagonal_filter_snd_eq (f g : α →₀ ℕ)
   [D : Π (p : (α →₀ ℕ) × (α →₀ ℕ)), decidable (p.2 = g)] :
-  (antidiagonal f).support.filter (λ p, p.2 = g) = if g ≤ f then {(f - g, g)} else ∅ :=
+  (antidiagonal f).filter (λ p, p.2 = g) = if g ≤ f then {(f - g, g)} else ∅ :=
 begin
   ext ⟨a, b⟩,
   suffices : b = g → (a + b = f ↔ g ≤ f ∧ a = f - g),
@@ -62,20 +67,20 @@ begin
   { rintro ⟨h, rfl⟩, exact nat_sub_add_cancel h }
 end
 
-@[simp] lemma antidiagonal_zero : antidiagonal (0 : α →₀ ℕ) = single (0,0) 1 :=
-by rw [← multiset.to_finsupp_singleton]; refl
+@[simp] lemma antidiagonal_zero : antidiagonal (0 : α →₀ ℕ) = singleton (0,0) :=
+by rw [antidiagonal, antidiagonal', multiset.to_finsupp_support]; refl
 
 @[to_additive]
-lemma prod_antidiagonal_support_swap {M : Type*} [comm_monoid M] (n : α →₀ ℕ)
+lemma prod_antidiagonal_swap {M : Type*} [comm_monoid M] (n : α →₀ ℕ)
   (f : (α →₀ ℕ) → (α →₀ ℕ) → M) :
-  ∏ p in (antidiagonal n).support, f p.1 p.2 = ∏ p in (antidiagonal n).support, f p.2 p.1 :=
-finset.prod_bij (λ p hp, p.swap) (λ p, swap_mem_antidiagonal_support.2) (λ p hp, rfl)
+  ∏ p in antidiagonal n, f p.1 p.2 = ∏ p in antidiagonal n, f p.2 p.1 :=
+finset.prod_bij (λ p hp, p.swap) (λ p, swap_mem_antidiagonal.2) (λ p hp, rfl)
   (λ p₁ p₂ _ _ h, prod.swap_injective h)
-  (λ p hp, ⟨p.swap, swap_mem_antidiagonal_support.2 hp, p.swap_swap.symm⟩)
+  (λ p hp, ⟨p.swap, swap_mem_antidiagonal.2 hp, p.swap_swap.symm⟩)
 
 /-- The set `{m : α →₀ ℕ | m ≤ n}` as a `finset`. -/
 def Iic_finset (n : α →₀ ℕ) : finset (α →₀ ℕ) :=
-(antidiagonal n).support.image prod.fst
+(antidiagonal n).image prod.fst
 
 @[simp] lemma mem_Iic_finset {m n : α →₀ ℕ} : m ∈ Iic_finset n ↔ m ≤ n :=
 by simp [Iic_finset, le_iff_exists_add, eq_comm]

src/data/mv_polynomial/basic.lean

@@ -405,7 +405,7 @@ begin
 end
 
 lemma coeff_mul (p q : mv_polynomial σ R) (n : σ →₀ ℕ) :
-  coeff n (p * q) = ∑ x in (antidiagonal n).support, coeff x.1 p * coeff x.2 q :=
+  coeff n (p * q) = ∑ x in antidiagonal n, coeff x.1 p * coeff x.2 q :=
 begin
   rw mul_def,
   -- We need to manipulate both sides into a shape to which we can apply `finset.sum_bij_ne_zero`,
@@ -420,7 +420,7 @@ begin
   -- We are now ready to show that both sums are equal using `finset.sum_bij_ne_zero`.
   apply finset.sum_bij_ne_zero (λ (x : (σ →₀ ℕ) × (σ →₀ ℕ)) _ _, (x.1, x.2)),
   { intros x hx hx',
-    simp only [mem_antidiagonal_support, eq_self_iff_true, if_false, forall_true_iff],
+    simp only [mem_antidiagonal, eq_self_iff_true, if_false, forall_true_iff],
     contrapose! hx',
     rw [if_neg hx'] },
   { rintros ⟨i, j⟩ ⟨k, l⟩ hij hij' hkl hkl',
@@ -430,7 +430,7 @@ begin
     { simp only [mem_support_iff, finset.mem_product],
       contrapose! hij',
       exact mul_eq_zero_of_ne_zero_imp_eq_zero hij' },
-    { rw [mem_antidiagonal_support] at hij,
+    { rw [mem_antidiagonal] at hij,
       simp only [exists_prop, true_and, ne.def, if_pos hij, hij', not_false_iff] } },
   { intros x hx hx',
     simp only [ne.def] at hx' ⊢,
@@ -442,11 +442,11 @@ end
 @[simp] lemma coeff_mul_X (m) (s : σ) (p : mv_polynomial σ R) :
   coeff (m + single s 1) (p * X s) = coeff m p :=
 begin
-  have : (m, single s 1) ∈ (m + single s 1).antidiagonal.support := mem_antidiagonal_support.2 rfl,
+  have : (m, single s 1) ∈ (m + single s 1).antidiagonal := mem_antidiagonal.2 rfl,
   rw [coeff_mul, ← finset.insert_erase this, finset.sum_insert (finset.not_mem_erase _ _),
       finset.sum_eq_zero, add_zero, coeff_X, mul_one],
   rintros ⟨i,j⟩ hij,
-  rw [finset.mem_erase, mem_antidiagonal_support] at hij,
+  rw [finset.mem_erase, mem_antidiagonal] at hij,
   by_cases H : single s 1 = j,
   { subst j, simpa using hij },
   { rw [coeff_X', if_neg H, mul_zero] },

src/data/mv_polynomial/variables.lean

@@ -295,7 +295,7 @@ begin
   contrapose! hd, cases hd,
   rw finset.sum_eq_zero,
   rintro ⟨d₁, d₂⟩ H,
-  rw finsupp.mem_antidiagonal_support at H,
+  rw finsupp.mem_antidiagonal at H,
   subst H,
   obtain H|H : i ∈ d₁.support ∨ i ∈ d₂.support,
   { simpa only [finset.mem_union] using finsupp.support_add hi, },

src/ring_theory/polynomial/homogeneous.lean

@@ -95,7 +95,7 @@ begin
     by_cases h : coeff d φ = 0;
     simp only [*, ne.def, not_false_iff, zero_mul, mul_zero] at * },
   specialize hφ aux.1, specialize hψ aux.2,
-  rw finsupp.mem_antidiagonal_support at hde,
+  rw finsupp.mem_antidiagonal at hde,
   classical,
   have hd' : d.support ⊆ d.support ∪ e.support := finset.subset_union_left _ _,
   have he' : e.support ⊆ d.support ∪ e.support := finset.subset_union_right _ _,

src/ring_theory/power_series/basic.lean

@@ -151,10 +151,10 @@ coeff_monomial_same 0 1
 lemma monomial_zero_one : monomial R (0 : σ →₀ ℕ) 1 = 1 := rfl
 
 instance : has_mul (mv_power_series σ R) :=
-⟨λ φ ψ n, ∑ p in (finsupp.antidiagonal n).support, coeff R p.1 φ * coeff R p.2 ψ⟩
+⟨λ φ ψ n, ∑ p in finsupp.antidiagonal n, coeff R p.1 φ * coeff R p.2 ψ⟩
 
 lemma coeff_mul : coeff R n (φ * ψ) =
-  ∑ p in (finsupp.antidiagonal n).support, coeff R p.1 φ * coeff R p.2 ψ := rfl
+  ∑ p in finsupp.antidiagonal n, coeff R p.1 φ * coeff R p.2 ψ := rfl
 
 protected lemma zero_mul : (0 : mv_power_series σ R) * φ = 0 :=
 ext $ λ n, by simp [coeff_mul]
@@ -165,21 +165,21 @@ ext $ λ n, by simp [coeff_mul]
 lemma coeff_monomial_mul (a : R) :
   coeff R m (monomial R n a * φ) = if n ≤ m then a * coeff R (m - n) φ else 0 :=
 begin
-  have : ∀ p ∈ (antidiagonal m).support,
+  have : ∀ p ∈ antidiagonal m,
     coeff R (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 (monomial R n a) * coeff R p.2 φ ≠ 0 → p.1 = n :=
     λ p _ hp, eq_of_coeff_monomial_ne_zero (left_ne_zero_of_mul hp),
-  rw [coeff_mul, ← finset.sum_filter_of_ne this, antidiagonal_support_filter_fst_eq,
+  rw [coeff_mul, ← finset.sum_filter_of_ne this, antidiagonal_filter_fst_eq,
     finset.sum_ite_index],
   simp only [finset.sum_singleton, coeff_monomial_same, finset.sum_empty]
 end
 
 lemma coeff_mul_monomial (a : R) :
   coeff R m (φ * monomial R n a) = if n ≤ m then coeff R (m - n) φ * a else 0 :=
 begin
-  have : ∀ p ∈ (antidiagonal m).support,
+  have : ∀ p ∈ antidiagonal m,
     coeff R (p : (σ →₀ ℕ) × (σ →₀ ℕ)).1 φ * coeff R p.2 (monomial R n a) ≠ 0 → p.2 = n :=
     λ p _ hp, eq_of_coeff_monomial_ne_zero (right_ne_zero_of_mul hp),
-  rw [coeff_mul, ← finset.sum_filter_of_ne this, antidiagonal_support_filter_snd_eq,
+  rw [coeff_mul, ← finset.sum_filter_of_ne this, antidiagonal_filter_snd_eq,
     finset.sum_ite_index],
   simp only [finset.sum_singleton, coeff_monomial_same, finset.sum_empty]
 end
@@ -218,7 +218,7 @@ begin
   ext1 n,
   simp only [coeff_mul, finset.sum_mul, finset.mul_sum, finset.sum_sigma'],
   refine finset.sum_bij (λ p _, ⟨(p.2.1, p.2.2 + p.1.2), (p.2.2, p.1.2)⟩) _ _ _ _;
-    simp only [mem_antidiagonal_support, finset.mem_sigma, heq_iff_eq, prod.mk.inj_iff, and_imp,
+    simp only [mem_antidiagonal, finset.mem_sigma, heq_iff_eq, prod.mk.inj_iff, and_imp,
       exists_prop],
   { rintros ⟨⟨i,j⟩, ⟨k,l⟩⟩, dsimp only, rintro rfl rfl,
     simp [add_assoc] },
@@ -246,7 +246,7 @@ end semiring
 
 instance [comm_semiring R] : comm_semiring (mv_power_series σ R) :=
 { mul_comm := λ φ ψ, ext $ λ n, by simpa only [coeff_mul, mul_comm]
-    using sum_antidiagonal_support_swap n (λ a b, coeff R a φ * coeff R b ψ),
+    using sum_antidiagonal_swap n (λ a b, coeff R a φ * coeff R b ψ),
   .. mv_power_series.semiring }
 
 instance [ring R] : ring (mv_power_series σ R) :=
@@ -527,21 +527,21 @@ begin
   { rintros ⟨φ, rfl⟩ m h,
     rw [coeff_mul, finset.sum_eq_zero],
     rintros ⟨i,j⟩ hij, rw [coeff_X_pow, if_neg, zero_mul],
-    contrapose! h, subst i, rw finsupp.mem_antidiagonal_support at hij,
+    contrapose! h, subst i, rw finsupp.mem_antidiagonal at hij,
     rw [← hij, finsupp.add_apply, finsupp.single_eq_same], exact nat.le_add_right n _ },
   { intro h, refine ⟨λ m, coeff R (m + (single s n)) φ, _⟩,
     ext m, by_cases H : m - single s n + single s n = m,
     { rw [coeff_mul, finset.sum_eq_single (single s n, m - single s n)],
       { rw [coeff_X_pow, if_pos rfl, one_mul],
         simpa using congr_arg (λ (m : σ →₀ ℕ), coeff R m φ) H.symm },
-      { rintros ⟨i,j⟩ hij hne, rw finsupp.mem_antidiagonal_support at hij,
+      { rintros ⟨i,j⟩ hij hne, rw finsupp.mem_antidiagonal at hij,
         rw coeff_X_pow, split_ifs with hi,
         { exfalso, apply hne, rw [← hij, ← hi, prod.mk.inj_iff], refine ⟨rfl, _⟩,
           ext t, simp only [nat.add_sub_cancel_left, finsupp.add_apply, finsupp.nat_sub_apply] },
         { exact zero_mul _ } },
-        { intro hni, exfalso, apply hni, rwa [finsupp.mem_antidiagonal_support, add_comm] } },
+        { intro hni, exfalso, apply hni, rwa [finsupp.mem_antidiagonal, add_comm] } },
     { rw [h, coeff_mul, finset.sum_eq_zero],
-      { rintros ⟨i,j⟩ hij, rw finsupp.mem_antidiagonal_support at hij,
+      { rintros ⟨i,j⟩ hij, rw finsupp.mem_antidiagonal at hij,
         rw coeff_X_pow, split_ifs with hi,
         { exfalso, apply H, rw [← hij, hi], ext,
           rw [coe_add, coe_add, pi.add_apply, pi.add_apply, nat_add_sub_cancel_left, add_comm], },
@@ -576,15 +576,15 @@ well-founded recursion on the coeffients of the inverse.
  an inverse of the constant coefficient `inv_of_unit`.-/
 protected noncomputable def inv.aux (a : R) (φ : mv_power_series σ R) : mv_power_series σ R
 | n := if n = 0 then a else
-- a * ∑ x in n.antidiagonal.support,
+- a * ∑ x in n.antidiagonal,
     if h : x.2 < n then coeff R x.1 φ * inv.aux x.2 else 0
 using_well_founded
 { rel_tac := λ _ _, `[exact ⟨_, finsupp.lt_wf σ⟩],
   dec_tac := tactic.assumption }
 
 lemma coeff_inv_aux (n : σ →₀ ℕ) (a : R) (φ : mv_power_series σ R) :
   coeff R n (inv.aux a φ) = if n = 0 then a else
-  - a * ∑ x in n.antidiagonal.support,
+  - a * ∑ x in n.antidiagonal,
     if x.2 < n then coeff R x.1 φ * coeff R x.2 (inv.aux a φ) else 0 :=
 show inv.aux a φ n = _, by { rw inv.aux, refl }
 
@@ -594,7 +594,7 @@ inv.aux (↑u⁻¹) φ
 
 lemma coeff_inv_of_unit (n : σ →₀ ℕ) (φ : mv_power_series σ R) (u : units R) :
   coeff R n (inv_of_unit φ u) = if n = 0 then ↑u⁻¹ else
-  - ↑u⁻¹ * ∑ x in n.antidiagonal.support,
+  - ↑u⁻¹ * ∑ x in n.antidiagonal,
     if x.2 < n then coeff R x.1 φ * coeff R x.2 (inv_of_unit φ u) else 0 :=
 coeff_inv_aux n (↑u⁻¹) φ
 
@@ -607,16 +607,16 @@ lemma mul_inv_of_unit (φ : mv_power_series σ R) (u : units R) (h : constant_co
 ext $ λ n, if H : n = 0 then by { rw H, simp [coeff_mul, support_single_ne_zero, h], }
 else
 begin
-  have : ((0 : σ →₀ ℕ), n) ∈ n.antidiagonal.support,
-  { rw [finsupp.mem_antidiagonal_support, zero_add] },
+  have : ((0 : σ →₀ ℕ), n) ∈ n.antidiagonal,
+  { rw [finsupp.mem_antidiagonal, zero_add] },
   rw [coeff_one, if_neg H, coeff_mul,
     ← finset.insert_erase this, finset.sum_insert (finset.not_mem_erase _ _),
     coeff_zero_eq_constant_coeff_apply, h, coeff_inv_of_unit, if_neg H,
     neg_mul_eq_neg_mul_symm, mul_neg_eq_neg_mul_symm, units.mul_inv_cancel_left,
     ← finset.insert_erase this, finset.sum_insert (finset.not_mem_erase _ _),
     finset.insert_erase this, if_neg (not_lt_of_ge $ le_refl _), zero_add, add_comm,
     ← sub_eq_add_neg, sub_eq_zero, finset.sum_congr rfl],
-  rintros ⟨i,j⟩ hij, rw [finset.mem_erase, finsupp.mem_antidiagonal_support] at hij,
+  rintros ⟨i,j⟩ hij, rw [finset.mem_erase, finsupp.mem_antidiagonal] at hij,
   cases hij with h₁ h₂,
   subst n, rw if_pos,
   suffices : (0 : _) + j < i + j, {simpa},
@@ -681,7 +681,7 @@ instance : has_inv (mv_power_series σ k) := ⟨mv_power_series.inv⟩
 
 lemma coeff_inv (n : σ →₀ ℕ) (φ : mv_power_series σ k) :
   coeff k n (φ⁻¹) = if n = 0 then (constant_coeff σ k φ)⁻¹ else
-  - (constant_coeff σ k φ)⁻¹ * ∑ x in n.antidiagonal.support,
+  - (constant_coeff σ k φ)⁻¹ * ∑ x in n.antidiagonal,
     if x.2 < n then coeff k x.1 φ * coeff k x.2 (φ⁻¹) else 0 :=
 coeff_inv_aux n _ φ
 
@@ -942,13 +942,13 @@ begin
   symmetry,
   apply finset.sum_bij (λ (p : ℕ × ℕ) h, (single () p.1, single () p.2)),
   { rintros ⟨i,j⟩ hij, rw finset.nat.mem_antidiagonal at hij,
-    rw [finsupp.mem_antidiagonal_support, ← finsupp.single_add, hij], },
+    rw [finsupp.mem_antidiagonal, ← finsupp.single_add, hij], },
   { rintros ⟨i,j⟩ hij, refl },
   { rintros ⟨i,j⟩ ⟨k,l⟩ hij hkl,
     simpa only [prod.mk.inj_iff, finsupp.unique_single_eq_iff] using id },
   { rintros ⟨f,g⟩ hfg,
     refine ⟨(f (), g ()), _, _⟩,
-    { rw finsupp.mem_antidiagonal_support at hfg,
+    { rw finsupp.mem_antidiagonal at hfg,
       rw [finset.nat.mem_antidiagonal, ← finsupp.add_apply, hfg, finsupp.single_eq_same] },
     { rw prod.mk.inj_iff, dsimp,
       exact ⟨finsupp.unique_single f, finsupp.unique_single g⟩ } }
@@ -1166,7 +1166,7 @@ begin
   symmetry,
   apply finset.sum_bij (λ (p : ℕ × ℕ) h, (single () p.1, single () p.2)),
   { rintros ⟨i,j⟩ hij, rw finset.nat.mem_antidiagonal at hij,
-    rw [finsupp.mem_antidiagonal_support, ← finsupp.single_add, hij], },
+    rw [finsupp.mem_antidiagonal, ← finsupp.single_add, hij], },
   { rintros ⟨i,j⟩ hij,
     by_cases H : j < n,
     { rw [if_pos H, if_pos], {refl},
@@ -1180,7 +1180,7 @@ begin
     simpa only [prod.mk.inj_iff, finsupp.unique_single_eq_iff] using id },
   { rintros ⟨f,g⟩ hfg,
     refine ⟨(f (), g ()), _, _⟩,
-    { rw finsupp.mem_antidiagonal_support at hfg,
+    { rw finsupp.mem_antidiagonal at hfg,
       rw [finset.nat.mem_antidiagonal, ← finsupp.add_apply, hfg, finsupp.single_eq_same] },
     { rw prod.mk.inj_iff, dsimp,
       exact ⟨finsupp.unique_single f, finsupp.unique_single g⟩ } }