refactor(data/dfinsupp/basic): Improve definitional equalities of coercions (#15521)

This means that `dfinsupp.coe_add` etc are true by definition, rather than requiring the application of `quotient.induction` first.
The key change is that the underlying function is no longer "hidden" under the quotient, as it does not need to be.

One motivation for this is to make the API more similar to that of `finsupp`.

This change eliminates `dfinsupp.pre`, instead using `{s : multiset ι // ∀ i, i ∈ s ∨ to_fun i = 0}` directly.
We no longer even need to create a `setoid` instance, since we can just use `trunc`.

While adjusting some proofs in `data/finsupp/interval` to use the new definition, this ended up eliminating some decidable arguments. I don't think that is a consequence of this redefinition, and is incidental cleanup that could have been performed separately.

Author: eric-wieser

src/algebra/direct_sum/basic.lean

@@ -49,8 +49,7 @@ variables [Π i, add_comm_group (β i)]
 instance : add_comm_group (direct_sum ι β) := dfinsupp.add_comm_group
 
 variables {β}
-@[simp] lemma sub_apply (g₁ g₂ : ⨁ i, β i) (i : ι) : (g₁ - g₂) i = g₁ i - g₂ i :=
-dfinsupp.sub_apply _ _ _
+@[simp] lemma sub_apply (g₁ g₂ : ⨁ i, β i) (i : ι) : (g₁ - g₂) i = g₁ i - g₂ i := rfl
 
 end add_comm_group
 
@@ -59,8 +58,7 @@ variables [Π i, add_comm_monoid (β i)]
 @[simp] lemma zero_apply (i : ι) : (0 : ⨁ i, β i) i = 0 := rfl
 
 variables {β}
-@[simp] lemma add_apply (g₁ g₂ : ⨁ i, β i) (i : ι) : (g₁ + g₂) i = g₁ i + g₂ i :=
-dfinsupp.add_apply _ _ _
+@[simp] lemma add_apply (g₁ g₂ : ⨁ i, β i) (i : ι) : (g₁ + g₂) i = g₁ i + g₂ i := rfl
 
 variables (β)
 include dec_ι
@@ -223,10 +221,10 @@ variables {α : ι → Type u} {δ : Π i, α i → Type w} [Π i j, add_comm_mo
 noncomputable def sigma_curry : (⨁ (i : Σ i, _), δ i.1 i.2) →+ ⨁ i j, δ i j :=
 { to_fun := @dfinsupp.sigma_curry _ _ δ _,
   map_zero' := dfinsupp.sigma_curry_zero,
-  map_add' := λ f g, dfinsupp.sigma_curry_add f g }
+  map_add' := λ f g, @dfinsupp.sigma_curry_add _ _ δ _ f g }
 
 @[simp] lemma sigma_curry_apply (f : ⨁ (i : Σ i, _), δ i.1 i.2) (i : ι) (j : α i) :
-  sigma_curry f i j = f ⟨i, j⟩ := dfinsupp.sigma_curry_apply f i j
+  sigma_curry f i j = f ⟨i, j⟩ := @dfinsupp.sigma_curry_apply _ _ δ _ f i j
 
 /--The natural map between `⨁ i (j : α i), δ i j` and `Π₀ (i : Σ i, α i), δ i.1 i.2`, inverse of
 `curry`.-/