Remove bad lemma.

Author: grunweg

Mathlib/Topology/LocallyFinite.lean

@@ -39,14 +39,6 @@ theorem point_finite (hf : LocallyFinite f) (x : X) : { b | x ∈ f b }.Finite :
   ht.subset fun _b hb => ⟨x, hb, mem_of_mem_nhds hxt⟩
 #align locally_finite.point_finite LocallyFinite.point_finite
 
-@[to_additive]
-theorem exists_finset_mulSupport_eq {M : Type*} [CommMonoid M] {ρ : ι → X → M}
-    (hρ : LocallyFinite fun i ↦ mulSupport <| ρ i) (x₀ : X) :
-    ∃ I : Finset ι, (mulSupport fun i ↦ ρ i x₀) = I := by
-  use (hρ.point_finite x₀).toFinset
-  rw [Finite.coe_toFinset]
-  exact rfl
-
 protected theorem subset (hf : LocallyFinite f) (hg : ∀ i, g i ⊆ f i) : LocallyFinite g := fun a =>
   let ⟨t, ht₁, ht₂⟩ := hf a
   ⟨t, ht₁, ht₂.subset fun i hi => hi.mono <| inter_subset_inter (hg i) Subset.rfl⟩