chore(*): remove some defeq abuse of ^ (#18136)

There are various places where the proofs relied on the defeq of `^`, namely that

* `rfl : x ^ 0 = 1`
* `rfl : x ^ (n : ℕ) = x ^ (↑n : ℤ)`
* `rfl : x ^ (n.succ : ℕ) = x * x ^ n`

While exploiting defeq is not always a bad thing, in some of these cases it was clear that this wasn't intentional, and the author had not noticed that they were working with integer instead of natural powers.

This change is motivated by two possible refactors:

* Changing the definition of `monoid.npow_rec` to match `function.iterate`
* Changing the definition of `real.has_pow` to be the elementwise power on the cauchy sequence (#8146)

src/analysis/special_functions/bernstein.lean

@@ -192,7 +192,8 @@ lemma le_of_mem_S_compl
   (1 : ℝ) ≤ (δ f ε h)^(-2 : ℤ) * (x - k/ₙ) ^ 2 :=
 begin
   simp only [finset.mem_compl, not_lt, set.mem_to_finset, set.mem_set_of_eq, S] at m,
-  erw [zpow_neg, ← div_eq_inv_mul, one_le_div (pow_pos δ_pos 2), sq_le_sq, abs_of_pos δ_pos],
+  rw [zpow_neg, ← div_eq_inv_mul, zpow_two, ←pow_two, one_le_div (pow_pos δ_pos 2), sq_le_sq,
+    abs_of_pos δ_pos],
   rwa [dist_comm] at m
 end
 

src/analysis/special_functions/integrals.lean

@@ -265,7 +265,7 @@ begin
 end
 
 @[simp] lemma integral_pow : ∫ x in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (n + 1) :=
-by simpa using integral_zpow (or.inl (int.coe_nat_nonneg n))
+by simpa only [←int.coe_nat_succ, zpow_coe_nat] using integral_zpow (or.inl (int.coe_nat_nonneg n))
 
 /-- Integral of `|x - a| ^ n` over `Ι a b`. This integral appears in the proof of the
 Picard-Lindelöf/Cauchy-Lipschitz theorem. -/

src/analysis/special_functions/pow.lean

@@ -570,13 +570,13 @@ by rw [rpow_def, complex.of_real_add, complex.cpow_add _ _ (complex.of_real_ne_z
   complex.of_real_mul_re, ← rpow_def, mul_comm]
 
 lemma rpow_add_nat {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℕ) : x ^ (y + n) = x ^ y * x ^ n :=
-rpow_add_int hx y n
+by simpa using rpow_add_int hx y n
 
 lemma rpow_sub_int {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℤ) : x ^ (y - n) = x ^ y / x ^ n :=
 by simpa using rpow_add_int hx y (-n)
 
 lemma rpow_sub_nat {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℕ) : x ^ (y - n) = x ^ y / x ^ n :=
-rpow_sub_int hx y n
+by simpa using rpow_sub_int hx y n
 
 lemma rpow_add_one {x : ℝ} (hx : x ≠ 0) (y : ℝ) : x ^ (y + 1) = x ^ y * x :=
 by simpa using rpow_add_nat hx y 1
@@ -589,7 +589,7 @@ by simp only [rpow_def, ← complex.of_real_zpow, complex.cpow_int_cast,
   complex.of_real_int_cast, complex.of_real_re]
 
 @[simp, norm_cast] lemma rpow_nat_cast (x : ℝ) (n : ℕ) : x ^ (n : ℝ) = x ^ n :=
-rpow_int_cast x n
+by simpa using rpow_int_cast x n
 
 @[simp] lemma rpow_two (x : ℝ) : x ^ (2 : ℝ) = x ^ 2 :=
 by { rw ← rpow_nat_cast, simp only [nat.cast_bit0, nat.cast_one] }
@@ -1121,7 +1121,7 @@ by simpa only [rpow_int_cast] using is_o_rpow_exp_pos_mul_at_top k hb
 /-- `x ^ k = o(exp(b * x))` as `x → ∞` for any natural `k` and positive `b`. -/
 lemma is_o_pow_exp_pos_mul_at_top (k : ℕ) {b : ℝ} (hb : 0 < b) :
   (λ x : ℝ, x ^ k) =o[at_top] (λ x, exp (b * x)) :=
-is_o_zpow_exp_pos_mul_at_top k hb
+by simpa using is_o_zpow_exp_pos_mul_at_top k hb
 
 /-- `x ^ s = o(exp x)` as `x → ∞` for any real `s`. -/
 lemma is_o_rpow_exp_at_top (s : ℝ) : (λ x : ℝ, x ^ s) =o[at_top] exp :=

src/analysis/special_functions/stirling.lean

@@ -104,7 +104,9 @@ begin
   have h_nonneg : 0 ≤ ((1 / (2 * (n.succ : ℝ) + 1)) ^ 2) := sq_nonneg _,
   have g : has_sum (λ k : ℕ, ((1 / (2 * (n.succ : ℝ) + 1)) ^ 2) ^ k.succ)
     ((1 / (2 * n.succ + 1)) ^ 2 / (1 - (1 / (2 * n.succ + 1)) ^ 2)),
-  { refine (has_sum_geometric_of_lt_1 h_nonneg _).mul_left ((1 / (2 * (n.succ : ℝ) + 1)) ^ 2),
+  { have := (has_sum_geometric_of_lt_1 h_nonneg _).mul_left ((1 / (2 * (n.succ : ℝ) + 1)) ^ 2),
+    { simp_rw ←pow_succ at this,
+      exact this, },
     rw [one_div, inv_pow],
     exact inv_lt_one (one_lt_pow ((lt_add_iff_pos_left 1).mpr $ by positivity) two_ne_zero) },
   have hab : ∀ (k : ℕ), (1 / (2 * (k.succ : ℝ) + 1)) * ((1 / (2 * n.succ + 1)) ^ 2) ^ k.succ ≤

src/data/real/cardinality.lean

@@ -66,6 +66,10 @@ lemma cantor_function_aux_eq (h : f n = g n) :
   cantor_function_aux c f n = cantor_function_aux c g n :=
 by simp [cantor_function_aux, h]
 
+lemma cantor_function_aux_zero (f : ℕ → bool) :
+  cantor_function_aux c f 0 = cond (f 0) 1 0 :=
+by { cases h : f 0; simp [h] }
+
 lemma cantor_function_aux_succ (f : ℕ → bool) :
   (λ n, cantor_function_aux c f (n + 1)) = λ n, c * cantor_function_aux c (λ n, f (n + 1)) n :=
 by { ext n, cases h : f (n + 1); simp [h, pow_succ] }
@@ -122,9 +126,9 @@ begin
     { rw [cantor_function_succ _ (le_of_lt h1) h3, div_eq_mul_inv,
           ←tsum_geometric_of_lt_1 (le_of_lt h1) h3],
       apply zero_add },
-    { convert tsum_eq_single 0 _,
-      { apply_instance },
-      { intros n hn, cases n, contradiction, refl } } },
+    { refine (tsum_eq_single 0 _).trans _,
+      { intros n hn, cases n, contradiction, refl },
+      { exact cantor_function_aux_zero _ }, } },
   rw [cantor_function_succ f (le_of_lt h1) h3, cantor_function_succ g (le_of_lt h1) h3],
   rw [hn 0 $ zero_lt_succ n],
   apply add_lt_add_left, rw mul_lt_mul_left h1, exact ih (λ k hk, hn _ $ nat.succ_lt_succ hk) fn gn

src/data/real/irrational.lean

@@ -351,7 +351,7 @@ theorem of_pow : ∀ n : ℕ, irrational (x^n) → irrational x
 | (n+1) := λ h, by { rw pow_succ at h, exact h.mul_cases.elim id (of_pow n) }
 
 theorem of_zpow : ∀ m : ℤ, irrational (x^m) → irrational x
-| (n:ℕ) := of_pow n
+| (n:ℕ) := λ h, by { rw zpow_coe_nat at h, exact h.of_pow _ }
 | -[1+n] := λ h, by { rw zpow_neg_succ_of_nat at h, exact h.of_inv.of_pow _ }
 
 end irrational

src/number_theory/padics/padic_integers.lean

@@ -314,7 +314,7 @@ begin
   { simp [hx] },
   have h : (1 : ℝ) < p := by exact_mod_cast hp.1.one_lt,
   rw [← neg_nonpos, ← (zpow_strict_mono h).le_iff_le],
-  show (p : ℝ) ^ -valuation x ≤ p ^ 0,
+  show (p : ℝ) ^ -valuation x ≤ p ^ (0 : ℤ),
   rw [← norm_eq_pow_val hx],
   simpa using x.property
 end

src/topology/metric_space/lipschitz.lean

@@ -240,7 +240,7 @@ end
 
 protected lemma iterate {f : α → α} (hf : lipschitz_with K f) :
   ∀n, lipschitz_with (K ^ n) (f^[n])
-| 0       := lipschitz_with.id
+| 0       := by simpa only [pow_zero] using lipschitz_with.id
 | (n + 1) := by rw [pow_succ']; exact (iterate n).comp hf
 
 lemma edist_iterate_succ_le_geometric {f : α → α} (hf : lipschitz_with K f) (x n) :
@@ -265,7 +265,7 @@ protected lemma list_prod (f : ι → function.End α) (K : ι → ℝ≥0)
 
 protected lemma pow {f : function.End α} {K} (h : lipschitz_with K f) :
   ∀ n : ℕ, lipschitz_with (K^n) (f^n : function.End α)
-| 0       := lipschitz_with.id
+| 0       := by simpa only [pow_zero] using lipschitz_with.id
 | (n + 1) := by { rw [pow_succ, pow_succ], exact h.mul (pow n) }
 
 end emetric

src/topology/metric_space/pi_nat.lean

@@ -709,6 +709,7 @@ begin
       apply apply_first_diff_ne hne',
       rw [le_zero_iff.1 h],
       apply apply_eq_of_dist_lt _ le_rfl,
+      rw pow_zero,
       exact hxy },
     have hn : first_diff x.1 y.1 = n + 1 := (nat.succ_pred_eq_of_pos diff_pos).symm,
     rw [dist', dist_eq_of_ne hne', hn],