feat: lemmas about parity and Nat.antidiagonal (#6540)

Author: ocfnash

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]
@@ -329,6 +330,9 @@ theorem Even.add_odd : Even m → Odd n → Odd (m + n) := by
   exact ⟨m + n, by rw [mul_add, ← two_mul, add_assoc]⟩
 #align even.add_odd Even.add_odd
 
+theorem Even.odd_add : Even m → Odd n → Odd (n + m) :=
+  fun he ho ↦ by simp only [he.add_odd ho, add_comm n m]
+
 theorem Odd.add_even (hm : Odd m) (hn : Even n) : Odd (m + n) := by
   rw [add_comm]
   exact hn.add_odd hm
@@ -346,11 +350,22 @@ theorem odd_one : Odd (1 : α) :=
   ⟨0, (zero_add _).symm.trans (congr_arg (· + (1 : α)) (mul_zero _).symm)⟩
 #align odd_one odd_one
 
-@[simp]
+@[simp] lemma Even.add_one (h : Even m) : Odd (m + 1) := h.add_odd odd_one
+
+@[simp] lemma Even.one_add (h : Even m) : Odd (1 + m) := h.odd_add odd_one
+
 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)) := 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 1 m]
+
+@[simp] lemma one_add_self_self : Odd (1 + m + m) := by simp [add_comm 1 m]
+
 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 +401,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

@@ -20,6 +20,7 @@ generally for sums going from `0` to `n`.
 This refines files `Data.List.NatAntidiagonal` and `Data.Multiset.NatAntidiagonal`.
 -/
 
+open Function
 
 namespace Finset
 
@@ -51,7 +52,7 @@ theorem antidiagonal_succ (n : ℕ) :
     antidiagonal (n + 1) =
       cons (0, n + 1)
         ((antidiagonal n).map
-          (Function.Embedding.prodMap ⟨Nat.succ, Nat.succ_injective⟩ (Function.Embedding.refl _)))
+          (Embedding.prodMap ⟨Nat.succ, Nat.succ_injective⟩ (Embedding.refl _)))
         (by simp) := by
   apply eq_of_veq
   rw [cons_val, map_val]
@@ -62,7 +63,7 @@ theorem antidiagonal_succ' (n : ℕ) :
     antidiagonal (n + 1) =
       cons (n + 1, 0)
         ((antidiagonal n).map
-          (Function.Embedding.prodMap (Function.Embedding.refl _) ⟨Nat.succ, Nat.succ_injective⟩))
+          (Embedding.prodMap (Embedding.refl _) ⟨Nat.succ, Nat.succ_injective⟩))
         (by simp) := by
   apply eq_of_veq
   rw [cons_val, map_val]
