chore: fix double instance declaration in FiniteAdeleRing (#38300)

`FiniteAdeleRing` has two `DFunLike` instance, defeq but not reducibly so, where the first one is not nice, and the second one is nice but with a proof using the first one. Instead, we give directly the nice instance with a direct proof.

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean

@@ -98,10 +98,9 @@ instance : CommRing (FiniteAdeleRing R K) := inferInstanceAs <|
 instance : TopologicalSpace (FiniteAdeleRing R K) := inferInstanceAs <|
   TopologicalSpace <| Πʳ v : HeightOneSpectrum R, [v.adicCompletion K, v.adicCompletionIntegers K]
 
-instance : DFunLike (FiniteAdeleRing R K) (HeightOneSpectrum R) (fun v ↦ v.adicCompletion K) :=
-  inferInstanceAs <|
-  DFunLike (Πʳ v : HeightOneSpectrum R, [v.adicCompletion K, v.adicCompletionIntegers K])
-    (HeightOneSpectrum R) (fun v ↦ v.adicCompletion K)
+instance : DFunLike (FiniteAdeleRing R K) (HeightOneSpectrum R) (adicCompletion K) where
+  coe a := a.1
+  coe_injective' _ _ := Subtype.ext
 
 namespace FiniteAdeleRing
 
@@ -135,10 +134,6 @@ variable {R} in
 lemma ext {a₁ a₂ : FiniteAdeleRing R K} (h : ∀ v, a₁ v = a₂ v) : a₁ = a₂ :=
   Subtype.ext <| funext h
 
-instance : DFunLike (FiniteAdeleRing R K) (HeightOneSpectrum R) (adicCompletion K) where
-  coe a := a.1
-  coe_injective' _a _b h := ext K (congrFun h)
-
 section Topology
 
 instance : IsTopologicalRing (FiniteAdeleRing R K) :=