case intro.intro
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
⊢ ∃ is n, n ∈ 𝓝 x ∧ (n ⊆ ⋂ (i : ι) (_ : i ∈ is), U i) ∧ ∀ (z : X), z ∈ n → (mulSupport fun i => f i z) ⊆ ↑is
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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, n ∈ 𝓝 x ∧ (n ⊆ ⋂ (i : ι) (_ : i ∈ is), U i) ∧ ∀ (z : X), z ∈ n → (mulSupport fun i => f i z) ⊆ ↑is
obtain ⟨n, hn, hnf⟩ := hlf x
case intro.intro
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
⊢ ∃ is n, n ∈ 𝓝 x ∧ (n ⊆ ⋂ (i : ι) (_ : i ∈ is), U i) ∧ ∀ (z : X), z ∈ n → (mulSupport fun i => f i z) ⊆ ↑is
case intro.intro
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
⊢ ∃ is n, n ∈ 𝓝 x ∧ (n ⊆ ⋂ (i : ι) (_ : i ∈ is), U i) ∧ ∀ (z : X), z ∈ n → (mulSupport fun i => f i z) ⊆ ↑is
let is := hnf.toFinset.filter fun i => x ∈ U i
case intro.intro
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
⊢ ∃ is n, n ∈ 𝓝 x ∧ (n ⊆ ⋂ (i : ι) (_ : i ∈ is), U i) ∧ ∀ (z : X), z ∈ n → (mulSupport fun i => f i z) ⊆ ↑is
case intro.intro
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
⊢ ∃ is n, n ∈ 𝓝 x ∧ (n ⊆ ⋂ (i : ι) (_ : i ∈ is), U i) ∧ ∀ (z : X), z ∈ n → (mulSupport fun i => f i z) ⊆ ↑is
let js := hnf.toFinset.filter fun j => x ∉ U j
case intro.intro.refine'_1
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
⊢ (⋂ (j : ι) (_ : j ∈ js), mulTSupport (f j)ᶜ) ∈ 𝓝 x

case intro.intro.refine'_2
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
⊢ (⋂ (i : ι) (_ : i ∈ is), U i) ∈ 𝓝 x

case intro.intro.refine'_3
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hz : z ∈ (n ∩ ⋂ (j : ι) (_ : j ∈ js), mulTSupport (f j)ᶜ) ∩ ⋂ (i : ι) (_ : i ∈ is), U i
⊢ (mulSupport fun i => f i z) ⊆ ↑is
case intro.intro
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
⊢ ∃ is n, n ∈ 𝓝 x ∧ (n ⊆ ⋂ (i : ι) (_ : i ∈ is), U i) ∧ ∀ (z : X), z ∈ n → (mulSupport fun i => f i z) ⊆ ↑is
refine'
  ⟨is, (n ∩ ⋂ j ∈ js, mulTSupport (f j)ᶜ) ∩ ⋂ i ∈ is, U i, inter_mem (inter_mem hn _) _,
    inter_subset_right _ _, fun z hz => _⟩
no goals
case intro.intro.refine'_1
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
⊢ (⋂ (j : ι) (_ : j ∈ js), mulTSupport (f j)ᶜ) ∈ 𝓝 x
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)
no goals
case intro.intro.refine'_2
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
⊢ (⋂ (i : ι) (_ : i ∈ is), U i) ∈ 𝓝 x
exact (biInter_finset_mem is).mpr fun i hi => (ho i).mem_nhds (Finset.mem_filter.mp hi).2
case intro.intro.refine'_3
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hz : z ∈ (n ∩ ⋂ (j : ι) (_ : j ∈ js), mulTSupport (f j)ᶜ) ∩ ⋂ (i : ι) (_ : i ∈ is), U i
hzn : z ∈ n
⊢ (mulSupport fun i => f i z) ⊆ ↑is
case intro.intro.refine'_3
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hz : z ∈ (n ∩ ⋂ (j : ι) (_ : j ∈ js), mulTSupport (f j)ᶜ) ∩ ⋂ (i : ι) (_ : i ∈ is), U i
⊢ (mulSupport fun i => f i z) ⊆ ↑is
have hzn : z ∈ n := by
  rw [inter_assoc] at hz
  exact mem_of_mem_inter_left hz
