feat: add lemma Finsupp.erase_apply (#11242)

Adds a lemma

Mathlib/Data/Finsupp/Defs.lean

@@ -661,6 +661,11 @@ theorem erase_ne {a a' : α} {f : α →₀ M} (h : a' ≠ a) : (f.erase a) a' =
   classical simp only [erase, coe_mk, h, ite_false]
 #align finsupp.erase_ne Finsupp.erase_ne
 
+theorem erase_apply [DecidableEq α] {a a' : α} {f : α →₀ M} :
+    f.erase a a' = if a' = a then 0 else f a' := by
+  rw [erase, coe_mk]
+  convert rfl
+
 @[simp]
 theorem erase_single {a : α} {b : M} : erase a (single a b) = 0 := by
   ext s; by_cases hs : s = a