…Choice` (#13025)

Co-authored-by: Pol'tta / Miyahara Kō <52843868+Komyyy@users.noreply.github.com>

…Choice` (#13025)

Co-authored-by: Pol'tta / Miyahara Kō <52843868+Komyyy@users.noreply.github.com>

…Choice` (#13025)

Co-authored-by: Pol'tta / Miyahara Kō <52843868+Komyyy@users.noreply.github.com>

…rom some `DFinsupp` functions (#13235)

This PR removes `Decidable` instances from these `DFinsupp` functions:
1.
```lean
def DFinsupp.sigmaUncurry
    {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → Zero (δ i j)]
    [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → Decidable (x ≠ 0)]
    (f : Π₀ (i : ι) (j : α i), δ i j) : Π₀ (i : (i : ι) × α i), δ i.fst i.snd

def DFinsupp.sigmaCurryEquiv
    {ι : Type u} [DecidableEq ι] {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → Zero (δ i j)]
    [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → Decidable (x ≠ 0)] :
  Π₀ (i : (i : ι) × α i), δ i.fst i.snd ≃ Π₀ (i : ι) (j : α i), δ i j
```
to
```lean
def DFinsupp.sigmaUncurry
    {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → Zero (δ i j)] [DecidableEq ι]
    (f : Π₀ (i : ι) (j : α i), δ i j) : Π₀ (i : (i : ι) × α i), δ i.fst i.snd

def DFinsupp.sigmaCurryEquiv
    {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [(i : ι) → (j : α i) → Zero (δ i j)] [DecidableEq ι] :
  Π₀ (i : (i : ι) × α i), δ i.fst i.snd ≃ Π₀ (i : ι) (j : α i), δ i j
```

We use `Trunc.finChoice` from #13025 to compute support with the only `DecidableEq ι` instance.

2.
```lean
instance DFinsupp.decidableZero
    {ι : Type u} {β : ι → Type v} [DecidableEq ι] [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x ≠ 0)] (f : Π₀ (i : ι), β i) :
  Decidable (0 = f)
```
to
```lean
instance DFinsupp.decidableZero
    {ι : Type u} {β : ι → Type v} [(i : ι) → Zero (β i)] [(i : ι) → (x : β i) → Decidable (x = 0)] (f : Π₀ (i : ι), β i) :
  Decidable (f = 0)
```

We remove the redundant `DecidableEq ι` instance. Additionally, We replace the `(i : ι) → (x : β i) → Decidable (x ≠ 0)` instance with `(i : ι) → (x : β i) → Decidable (x = 0)` because it's more principal, and swaps `f` and `0`.

3.
```lean
noncomputable def DFinsupp.comapDomain
    {ι : Type u} {β : ι → Type v} [DecidableEq ι] {κ : Type u_1} [(i : ι) → Zero (β i)] (h : κ → ι) (hh : Function.Injective h) (f : Π₀ (i : ι), β i) :
  Π₀ (k : κ), β (h k)
```
to
```lean
noncomputable def DFinsupp.comapDomain
    {ι : Type u} {β : ι → Type v} {κ : Type u_1} [(i : ι) → Zero (β i)] (h : κ → ι) (hh : Function.Injective h) (f : Π₀ (i : ι), β i) :
  Π₀ (k : κ), β (h k)
```

`DecidableEq ι` is required to compute unconstructive support so this is redundant.



Co-authored-by: Pol'tta / Miyahara Kō <52843868+Komyyy@users.noreply.github.com>