case intro.intro.refine'_3
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
hz : z ∈ ⋂ (j : ι) (_ : j ∈ js), mulTSupport (f j)ᶜ
⊢ (mulSupport fun i => f i z) ⊆ ↑is
case intro.intro.refine'_3
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hz : z ∈ (n ∩ ⋂ (j : ι) (_ : j ∈ js), mulTSupport (f j)ᶜ) ∩ ⋂ (i : ι) (_ : i ∈ is), U i
hzn : z ∈ n
⊢ (mulSupport fun i => f i z) ⊆ ↑is
replace hz := mem_of_mem_inter_right (mem_of_mem_inter_left hz)
case intro.intro.refine'_3
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
hz : ∀ (i : ι), Set.Nonempty (mulSupport (f i) ∩ n) → ¬x ∈ U i → z ∈ mulTSupport (f i)ᶜ
⊢ (mulSupport fun i => f i z) ⊆ ↑is
case intro.intro.refine'_3
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
hz : z ∈ ⋂ (j : ι) (_ : j ∈ js), mulTSupport (f j)ᶜ
⊢ (mulSupport fun i => f i z) ⊆ ↑is
simp only [Finset.mem_filter, Finite.mem_toFinset, mem_setOf_eq, mem_iInter, and_imp] at hz
case intro.intro.refine'_3
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
hz : ∀ (i : ι), Set.Nonempty (mulSupport (f i) ∩ n) → ¬x ∈ U i → z ∈ mulTSupport (f i)ᶜ
⊢ (mulSupport fun i => f i z) ⊆ ↑(Finite.toFinset hnf)
case intro.intro.refine'_3
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
hz : ∀ (i : ι), Set.Nonempty (mulSupport (f i) ∩ n) → ¬x ∈ U i → z ∈ mulTSupport (f i)ᶜ
⊢ (mulSupport fun i => f i z) ⊆ ↑is
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]
case intro.intro.refine'_3
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
hz : ∀ (i : ι), Set.Nonempty (mulSupport (f i) ∩ n) → ¬x ∈ U i → z ∈ mulTSupport (f i)ᶜ
i : ι
hi : i ∈ mulSupport fun i => f i z
⊢ i ∈ ↑(Finite.toFinset hnf)
case intro.intro.refine'_3
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
hz : ∀ (i : ι), Set.Nonempty (mulSupport (f i) ∩ n) → ¬x ∈ U i → z ∈ mulTSupport (f i)ᶜ
⊢ (mulSupport fun i => f i z) ⊆ ↑(Finite.toFinset hnf)
intro i hi
case intro.intro.refine'_3
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
hz : ∀ (i : ι), Set.Nonempty (mulSupport (f i) ∩ n) → ¬x ∈ U i → z ∈ mulTSupport (f i)ᶜ
i : ι
hi : i ∈ mulSupport fun i => f i z
⊢ Set.Nonempty (mulSupport (f i) ∩ n)
case intro.intro.refine'_3
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
hz : ∀ (i : ι), Set.Nonempty (mulSupport (f i) ∩ n) → ¬x ∈ U i → z ∈ mulTSupport (f i)ᶜ
i : ι
hi : i ∈ mulSupport fun i => f i z
⊢ i ∈ ↑(Finite.toFinset hnf)
simp only [Finite.coe_toFinset, mem_setOf_eq]
no goals
case intro.intro.refine'_3
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
hz : ∀ (i : ι), Set.Nonempty (mulSupport (f i) ∩ n) → ¬x ∈ U i → z ∈ mulTSupport (f i)ᶜ
i : ι
hi : i ∈ mulSupport fun i => f i z
⊢ Set.Nonempty (mulSupport (f i) ∩ n)
exact ⟨z, ⟨hi, hzn⟩⟩
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hz : z ∈ n ∩ ((⋂ (j : ι) (_ : j ∈ js), mulTSupport (f j)ᶜ) ∩ ⋂ (i : ι) (_ : i ∈ is), U i)
⊢ z ∈ n
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hz : z ∈ (n ∩ ⋂ (j : ι) (_ : j ∈ js), mulTSupport (f j)ᶜ) ∩ ⋂ (i : ι) (_ : i ∈ is), U i
⊢ z ∈ n
rw [inter_assoc] at hz
no goals
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hz : z ∈ n ∩ ((⋂ (j : ι) (_ : j ∈ js), mulTSupport (f j)ᶜ) ∩ ⋂ (i : ι) (_ : i ∈ is), U i)
⊢ z ∈ n
exact mem_of_mem_inter_left hz
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
hz : ∀ (i : ι), Set.Nonempty (mulSupport (f i) ∩ n) → ¬x ∈ U i → z ∈ mulTSupport (f i)ᶜ
this : (mulSupport fun i => f i z) ⊆ ↑(Finite.toFinset hnf)
i : ι
hi : i ∈ mulSupport fun i => f i z
⊢ x ∈ U i
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
hz : ∀ (i : ι), Set.Nonempty (mulSupport (f i) ∩ n) → ¬x ∈ U i → z ∈ mulTSupport (f i)ᶜ
this : (mulSupport fun i => f i z) ⊆ ↑(Finite.toFinset hnf)
⊢ (mulSupport fun i => f i z) ⊆ ↑is
refine' hnf.toFinset.subset_coe_filter_of_subset_forall _ this fun i hi => _
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
this : (mulSupport fun i => f i z) ⊆ ↑(Finite.toFinset hnf)
i : ι
hi : i ∈ mulSupport fun i => f i z
hz : ¬x ∈ U i → z ∈ mulTSupport (f i)ᶜ
⊢ x ∈ U i
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
hz : ∀ (i : ι), Set.Nonempty (mulSupport (f i) ∩ n) → ¬x ∈ U i → z ∈ mulTSupport (f i)ᶜ
this : (mulSupport fun i => f i z) ⊆ ↑(Finite.toFinset hnf)
i : ι
hi : i ∈ mulSupport fun i => f i z
⊢ x ∈ U i
specialize hz i ⟨z, ⟨hi, hzn⟩⟩
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
this : (mulSupport fun i => f i z) ⊆ ↑(Finite.toFinset hnf)
i : ι
hi : i ∈ mulSupport fun i => f i z
hz : ¬x ∈ U i
⊢ ¬(¬x ∈ U i → z ∈ mulTSupport (f i)ᶜ)
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
this : (mulSupport fun i => f i z) ⊆ ↑(Finite.toFinset hnf)
i : ι
hi : i ∈ mulSupport fun i => f i z
hz : ¬x ∈ U i → z ∈ mulTSupport (f i)ᶜ
⊢ x ∈ U i
contrapose hz
no goals
X : Type u_2
α : Type ?u.34493
α' : Type ?u.34496
β : Type ?u.34499
γ : Type ?u.34502
δ : Type ?u.34505
M : Type ?u.34508
E : Type ?u.34511
R : Type u_3
ι : Type u_1
U : ι → Set X
inst✝¹ : TopologicalSpace 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 : Set.Finite {i | Set.Nonempty ((fun i => mulSupport (f i)) i ∩ n)}
is : Finset ι := Finset.filter (fun i => x ∈ U i) (Finite.toFinset hnf)
js : Finset ι := Finset.filter (fun j => ¬x ∈ U j) (Finite.toFinset hnf)
z : X
hzn : z ∈ n
this : (mulSupport fun i => f i z) ⊆ ↑(Finite.toFinset hnf)
i : ι
hi : i ∈ mulSupport fun i => f i z
hz : ¬x ∈ U i
⊢ ¬(¬x ∈ U i → z ∈ mulTSupport (f i)ᶜ)
simp [hz, subset_mulTSupport (f i) hi]