feat: add a few simp lemmas (#8750)

* Remove simp-lemma `bitwise_of_ne_zero`, since it wasn't used, and could cause loops in an inconsistent context.
leanprover-community · Nov 30, 2023 · 89670c5 · 89670c5
1 parent d9ec145
commit 89670c5
Show file tree

Hide file tree

Showing 10 changed files with 11 additions and 20 deletions.
diff --git a/Mathlib/Algebra/CharZero/Lemmas.lean b/Mathlib/Algebra/CharZero/Lemmas.lean
@@ -21,7 +21,6 @@ with `1`.
 * Characteristic zero implies that the additive monoid is infinite.
 -/
 
-
 namespace Nat
 
 variable {R : Type*} [AddMonoidWithOne R] [CharZero R]
@@ -98,11 +97,11 @@ section
 
 variable {R : Type*} [NonAssocRing R] [NoZeroDivisors R] [CharZero R]
 
-theorem neg_eq_self_iff {a : R} : -a = a ↔ a = 0 :=
+@[simp] theorem neg_eq_self_iff {a : R} : -a = a ↔ a = 0 :=
   neg_eq_iff_add_eq_zero.trans add_self_eq_zero
 #align neg_eq_self_iff neg_eq_self_iff
 
-theorem eq_neg_self_iff {a : R} : a = -a ↔ a = 0 :=
+@[simp] theorem eq_neg_self_iff {a : R} : a = -a ↔ a = 0 :=
   eq_neg_iff_add_eq_zero.trans add_self_eq_zero
 #align eq_neg_self_iff eq_neg_self_iff
 

diff --git a/Mathlib/Algebra/GroupPower/Ring.lean b/Mathlib/Algebra/GroupPower/Ring.lean
@@ -66,6 +66,7 @@ theorem pow_eq_zero_iff [NoZeroDivisors M] {a : M} {n : ℕ} (hn : 0 < n) : a ^
   exact zero_pow hn
 #align pow_eq_zero_iff pow_eq_zero_iff
 
+@[simp]
 theorem pow_eq_zero_iff' [NoZeroDivisors M] [Nontrivial M] {a : M} {n : ℕ} :
     a ^ n = 0 ↔ a = 0 ∧ n ≠ 0 := by cases (zero_le n).eq_or_gt <;> simp [*, ne_of_gt]
 #align pow_eq_zero_iff' pow_eq_zero_iff'

diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean
@@ -233,7 +233,7 @@ theorem tendsto_pow_const_mul_const_pow_of_abs_lt_one (k : ℕ) {r : ℝ} (hr :
     Tendsto (fun n ↦ (n : ℝ) ^ k * r ^ n : ℕ → ℝ) atTop (𝓝 0) := by
   by_cases h0 : r = 0
   · exact tendsto_const_nhds.congr'
-      (mem_atTop_sets.2 ⟨1, fun n hn ↦ by simp [zero_lt_one.trans_le hn, h0]⟩)
+      (mem_atTop_sets.2 ⟨1, fun n hn ↦ by simp [zero_lt_one.trans_le hn |>.ne', h0]⟩)
   have hr' : 1 < |r|⁻¹ := one_lt_inv (abs_pos.2 h0) hr
   rw [tendsto_zero_iff_norm_tendsto_zero]
   simpa [div_eq_mul_inv] using tendsto_pow_const_div_const_pow_of_one_lt k hr'

diff --git a/Mathlib/Data/Int/ModEq.lean b/Mathlib/Data/Int/ModEq.lean
@@ -42,7 +42,7 @@ instance : Decidable (ModEq n a b) := decEq (a % n) (b % n)
 
 namespace ModEq
 
-@[refl]
+@[refl, simp]
 protected theorem refl (a : ℤ) : a ≡ a [ZMOD n] :=
   @rfl _ _
 #align int.modeq.refl Int.ModEq.refl

diff --git a/Mathlib/Data/Int/Order/Units.lean b/Mathlib/Data/Int/Order/Units.lean
@@ -48,9 +48,7 @@ theorem units_coe_mul_self (u : ℤˣ) : (u * u : ℤ) = 1 := by
   rw [← Units.val_mul, units_mul_self, Units.val_one]
 #align int.units_coe_mul_self Int.units_coe_mul_self
 
-@[simp]
-theorem neg_one_pow_ne_zero {n : ℕ} : (-1 : ℤ) ^ n ≠ 0 :=
-  pow_ne_zero _ (abs_pos.mp (by simp))
+theorem neg_one_pow_ne_zero {n : ℕ} : (-1 : ℤ) ^ n ≠ 0 := by simp
 #align int.neg_one_pow_ne_zero Int.neg_one_pow_ne_zero
 
 theorem sq_eq_one_of_sq_lt_four {x : ℤ} (h1 : x ^ 2 < 4) (h2 : x ≠ 0) : x ^ 2 = 1 :=

diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean
@@ -61,7 +61,6 @@ lemma bitwise_zero : bitwise f 0 0 = 0 := by
   simp only [bitwise_zero_right, ite_self]
 #align nat.bitwise_zero Nat.bitwise_zero
 
-@[simp]
 lemma bitwise_of_ne_zero {n m : Nat} (hn : n ≠ 0) (hm : m ≠ 0) :
     bitwise f n m = bit (f (bodd n) (bodd m)) (bitwise f (n / 2) (m / 2)) := by
   conv_lhs => unfold bitwise

diff --git a/Mathlib/Geometry/Euclidean/Triangle.lean b/Mathlib/Geometry/Euclidean/Triangle.lean
@@ -238,14 +238,9 @@ theorem angle_add_angle_sub_add_angle_sub_eq_pi {x y : V} (hx : x ≠ 0) (hy : y
     replace h3lt := lt_of_mul_lt_mul_right h3lt (le_of_lt Real.pi_pos)
     norm_cast at h3lt
   interval_cases n
-  · rw [hn] at hcos
-    simp at hcos
-    norm_num at hcos
-  · rw [hn]
-    norm_num
-  · rw [hn] at hcos
-    simp at hcos
-    norm_num at hcos
+  · simp [hn] at hcos
+  · norm_num [hn]
+  · simp [hn] at hcos
 #align inner_product_geometry.angle_add_angle_sub_add_angle_sub_eq_pi InnerProductGeometry.angle_add_angle_sub_add_angle_sub_eq_pi
 
 end InnerProductGeometry

diff --git a/Mathlib/RingTheory/Polynomial/IntegralNormalization.lean b/Mathlib/RingTheory/Polynomial/IntegralNormalization.lean
@@ -99,7 +99,7 @@ theorem support_integralNormalization {f : R[X]} :
   refine' ⟨fun h => integralNormalization_support h, _⟩
   simp only [integralNormalization_coeff, mem_support_iff]
   intro hfi
-  split_ifs with hi <;> simp [hfi, hi, pow_ne_zero _ (leadingCoeff_ne_zero.mpr hf)]
+  split_ifs with hi <;> simp [hf, hfi, hi]
 #align polynomial.support_integral_normalization Polynomial.support_integralNormalization
 
 end IsDomain

diff --git a/Mathlib/RingTheory/WittVector/Frobenius.lean b/Mathlib/RingTheory/WittVector/Frobenius.lean
@@ -189,7 +189,7 @@ theorem map_frobeniusPoly (n : ℕ) :
         (p : ℚ) ^ (n - i - v p ⟨j + 1, j.succ_pos⟩) by
     have aux : ∀ k : ℕ, (p : ℚ)^ k ≠ 0 := by
       intro; apply pow_ne_zero; exact mod_cast hp.1.ne_zero
-    simpa [aux, -one_div, field_simps] using this.symm
+    simpa [aux, -one_div, -pow_eq_zero_iff', field_simps] using this.symm
   rw [mul_comm _ (p : ℚ), mul_assoc, mul_assoc, ← pow_add,
     map_frobeniusPoly.key₂ p hi.le hj, Nat.cast_mul, Nat.cast_pow]
   ring

diff --git a/Mathlib/Topology/MetricSpace/PiNat.lean b/Mathlib/Topology/MetricSpace/PiNat.lean
@@ -308,7 +308,6 @@ protected theorem dist_triangle (x y z : ∀ n, E n) : dist x z ≤ dist x y + d
 protected theorem eq_of_dist_eq_zero (x y : ∀ n, E n) (hxy : dist x y = 0) : x = y := by
   rcases eq_or_ne x y with (rfl | h); · rfl
   simp [dist_eq_of_ne h] at hxy
-  exact (two_ne_zero (pow_eq_zero hxy)).elim
 #align pi_nat.eq_of_dist_eq_zero PiNat.eq_of_dist_eq_zero
 
 theorem mem_cylinder_iff_dist_le {x y : ∀ n, E n} {n : ℕ} :