chore(algebra): trivial lemmas on powers (#4977)

Author: sgouezel

src/algebra/group_power/basic.lean

@@ -572,13 +572,15 @@ calc a ^ n = a ^ n * 1 : (mul_one _).symm
 
 lemma pow_lt_pow {a : R} {n m : ℕ} (h : 1 < a) (h2 : n < m) : a ^ n < a ^ m :=
 begin
-  nontriviality,
   have h' : 1 ≤ a := le_of_lt h,
   have h'' : 0 < a := lt_trans zero_lt_one h,
   cases m, cases h2, rw [pow_succ, ←one_mul (a ^ n)],
   exact mul_lt_mul h (pow_le_pow h' (nat.le_of_lt_succ h2)) (pow_pos h'' _) (le_of_lt h'')
 end
 
+lemma pow_lt_pow_iff {a : R} {n m : ℕ} (h : 1 < a) : a ^ n < a ^ m ↔ n < m :=
+strict_mono.lt_iff_lt $ λ m n, pow_lt_pow h
+
 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) := mul_le_mul hab (pow_le_pow_of_le_left _) (pow_nonneg ha _) (le_trans ha hab)

src/algebra/group_power/lemmas.lean

@@ -323,6 +323,13 @@ lemma pow_lt_pow_of_lt_one  {a : R} (h : 0 < a) (ha : a < 1)
 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 {a : R} {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  {a : R} (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_with_zero_power.lean

@@ -239,6 +239,10 @@ theorem one_div_fpow {a : G₀} (n : ℤ) :
   (1 / a) ^ n = 1 / a ^ n :=
 by simp only [one_div, inv_fpow]
 
+@[simp] lemma inv_fpow' {a : G₀} (n : ℤ) :
+  (a ⁻¹) ^ n = a ^ (-n) :=
+by { rw [inv_fpow, ← fpow_neg_one, ← fpow_mul], simp }
+
 end int_pow
 
 section

src/analysis/calculus/darboux.lean

@@ -46,7 +46,7 @@ begin
       simpa [-sub_nonneg, -continuous_linear_map.map_sub]
         using hc.localize.has_fderiv_within_at_nonneg (hg a (left_mem_Icc.2 hab)) this },
     cases eq_or_lt_of_le cmem.2 with hbc hbc,
-    -- Show that `c` can't be equal to `a`
+    -- Show that `c` can't be equal to `b`
     { subst c,
       refine absurd (sub_nonpos.1 $ nonpos_of_mul_nonneg_right _ (sub_lt_zero.2 hab'))
         (not_le_of_lt hmb),

src/analysis/calculus/extend_deriv.lean

@@ -47,7 +47,7 @@ begin
   /- One needs to show that `∥f y - f x - f' (y - x)∥ ≤ ε ∥y - x∥` for `y` close to `x` in `closure
   s`, where `ε` is an arbitrary positive constant. By continuity of the functions, it suffices to
   prove this for nearby points inside `s`. In a neighborhood of `x`, the derivative of `f` is
-  arbitrarily close to f' by assumption. The mean value inequality completes the proof. -/
+  arbitrarily close to `f'` by assumption. The mean value inequality completes the proof. -/
   assume ε ε_pos,
   obtain ⟨δ, δ_pos, hδ⟩ : ∃ δ > 0, ∀ y ∈ s, dist y x < δ → ∥fderiv ℝ f y - f'∥ < ε,
     by simpa [dist_zero_right] using tendsto_nhds_within_nhds.1 h ε ε_pos,