fix: make an ideal lemma more constructive (#6080)

This generalizes `Ideal.pow_multiset_sum_mem_span_pow` away from `Classical.decEq`.

Mathlib/RingTheory/Ideal/Basic.lean

@@ -36,7 +36,7 @@ variable {α : Type u} {β : Type v}
 
 open Set Function
 
-open Classical BigOperators Pointwise
+open BigOperators Pointwise
 
 /-- A (left) ideal in a semiring `R` is an additive submonoid `s` such that
 `a * b ∈ s` whenever `b ∈ s`. If `R` is a ring, then `s` is an additive subgroup.  -/
@@ -582,7 +582,8 @@ theorem IsPrime.pow_mem_iff_mem {I : Ideal α} (hI : I.IsPrime) {r : α} (n : 
   ⟨hI.mem_of_pow_mem n, fun hr => I.pow_mem_of_mem hr n hn⟩
 #align ideal.is_prime.pow_mem_iff_mem Ideal.IsPrime.pow_mem_iff_mem
 
-theorem pow_multiset_sum_mem_span_pow (s : Multiset α) (n : ℕ) : s.sum ^ (Multiset.card s * n + 1) ∈
+theorem pow_multiset_sum_mem_span_pow [DecidableEq α] (s : Multiset α) (n : ℕ) :
+    s.sum ^ (Multiset.card s * n + 1) ∈
     span ((s.map fun (x:α) ↦ x ^ (n + 1)).toFinset : Set α) := by
   induction' s using Multiset.induction_on with a s hs
   · simp
@@ -610,6 +611,7 @@ theorem pow_multiset_sum_mem_span_pow (s : Multiset α) (n : ℕ) : s.sum ^ (Mul
 
 theorem sum_pow_mem_span_pow {ι} (s : Finset ι) (f : ι → α) (n : ℕ) :
     (∑ i in s, f i) ^ (s.card * n + 1) ∈ span ((fun i => f i ^ (n + 1)) '' s) := by
+  classical
   simpa only [Multiset.card_map, Multiset.map_map, comp_apply, Multiset.toFinset_map,
     Finset.coe_image, Finset.val_toFinset] using pow_multiset_sum_mem_span_pow (s.1.map f) n
 #align ideal.sum_pow_mem_span_pow Ideal.sum_pow_mem_span_pow