-- 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:
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))ᶜ)

Tactic:
simp [hz, subset_mulTSupport (f i) hi]

Result:
no goals

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, ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport fun i => f i z) ⊆ ↑is

Tactic:
let is := hnf.toFinset.filter fun i => x ∈ U i

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
⊢ ∃ is, ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport fun i => f i z) ⊆ ↑is

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
hzn : z ∈ n
hz : z ∈ ⋂ j ∈ js, (mulTSupport (f j))ᶜ
⊢ (mulSupport fun i => f i z) ⊆ ↑is

Tactic:
simp only [js, Finset.mem_filter, Finite.mem_toFinset, mem_setOf_eq, mem_iInter,
  and_imp] at 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 : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
⊢ (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
⊢ ∃ is, ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport fun i => f i z) ⊆ ↑is

Tactic:
obtain ⟨n, hn, hnf⟩ := hlf x

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, ∃ 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
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
this : (mulSupport fun i => f i z) ⊆ ↑hnf.toFinset
i : ι
hi : i ∈ mulSupport fun i => f i z
⊢ x ∈ U i

Tactic:
specialize hz i ⟨z, ⟨hi, hzn⟩⟩

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 → z ∈ (mulTSupport (f i))ᶜ
⊢ x ∈ U i

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
hz : z ∈ n ∩ ((⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i)
⊢ z ∈ n

Tactic:
exact mem_of_mem_inter_left hz

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
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
⊢ (mulSupport fun i => f i z) ⊆ ↑is

Tactic:
suffices (mulSupport fun i => f i z) ⊆ hnf.toFinset by
  refine hnf.toFinset.subset_coe_filter_of_subset_forall _ this fun i hi => ?_
  specialize hz i ⟨z, ⟨hi, hzn⟩⟩
  contrapose hz
  simp [hz, subset_mulTSupport (f i) hi]

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 : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
⊢ (mulSupport fun i => f i z) ⊆ ↑hnf.toFinset