chore: simplify the formatting of gcd_eq_zero_iffs a little (#28898)

Related to #28897.

Author: ShreckYe

Mathlib/Algebra/GCDMonoid/Finset.lean

@@ -173,7 +173,7 @@ theorem gcd_image [DecidableEq β] {g : γ → β} (s : Finset γ) :
 theorem gcd_eq_gcd_image [DecidableEq α] : s.gcd f = (s.image f).gcd id :=
   Eq.symm <| gcd_image _
 
-theorem gcd_eq_zero_iff : s.gcd f = 0 ↔ ∀ x : β, x ∈ s → f x = 0 := by
+theorem gcd_eq_zero_iff : s.gcd f = 0 ↔ ∀ x ∈ s, f x = 0 := by
   rw [gcd_def, Multiset.gcd_eq_zero_iff]
   constructor <;> intro h
   · intro b bs

Mathlib/Algebra/GCDMonoid/Multiset.lean

@@ -140,7 +140,7 @@ theorem gcd_mono {s₁ s₂ : Multiset α} (h : s₁ ⊆ s₂) : s₂.gcd ∣ s
 theorem normalize_gcd (s : Multiset α) : normalize s.gcd = s.gcd :=
   Multiset.induction_on s (by simp) fun a s _ ↦ by simp
 
-theorem gcd_eq_zero_iff (s : Multiset α) : s.gcd = 0 ↔ ∀ x : α, x ∈ s → x = 0 := by
+theorem gcd_eq_zero_iff (s : Multiset α) : s.gcd = 0 ↔ ∀ x ∈ s, x = 0 := by
   constructor
   · intro h x hx
     apply eq_zero_of_zero_dvd