From a45fd777dd5d1cde416a336004731b0ff3ac6bb2 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Sat, 16 Dec 2023 00:58:55 +0000
Subject: [PATCH] feat(Data/Fin): add lemmas (#8974)

- move `Nat.dvd_one` to `Data.Nat.Basic`; it should go to Std4;
- rename `Fin.ofNat_eq_val` to `Fin.ofNat''_eq_cast`;
- add `@[simp]` lemmas `Fin.val_nat_cast`, `Fin.nat_cast_self`, and `Fin.nat_cast_eq_zero`;
- add `@[simp]` to `Fin.cast_nat_eq_last` and `ZMod.val_nat_cast`;
- add `binomial_apply_last`, as the LHS of `binomial_apply_self` is no longer in simp normal form.
---
 Mathlib/Data/Fin/Basic.lean                   | 42 +++++++++----------
 Mathlib/Data/Nat/Basic.lean                   |  9 ++--
 Mathlib/Data/Nat/Order/Lemmas.lean            |  6 ---
 Mathlib/Data/ZMod/Basic.lean                  | 16 ++++---
 .../ProbabilityMassFunction/Binomial.lean     |  7 +++-
 5 files changed, 38 insertions(+), 42 deletions(-)

diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean
index 957ee6a5f093e..794cd85e5db8d 100644
--- a/Mathlib/Data/Fin/Basic.lean
+++ b/Mathlib/Data/Fin/Basic.lean
@@ -640,23 +640,23 @@ end Bit
 section OfNatCoe
 
 @[simp]
-theorem ofNat_eq_val (n : ℕ) [NeZero n] (a : ℕ) : (Fin.ofNat'' a : Fin n) = a :=
+theorem ofNat''_eq_cast (n : ℕ) [NeZero n] (a : ℕ) : (Fin.ofNat'' a : Fin n) = a :=
   rfl
-#align fin.of_nat_eq_coe Fin.ofNat_eq_val
+#align fin.of_nat_eq_coe Fin.ofNat''_eq_cast
+
+@[simp] lemma val_nat_cast (a n : ℕ) [NeZero n] : (a : Fin n).val = a % n := rfl
 
 -- porting note: is this the right name for things involving `Nat.cast`?
 /-- Converting an in-range number to `Fin (n + 1)` produces a result
 whose value is the original number.  -/
-theorem val_cast_of_lt {n : ℕ} [NeZero n] {a : ℕ} (h : a < n) : (a : Fin n).val = a := by
-  rw [← ofNat_eq_val]
-  exact Nat.mod_eq_of_lt h
+theorem val_cast_of_lt {n : ℕ} [NeZero n] {a : ℕ} (h : a < n) : (a : Fin n).val = a :=
+  Nat.mod_eq_of_lt h
 #align fin.coe_val_of_lt Fin.val_cast_of_lt
 
 /-- Converting the value of a `Fin (n + 1)` to `Fin (n + 1)` results
 in the same value.  -/
-theorem cast_val_eq_self {n : ℕ} [NeZero n] (a : Fin n) : (a.val : Fin n) = a := by
-  rw [Fin.eq_iff_veq]
-  exact val_cast_of_lt a.isLt
+theorem cast_val_eq_self {n : ℕ} [NeZero n] (a : Fin n) : (a.val : Fin n) = a :=
+  ext <| val_cast_of_lt a.isLt
 #align fin.coe_val_eq_self Fin.cast_val_eq_self
 
 -- porting note: this is syntactically the same as `val_cast_of_lt`
@@ -665,9 +665,13 @@ theorem cast_val_eq_self {n : ℕ} [NeZero n] (a : Fin n) : (a.val : Fin n) = a
 -- porting note: this is syntactically the same as `cast_val_of_lt`
 #align fin.coe_coe_eq_self Fin.cast_val_eq_self
 
-theorem cast_nat_eq_last (n) : (n : Fin (n + 1)) = Fin.last n := by
-  rw [← Fin.ofNat_eq_val, Fin.ofNat'', Fin.last]
-  simp only [Nat.mod_eq_of_lt n.lt_succ_self]
+@[simp] lemma nat_cast_self (n : ℕ) [NeZero n] : (n : Fin n) = 0 := by ext; simp
+
+@[simp] lemma nat_cast_eq_zero {a n : ℕ} [NeZero n] : (a : Fin n) = 0 ↔ n ∣ a := by
+  simp [eq_iff_veq, Nat.dvd_iff_mod_eq_zero]
+
+@[simp]
+theorem cast_nat_eq_last (n) : (n : Fin (n + 1)) = Fin.last n := by ext; simp
 #align fin.coe_nat_eq_last Fin.cast_nat_eq_last
 
 theorem le_val_last (i : Fin (n + 1)) : i ≤ n := by
@@ -682,19 +686,13 @@ end OfNatCoe
 #align fin.zero_ne_one Fin.zero_ne_one
 
 @[simp]
-theorem zero_eq_one_iff [NeZero n] : (0 : Fin n) = 1 ↔ n = 1 := by
-  constructor
-  · intro h
-    have := congr_arg ((↑) : Fin n → ℕ) h
-    simp only [val_zero', val_one', @eq_comm _ 0, ← Nat.dvd_iff_mod_eq_zero] at this
-    exact eq_one_of_dvd_one this
-  · rintro rfl
-    rfl
-#align fin.zero_eq_one_iff Fin.zero_eq_one_iff
+theorem one_eq_zero_iff [NeZero n] : (1 : Fin n) = 0 ↔ n = 1 := by
+  rw [← Nat.cast_one, nat_cast_eq_zero, Nat.dvd_one]
+#align fin.one_eq_zero_iff Fin.one_eq_zero_iff
 
 @[simp]
-theorem one_eq_zero_iff [NeZero n] : (1 : Fin n) = 0 ↔ n = 1 := by rw [eq_comm, zero_eq_one_iff]
-#align fin.one_eq_zero_iff Fin.one_eq_zero_iff
+theorem zero_eq_one_iff [NeZero n] : (0 : Fin n) = 1 ↔ n = 1 := by rw [eq_comm, one_eq_zero_iff]
+#align fin.zero_eq_one_iff Fin.zero_eq_one_iff
 
 end Add
 
diff --git a/Mathlib/Data/Nat/Basic.lean b/Mathlib/Data/Nat/Basic.lean
index 69fecd7a3760d..1cd9067d80f1b 100644
--- a/Mathlib/Data/Nat/Basic.lean
+++ b/Mathlib/Data/Nat/Basic.lean
@@ -782,11 +782,14 @@ protected theorem mul_dvd_mul_iff_right {a b c : ℕ} (hc : 0 < c) : a * c ∣ b
   exists_congr fun d => by rw [Nat.mul_right_comm, mul_left_inj' hc.ne']
 #align nat.mul_dvd_mul_iff_right Nat.mul_dvd_mul_iff_right
 
+@[simp] -- TODO: move to Std4
+theorem dvd_one {a : ℕ} : a ∣ 1 ↔ a = 1 :=
+  ⟨eq_one_of_dvd_one, fun h ↦ h.symm ▸ Nat.dvd_refl _⟩
+#align nat.dvd_one Nat.dvd_one
+
 @[simp]
 theorem mod_mod_of_dvd (n : Nat) {m k : Nat} (h : m ∣ k) : n % k % m = n % m := by
-  conv =>
-  rhs
-  rw [← mod_add_div n k]
+  conv_rhs => rw [← mod_add_div n k]
   rcases h with ⟨t, rfl⟩
   rw [mul_assoc, add_mul_mod_self_left]
 #align nat.mod_mod_of_dvd Nat.mod_mod_of_dvd
diff --git a/Mathlib/Data/Nat/Order/Lemmas.lean b/Mathlib/Data/Nat/Order/Lemmas.lean
index 53533ef5aaddf..252ea0b800df8 100644
--- a/Mathlib/Data/Nat/Order/Lemmas.lean
+++ b/Mathlib/Data/Nat/Order/Lemmas.lean
@@ -93,12 +93,6 @@ protected lemma div_pos_iff (hb : b ≠ 0) : 0 < a / b ↔ b ≤ a := by
 
 /-! ### `mod`, `dvd` -/
 
-
-@[simp]
-protected theorem dvd_one {n : ℕ} : n ∣ 1 ↔ n = 1 :=
-  ⟨eq_one_of_dvd_one, fun e => e.symm ▸ dvd_rfl⟩
-#align nat.dvd_one Nat.dvd_one
-
 set_option linter.deprecated false in
 @[simp]
 protected theorem not_two_dvd_bit1 (n : ℕ) : ¬2 ∣ bit1 n := by
diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean
index 01ab7207a8b07..c0f99cf4d0983 100644
--- a/Mathlib/Data/ZMod/Basic.lean
+++ b/Mathlib/Data/ZMod/Basic.lean
@@ -81,25 +81,23 @@ theorem val_mul' {m n : ZMod 0} : (m * n).val = m.val * n.val :=
   Int.natAbs_mul m n
 #align zmod.val_mul' ZMod.val_mul'
 
+@[simp]
 theorem val_nat_cast {n : ℕ} (a : ℕ) : (a : ZMod n).val = a % n := by
   cases n
   · rw [Nat.mod_zero]
     exact Int.natAbs_ofNat a
-  rw [← Fin.ofNat_eq_val]
-  rfl
+  · apply Fin.val_nat_cast
 #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
-      cases' n with n
-      · simp [zero_dvd_iff, Int.coe_nat_eq_zero, Nat.zero_eq]
-      rw [Fin.eq_iff_veq]
-      show (k : ZMod (n + 1)).val = (0 : ZMod (n + 1)).val ↔ _
-      rw [val_nat_cast, val_zero, Nat.dvd_iff_mod_eq_zero]
+  cast_eq_zero_iff' := by
+    intro k
+    cases' n with n
+    · simp [zero_dvd_iff, Int.coe_nat_eq_zero, Nat.zero_eq]
+    · exact Fin.nat_cast_eq_zero
 
 @[simp]
 theorem addOrderOf_one (n : ℕ) : addOrderOf (1 : ZMod n) = n :=
diff --git a/Mathlib/Probability/ProbabilityMassFunction/Binomial.lean b/Mathlib/Probability/ProbabilityMassFunction/Binomial.lean
index efb03d4a3bc12..dea0165accca0 100644
--- a/Mathlib/Probability/ProbabilityMassFunction/Binomial.lean
+++ b/Mathlib/Probability/ProbabilityMassFunction/Binomial.lean
@@ -43,9 +43,12 @@ theorem binomial_apply_zero (p : ℝ≥0∞) (h : p ≤ 1) (n : ℕ) :
   simp [binomial_apply]
 
 @[simp]
+theorem binomial_apply_last (p : ℝ≥0∞) (h : p ≤ 1) (n : ℕ) :
+    binomial p h n (.last n) = p^n := by
+  simp [binomial_apply]
+
 theorem binomial_apply_self (p : ℝ≥0∞) (h : p ≤ 1) (n : ℕ) :
-    binomial p h n n = p^n := by
-  simp [binomial_apply, Nat.mod_eq_of_lt]
+    binomial p h n n = p^n := by simp
 
 /-- The binomial distribution on one coin is the bernoully distribution. -/
 theorem binomial_one_eq_bernoulli (p : ℝ≥0∞) (h : p ≤ 1) :