[Merged by Bors] - feat(Data/Finsupp): make toMultiset and antidiagonal computable

Mathlib/Data/DFinsupp/Multiset.lean

@@ -12,8 +12,6 @@ import Mathlib.Data.DFinsupp.Order
 
 This defines `DFinsupp.toMultiset` the equivalence between `Π₀ a : α, ℕ` and `Multiset α`, along
 with `Multiset.toDFinsupp` the reverse equivalence.
-
-Note that this provides a computable alternative to `Finsupp.toMultiset`.
 -/
 
 open Function
@@ -29,7 +27,7 @@ instance addZeroClass' {β} [AddZeroClass β] : AddZeroClass (Π₀ _ : α, β)
 
 variable [DecidableEq α] {s t : Multiset α}
 
-/-- A computable version of `Finsupp.toMultiset`. -/
+/-- A DFinsupp version of `Finsupp.toMultiset`. -/
 def toMultiset : (Π₀ _ : α, ℕ) →+ Multiset α :=
   DFinsupp.sumAddHom fun a : α ↦ Multiset.replicateAddMonoidHom a
 #align dfinsupp.to_multiset DFinsupp.toMultiset
@@ -46,7 +44,7 @@ namespace Multiset
 
 variable [DecidableEq α] {s t : Multiset α}
 
