[Merged by Bors] - feat: lemmas about parity and Nat.antidiagonal

Mathlib/Algebra/GroupPower/Ring.lean

@@ -201,7 +201,6 @@ theorem neg_pow (a : R) (n : ℕ) : (-a) ^ n = (-1) ^ n * a ^ n :=
 section
 set_option linter.deprecated false
 
-@[simp]
 theorem neg_pow_bit0 (a : R) (n : ℕ) : (-a) ^ bit0 n = a ^ bit0 n := by
   rw [pow_bit0', neg_mul_neg, pow_bit0']
 #align neg_pow_bit0 neg_pow_bit0
@@ -213,7 +212,6 @@ theorem neg_pow_bit1 (a : R) (n : ℕ) : (-a) ^ bit1 n = -a ^ bit1 n := by
 
 end
 
-@[simp]
 theorem neg_sq (a : R) : (-a) ^ 2 = a ^ 2 := by simp [sq]
 #align neg_sq neg_sq
 

Mathlib/Algebra/Parity.lean

@@ -129,6 +129,7 @@ theorem IsSquare_sq (a : α) : IsSquare (a ^ 2) :=
 
 variable [HasDistribNeg α]
 
+@[simp]
 theorem Even.neg_pow : Even n → ∀ a : α, (-a) ^ n = a ^ n := by
   rintro ⟨c, rfl⟩ a
   simp_rw [← two_mul, pow_mul, neg_sq]
@@ -351,6 +352,14 @@ theorem odd_two_mul_add_one (m : α) : Odd (2 * m + 1) :=
   ⟨m, rfl⟩
 #align odd_two_mul_add_one odd_two_mul_add_one
 
+@[simp] lemma odd_add_self_one : Odd (m + m + 1) := ⟨m, by rw [two_mul]⟩
+
+@[simp] lemma odd_add_self_one' : Odd (m + (m + 1)) := by simp [← add_assoc]
+
+@[simp] lemma odd_add_one_self : Odd (m + 1 + m) := by simp [add_comm _ m]
+
+@[simp] lemma odd_add_one_self' : Odd (m + (1 + m)) := by simp [add_comm]
+
 theorem Odd.map [RingHomClass F α β] (f : F) : Odd m → Odd (f m) := by
   rintro ⟨m, rfl⟩
   exact ⟨f m, by simp [two_mul]⟩
@@ -386,6 +395,7 @@ theorem Odd.neg_pow : Odd n → ∀ a : α, (-a) ^ n = -a ^ n := by
   simp_rw [pow_add, pow_mul, neg_sq, pow_one, mul_neg]
 #align odd.neg_pow Odd.neg_pow
 
+@[simp]
 theorem Odd.neg_one_pow (h : Odd n) : (-1 : α) ^ n = -1 := by rw [h.neg_pow, one_pow]
 #align odd.neg_one_pow Odd.neg_one_pow
 

Mathlib/Data/Finset/NatAntidiagonal.lean

@@ -126,6 +126,14 @@ theorem filter_snd_eq_antidiagonal (n m : ℕ) :
   simp [filter_map, this, filter_fst_eq_antidiagonal, apply_ite (Finset.map _)]
 #align finset.nat.filter_snd_eq_antidiagonal Finset.Nat.filter_snd_eq_antidiagonal
 
+@[simp] lemma antidiagonal_filter_le_fst {n : ℕ} :
+    (antidiagonal n).filter (fun a ↦ n ≤ a.fst) = {(n, 0)} := by
+  ext; aesop
+
+@[simp] lemma antidiagonal_filter_le_snd {n : ℕ} :
+    (antidiagonal n).filter (fun a ↦ n ≤ a.snd) = {(0, n)} := by
+  ext; aesop
+
 section EquivProd
 
 /-- The disjoint union of antidiagonals `Σ (n : ℕ), antidiagonal n` is equivalent to the product

Mathlib/NumberTheory/Cyclotomic/Discriminant.lean

@@ -153,7 +153,7 @@ theorem discr_prime_pow [hcycl : IsCyclotomicExtension {p ^ k} K L] [hp : Fact (
       minpoly.eq_X_sub_C_of_algebraMap_inj _ (algebraMap K L).injective, natDegree_X_sub_C]
     simp only [traceMatrix, map_one, one_pow, Matrix.det_unique, traceForm_apply, mul_one]
     rw [← (algebraMap K L).map_one, trace_algebraMap, finrank _ hirr]
-    simp; norm_num
+    simp
   · by_cases hk : p ^ (k + 1) = 2
     · have coe_two : 2 = ((2 : ℕ+) : ℕ) := rfl
       have hp : p = 2 := by
@@ -167,7 +167,6 @@ theorem discr_prime_pow [hcycl : IsCyclotomicExtension {p ^ k} K L] [hp : Fact (
       rw [add_left_eq_self] at hk
       rw [hp, hk] at hζ; norm_num at hζ; rw [← coe_two] at hζ
       rw [coe_basis, powerBasis_gen]; simp only [hp, hk]; norm_num
-      rw [← coe_two, totient_two, show 1 / 2 = 0 by rfl, _root_.pow_zero]
       -- Porting note: the goal at this point is `(discr K fun i ↦ ζ ^ ↑i) = 1`.
       -- This `simp_rw` is needed so the next `rw` can rewrite the type of `i` from
       -- `Fin (natDegree (minpoly K ζ))` to `Fin 1`