feat: some lemmas about List and ZMod (#7424)

Co-authored-by: Alex J Best <alex.j.best@gmail.com>

Mathlib/Data/List/Basic.lean

@@ -2061,6 +2061,7 @@ theorem drop_eq_nil_iff_le {l : List α} {k : ℕ} : l.drop k = [] ↔ l.length
       simpa [Nat.succ_le_succ_iff] using hk h
 #align list.drop_eq_nil_iff_le List.drop_eq_nil_iff_le
 
+@[simp]
 theorem tail_drop (l : List α) (n : ℕ) : (l.drop n).tail = l.drop (n + 1) := by
   induction' l with hd tl hl generalizing n
   · simp
@@ -2069,6 +2070,10 @@ theorem tail_drop (l : List α) (n : ℕ) : (l.drop n).tail = l.drop (n + 1) :=
     · simp [hl]
 #align list.tail_drop List.tail_drop
 
+@[simp]
+theorem drop_tail (l : List α) (n : ℕ) : l.tail.drop n = l.drop (n + 1) := by
+  induction' l <;> simp
+
 theorem cons_get_drop_succ {l : List α} {n} :
     l.get n :: l.drop (n.1 + 1) = l.drop n.1 := by
   induction' l with hd tl hl

Mathlib/Data/ZMod/Basic.lean

@@ -88,6 +88,9 @@ theorem val_nat_cast {n : ℕ} (a : ℕ) : (a : ZMod n).val = a % n := by
   rfl
 #align zmod.val_nat_cast ZMod.val_nat_cast
 
+theorem val_nat_cast_of_lt {n a : ℕ} (h : a < n) : (a : ZMod n).val = a := by
+  rwa [val_nat_cast, Nat.mod_eq_of_lt]
+
 instance charP (n : ℕ) : CharP (ZMod n) n where
     cast_eq_zero_iff' := by
       intro k
@@ -566,6 +569,22 @@ theorem ker_int_castRingHom (n : ℕ) :
   rw [Ideal.mem_span_singleton, RingHom.mem_ker, Int.coe_castRingHom, int_cast_zmod_eq_zero_iff_dvd]
 #align zmod.ker_int_cast_ring_hom ZMod.ker_int_castRingHom
 
+theorem cast_injective_of_lt {m n : ℕ} [nzm : NeZero m] (h : m < n) :
+    Function.Injective (@cast (ZMod n) _ m) := by
+  cases m with
+  | zero => cases nzm; simp_all
+  | succ m =>
+    rintro ⟨x, hx⟩ ⟨y, hy⟩ f
+    simp only [cast, val, nat_cast_eq_nat_cast_iff',
+      Nat.mod_eq_of_lt (lt_trans hx h), Nat.mod_eq_of_lt (lt_trans hy h)] at f
+    apply Fin.ext
+    exact f
+
+theorem cast_zmod_eq_zero_iff_of_lt {m n : ℕ} [NeZero m] (h : m < n) (a : ZMod m) :
+    (a : ZMod n) = 0 ↔ a = 0 := by
+  rw [← ZMod.cast_zero (n := m)]
+  exact Injective.eq_iff' (cast_injective_of_lt h) rfl
+
 --Porting note: commented
 -- attribute [local semireducible] Int.NonNeg
 
@@ -575,7 +594,7 @@ theorem nat_cast_toNat (p : ℕ) : ∀ {z : ℤ} (_h : 0 ≤ z), (z.toNat : ZMod
   | Int.negSucc n, h => by simp at h
 #align zmod.nat_cast_to_nat ZMod.nat_cast_toNat
 
-theorem val_injective (n : ℕ) [NeZero n] : Function.Injective (ZMod.val : ZMod n → ℕ) := by
+theorem val_injective (n : ℕ) [NeZero n] : Function.Injective (val : ZMod n → ℕ) := by
   cases n
   · cases NeZero.ne 0 rfl
   intro a b h
@@ -599,13 +618,43 @@ theorem val_add {n : ℕ} [NeZero n] (a b : ZMod n) : (a + b).val = (a.val + b.v
   · apply Fin.val_add
 #align zmod.val_add ZMod.val_add
 
+theorem val_add_of_lt {n : ℕ} {a b : ZMod n} (h : a.val + b.val < n) :
+    (a + b).val = a.val + b.val := by
+  have : NeZero n := by constructor; rintro rfl; simp at h
+  rw [ZMod.val_add, Nat.mod_eq_of_lt h]
+
+theorem val_add_val_of_le {n : ℕ} [NeZero n] {a b : ZMod n} (h : n ≤ a.val + b.val) :
+    a.val + b.val = (a + b).val + n := by
+  rw [val_add, Nat.add_mod_add_of_le_add_mod, Nat.mod_eq_of_lt (val_lt _),
+    Nat.mod_eq_of_lt (val_lt _)]
+  rwa [Nat.mod_eq_of_lt (val_lt _), Nat.mod_eq_of_lt (val_lt _)]
+
+theorem val_add_of_le {n : ℕ} [NeZero n] {a b : ZMod n} (h : n ≤ a.val + b.val) :
+    (a + b).val = a.val + b.val - n := by
+  rw [val_add_val_of_le h]
+  exact eq_tsub_of_add_eq rfl
+
+theorem val_add_le {n : ℕ} (a b : ZMod n) : (a + b).val ≤ a.val + b.val := by
+  cases n
+  · simp [ZMod.val]; apply Int.natAbs_add_le
+  · simp [ZMod.val_add]; apply Nat.mod_le
+
 theorem val_mul {n : ℕ} (a b : ZMod n) : (a * b).val = a.val * b.val % n := by
   cases n
   · rw [Nat.mod_zero]
     apply Int.natAbs_mul
   · apply Fin.val_mul
 #align zmod.val_mul ZMod.val_mul
 
+theorem val_mul_le {n : ℕ} (a b : ZMod n) : (a * b).val ≤ a.val * b.val := by
+  rw [val_mul]
+  apply Nat.mod_le
+
+theorem val_mul_of_lt {n : ℕ} {a b : ZMod n} (h : a.val * b.val < n) :
+    (a * b).val = a.val * b.val := by
+  rw [val_mul]
+  apply Nat.mod_eq_of_lt h
+
 instance nontrivial (n : ℕ) [Fact (1 < n)] : Nontrivial (ZMod n) :=
   ⟨⟨0, 1, fun h =>
       zero_ne_one <|
@@ -821,6 +870,9 @@ theorem val_eq_zero : ∀ {n : ℕ} (a : ZMod n), a.val = 0 ↔ a = 0
     exact Iff.rfl
 #align zmod.val_eq_zero ZMod.val_eq_zero
 
+theorem val_ne_zero {n : ℕ} (a : ZMod n) : a.val ≠ 0 ↔ a ≠ 0 :=
+  (val_eq_zero a).not
+
 theorem neg_eq_self_iff {n : ℕ} (a : ZMod n) : -a = a ↔ a = 0 ∨ 2 * a.val = n := by
   rw [neg_eq_iff_add_eq_zero, ← two_mul]
   cases n
@@ -873,6 +925,28 @@ theorem neg_val {n : ℕ} [NeZero n] (a : ZMod n) : (-a).val = if a = 0 then 0 e
   rwa [le_zero_iff, val_eq_zero] at h
 #align zmod.neg_val ZMod.neg_val
 
+theorem val_neg_of_ne_zero {n : ℕ} [nz : NeZero n] (a : ZMod n) [na : NeZero a] :
+    (- a).val = n - a.val := by simp_all [neg_val a, na.out]
+
+theorem val_sub {n : ℕ} [NeZero n] {a b : ZMod n} (h : b.val ≤ a.val) :
+    (a - b).val = a.val - b.val := by
+  by_cases hb : b = 0
+  · cases hb; simp
+  · have : NeZero b := ⟨hb⟩
+    rw [sub_eq_add_neg, val_add, val_neg_of_ne_zero, ← Nat.add_sub_assoc (le_of_lt (val_lt _)),
+      add_comm, Nat.add_sub_assoc h, Nat.add_mod_left]
+    apply Nat.mod_eq_of_lt (tsub_lt_of_lt (val_lt _))
+
+theorem val_cast_eq_val_of_lt {m n : ℕ} [nzm : NeZero m] {a : ZMod m}
+    (h : a.val < n) : (a.cast : ZMod n).val = a.val := by
+  have nzn : NeZero n := by constructor; rintro rfl; simp at h
+  cases m with
+  | zero => cases nzm; simp_all
+  | succ m =>
+    cases n with
+    | zero => cases nzn; simp_all
+    | succ n => exact Fin.val_cast_of_lt h
+
 /-- `valMinAbs x` returns the integer in the same equivalence class as `x` that is closest to `0`,
   The result will be in the interval `(-n/2, n/2]`. -/
 def valMinAbs : ∀ {n : ℕ}, ZMod n → ℤ

Mathlib/Logic/Basic.lean

@@ -1280,4 +1280,21 @@ theorem ite_ite_comm (h : P → ¬Q) :
   dite_dite_comm P Q h
 #align ite_ite_comm ite_ite_comm
 
+variable {R : Prop}
+
+theorem ite_prop_iff_or : (if P then Q else R) ↔ (P ∧ Q ∨ ¬ P ∧ R) := by
+  by_cases p : P <;> simp [p]
+
+theorem dite_prop_iff_or {Q : P → Prop} {R : ¬P → Prop} [Decidable P] :
+    dite P Q R ↔ (∃ p, Q p) ∨ (∃ p, R p) := by
+  by_cases h : P <;> simp [h, exists_prop_of_false, exists_prop_of_true]
+
+-- TODO make this a simp lemma in a future PR
+theorem ite_prop_iff_and : (if P then Q else R) ↔ ((P → Q) ∧ (¬ P → R)) := by
+  by_cases p : P <;> simp [p]
+
+theorem dite_prop_iff_and {Q : P → Prop} {R : ¬P → Prop} [Decidable P] :
+    dite P Q R ↔ (∀ h, Q h) ∧ (∀ h, R h) := by
+  by_cases h : P <;> simp [h, forall_prop_of_false, forall_prop_of_true]
+
 end ite