[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝¹ : One α
inst✝ : TopologicalSpace X
f : X → α
⊢ mulTSupport f = ∅ ↔ f = 1
[PROOFSTEP]
rw [mulTSupport, closure_empty_iff, mulSupport_eq_empty_iff]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
⊢ ¬x ∈ mulTSupport f ↔ f =ᶠ[𝓝 x] 1
[PROOFSTEP]
simp_rw [mulTSupport, mem_closure_iff_nhds, not_forall, not_nonempty_iff_eq_empty, exists_prop, ←
  disjoint_iff_inter_eq_empty, disjoint_mulSupport_iff, eventuallyEq_iff_exists_mem]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
⊢ HasCompactMulSupport f ↔ IsCompact (closure (mulSupport f))
[PROOFSTEP]
rfl
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace α'
inst✝³ : One β
inst✝² : One γ
inst✝¹ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
inst✝ : T2Space α
⊢ (∃ K, IsCompact K ∧ ∀ (x : α), ¬x ∈ K → f x = 1) ↔ HasCompactMulSupport f
[PROOFSTEP]
simp_rw [← nmem_mulSupport, ← mem_compl_iff, ← subset_def, compl_subset_compl, hasCompactMulSupport_def,
  exists_compact_superset_iff]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace α'
inst✝³ : One β
inst✝² : One γ
inst✝¹ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
inst✝ : TopologicalSpace β
h : HasCompactMulSupport f
hf : Continuous f
⊢ IsCompact (range f)
[PROOFSTEP]
cases' range_eq_image_mulTSupport_or f with h2 h2
[GOAL]
case inl
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace α'
inst✝³ : One β
inst✝² : One γ
inst✝¹ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
inst✝ : TopologicalSpace β
h : HasCompactMulSupport f
hf : Continuous f
h2 : range f = f '' mulTSupport f
⊢ IsCompact (range f)
[PROOFSTEP]
rw [h2]
[GOAL]
case inr
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace α'
inst✝³ : One β
inst✝² : One γ
inst✝¹ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
inst✝ : TopologicalSpace β
h : HasCompactMulSupport f
hf : Continuous f
h2 : range f = insert 1 (f '' mulTSupport f)
⊢ IsCompact (range f)
[PROOFSTEP]
rw [h2]
[GOAL]
case inl
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace α'
inst✝³ : One β
inst✝² : One γ
inst✝¹ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
inst✝ : TopologicalSpace β
h : HasCompactMulSupport f
hf : Continuous f
h2 : range f = f '' mulTSupport f
⊢ IsCompact (f '' mulTSupport f)
case inr
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace α'
inst✝³ : One β
inst✝² : One γ
inst✝¹ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
inst✝ : TopologicalSpace β
h : HasCompactMulSupport f
hf : Continuous f
h2 : range f = insert 1 (f '' mulTSupport f)
⊢ IsCompact (insert 1 (f '' mulTSupport f))
[PROOFSTEP]
exacts [h.image hf, (h.image hf).insert 1]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hg : ∀ {x : β}, g x = 1 ↔ x = 1
⊢ HasCompactMulSupport (g ∘ f) ↔ HasCompactMulSupport f
[PROOFSTEP]
simp_rw [hasCompactMulSupport_def, mulSupport_comp_eq g (@hg) f]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g✝ : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : HasCompactMulSupport f
g : α' → α
hg : ClosedEmbedding g
⊢ HasCompactMulSupport (f ∘ g)
[PROOFSTEP]
rw [hasCompactMulSupport_def, Function.mulSupport_comp_eq_preimage]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g✝ : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : HasCompactMulSupport f
g : α' → α
hg : ClosedEmbedding g
⊢ IsCompact (closure (g ⁻¹' mulSupport f))
[PROOFSTEP]
refine' isCompact_of_isClosed_subset (hg.isCompact_preimage hf) isClosed_closure _
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g✝ : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : HasCompactMulSupport f
g : α' → α
hg : ClosedEmbedding g
⊢ closure (g ⁻¹' mulSupport f) ⊆ g ⁻¹' mulTSupport f
[PROOFSTEP]
rw [hg.toEmbedding.closure_eq_preimage_closure_image]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g✝ : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : HasCompactMulSupport f
g : α' → α
hg : ClosedEmbedding g
⊢ g ⁻¹' closure (g '' (g ⁻¹' mulSupport f)) ⊆ g ⁻¹' mulTSupport f
[PROOFSTEP]
exact preimage_mono (closure_mono <| image_preimage_subset _ _)
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : HasCompactMulSupport f
hf₂ : HasCompactMulSupport f₂
hm : m 1 1 = 1
⊢ HasCompactMulSupport fun x => m (f x) (f₂ x)
[PROOFSTEP]
rw [hasCompactMulSupport_iff_eventuallyEq] at hf hf₂ ⊢
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x : α
hf : f =ᶠ[coclosedCompact α] 1
hf₂ : f₂ =ᶠ[coclosedCompact α] 1
hm : m 1 1 = 1
⊢ (fun x => m (f x) (f₂ x)) =ᶠ[coclosedCompact α] 1
[PROOFSTEP]
filter_upwards [hf, hf₂] using fun x hx hx₂ => by simp_rw [hx, hx₂, Pi.one_apply, hm]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace α'
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
g : β → γ
f : α → β
f₂ : α → γ
m : β → γ → δ
x✝ : α
hf : f =ᶠ[coclosedCompact α] 1
hf₂ : f₂ =ᶠ[coclosedCompact α] 1
hm : m 1 1 = 1
x : α
hx : f x = OfNat.ofNat 1 x
hx₂ : f₂ x = OfNat.ofNat 1 x
⊢ m (f x) (f₂ x) = OfNat.ofNat 1 x
[PROOFSTEP]
simp_rw [hx, hx₂, Pi.one_apply, hm]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝³ : TopologicalSpace α
inst✝² : MonoidWithZero R
inst✝¹ : AddMonoid M
inst✝ : DistribMulAction R M
f : α → R
f' : α → M
x : α
hf : HasCompactSupport f'
⊢ HasCompactSupport (f • f')
[PROOFSTEP]
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝³ : TopologicalSpace α
inst✝² : MonoidWithZero R
inst✝¹ : AddMonoid M
inst✝ : DistribMulAction R M
f : α → R
f' : α → M
x : α
hf : f' =ᶠ[coclosedCompact α] 0
⊢ f • f' =ᶠ[coclosedCompact α] 0
[PROOFSTEP]
exact hf.mono fun x hx => by simp_rw [Pi.smul_apply', hx, Pi.zero_apply, smul_zero]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝³ : TopologicalSpace α
inst✝² : MonoidWithZero R
inst✝¹ : AddMonoid M
inst✝ : DistribMulAction R M
f : α → R
f' : α → M
x✝ : α
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = OfNat.ofNat 0 x
⊢ (f • f') x = OfNat.ofNat 0 x
[PROOFSTEP]
simp_rw [Pi.smul_apply', hx, Pi.zero_apply, smul_zero]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
x : α
hf : HasCompactSupport f
⊢ HasCompactSupport (f • f')
[PROOFSTEP]
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
x : α
hf : f =ᶠ[coclosedCompact α] 0
⊢ f • f' =ᶠ[coclosedCompact α] 0
[PROOFSTEP]
exact hf.mono fun x hx => by simp_rw [Pi.smul_apply', hx, Pi.zero_apply, zero_smul]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
x✝ : α
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = OfNat.ofNat 0 x
⊢ (f • f') x = OfNat.ofNat 0 x
[PROOFSTEP]
simp_rw [Pi.smul_apply', hx, Pi.zero_apply, zero_smul]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
x : α
hf : HasCompactSupport f'
⊢ HasCompactSupport (f • f')
[PROOFSTEP]
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
x : α
hf : f' =ᶠ[coclosedCompact α] 0
⊢ f • f' =ᶠ[coclosedCompact α] 0
[PROOFSTEP]
refine' hf.mono fun x hx => by simp_rw [Pi.smul_apply', hx, Pi.zero_apply, smul_zero]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝³ : TopologicalSpace α
inst✝² : Zero R
inst✝¹ : Zero M
inst✝ : SMulWithZero R M
f : α → R
f' : α → M
x✝ : α
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = OfNat.ofNat 0 x
⊢ (f • f') x = OfNat.ofNat 0 x
[PROOFSTEP]
simp_rw [Pi.smul_apply', hx, Pi.zero_apply, smul_zero]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
x : α
hf : HasCompactSupport f
⊢ HasCompactSupport (f * f')
[PROOFSTEP]
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
x : α
hf : f =ᶠ[coclosedCompact α] 0
⊢ f * f' =ᶠ[coclosedCompact α] 0
[PROOFSTEP]
refine' hf.mono fun x hx => by simp_rw [Pi.mul_apply, hx, Pi.zero_apply, zero_mul]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
x✝ : α
hf : f =ᶠ[coclosedCompact α] 0
x : α
hx : f x = OfNat.ofNat 0 x
⊢ (f * f') x = OfNat.ofNat 0 x
[PROOFSTEP]
simp_rw [Pi.mul_apply, hx, Pi.zero_apply, zero_mul]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
x : α
hf : HasCompactSupport f'
⊢ HasCompactSupport (f * f')
[PROOFSTEP]
rw [hasCompactSupport_iff_eventuallyEq] at hf ⊢
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
x : α
hf : f' =ᶠ[coclosedCompact α] 0
⊢ f * f' =ᶠ[coclosedCompact α] 0
[PROOFSTEP]
refine' hf.mono fun x hx => by simp_rw [Pi.mul_apply, hx, Pi.zero_apply, mul_zero]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
inst✝¹ : TopologicalSpace α
inst✝ : MulZeroClass β
f f' : α → β
x✝ : α
hf : f' =ᶠ[coclosedCompact α] 0
x : α
hx : f' x = OfNat.ofNat 0 x
⊢ (f * f') x = OfNat.ofNat 0 x
[PROOFSTEP]
simp_rw [Pi.mul_apply, hx, Pi.zero_apply, mul_zero]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
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
[PROOFSTEP]
obtain ⟨n, hn, hnf⟩ := hlf x
[GOAL]
case intro.intro
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
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
[PROOFSTEP]
classical
let is := hnf.toFinset.filter fun i => x ∈ U i
let js := hnf.toFinset.filter fun j => 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.not_mem_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 [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⟩⟩
[GOAL]
case intro.intro
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
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
[PROOFSTEP]
let is := hnf.toFinset.filter fun i => x ∈ U i
[GOAL]
case intro.intro
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
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
[PROOFSTEP]
let js := hnf.toFinset.filter fun j => x ∉ U j
[GOAL]
case intro.intro
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
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
[PROOFSTEP]
refine'
  ⟨is, (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i, inter_mem (inter_mem hn _) _, inter_subset_right _ _,
    fun z hz => _⟩
[GOAL]
case intro.intro.refine'_1
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
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
[PROOFSTEP]
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)
[GOAL]
case intro.intro.refine'_2
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
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
[PROOFSTEP]
exact (biInter_finset_mem is).mpr fun i hi => (ho i).mem_nhds (Finset.mem_filter.mp hi).2
[GOAL]
case intro.intro.refine'_3
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
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
[PROOFSTEP]
have hzn : z ∈ n := by
  rw [inter_assoc] at hz 
  exact mem_of_mem_inter_left hz
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
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
[PROOFSTEP]
rw [inter_assoc] at hz 
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
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
[PROOFSTEP]
exact mem_of_mem_inter_left hz
[GOAL]
case intro.intro.refine'_3
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
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
[PROOFSTEP]
replace hz := mem_of_mem_inter_right (mem_of_mem_inter_left hz)
[GOAL]
case intro.intro.refine'_3
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
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
[PROOFSTEP]
simp only [Finset.mem_filter, Finite.mem_toFinset, mem_setOf_eq, mem_iInter, and_imp] at hz 
[GOAL]
case intro.intro.refine'_3
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
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
[PROOFSTEP]
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]
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
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
[PROOFSTEP]
refine' hnf.toFinset.subset_coe_filter_of_subset_forall _ this fun i hi => _
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
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
[PROOFSTEP]
specialize hz i ⟨z, ⟨hi, hzn⟩⟩
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
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
[PROOFSTEP]
contrapose hz
[GOAL]
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
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))ᶜ)
[PROOFSTEP]
simp [hz, subset_mulTSupport (f i) hi]
[GOAL]
case intro.intro.refine'_3
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
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)
[PROOFSTEP]
intro i hi
[GOAL]
case intro.intro.refine'_3
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
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)
[PROOFSTEP]
simp only [Finite.coe_toFinset, mem_setOf_eq]
[GOAL]
case intro.intro.refine'_3
X : Type u_1
α : Type u_2
α' : Type u_3
β : Type u_4
γ : Type u_5
δ : Type u_6
M : Type u_7
E : Type u_8
R : Type u_9
ι : Type u_10
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)
[PROOFSTEP]
exact ⟨z, ⟨hi, hzn⟩⟩
