chore(algebra/group_power): golf a few proofs (#10498)

* move `pow_lt_pow_of_lt_one` and `pow_lt_pow_iff_of_lt_one` from
  `algebra.group_power.lemmas` to `algebra.group_power.order`;
* add `strict_anti_pow`, use it to golf the proofs of the two lemmas
  above;
* golf a few other proofs;
* add `nnreal.exists_pow_lt_of_lt_one`.

Author: urkud

src/algebra/group_power/lemmas.lean

@@ -429,39 +429,12 @@ calc 1 + (↑(n + 2) : R) * a ≤ 1 + ↑(n + 2) * a + (n * (a * a * (2 + a)) +
   mul_le_mul_of_nonneg_left (one_add_mul_le_pow' n) Hsq'
 ... = (1 + a)^(n + 2) : by simp only [pow_succ, mul_assoc]
 
-private lemma pow_lt_pow_of_lt_one_aux (h : 0 < a) (ha : a < 1) (i : ℕ) :
-  ∀ k : ℕ, a ^ (i + k + 1) < a ^ i
-| 0 :=
-  begin
-    rw [←one_mul (a^i), add_zero, pow_succ],
-    exact mul_lt_mul ha (le_refl _) (pow_pos h _) zero_le_one
-  end
-| (k+1) :=
-  begin
-    rw [←one_mul (a^i), pow_succ],
-    apply mul_lt_mul ha _ _ zero_le_one,
-    { apply le_of_lt, apply pow_lt_pow_of_lt_one_aux },
-    { show 0 < a ^ (i + (k + 1) + 0), apply pow_pos h }
-  end
-
 private lemma pow_le_pow_of_le_one_aux (h : 0 ≤ a) (ha : a ≤ 1) (i : ℕ) :
   ∀ k : ℕ, a ^ (i + k) ≤ a ^ i
 | 0 := by simp
 | (k+1) := by { rw [←add_assoc, ←one_mul (a^i), pow_succ],
                 exact mul_le_mul ha (pow_le_pow_of_le_one_aux _) (pow_nonneg h _) zero_le_one }
 
-lemma pow_lt_pow_of_lt_one (h : 0 < a) (ha : a < 1)
-  {i j : ℕ} (hij : i < j) : a ^ j < a ^ i :=
-let ⟨k, hk⟩ := nat.exists_eq_add_of_lt hij in
-by rw hk; exact pow_lt_pow_of_lt_one_aux h ha _ _
-
-lemma pow_lt_pow_iff_of_lt_one {n m : ℕ} (hpos : 0 < a) (h : a < 1) :
-  a ^ m < a ^ n ↔ n < m :=
-begin
-  have : strict_mono (λ (n : order_dual ℕ), a ^ (id n : ℕ)) := λ m n, pow_lt_pow_of_lt_one hpos h,
-  exact this.lt_iff_lt
-end
-
 lemma pow_le_pow_of_le_one (h : 0 ≤ a) (ha : a ≤ 1) {i j : ℕ} (hij : i ≤ j) :
   a ^ j ≤ a ^ i :=
 let ⟨k, hk⟩ := nat.exists_eq_add_of_le hij in

src/algebra/group_power/order.lean

@@ -191,20 +191,23 @@ strict_mono_pow h h2
 lemma pow_lt_pow_iff (h : 1 < a) : a ^ n < a ^ m ↔ n < m :=
 (strict_mono_pow h).lt_iff_lt
 
+lemma strict_anti_pow (h₀ : 0 < a) (h₁ : a < 1) : strict_anti (λ n : ℕ, a ^ n) :=
+strict_anti_nat_of_succ_lt $ λ n,
+  by simpa only [pow_succ, one_mul] using mul_lt_mul h₁ le_rfl (pow_pos h₀ n) zero_le_one
+
+lemma pow_lt_pow_iff_of_lt_one (h₀ : 0 < a) (h₁ : a < 1) : a ^ m < a ^ n ↔ n < m :=
+(strict_anti_pow h₀ h₁).lt_iff_lt
+
+lemma pow_lt_pow_of_lt_one (h : 0 < a) (ha : a < 1) {i j : ℕ} (hij : i < j) : a ^ j < a ^ i :=
+(pow_lt_pow_iff_of_lt_one h ha).2 hij
+
 @[mono] lemma pow_le_pow_of_le_left {a b : R} (ha : 0 ≤ a) (hab : a ≤ b) : ∀ i : ℕ, a^i ≤ b^i
 | 0     := by simp
 | (k+1) := by { rw [pow_succ, pow_succ],
     exact mul_le_mul hab (pow_le_pow_of_le_left _) (pow_nonneg ha _) (le_trans ha hab) }
 
-lemma one_lt_pow (ha : 1 < a) : ∀ {n : ℕ}, n ≠ 0 → 1 < a ^ n
-| 0       h := (h rfl).elim
-| 1       h := (pow_one a).symm.subst ha
-| (n + 2) h :=
-  begin
-    nontriviality R,
-    rw [←one_mul (1 : R), pow_succ],
-    exact mul_lt_mul ha (one_lt_pow (nat.succ_ne_zero _)).le zero_lt_one (zero_lt_one.trans ha).le,
-  end
+lemma one_lt_pow (ha : 1 < a) {n : ℕ} (hn : n ≠ 0) : 1 < a ^ n :=
+pow_zero a ▸ pow_lt_pow ha (pos_iff_ne_zero.2 hn)
 
 lemma pow_le_one : ∀ (n : ℕ) (h₀ : 0 ≤ a) (h₁ : a ≤ 1), a ^ n ≤ 1
 | 0       h₀ h₁ := (pow_zero a).le

src/algebra/order/ring.lean

@@ -714,16 +714,14 @@ lemma mul_le_iff_le_one_left (hb : 0 < b) : a * b ≤ b ↔ a ≤ 1 :=
   λ h, le_of_not_lt (mt (lt_mul_iff_one_lt_left hb).1 h.not_lt) ⟩
 
 lemma mul_lt_iff_lt_one_left (hb : 0 < b) : a * b < b ↔ a < 1 :=
-⟨ λ h, lt_of_not_ge (mt (le_mul_iff_one_le_left hb).2 h.not_le),
-  λ h, lt_of_not_ge (mt (le_mul_iff_one_le_left hb).1 h.not_le) ⟩
+lt_iff_lt_of_le_iff_le $ le_mul_iff_one_le_left hb
 
 lemma mul_le_iff_le_one_right (hb : 0 < b) : b * a ≤ b ↔ a ≤ 1 :=
 ⟨ λ h, le_of_not_lt (mt (lt_mul_iff_one_lt_right hb).2 h.not_lt),
   λ h, le_of_not_lt (mt (lt_mul_iff_one_lt_right hb).1 h.not_lt) ⟩
 
 lemma mul_lt_iff_lt_one_right (hb : 0 < b) : b * a < b ↔ a < 1 :=
-⟨ λ h, lt_of_not_ge (mt (le_mul_iff_one_le_right hb).2 h.not_le),
-  λ h, lt_of_not_ge (mt (le_mul_iff_one_le_right hb).1 h.not_le) ⟩
+lt_iff_lt_of_le_iff_le $ le_mul_iff_one_le_right hb
 
 lemma nonpos_of_mul_nonneg_left (h : 0 ≤ a * b) (hb : b < 0) : a ≤ 0 :=
 le_of_not_gt (λ ha, absurd h (mul_neg_of_pos_of_neg ha hb).not_le)

src/data/real/nnreal.lean

@@ -488,12 +488,11 @@ section pow
 
 lemma pow_antitone_exp {a : ℝ≥0} (m n : ℕ) (mn : m ≤ n) (a1 : a ≤ 1) :
   a ^ n ≤ a ^ m :=
-begin
-  rcases le_iff_exists_add.mp mn with ⟨k, rfl⟩,
-  rw [← mul_one (a ^ m), pow_add],
-  refine mul_le_mul rfl.le (pow_le_one _ (zero_le a) a1) _ _;
-  exact pow_nonneg (zero_le _) _,
-end
+pow_le_pow_of_le_one (zero_le a) a1 mn
+
+lemma exists_pow_lt_of_lt_one {a b : ℝ≥0} (ha : 0 < a) (hb : b < 1) : ∃ n : ℕ, b ^ n < a :=
+by simpa only [← coe_pow, nnreal.coe_lt_coe]
+  using exists_pow_lt_of_lt_one (nnreal.coe_pos.2 ha) (nnreal.coe_lt_coe.2 hb)
 
 lemma exists_mem_Ico_zpow
   {x : ℝ≥0} {y : ℝ≥0} (hx : x ≠ 0) (hy : 1 < y) :