refactor(logic/equiv/basic): remove fin_equiv_subtype (#14603)

The types `fin n` and `{m // m < n}` are definitionally equal, so it doesn't make sense to have a dedicated equivalence between them (other than `equiv.refl`). We remove this equivalence and golf the places where it was used.

src/computability/primrec.lean

@@ -1026,7 +1026,7 @@ def subtype {p : α → Prop} [decidable_pred p]
 instance fin {n} : primcodable (fin n) :=
 @of_equiv _ _
   (subtype $ nat_lt.comp primrec.id (const n))
-  (equiv.fin_equiv_subtype _)
+  (equiv.refl _)
 
 instance vector {n} : primcodable (vector α n) :=
 subtype ((@primrec.eq _ _ nat.decidable_eq).comp list_length (const _))

src/data/fintype/card.lean

@@ -184,8 +184,7 @@ e.bijective.prod_comp f
 lemma fin.prod_univ_eq_prod_range [comm_monoid α] (f : ℕ → α) (n : ℕ) :
   ∏ i : fin n, f i = ∏ i in range n, f i :=
 calc (∏ i : fin n, f i) = ∏ i : {x // x ∈ range n}, f i :
-  ((equiv.fin_equiv_subtype n).trans
-    (equiv.subtype_equiv_right (λ _, mem_range.symm))).prod_comp (f ∘ coe)
+  (equiv.subtype_equiv_right $ λ m, (@mem_range n m).symm).prod_comp (f ∘ coe)
 ... = ∏ i in range n, f i : by rw [← attach_eq_univ, prod_attach]
 
 @[to_additive]

src/field_theory/finite/polynomial.lean

@@ -192,7 +192,7 @@ calc module.rank K (R σ K) =
   ... = #(σ → {n // n < fintype.card K}) :
     (@equiv.subtype_pi_equiv_pi σ (λ_, ℕ) (λs n, n < fintype.card K)).cardinal_eq
   ... = #(σ → fin (fintype.card K)) :
-    (equiv.arrow_congr (equiv.refl σ) (equiv.fin_equiv_subtype _).symm).cardinal_eq
+    (equiv.arrow_congr (equiv.refl σ) (equiv.refl _)).cardinal_eq
   ... = #(σ → K) :
     (equiv.arrow_congr (equiv.refl σ) (fintype.equiv_fin K).symm).cardinal_eq
   ... = fintype.card (σ → K) : cardinal.mk_fintype _

src/logic/encodable/basic.lean

@@ -299,7 +299,7 @@ by cases a; refl
 end subtype
 
 instance _root_.fin.encodable (n) : encodable (fin n) :=
-of_equiv _ (equiv.fin_equiv_subtype _)
+subtype.encodable
 
 instance _root_.int.encodable : encodable ℤ :=
 of_equiv _ equiv.int_equiv_nat

src/logic/equiv/basic.lean

@@ -1281,10 +1281,6 @@ def list_equiv_of_equiv {α β : Type*} (e : α ≃ β) : list α ≃ list β :=
   left_inv := λ l, by rw [list.map_map, e.symm_comp_self, list.map_id],
   right_inv := λ l, by rw [list.map_map, e.self_comp_symm, list.map_id] }
 
-/-- `fin n` is equivalent to `{m // m < n}`. -/
-def fin_equiv_subtype (n : ℕ) : fin n ≃ {m // m < n} :=
-⟨λ x, ⟨x.1, x.2⟩, λ x, ⟨x.1, x.2⟩, λ ⟨a, b⟩, rfl,λ ⟨a, b⟩, rfl⟩
-
 /-- If `α` is equivalent to `β`, then `unique α` is equivalent to `unique β`. -/
 def unique_congr (e : α ≃ β) : unique α ≃ unique β :=
 { to_fun := λ h, @equiv.unique _ _ h e.symm,