chore(*): more assumptions to lemmas that are removable (#13364)

This time I look at assumptions that are actually provable by simp from the earlier assumptions (fortunately there are only a couple of these), and one more from the review of #13316 that was slightly too nontrivial to be found automatically.

Author: alexjbest

src/analysis/special_functions/pow.lean

@@ -1113,8 +1113,8 @@ begin
     exact rpow_pos_of_nonneg (neg_pos.mpr hp_neg) },
 end
 
-lemma rpow_lt_one {x : ℝ≥0} {z : ℝ} (hx : 0 ≤ x) (hx1 : x < 1) (hz : 0 < z) : x^z < 1 :=
-real.rpow_lt_one hx hx1 hz
+lemma rpow_lt_one {x : ℝ≥0} {z : ℝ} (hx1 : x < 1) (hz : 0 < z) : x^z < 1 :=
+real.rpow_lt_one (coe_nonneg x) hx1 hz
 
 lemma rpow_le_one {x : ℝ≥0} {z : ℝ} (hx2 : x ≤ 1) (hz : 0 ≤ z) : x^z ≤ 1 :=
 real.rpow_le_one x.2 hx2 hz
@@ -1581,7 +1581,7 @@ lemma rpow_lt_one {x : ℝ≥0∞} {z : ℝ} (hx : x < 1) (hz : 0 < z) : x^z < 1
 begin
   lift x to ℝ≥0 using ne_of_lt (lt_of_lt_of_le hx le_top),
   simp only [coe_lt_one_iff] at hx,
-  simp [coe_rpow_of_nonneg _ (le_of_lt hz), nnreal.rpow_lt_one (zero_le x) hx hz],
+  simp [coe_rpow_of_nonneg _ (le_of_lt hz), nnreal.rpow_lt_one hx hz],
 end
 
 lemma rpow_le_one {x : ℝ≥0∞} {z : ℝ} (hx : x ≤ 1) (hz : 0 ≤ z) : x^z ≤ 1 :=

src/data/nat/log.lean

@@ -128,9 +128,12 @@ begin
   simp [hn, this]
 end
 
-lemma lt_pow_succ_log_self {b : ℕ} (hb : 1 < b) {x : ℕ} (hx : 0 < x) :
+lemma lt_pow_succ_log_self {b : ℕ} (hb : 1 < b) (x : ℕ) :
   x < b ^ (log b x).succ :=
 begin
+  cases x.eq_zero_or_pos with hx hx,
+  { simp only [hx, log_zero_right, pow_one],
+    exact pos_of_gt hb },
   rw [←not_le, pow_le_iff_le_log hb hx, not_le],
   exact lt_succ_self _,
 end

src/ring_theory/adjoin/basic.lean

@@ -83,17 +83,14 @@ lemma adjoin_induction₂ {p : A → A → Prop} {a b : A} (ha : a ∈ adjoin R
   (Hadd_left : ∀ x₁ x₂ y, p x₁ y → p x₂ y → p (x₁ + x₂) y)
   (Hadd_right : ∀ x y₁ y₂, p x y₁ → p x y₂ → p x (y₁ + y₂))
   (Hmul_left : ∀ x₁ x₂ y, p x₁ y → p x₂ y → p (x₁ * x₂) y)
-  (Hmul_right : ∀ x y₁ y₂, p x y₁ → p x y₂ → p x (y₁ * y₂))
-  (Hadd_alg : ∀ x y r, p x (algebra_map R A r) →
-                  p y (algebra_map R A r) → p (x + y) (algebra_map R A r))
-  (Hmul_alg : ∀ x y r, p x (algebra_map R A r) →
-                  p y (algebra_map R A r) → p (x * y) (algebra_map R A r)) : p a b :=
+  (Hmul_right : ∀ x y₁ y₂, p x y₁ → p x y₂ → p x (y₁ * y₂)) : p a b :=
 begin
   refine adjoin_induction hb _ (λ r, _) (Hadd_right a) (Hmul_right a),
   { exact adjoin_induction ha Hs Halg_left (λ x y Hx Hy z hz, Hadd_left x y z (Hx z hz) (Hy z hz))
       (λ x y Hx Hy z hz, Hmul_left x y z (Hx z hz) (Hy z hz)) },
-  { exact adjoin_induction ha (Halg_right r) (λ r', Halg r' r) (λ x y, Hadd_alg x y r)
-      (λ x y, Hmul_alg x y r) },
+  { exact adjoin_induction ha (Halg_right r) (λ r', Halg r' r)
+      (λ x y, Hadd_left x y ((algebra_map R A) r))
+      (λ x y, Hmul_left x y ((algebra_map R A) r)) },
 end
 
 /-- The difference with `algebra.adjoin_induction` is that this acts on the subtype. -/
@@ -236,8 +233,6 @@ def adjoin_comm_semiring_of_comm {s : set A} (hcomm : ∀ (a ∈ s) (b ∈ s), a
       (λ _ _ _ h₁ h₂, by simp only [add_mul, mul_add, h₁, h₂])
       (λ x₁ x₂ y₁ h₁ h₂, by rw [mul_assoc, h₂, ←mul_assoc y₁, ←h₁, mul_assoc x₁])
       (λ x₁ x₂ y₁ h₁ h₂, by rw [mul_assoc x₂, ←h₂, ←mul_assoc x₂, ←h₁, ←mul_assoc])
-      (λ _ _ _ _ _, by simp only [add_mul, mul_add, commutes])
-      (λ _ _ _ _ _, by rw [commutes])
   end,
   ..(adjoin R s).to_semiring }