chore: deprecate prod_zero_iff_exists_zero (#9281)

- Make `Multiset.prod_eq_zero_iff` a `simp` lemma.
- Golf and deprecate `prod_zero_iff_exists_zero`; it was a bad API version of `Multiset.prod_eq_zero_iff`.
- Make `Ideal.mul_eq_bot` a `simp` lemma`.
- Add `Ideal.multiset_prod_eq_bot` (a `simp` lemma), deprecate `Ideal.prod_eq_bot`.

The deprecated lemmas `prod_zero_iff_exists_zero` and `Ideal.prod_eq_bot` use `∃ x ∈ s, x = 0` instead of a simpler `0 ∈ s` in the RHS.

Mathlib/Algebra/BigOperators/Multiset/Basic.lean

@@ -285,6 +285,7 @@ theorem prod_eq_zero {s : Multiset α} (h : (0 : α) ∈ s) : s.prod = 0 := by
 
 variable [NoZeroDivisors α] [Nontrivial α] {s : Multiset α}
 
+@[simp]
 theorem prod_eq_zero_iff : s.prod = 0 ↔ (0 : α) ∈ s :=
   Quotient.inductionOn s fun l => by
     rw [quot_mk_to_coe, coe_prod]

Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

@@ -234,22 +234,10 @@ theorem nonZeroDivisors_le_comap_nonZeroDivisors_of_injective [NoZeroDivisors M'
   Submonoid.le_comap_of_map_le _ (map_le_nonZeroDivisors_of_injective _ hf le_rfl)
 #align non_zero_divisors_le_comap_non_zero_divisors_of_injective nonZeroDivisors_le_comap_nonZeroDivisors_of_injective
 
+@[deprecated Multiset.prod_eq_zero_iff] -- since 26 Dec 2023
 theorem prod_zero_iff_exists_zero [NoZeroDivisors M₁] [Nontrivial M₁] {s : Multiset M₁} :
     s.prod = 0 ↔ ∃ (r : M₁) (_ : r ∈ s), r = 0 := by
-  constructor; swap
-  · rintro ⟨r, hrs, rfl⟩
-    exact Multiset.prod_eq_zero hrs
-  induction' s using Multiset.induction_on with a s ih
-  · intro habs
-    simp at habs
-  · rw [Multiset.prod_cons]
-    intro hprod
-    replace hprod := eq_zero_or_eq_zero_of_mul_eq_zero hprod
-    cases' hprod with ha hb
-    · exact ⟨a, Multiset.mem_cons_self a s, ha⟩
-    · apply (ih hb).imp _
-      rintro b ⟨hb₁, hb₂⟩
-      exact ⟨Multiset.mem_cons_of_mem hb₁, hb₂⟩
+  simp [Multiset.prod_eq_zero_iff]
 #align prod_zero_iff_exists_zero prod_zero_iff_exists_zero
 
 end nonZeroDivisors

Mathlib/NumberTheory/ArithmeticFunction.lean

@@ -919,13 +919,9 @@ theorem cardFactors_mul {m n : ℕ} (m0 : m ≠ 0) (n0 : n ≠ 0) : Ω (m * n) =
 
 theorem cardFactors_multiset_prod {s : Multiset ℕ} (h0 : s.prod ≠ 0) :
     Ω s.prod = (Multiset.map Ω s).sum := by
-  revert h0
-  -- porting note: was `apply s.induction_on`
-  refine s.induction_on ?_ ?_
-  · simp
-  intro a t h h0
-  rw [Multiset.prod_cons, mul_ne_zero_iff] at h0
-  simp [h0, cardFactors_mul, h]
+  induction s using Multiset.induction_on with
+  | empty => simp
+  | cons ih => simp_all [cardFactors_mul, not_or]
 #align nat.arithmetic_function.card_factors_multiset_prod Nat.ArithmeticFunction.cardFactors_multiset_prod
 
 @[simp]

Mathlib/RingTheory/Ideal/Operations.lean

@@ -809,6 +809,7 @@ theorem pow_right_mono {I J : Ideal R} (e : I ≤ J) (n : ℕ) : I ^ n ≤ J ^ n
     exact Ideal.mul_mono e hn
 #align ideal.pow_right_mono Ideal.pow_right_mono
 
+@[simp]
 theorem mul_eq_bot {R : Type*} [CommSemiring R] [NoZeroDivisors R] {I J : Ideal R} :
     I * J = ⊥ ↔ I = ⊥ ∨ J = ⊥ :=
   ⟨fun hij =>
@@ -823,9 +824,15 @@ instance {R : Type*} [CommSemiring R] [NoZeroDivisors R] : NoZeroDivisors (Ideal
   eq_zero_or_eq_zero_of_mul_eq_zero := mul_eq_bot.1
 
 /-- A product of ideals in an integral domain is zero if and only if one of the terms is zero. -/
+@[simp]
+lemma multiset_prod_eq_bot {R : Type*} [CommRing R] [IsDomain R] {s : Multiset (Ideal R)} :
+    s.prod = ⊥ ↔ ⊥ ∈ s :=
+  Multiset.prod_eq_zero_iff
+
+/-- A product of ideals in an integral domain is zero if and only if one of the terms is zero. -/
+@[deprecated multiset_prod_eq_bot] -- since 26 Dec 2023
 theorem prod_eq_bot {R : Type*} [CommRing R] [IsDomain R] {s : Multiset (Ideal R)} :
     s.prod = ⊥ ↔ ∃ I ∈ s, I = ⊥ := by
-  rw [bot_eq_zero, prod_zero_iff_exists_zero]
   simp
 #align ideal.prod_eq_bot Ideal.prod_eq_bot