-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_1
R : Type u_8
ι : Type u_9
inst : TopologicalSpace X
U : ι → Set X
inst_1 : One R
f : ι → X → R
hlf : LocallyFinite.{u_9, u_1} (X := X) fun (i : ι) ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : Set.Finite.{u_9} (α := ι) {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}
let let₁ let₂ let₃ :
  ∃ (is : Finset ι),
    ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)
refine_1 :
  let js := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j};
  ⋂ j ∈ js, (mulTSupport (f j))ᶜ ∈ 𝓝 x
refine_2 :
  let is := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i};
  ⋂ i ∈ is, U i ∈ 𝓝 x
refine_3 :
  let is := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i};
  let js := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j};
  ∀ (z : X) (hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i),
    (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)
refine_2₁ :
  let is := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i};
  ⋂ i ∈ is, U i ∈ 𝓝 x
refine_3₁ refine_3₂ :
  let is := {i ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∈ U i};
  let js := {j ∈ hnf.toFinset (s := {i : ι | ((fun (i : ι) ↦ mulSupport (f i)) i ∩ n).Nonempty}) | x ∉ U j};
  ∀ (z : X) (hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i),
    (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)
⊢ ∃ (is : Finset ι),
    ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport.{u_9, u_8} (M := R) fun (i : ι) ↦ f i z) ⊆ (↑is : Set ι)

Tactic:
classical
    let is := {i ∈ hnf.toFinset | x ∈ U i}
    let js := {j ∈ hnf.toFinset | x ∉ U j}
    refine
      ⟨is, (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i, inter_mem (inter_mem hn ?_) ?_,
        inter_subset_right, fun z hz => ?_⟩
    · exact (biInter_finset_mem js).mpr fun j hj => IsClosed.compl_mem_nhds (isClosed_mulTSupport _)
        (Set.notMem_subset (hso j) (Finset.mem_filter.mp hj).2)
    · exact (biInter_finset_mem is).mpr fun i hi => (ho i).mem_nhds (Finset.mem_filter.mp hi).2
    · have hzn : z ∈ n := by
        rw [inter_assoc] at hz
        exact mem_of_mem_inter_left hz
      replace hz := mem_of_mem_inter_right (mem_of_mem_inter_left hz)
      simp only [js, Finset.mem_filter, Finite.mem_toFinset, mem_setOf_eq, mem_iInter,
        and_imp] at hz
      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]
      intro i hi
      simp only [Finite.coe_toFinset, mem_setOf_eq]
      exact ⟨z, ⟨hi, hzn⟩⟩

Premises used: and_imp, Set.Finite.mem_toFinset, Set.Finite.coe_toFinset, Set.mem_setOf_eq, Set.mem_iInter, Finset.mem_filter