feat(Algebra/GroupPower): weaken TC assumptions (#6389)

- Assume `OrderedSemiring` instead of `StrictOrderedSemiring`
  here and there.
- Add `@[simp]` to `zsmul_one`.
- Add `exists_lt_nsmul`.

Mathlib/Algebra/GroupPower/Lemmas.lean

@@ -125,6 +125,7 @@ theorem smul_pow' [MulDistribMulAction M N] (x : M) (m : N) (n : ℕ) : x • m
 
 end Monoid
 
+@[simp]
 theorem zsmul_one [AddGroupWithOne A] (n : ℤ) : n • (1 : A) = n := by cases n <;> simp
 #align zsmul_one zsmul_one
 
@@ -630,9 +631,9 @@ theorem neg_one_pow_eq_pow_mod_two [Ring R] {n : ℕ} : (-1 : R) ^ n = (-1) ^ (n
   rw [← Nat.mod_add_div n 2, pow_add, pow_mul]; simp [sq]
 #align neg_one_pow_eq_pow_mod_two neg_one_pow_eq_pow_mod_two
 
-section StrictOrderedSemiring
+section OrderedSemiring
 
-variable [StrictOrderedSemiring R] {a : R}
+variable [OrderedSemiring R] {a : R}
 
 /-- Bernoulli's inequality. This version works for semirings but requires
 additional hypotheses `0 ≤ a * a` and `0 ≤ (1 + a) * (1 + a)`. -/
@@ -645,13 +646,13 @@ theorem one_add_mul_le_pow' (Hsq : 0 ≤ a * a) (Hsq' : 0 ≤ (1 + a) * (1 + a))
       add_nonneg (mul_nonneg n.cast_nonneg (mul_nonneg Hsq H)) Hsq
     calc
       1 + (↑(n + 2) : R) * a ≤ 1 + ↑(n + 2) * a + (n * (a * a * (2 + a)) + a * a) :=
-        (le_add_iff_nonneg_right _).2 this
+        le_add_of_nonneg_right this
       _ = (1 + a) * (1 + a) * (1 + n * a) := by {
           simp only [Nat.cast_add, add_mul, mul_add, one_mul, mul_one, ← one_add_one_eq_two,
             Nat.cast_one, add_assoc, add_right_inj]
           simp only [← add_assoc, add_comm _ (↑n * a)]
-          simp only [add_assoc, add_right_inj, (n.cast_commute (_ : R)).left_comm]
-          ac_rfl }
+          simp only [add_assoc, (n.cast_commute (_ : R)).left_comm]
+          simp only [add_comm, add_left_comm] }
       _ ≤ (1 + a) * (1 + a) * (1 + a) ^ n :=
         mul_le_mul_of_nonneg_left (one_add_mul_le_pow' Hsq Hsq' H _) Hsq'
       _ = (1 + a) ^ (n + 2) := by simp only [pow_succ, mul_assoc]
@@ -678,7 +679,7 @@ theorem sq_le (h₀ : 0 ≤ a) (h₁ : a ≤ 1) : a ^ 2 ≤ a :=
   pow_le_of_le_one h₀ h₁ two_ne_zero
 #align sq_le sq_le
 
-end StrictOrderedSemiring
+end OrderedSemiring
 
 section LinearOrderedSemiring
 

Mathlib/Algebra/Order/Archimedean.lean

@@ -47,6 +47,11 @@ instance OrderDual.archimedean [OrderedAddCommGroup α] [Archimedean α] : Archi
     ⟨n, by rwa [neg_nsmul, neg_le_neg_iff] at hn⟩⟩
 #align order_dual.archimedean OrderDual.archimedean
 
+theorem exists_lt_nsmul [OrderedAddCommMonoid M] [Archimedean M]
+    [CovariantClass M M (· + ·) (· < ·)] {a : M} (ha : 0 < a) (b : M) :
+    ∃ n : ℕ, b < n • a :=
+  let ⟨k, hk⟩ := Archimedean.arch b ha; ⟨k + 1, hk.trans_lt <| nsmul_lt_nsmul ha k.lt_succ_self⟩
+
 section LinearOrderedAddCommGroup
 
 variable [LinearOrderedAddCommGroup α] [Archimedean α]
@@ -110,20 +115,18 @@ theorem existsUnique_sub_zsmul_mem_Ioc {a : α} (ha : 0 < a) (b c : α) :
 end LinearOrderedAddCommGroup
 
 theorem exists_nat_gt [StrictOrderedSemiring α] [Archimedean α] (x : α) : ∃ n : ℕ, x < n :=
-  let ⟨n, h⟩ := Archimedean.arch x zero_lt_one
-  ⟨n + 1, lt_of_le_of_lt (by rwa [← nsmul_one]) (Nat.cast_lt.2 (Nat.lt_succ_self _))⟩
+  (exists_lt_nsmul zero_lt_one x).imp fun n hn ↦ by rwa [← nsmul_one]
 #align exists_nat_gt exists_nat_gt
 
-theorem exists_nat_ge [StrictOrderedSemiring α] [Archimedean α] (x : α) : ∃ n : ℕ, x ≤ n := by
+theorem exists_nat_ge [OrderedSemiring α] [Archimedean α] (x : α) : ∃ n : ℕ, x ≤ n := by
   nontriviality α
-  exact (exists_nat_gt x).imp fun n => le_of_lt
+  exact (Archimedean.arch x one_pos).imp fun n h => by rwa [← nsmul_one]
 #align exists_nat_ge exists_nat_ge
 
 theorem add_one_pow_unbounded_of_pos [StrictOrderedSemiring α] [Archimedean α] (x : α) {y : α}
     (hy : 0 < y) : ∃ n : ℕ, x < (y + 1) ^ n :=
   have : 0 ≤ 1 + y := add_nonneg zero_le_one hy.le
-  let ⟨n, h⟩ := Archimedean.arch x hy
-  ⟨n,
+  (Archimedean.arch x hy).imp fun n h ↦
     calc
       x ≤ n • y := h
       _ = n * y := nsmul_eq_mul _ _
@@ -132,7 +135,6 @@ theorem add_one_pow_unbounded_of_pos [StrictOrderedSemiring α] [Archimedean α]
         one_add_mul_le_pow' (mul_nonneg hy.le hy.le) (mul_nonneg this this)
           (add_nonneg zero_le_two hy.le) _
       _ = (y + 1) ^ n := by rw [add_comm]
-      ⟩
 #align add_one_pow_unbounded_of_pos add_one_pow_unbounded_of_pos
 
 section StrictOrderedRing