Finsupp with DecidableEq

Stream: new members

[Snir Broshi]

Hello, I wanted to see Finsupp instances with #eval such as:

import Mathlib
#eval fun₀ | 1 => 5 | 4 => 7
#eval (360).factorization + (5040).factorization

which fail because many Finsupp definitions use Classical.decEq:
docs#Finsupp.single, docs#Finsupp.update, docs#Finsupp.zipWith, docs#Finsupp.onFinset, docs#Finsupp.instAdd

But in the cases above, ℕ does have DecidableEq. Is there a simple way to make it "skip" the Classical.decEq calls and use the existing DecidableEq ℕ instance?

If not, is it possible to define alternate definitions of these Finsupp stuff, such as:

import Mathlib

def onFinset' {α M : Type*} [Zero M] [DecidableEq M]
    (s : Finset α) (f : α → M) (hf : ∀ a, f a ≠ 0 → a ∈ s) : α →₀ M where
  support := {a ∈ s | f a ≠ 0}
  toFun := f
  mem_support_toFun := by simpa

def zipWith' {α P M N : Type*} [Zero M] [Zero N] [Zero P] [DecidableEq α] [DecidableEq P]
    (f : M → N → P) (hf : f 0 0 = 0) (g₁ : α →₀ M) (g₂ : α →₀ N) : α →₀ P :=
  onFinset'
    (g₁.support ∪ g₂.support)
    (fun a => f (g₁ a) (g₂ a))
    fun a (H : f _ _ ≠ 0) => by
      rw [Finset.mem_union, Finsupp.mem_support_iff, Finsupp.mem_support_iff, ← not_and_or]
      rintro ⟨h₁, h₂⟩; rw [h₁, h₂] at H; exact H hf

instance instAdd' {M N : Type*} [AddZeroClass M] [DecidableEq M] [DecidableEq N] : Add (N →₀ M) where
  add := zipWith' (· + ·) (add_zero 0)

#eval (360).factorization + (5040).factorization

From my testing it looks like Lean chooses the correct Add instance based on whether a type has DecidableEq or not, but is it guaranteed or does it depend on the order of the instance definitions?

Also, how can I add Finsupp.single' and Finsupp.update' such that the fun₀ notation uses it when possible?

Thanks!