chore(data/fin/basic): remove fin.coe_of_nat_eq_mod (#18131)

It can be proved by `fin.coe_of_nat_eq_mod'`.
leanprover-community · Jan 12, 2023 · 008af8b · 008af8b
1 parent 579cdfe
commit 008af8b
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 8 deletions.
diff --git 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
@@ -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
 
 /-!