[Merged by Bors] - refactor(algebra/group_power, data/nat/basic): remove redundant lemmas

archive/imo/imo1988_q6.lean

@@ -24,7 +24,7 @@ To illustrate the technique, we also prove a similar result.
 -- open_locale classical
 
 local attribute [instance] classical.prop_decidable
-local attribute [simp] nat.pow_two
+local attribute [simp] pow_two
 
 /-- Constant descent Vieta jumping.
 
@@ -187,7 +187,7 @@ lemma imo1988_q6 {a b : ℕ} (h : (a*b+1) ∣ a^2 + b^2) :
 begin
   rcases h with ⟨k, hk⟩,
   rw [hk, nat.mul_div_cancel_left _ (nat.succ_pos (a*b))],
-  simp only [nat.pow_two] at hk,
+  simp only [pow_two] at hk,
   apply constant_descent_vieta_jumping a b hk (λ x, k * x) (λ x, x*x - k) (λ x y, false);
   clear hk a b,
   { -- We will now show that the fibers of the solution set are described by a quadratic equation.
@@ -246,7 +246,7 @@ example {a b : ℕ} (h : a*b ∣ a^2 + b^2 + 1) :
 begin
   rcases h with ⟨k, hk⟩,
   suffices : k = 3, { simp * at *, ring, },
-  simp only [nat.pow_two] at hk,
+  simp only [pow_two] at hk,
   apply constant_descent_vieta_jumping a b hk (λ x, k * x) (λ x, x*x + 1) (λ x y, x ≤ 1);
   clear hk a b,
   { -- We will now show that the fibers of the solution set are described by a quadratic equation.

archive/miu_language/decision_suf.lean

@@ -56,7 +56,7 @@ private lemma der_cons_repeat (n : ℕ) : derivable (M::(repeat I (2^n))) :=
 begin
   induction n with k hk,
   { constructor, }, -- base case
-  { rw [succ_eq_add_one, nat.pow_add, nat.pow_one 2, mul_two,repeat_add], -- inductive step
+  { rw [succ_eq_add_one, pow_add, pow_one 2, mul_two,repeat_add], -- inductive step
     exact derivable.r2 hk, },
 end
 
@@ -157,10 +157,10 @@ begin
     { use g, exact ⟨hp,hgmod⟩ },
     use (g+2),
     { split,
-      { rw [mul_succ, ←add_assoc,nat.pow_add],
+      { rw [mul_succ, ←add_assoc, pow_add],
         change 2^2 with (1+3), rw [mul_add (2^g) 1 3, mul_one],
         linarith [hkg, one_le_two_pow g], },
-      { rw [nat.pow_add,←mul_one c],
+      { rw [pow_add,←mul_one c],
         exact modeq.modeq_mul hgmod rfl, }, }, },
 end
 

archive/sensitivity.lean

@@ -373,7 +373,7 @@ begin
   rw ← findim_eq_dim ℝ at ⊢ dim_le dim_add dimW,
   rw [← findim_eq_dim ℝ, ← findim_eq_dim ℝ] at dim_add,
   norm_cast at ⊢ dim_le dim_add dimW,
-  rw nat.pow_succ at dim_le,
+  rw pow_succ' at dim_le,
   rw set.to_finset_card at hH,
   linarith
 end

src/algebra/associated.lean

@@ -179,7 +179,7 @@ lemma succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul [comm_cancel_monoid_with_zero α]
   p ^ k ∣ a → p ^ l ∣ b → p ^ ((k + l) + 1) ∣ a * b → p ^ (k + 1) ∣ a ∨ p ^ (l + 1) ∣ b :=
 λ ⟨x, hx⟩ ⟨y, hy⟩ ⟨z, hz⟩,
 have h : p ^ (k + l) * (x * y) = p ^ (k + l) * (p * z),
-  by simpa [mul_comm, _root_.pow_add, hx, hy, mul_assoc, mul_left_comm] using hz,
+  by simpa [mul_comm, pow_add, hx, hy, mul_assoc, mul_left_comm] using hz,
 have hp0: p ^ (k + l) ≠ 0, from pow_ne_zero _ hp.ne_zero,
 have hpd : p ∣ x * y, from ⟨z, by rwa [mul_right_inj' hp0] at h⟩,
 (hp.div_or_div hpd).elim

src/algebra/big_operators/basic.lean

@@ -677,12 +677,7 @@ by rw [prod_insert has, card_insert_of_not_mem has, pow_succ, ih])
 lemma prod_pow (s : finset α) (n : ℕ) (f : α → β) :
   (∏ x in s, f x ^ n) = (∏ x in s, f x) ^ n :=
 by haveI := classical.dec_eq α; exact
-finset.induction_on s (by simp) (by simp [_root_.mul_pow] {contextual := tt})
-
-lemma prod_nat_pow (s : finset α) (n : ℕ) (f : α → ℕ) :
-  (∏ x in s, f x ^ n) = (∏ x in s, f x) ^ n :=
-by haveI := classical.dec_eq α; exact
-finset.induction_on s (by simp) (by simp [nat.mul_pow] {contextual := tt})
+finset.induction_on s (by simp) (by simp [mul_pow] {contextual := tt})
 
 -- `to_additive` fails on this lemma, so we prove it manually below
 lemma prod_flip {n : ℕ} (f : ℕ → β) :

src/algebra/char_p.lean

@@ -98,7 +98,7 @@ theorem add_pow_char_pow_of_commute (R : Type u) [ring R] {p : ℕ} [fact p.prim
   (x + y) ^ (p ^ n) = x ^ (p ^ n) + y ^ (p ^ n) :=
 begin
   induction n, { simp, },
-  rw [nat.pow_succ, pow_mul, pow_mul, pow_mul, n_ih],
+  rw [pow_succ', pow_mul, pow_mul, pow_mul, n_ih],
   apply add_pow_char_of_commute, apply commute.pow_pow h,
 end
 
@@ -115,7 +115,7 @@ theorem sub_pow_char_pow_of_commute (R : Type u) [ring R] {p : ℕ} [fact p.prim
   (x - y) ^ (p ^ n) = x ^ (p ^ n) - y ^ (p ^ n) :=
 begin
   induction n, { simp, },
-  rw [nat.pow_succ, pow_mul, pow_mul, pow_mul, n_ih],
+  rw [pow_succ', pow_mul, pow_mul, pow_mul, n_ih],
   apply sub_pow_char_of_commute, apply commute.pow_pow h,
 end
 
@@ -174,7 +174,7 @@ theorem frobenius_def : frobenius R p x = x ^ p := rfl
 theorem iterate_frobenius (n : ℕ) : (frobenius R p)^[n] x = x ^ p ^ n :=
 begin
   induction n, {simp},
-  rw [function.iterate_succ', nat.pow_succ, pow_mul, function.comp_apply, frobenius_def, n_ih]
+  rw [function.iterate_succ', pow_succ', pow_mul, function.comp_apply, frobenius_def, n_ih]
 end
 
 theorem frobenius_mul : frobenius R p (x * y) = frobenius R p x * frobenius R p y :=