Remove stuff that's irrelevant for this PR

Author: Raph-DG

Mathlib/Topology/LocallyFinsupp.lean

@@ -126,14 +126,6 @@ instance [Zero Y] : FunLike (locallyFinsuppWithin U Y) X Y where
   coe D := D.toFun
   coe_injective' := fun ⟨_, _, _⟩ ⟨_, _, _⟩ ↦ by simp
 
-@[simp]
-lemma toFun_eq_coe [Zero Y] (c : locallyFinsuppWithin U Y) : c.toFun = ⇑c := rfl
-
-@[simp]
-lemma coe_mk [Zero Y] (f : X → Y) (h : f.support ⊆ U)
-    (h' : ∀ z ∈ U, ∃ t ∈ 𝓝 z, Set.Finite (t ∩ f.support)) :
-    ⇑(Function.locallyFinsuppWithin.mk f h h') = f := rfl
-
 /-- This allows writing `D.support` instead of `Function.support D` -/
 abbrev support [Zero Y] (D : locallyFinsuppWithin U Y) := Function.support D