@@ -74,19 +75,24 @@ theorem antidiagonal_succ_succ' {n : ℕ} :
       cons (0, n + 2)
         (cons (n + 2, 0)
             ((antidiagonal n).map
-              (Function.Embedding.prodMap ⟨Nat.succ, Nat.succ_injective⟩
+              (Embedding.prodMap ⟨Nat.succ, Nat.succ_injective⟩
                 ⟨Nat.succ, Nat.succ_injective⟩)) <|
           by simp)
         (by simp) := by
   simp_rw [antidiagonal_succ (n + 1), antidiagonal_succ', Finset.map_cons, map_map]
   rfl
 #align finset.nat.antidiagonal_succ_succ' Finset.Nat.antidiagonal_succ_succ'
 
-theorem map_swap_antidiagonal {n : ℕ} :
+/-- See also `Finset.map.map_prodComm_antidiagonal`. -/
+@[simp] theorem map_swap_antidiagonal {n : ℕ} :
     (antidiagonal n).map ⟨Prod.swap, Prod.swap_injective⟩ = antidiagonal n :=
   eq_of_veq <| by simp [antidiagonal, Multiset.Nat.map_swap_antidiagonal]
 #align finset.nat.map_swap_antidiagonal Finset.Nat.map_swap_antidiagonal
 
+@[simp] theorem map_prodComm_antidiagonal {n : ℕ} :
+    (antidiagonal n).map (Equiv.prodComm ℕ ℕ) = antidiagonal n :=
+  map_swap_antidiagonal
+
 /-- A point in the antidiagonal is determined by its first co-ordinate. -/
 theorem antidiagonal_congr {n : ℕ} {p q : ℕ × ℕ} (hp : p ∈ antidiagonal n)
     (hq : q ∈ antidiagonal n) : p = q ↔ p.fst = q.fst := by
@@ -122,10 +128,61 @@ theorem filter_snd_eq_antidiagonal (n m : ℕ) :
     filter (fun x : ℕ × ℕ ↦ x.snd = m) (antidiagonal n) = if m ≤ n then {(n - m, m)} else ∅ := by
   have : (fun x : ℕ × ℕ ↦ (x.snd = m)) ∘ Prod.swap = fun x : ℕ × ℕ ↦ x.fst = m := by
     ext; simp
-  rw [← map_swap_antidiagonal]
-  simp [filter_map, this, filter_fst_eq_antidiagonal, apply_ite (Finset.map _)]
+  rw [← map_swap_antidiagonal, filter_map]
+  simp [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_snd_le_of_le {n k : ℕ} (h : k ≤ n) :
+    (antidiagonal n).filter (fun a ↦ a.snd ≤ k) = (antidiagonal k).map
+      (Embedding.prodMap ⟨_, add_left_injective (n - k)⟩ (Embedding.refl ℕ)) := by
+  ext ⟨i, j⟩
+  suffices : i + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i
+  · simpa
+  refine' ⟨fun hi ↦ ⟨k - j, tsub_add_cancel_of_le hi.2, _⟩, _⟩
+  · rw [add_comm, tsub_add_eq_add_tsub h, ← hi.1, add_assoc, Nat.add_sub_of_le hi.2,
+      add_tsub_cancel_right]
+  · rintro ⟨l, hl, rfl⟩
+    refine' ⟨_, hl ▸ Nat.le_add_left j l⟩
+    rw [add_assoc, add_comm, add_assoc, add_comm j l, hl]
+    exact Nat.sub_add_cancel h
+
+@[simp] lemma antidiagonal_filter_fst_le_of_le {n k : ℕ} (h : k ≤ n) :
+    (antidiagonal n).filter (fun a ↦ a.fst ≤ k) = (antidiagonal k).map
+      (Embedding.prodMap (Embedding.refl ℕ) ⟨_, add_left_injective (n - k)⟩) := by
+  have aux₁ : fun a ↦ a.fst ≤ k = (fun a ↦ a.snd ≤ k) ∘ (Equiv.prodComm ℕ ℕ).symm := rfl
+  have aux₂ : ∀ i j, (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔
+                      ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j :=
+    fun i j ↦ by rw [exists_comm]; exact exists₂_congr (fun a b ↦ by rw [add_comm])
+  rw [← map_prodComm_antidiagonal]
+  simp_rw [aux₁, ← map_filter, antidiagonal_filter_snd_le_of_le h, map_map]
+  ext ⟨i, j⟩
+  simpa using aux₂ i j
+
+@[simp] lemma antidiagonal_filter_le_fst_of_le {n k : ℕ} (h : k ≤ n) :
+    (antidiagonal n).filter (fun a ↦ k ≤ a.fst) = (antidiagonal (n - k)).map
+      (Embedding.prodMap ⟨_, add_left_injective k⟩ (Embedding.refl ℕ)) := by
+  ext ⟨i, j⟩
+  suffices : i + j = n ∧ k ≤ i ↔ ∃ a, a + j = n - k ∧ a + k = i
+  · simpa
+  refine' ⟨fun hi ↦ ⟨i - k, _, tsub_add_cancel_of_le hi.2⟩, _⟩
+  · rw [← Nat.sub_add_comm hi.2, hi.1]
+  · rintro ⟨l, hl, rfl⟩
+    refine' ⟨_, Nat.le_add_left k l⟩
+    rw [add_right_comm, hl]
+    exact tsub_add_cancel_of_le h
+
+@[simp] lemma antidiagonal_filter_le_snd_of_le {n k : ℕ} (h : k ≤ n) :
+    (antidiagonal n).filter (fun a ↦ k ≤ a.snd) = (antidiagonal (n - k)).map
+      (Embedding.prodMap (Embedding.refl ℕ) ⟨_, add_left_injective k⟩) := by
+  have aux₁ : fun a ↦ k ≤ a.snd = (fun a ↦ k ≤ a.fst) ∘ (Equiv.prodComm ℕ ℕ).symm := rfl
+  have aux₂ : ∀ i j, (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔
+                      ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j :=
+    fun i j ↦ by rw [exists_comm]; exact exists₂_congr (fun a b ↦ by rw [add_comm])
+  rw [← map_prodComm_antidiagonal]
+  simp_rw [aux₁, ← map_filter, antidiagonal_filter_le_fst_of_le h, map_map]
+  ext ⟨i, j⟩
+  simpa using aux₂ i j
+
 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
+    norm_num
   · 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`