-- Mathlib/Topology/Algebra/Support.lean
theorem LocallyFinite.exists_finset_nhd_mulSupport_subset {U : ι → Set X} [One R] {f : ι → X → R}
    (hlf : LocallyFinite fun i => mulSupport (f i)) (hso : ∀ i, mulTSupport (f i) ⊆ U i)
    (ho : ∀ i, IsOpen (U i)) (x : X) :
    ∃ (is : Finset ι), ∃ n, n ∈ 𝓝 x ∧ (n ⊆ ⋂ i ∈ is, U i) ∧
      ∀ z ∈ n, (mulSupport fun i => f i z) ⊆ is

Proof state:
case intro.intro
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i => mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := Finset.filter (fun i => x ∈ U i) hnf.toFinset
js : Finset ι := Finset.filter (fun j => x ∉ U j) hnf.toFinset
⊢ ∃ is, ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport fun i => f i z) ⊆ ↑is

Tactic:
refine
  ⟨is, (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i, inter_mem (inter_mem hn ?_) ?_,
    inter_subset_right, fun z hz => ?_⟩

Result:
case intro.intro.refine_1
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i => mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := Finset.filter (fun i => x ∈ U i) hnf.toFinset
js : Finset ι := Finset.filter (fun j => x ∉ U j) hnf.toFinset
⊢ ⋂ j ∈ js, (mulTSupport (f j))ᶜ ∈ 𝓝 x

case intro.intro.refine_2
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i => mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := Finset.filter (fun i => x ∈ U i) hnf.toFinset
js : Finset ι := Finset.filter (fun j => x ∉ U j) hnf.toFinset
⊢ ⋂ i ∈ is, U i ∈ 𝓝 x

case intro.intro.refine_3
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i => mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := Finset.filter (fun i => x ∈ U i) hnf.toFinset
js : Finset ι := Finset.filter (fun j => x ∉ U j) hnf.toFinset
z : X
hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i
⊢ (mulSupport fun i => f i z) ⊆ ↑is

Proof state:
case intro.intro.refine_1
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i => mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := Finset.filter (fun i => x ∈ U i) hnf.toFinset
js : Finset ι := Finset.filter (fun j => x ∉ U j) hnf.toFinset
⊢ ⋂ j ∈ js, (mulTSupport (f j))ᶜ ∈ 𝓝 x

Tactic:
exact (biInter_finset_mem js).mpr fun j hj => IsClosed.compl_mem_nhds (isClosed_mulTSupport _)
  (Set.not_mem_subset (hso j) (Finset.mem_filter.mp hj).2)

Result:
no goals

Proof state:
case intro.intro.refine_3
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i => mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := Finset.filter (fun i => x ∈ U i) hnf.toFinset
js : Finset ι := Finset.filter (fun j => x ∉ U j) hnf.toFinset
z : X
hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i
hzn : z ∈ n
⊢ (mulSupport fun i => f i z) ⊆ ↑is

Tactic:
replace hz := mem_of_mem_inter_right (mem_of_mem_inter_left hz)

Result:
case intro.intro.refine_3
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i => mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := Finset.filter (fun i => x ∈ U i) hnf.toFinset
js : Finset ι := Finset.filter (fun j => x ∉ U j) hnf.toFinset
z : X
hzn : z ∈ n
hz : z ∈ ⋂ j ∈ js, (mulTSupport (f j))ᶜ
⊢ (mulSupport fun i => f i z) ⊆ ↑is

Proof state:
case intro.intro
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i => mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := Finset.filter (fun i => x ∈ U i) hnf.toFinset
⊢ ∃ is, ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport fun i => f i z) ⊆ ↑is

Tactic:
let js := hnf.toFinset.filter fun j => x ∉ U j

Result:
case intro.intro
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i => mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := Finset.filter (fun i => x ∈ U i) hnf.toFinset
js : Finset ι := Finset.filter (fun j => x ∉ U j) hnf.toFinset
⊢ ∃ is, ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport fun i => f i z) ⊆ ↑is

Proof state:
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i => mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := Finset.filter (fun i => x ∈ U i) hnf.toFinset
js : Finset ι := Finset.filter (fun j => x ∉ U j) hnf.toFinset
z : X
hzn : z ∈ n
this : (mulSupport fun i => f i z) ⊆ ↑hnf.toFinset
i : ι
hi : i ∈ mulSupport fun i => f i z
hz : x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
⊢ x ∈ U i

Tactic:
contrapose hz

Result:
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i => mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i => mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := Finset.filter (fun i => x ∈ U i) hnf.toFinset
js : Finset ι := Finset.filter (fun j => x ∉ U j) hnf.toFinset
z : X
hzn : z ∈ n
this : (mulSupport fun i => f i z) ⊆ ↑hnf.toFinset
i : ι
hi : i ∈ mulSupport fun i => f i z
hz : x ∉ U i
⊢ ¬(x ∉ U i → z ∈ (mulTSupport (f i))ᶜ)