From 008af8bb14b3ebef7e04ec3b0d63b947dee4d26a Mon Sep 17 00:00:00 2001
From: negiizhao <egresf@gmail.com>
Date: Thu, 12 Jan 2023 11:00:11 +0000
Subject: [PATCH] chore(data/fin/basic): remove `fin.coe_of_nat_eq_mod`
 (#18131)

It can be proved by `fin.coe_of_nat_eq_mod'`.
---
 src/data/bitvec/basic.lean | 4 ++--
 src/data/fin/basic.lean    | 7 +------
 2 files changed, 3 insertions(+), 8 deletions(-)

diff --git a/src/data/bitvec/basic.lean b/src/data/bitvec/basic.lean
index c5715812f85be..5e76ec218b003 100644
--- a/src/data/bitvec/basic.lean
+++ b/src/data/bitvec/basic.lean
@@ -22,7 +22,7 @@ by rw [of_fin,to_nat_of_nat,nat.mod_eq_of_lt]; apply i.is_lt
 
 /-- convert `bitvec` to `fin` -/
 def to_fin {n : ℕ} (i : bitvec n) : fin $ 2^n :=
-fin.of_nat' i.to_nat
+i.to_nat
 
 lemma add_lsb_eq_twice_add_one {x b} :
   add_lsb x b = 2 * x + cond b 1 0 :=
@@ -77,7 +77,7 @@ begin
 end
 
 lemma to_fin_val {n : ℕ} (v : bitvec n) : (to_fin v : ℕ) = v.to_nat :=
-by rw [to_fin, fin.of_nat'_eq_coe, fin.coe_of_nat_eq_mod', nat.mod_eq_of_lt]; apply to_nat_lt
+by rw [to_fin, fin.coe_of_nat_eq_mod, nat.mod_eq_of_lt]; apply to_nat_lt
 
 lemma to_fin_le_to_fin_of_le {n} {v₀ v₁ : bitvec n} (h : v₀ ≤ v₁) : v₀.to_fin ≤ v₁.to_fin :=
 show (v₀.to_fin : ℕ) ≤ v₁.to_fin,
diff --git a/src/data/fin/basic.lean b/src/data/fin/basic.lean
index aae2f9ffddc75..2be427042b554 100644
--- a/src/data/fin/basic.lean
+++ b/src/data/fin/basic.lean
@@ -1866,15 +1866,10 @@ def clamp (n m : ℕ) : fin (m + 1) := of_nat $ min n m
 @[simp] lemma coe_clamp (n m : ℕ) : (clamp n m : ℕ) = min n m :=
 nat.mod_eq_of_lt $ nat.lt_succ_iff.mpr $ min_le_right _ _
 
-@[simp] lemma coe_of_nat_eq_mod' (m n : ℕ) [I : ne_zero m] :
+@[simp] lemma coe_of_nat_eq_mod (m n : ℕ) [ne_zero m] :
   ((n : fin m) : ℕ) = n % m :=
 rfl
 
-@[simp]
-lemma coe_of_nat_eq_mod (m n : ℕ) :
-  ((n : fin (succ m)) : ℕ) = n % succ m :=
-by rw [← of_nat_eq_coe]; refl
-
 section mul
 
 /-!