-/-- A computable version of `Multiset.toFinsupp`. -/
+/-- A DFinsupp version of `Multiset.toFinsupp`. -/
 def toDFinsupp : Multiset α →+ Π₀ _ : α, ℕ where
   toFun s :=
     { toFun := fun n ↦ s.count n

Mathlib/Data/Finsupp/Antidiagonal.lean

@@ -17,17 +17,16 @@ all pairs `(t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ)` such that `t₁ +
 -/
 
 
-noncomputable section
 
-open Classical BigOperators
+open BigOperators
 
 namespace Finsupp
 
 open Finset
 
 universe u
 
-variable {α : Type u}
+variable {α : Type u} [DecidableEq α]
 
 /-- The `Finsupp` counterpart of `Multiset.antidiagonal`: the antidiagonal of
 `s : α →₀ ℕ` consists of all pairs `(t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ)` such that `t₁ + t₂ = s`.
@@ -46,7 +45,8 @@ def antidiagonal (f : α →₀ ℕ) : Finset ((α →₀ ℕ) × (α →₀ ℕ
 theorem mem_antidiagonal {f : α →₀ ℕ} {p : (α →₀ ℕ) × (α →₀ ℕ)} :
     p ∈ antidiagonal f ↔ p.1 + p.2 = f := by
   rcases p with ⟨p₁, p₂⟩
-  simp [antidiagonal, antidiagonal', ← and_assoc, ← Finsupp.toMultiset.apply_eq_iff_eq]
+  simp [antidiagonal, antidiagonal', ← and_assoc, Multiset.toFinsupp_eq_iff,
+    ← Multiset.toFinsupp_eq_iff (f := f)]
 #align finsupp.mem_antidiagonal Finsupp.mem_antidiagonal
 
 theorem swap_mem_antidiagonal {n : α →₀ ℕ} {f : (α →₀ ℕ) × (α →₀ ℕ)} :
@@ -85,8 +85,7 @@ theorem antidiagonal_filter_snd_eq (f g : α →₀ ℕ)
 #align finsupp.antidiagonal_filter_snd_eq Finsupp.antidiagonal_filter_snd_eq
 
 @[simp]
-theorem antidiagonal_zero : antidiagonal (0 : α →₀ ℕ) = singleton (0, 0) := by
-  rw [antidiagonal, antidiagonal', Multiset.toFinsupp_support]; rfl
+theorem antidiagonal_zero : antidiagonal (0 : α →₀ ℕ) = singleton (0, 0) := rfl
 #align finsupp.antidiagonal_zero Finsupp.antidiagonal_zero
 
 @[to_additive]

Mathlib/Data/Finsupp/Multiset.lean

@@ -19,28 +19,24 @@ promoted to an order isomorphism.
 
 open Finset
 
-open BigOperators Classical
-
-noncomputable section
+open BigOperators
 
 variable {α β ι : Type _}
 
 namespace Finsupp
+
 /-- Given `f : α →₀ ℕ`, `f.toMultiset` is the multiset with multiplicities given by the values of
-`f` on the elements of `α`. We define this function as an `AddEquiv`. -/
-def toMultiset : (α →₀ ℕ) ≃+ Multiset α where
+`f` on the elements of `α`. We define this function as an `AddMonoidHom`.
+
+Under the additional assumption of `[DecidableEq α]`, this is available as
+`Multiset.toFinsupp : Multiset α ≃+ (α →₀ ℕ)`; the two declarations are separate as this assumption
+is only needed for one direction. -/
+def toMultiset : (α →₀ ℕ) →+ Multiset α where
   toFun f := Finsupp.sum f fun a n => n • {a}
-  invFun s := ⟨s.toFinset, fun a => s.count a, fun a => by simp⟩
-  left_inv f :=
-    ext fun a => by
-      simp only [sum, Multiset.count_sum', Multiset.count_singleton, mul_boole, coe_mk,
-        mem_support_iff, Multiset.count_nsmul, Finset.sum_ite_eq, ite_not, ite_eq_right_iff]
-      exact Eq.symm
-  right_inv s := by simp only [sum, coe_mk, Multiset.toFinset_sum_count_nsmul_eq]
   -- Porting note: times out if h is not specified
-  map_add' f g := sum_add_index' (h := fun a n => n • ({a} : Multiset α))
+  map_add' _f _g := sum_add_index' (h := fun a n => n • ({a} : Multiset α))
     (fun _ ↦ zero_nsmul _) (fun _ ↦ add_nsmul _)
-#align finsupp.to_multiset Finsupp.toMultiset
+  map_zero' := sum_zero_index
 
 theorem toMultiset_zero : toMultiset (0 : α →₀ ℕ) = 0 :=
   rfl
@@ -54,15 +50,6 @@ theorem toMultiset_apply (f : α →₀ ℕ) : toMultiset f = f.sum fun a n => n
   rfl
 #align finsupp.to_multiset_apply Finsupp.toMultiset_apply
 
-@[simp]
-theorem toMultiset_symm_apply [DecidableEq α] (s : Multiset α) (x : α) :
-    Finsupp.toMultiset.symm s x = s.count x := by
-    -- Porting note: proof used to be `convert rfl`
-    have : Finsupp.toMultiset.symm s x = Finsupp.toMultiset.invFun s x := rfl
-    simp_rw [this, toMultiset, coe_mk]
-    congr
-#align finsupp.to_multiset_symm_apply Finsupp.toMultiset_symm_apply
-
 @[simp]
 theorem toMultiset_single (a : α) (n : ℕ) : toMultiset (single a n) = n • {a} := by
   rw [toMultiset_apply, sum_single_index]; apply zero_nsmul
@@ -130,34 +117,42 @@ theorem count_toMultiset [DecidableEq α] (f : α →₀ ℕ) (a : α) : (toMult
 
 @[simp]
 theorem mem_toMultiset (f : α →₀ ℕ) (i : α) : i ∈ toMultiset f ↔ i ∈ f.support := by
+  classical
   rw [← Multiset.count_ne_zero, Finsupp.count_toMultiset, Finsupp.mem_support_iff]
 #align finsupp.mem_to_multiset Finsupp.mem_toMultiset
 
 end Finsupp
 
 namespace Multiset
 
+variable [DecidableEq α]
+
 /-- Given a multiset `s`, `s.toFinsupp` returns the finitely supported function on `ℕ` given by
 the multiplicities of the elements of `s`. -/
-def toFinsupp : Multiset α ≃+ (α →₀ ℕ) :=
-  Finsupp.toMultiset.symm
+@[simps symm_apply]
+def toFinsupp : Multiset α ≃+ (α →₀ ℕ) where
+  toFun s := ⟨s.toFinset, fun a => s.count a, fun a => by simp⟩
+  invFun f := Finsupp.toMultiset f
+  map_add' s t := Finsupp.ext <| fun _ => count_add _ _ _
+  right_inv f :=
+    Finsupp.ext fun a => by
+      simp only [Finsupp.toMultiset_apply, Finsupp.sum, Multiset.count_sum',
+        Multiset.count_singleton, mul_boole, Finsupp.coe_mk, Finsupp.mem_support_iff,
+        Multiset.count_nsmul, Finset.sum_ite_eq, ite_not, ite_eq_right_iff]
+      exact Eq.symm
+  left_inv s := by simp only [Finsupp.toMultiset_apply, Finsupp.sum, Finsupp.coe_mk,
+    Multiset.toFinset_sum_count_nsmul_eq]
 #align multiset.to_finsupp Multiset.toFinsupp
 
 @[simp]
-theorem toFinsupp_support [DecidableEq α] (s : Multiset α) : s.toFinsupp.support = s.toFinset := by
-  -- Porting note: used to be `convert rfl`
-  ext
-  simp [toFinsupp]
+theorem toFinsupp_support (s : Multiset α) : s.toFinsupp.support = s.toFinset := rfl
 #align multiset.to_finsupp_support Multiset.toFinsupp_support
 
 @[simp]
-theorem toFinsupp_apply [DecidableEq α] (s : Multiset α) (a : α) : toFinsupp s a = s.count a := by
-  -- Porting note: used to be `convert rfl`
-  exact Finsupp.toMultiset_symm_apply s a
+theorem toFinsupp_apply (s : Multiset α) (a : α) : toFinsupp s a = s.count a := rfl
 #align multiset.to_finsupp_apply Multiset.toFinsupp_apply
 
-theorem toFinsupp_zero : toFinsupp (0 : Multiset α) = 0 :=
-  AddEquiv.map_zero _
+theorem toFinsupp_zero : toFinsupp (0 : Multiset α) = 0 := _root_.map_zero _
 #align multiset.to_finsupp_zero Multiset.toFinsupp_zero
 
 theorem toFinsupp_add (s t : Multiset α) : toFinsupp (s + t) = toFinsupp s + toFinsupp t :=
@@ -166,55 +161,53 @@ theorem toFinsupp_add (s t : Multiset α) : toFinsupp (s + t) = toFinsupp s + to
 
 @[simp]
 theorem toFinsupp_singleton (a : α) : toFinsupp ({a} : Multiset α) = Finsupp.single a 1 :=
-  Finsupp.toMultiset.symm_apply_eq.2 <| by simp
+  by ext; rw [toFinsupp_apply, count_singleton, Finsupp.single_eq_pi_single, Pi.single_apply]
 #align multiset.to_finsupp_singleton Multiset.toFinsupp_singleton
 
 @[simp]
 theorem toFinsupp_toMultiset (s : Multiset α) : Finsupp.toMultiset (toFinsupp s) = s :=
-  Finsupp.toMultiset.apply_symm_apply s
+  Multiset.toFinsupp.symm_apply_apply s
 #align multiset.to_finsupp_to_multiset Multiset.toFinsupp_toMultiset
 
 theorem toFinsupp_eq_iff {s : Multiset α} {f : α →₀ ℕ} :
     toFinsupp s = f ↔ s = Finsupp.toMultiset f :=
-  Finsupp.toMultiset.symm_apply_eq
+  Multiset.toFinsupp.apply_eq_iff_symm_apply
 #align multiset.to_finsupp_eq_iff Multiset.toFinsupp_eq_iff
 
 end Multiset
 
 @[simp]
-theorem Finsupp.toMultiset_toFinsupp (f : α →₀ ℕ) :
+theorem Finsupp.toMultiset_toFinsupp [DecidableEq α] (f : α →₀ ℕ) :
     Multiset.toFinsupp (Finsupp.toMultiset f) = f :=
-  Finsupp.toMultiset.symm_apply_apply f
+  Multiset.toFinsupp.apply_symm_apply _
 #align finsupp.to_multiset_to_finsupp Finsupp.toMultiset_toFinsupp
 
-/-! ### As an order isomorphism -/
+theorem Finsupp.toMultiset_eq_iff [DecidableEq α] {f : α →₀ ℕ} {s : Multiset α}:
+    Finsupp.toMultiset f = s ↔ f = Multiset.toFinsupp s :=
+  Multiset.toFinsupp.symm_apply_eq
 
+/-! ### As an order isomorphism -/
 
 namespace Finsupp
 /-- `Finsupp.toMultiset` as an order isomorphism. -/
-def orderIsoMultiset : (ι →₀ ℕ) ≃o Multiset ι where
-  toEquiv := toMultiset.toEquiv
-  map_rel_iff' := by
-    -- Porting note: This proof used to be simp [Multiset.le_iff_count, le_def]
-    intro f g
-    -- Porting note: the following should probably be a simp lemma somewhere;
-    -- maybe coe_toEquiv in Hom/Equiv/Basic?
-    have : ⇑ (toMultiset (α := ι)).toEquiv = toMultiset := rfl
-    simp [Multiset.le_iff_count, le_def, ← toMultiset_symm_apply, this]
+def orderIsoMultiset [DecidableEq ι] : (ι →₀ ℕ) ≃o Multiset ι where
+  toEquiv := Multiset.toFinsupp.symm.toEquiv
+  map_rel_iff' {f g} := by simp [le_def, Multiset.le_iff_count]
 #align finsupp.order_iso_multiset Finsupp.orderIsoMultiset
 
 @[simp]
-theorem coe_orderIsoMultiset : ⇑(@orderIsoMultiset ι) = toMultiset :=
+theorem coe_orderIsoMultiset [DecidableEq ι] : ⇑(@orderIsoMultiset ι _) = toMultiset :=
   rfl
 #align finsupp.coe_order_iso_multiset Finsupp.coe_orderIsoMultiset
 
 @[simp]
-theorem coe_orderIsoMultiset_symm : ⇑(@orderIsoMultiset ι).symm = Multiset.toFinsupp :=
+theorem coe_orderIsoMultiset_symm [DecidableEq ι] :
+  ⇑(@orderIsoMultiset ι).symm = Multiset.toFinsupp :=
   rfl
 #align finsupp.coe_order_iso_multiset_symm Finsupp.coe_orderIsoMultiset_symm
 
 theorem toMultiset_strictMono : StrictMono (@toMultiset ι) :=
-  (@orderIsoMultiset ι).strictMono
+  by classical exact (@orderIsoMultiset ι _).strictMono
 #align finsupp.to_multiset_strict_mono Finsupp.toMultiset_strictMono
 
 theorem sum_id_lt_of_lt (m n : ι →₀ ℕ) (h : m < n) : (m.sum fun _ => id) < n.sum fun _ => id := by
@@ -237,6 +230,6 @@ instance : WellFoundedRelation (ι →₀ ℕ) where
 
 end Finsupp
 
-theorem Multiset.toFinsupp_strictMono : StrictMono (@Multiset.toFinsupp ι) :=
+theorem Multiset.toFinsupp_strictMono [DecidableEq ι] : StrictMono (@Multiset.toFinsupp ι _) :=
   (@Finsupp.orderIsoMultiset ι).symm.strictMono
 #align multiset.to_finsupp_strict_mono Multiset.toFinsupp_strictMono

Mathlib/Data/MvPolynomial/Basic.lean

@@ -698,7 +698,7 @@ theorem coeff_C_mul (m) (a : R) (p : MvPolynomial σ R) : coeff m (C a * p) = a
   simp
 #align mv_polynomial.coeff_C_mul MvPolynomial.coeff_C_mul
 
-theorem coeff_mul (p q : MvPolynomial σ R) (n : σ →₀ ℕ) :
+theorem coeff_mul [DecidableEq σ] (p q : MvPolynomial σ R) (n : σ →₀ ℕ) :
     coeff n (p * q) = ∑ x in antidiagonal n, coeff x.1 p * coeff x.2 q :=
   AddMonoidAlgebra.mul_apply_antidiagonal p q _ _ mem_antidiagonal
 #align mv_polynomial.coeff_mul MvPolynomial.coeff_mul
@@ -856,7 +856,7 @@ def constantCoeff : MvPolynomial σ R →+* R
     where
   toFun := coeff 0
   map_one' := by simp [AddMonoidAlgebra.one_def]
-  map_mul' := by simp [coeff_mul, Finsupp.support_single_ne_zero]
+  map_mul' := by classical simp [coeff_mul, Finsupp.support_single_ne_zero]
   map_zero' := coeff_zero _
   map_add' := coeff_add _
 #align mv_polynomial.constant_coeff MvPolynomial.constantCoeff

Mathlib/Data/Nat/Choose/Multinomial.lean

@@ -199,7 +199,7 @@ variable {α : Type _}
 /-- Alternative definition of multinomial based on `Multiset` delegating to the
   finsupp definition
 -/
-noncomputable def multinomial (m : Multiset α) : ℕ :=
+def multinomial [DecidableEq α] (m : Multiset α) : ℕ :=
   m.toFinsupp.multinomial
 #align multiset.multinomial Multiset.multinomial
 
@@ -208,7 +208,6 @@ theorem multinomial_filter_ne [DecidableEq α] (a : α) (m : Multiset α) :
   dsimp only [multinomial]
   convert Finsupp.multinomial_update a _
   · rw [← Finsupp.card_toMultiset, m.toFinsupp_toMultiset]
-  · simp only [toFinsupp_apply]
   · ext1 a
     rw [toFinsupp_apply, count_filter, Finsupp.coe_update]
     split_ifs with h

Mathlib/Logic/Hydra.lean

@@ -59,7 +59,7 @@ def CutExpand (r : α → α → Prop) (s' s : Multiset α) : Prop :=
 
 variable {r : α → α → Prop}
 
-theorem cutExpand_le_invImage_lex [IsIrrefl α r] :
+theorem cutExpand_le_invImage_lex [DecidableEq α] [IsIrrefl α r] :
     CutExpand r ≤ InvImage (Finsupp.Lex (rᶜ ⊓ (· ≠ ·)) (· < ·)) toFinsupp := by
   rintro s t ⟨u, a, hr, he⟩
   replace hr := fun a' ↦ mt (hr a')

Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

@@ -89,6 +89,7 @@ theorem homogeneousSubmodule_mul [CommSemiring R] (m n : ℕ) :
     homogeneousSubmodule σ R m * homogeneousSubmodule σ R n ≤ homogeneousSubmodule σ R (m + n) := by
   rw [Submodule.mul_le]
   intro φ hφ ψ hψ c hc
+  classical
   rw [coeff_mul] at hc
   obtain ⟨⟨d, e⟩, hde, H⟩ := Finset.exists_ne_zero_of_sum_ne_zero hc
   have aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0 := by

Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean

@@ -176,6 +176,7 @@ variable {R}
 theorem weightedHomogeneousSubmodule_mul (w : σ → M) (m n : M) :
     weightedHomogeneousSubmodule R w m * weightedHomogeneousSubmodule R w n ≤
       weightedHomogeneousSubmodule R w (m + n) := by
+  classical
   rw [Submodule.mul_le]
   intro φ hφ ψ hψ c hc
   rw [coeff_mul] at hc

Mathlib/RingTheory/PowerSeries/Basic.lean

@@ -208,9 +208,10 @@ instance : AddMonoidWithOne (MvPowerSeries σ R) :=
 instance : Mul (MvPowerSeries σ R) :=
   ⟨fun φ ψ n => ∑ p in Finsupp.antidiagonal n, coeff R p.1 φ * coeff R p.2 ψ⟩
 
-theorem coeff_mul :
-    coeff R n (φ * ψ) = ∑ p in Finsupp.antidiagonal n, coeff R p.1 φ * coeff R p.2 ψ :=
-  rfl
+theorem coeff_mul [DecidableEq σ] :
+    coeff R n (φ * ψ) = ∑ p in Finsupp.antidiagonal n, coeff R p.1 φ * coeff R p.2 ψ := by
+  refine Finset.sum_congr ?_ fun _ _ => rfl
+  rw [Subsingleton.elim (fun a b => propDecidable (a = b)) ‹DecidableEq σ›]
 #align mv_power_series.coeff_mul MvPowerSeries.coeff_mul
 
 protected theorem zero_mul : (0 : MvPowerSeries σ R) * φ = 0 :=
@@ -1472,6 +1473,8 @@ theorem coeff_zero_one : coeff R 0 (1 : PowerSeries R) = 1 :=
 
 theorem coeff_mul (n : ℕ) (φ ψ : PowerSeries R) :
     coeff R n (φ * ψ) = ∑ p in Finset.Nat.antidiagonal n, coeff R p.1 φ * coeff R p.2 ψ := by
+  -- `rw` can't see that `PowerSeries = MvPowerSeries Unit`, so use `.trans`
+  refine (MvPowerSeries.coeff_mul _ φ ψ).trans ?_
   symm
   apply Finset.sum_bij fun (p : ℕ × ℕ) _h => (single () p.1, single () p.2)
   · rintro ⟨i, j⟩ hij