chore(Algebra/Order/GroupWithZero): generalize some hypotheses from pos to nonneg (leanprover-community#34992)

Co-authored-by: David Ledvinka <dledvinka.ledvinka@mail.utoronto.ca>

Author: DavidLedvinka

Mathlib/Algebra/MvPolynomial/SchwartzZippel.lean

@@ -199,7 +199,7 @@ lemma schwartz_zippel_totalDegree {n} {p : MvPolynomial (Fin n) R} (hp : p ≠ 0
       · simp
         simp only [← _root_.bot_eq_zero, sup_bot]
       simp_rw [totalDegree, Nat.cast_finsetSup]
-      rw [sup_div₀ (ha := show 0 < (#S : ℚ≥0) by positivity)]
+      rw [sup_div₀ (by positivity)]
       simp [← sum_div, Finsupp.sum_fintype]
 
 end MvPolynomial

Mathlib/Algebra/Order/GroupWithZero/Finset.lean

@@ -46,20 +46,28 @@ end MonoidWithZero
 section GroupWithZero
 variable [GroupWithZero G₀] [SemilatticeSup G₀] {s : Finset ι} {a : G₀}
 
-lemma sup'_mul₀ [MulPosReflectLT G₀] (ha : 0 < a) (f : ι → G₀) (s : Finset ι) (hs) :
-    s.sup' hs f * a = s.sup' hs fun i ↦ f i * a := map_finset_sup' (OrderIso.mulRight₀ _ ha) hs f
+lemma sup'_mul₀ [MulPosReflectLT G₀] (ha : 0 ≤ a) (f : ι → G₀) (s : Finset ι) (hs) :
+    s.sup' hs f * a = s.sup' hs fun i ↦ f i * a := by
+  by_cases! h : 0 = a
+  · simp [← h]
+  exact map_finset_sup' (OrderIso.mulRight₀ _ (lt_of_le_of_ne ha h)) hs f
 
 set_option linter.docPrime false in
-lemma mul₀_sup' [PosMulReflectLT G₀] (ha : 0 < a) (f : ι → G₀) (s : Finset ι) (hs) :
-    a * s.sup' hs f = s.sup' hs fun i ↦ a * f i := map_finset_sup' (OrderIso.mulLeft₀ _ ha) hs f
-
-lemma sup'_div₀ [MulPosReflectLT G₀] (ha : 0 < a) (f : ι → G₀) (s : Finset ι) (hs) :
-    s.sup' hs f / a = s.sup' hs fun i ↦ f i / a :=
-  map_finset_sup' (OrderIso.divRight₀ _ ha) hs f
+lemma mul₀_sup' [PosMulReflectLT G₀] (ha : 0 ≤ a) (f : ι → G₀) (s : Finset ι) (hs) :
+    a * s.sup' hs f = s.sup' hs fun i ↦ a * f i := by
+  by_cases! h : 0 = a
+  · simp [← h]
+  exact map_finset_sup' (OrderIso.mulLeft₀ _ (lt_of_le_of_ne ha h)) hs f
+
+lemma sup'_div₀ [MulPosReflectLT G₀] (ha : 0 ≤ a) (f : ι → G₀) (s : Finset ι) (hs) :
+    s.sup' hs f / a = s.sup' hs fun i ↦ f i / a := by
+  by_cases! h : 0 = a
+  · simp [← h]
+  exact map_finset_sup' (OrderIso.divRight₀ _ (lt_of_le_of_ne ha h)) hs f
 
 end GroupWithZero
 
-lemma sup_div₀ [LinearOrderedCommGroupWithZero G₀] {a : G₀} (ha : 0 < a)
+lemma sup_div₀ [LinearOrderedCommGroupWithZero G₀] {a : G₀} (ha : 0 ≤ a)
     (s : Finset ι) (f : ι → G₀) : s.sup f / a = s.sup fun i ↦ f i / a := by
   obtain rfl | hs := s.eq_empty_or_nonempty
   · simp [← show (0 : G₀) = ⊥ from bot_unique zero_le']