α : Type u
β : Type v
γ : Type ?u.340703
δ : Type ?u.340706
ε : Type ?u.340709
ζ : Type ?u.340712
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.340723
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : DecidableEq ι
s : Set ((a : ι) → π a)
x y : (a : ι) → π a
hs : ∃ I t, (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ Set.pi (↑I) t ⊆ s
⊢ ∃ I, Finset.piecewise I x y ∈ s
α : Type u
β : Type v
γ : Type ?u.340703
δ : Type ?u.340706
ε : Type ?u.340709
ζ : Type ?u.340712
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.340723
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : DecidableEq ι
s : Set ((a : ι) → π a)
x : (a : ι) → π a
hs : s ∈ 𝓝 x
y : (a : ι) → π a
⊢ ∃ I, Finset.piecewise I x y ∈ s
simp only [nhds_pi, Filter.mem_pi'] at hs
case intro.intro.intro
α : Type u
β : Type v
γ : Type ?u.340703
δ : Type ?u.340706
ε : Type ?u.340709
ζ : Type ?u.340712
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.340723
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : DecidableEq ι
s : Set ((a : ι) → π a)
x y : (a : ι) → π a
I : Finset ι
t : (i : ι) → Set (π i)
htx : ∀ (i : ι), t i ∈ 𝓝 (x i)
hts : Set.pi (↑I) t ⊆ s
⊢ ∃ I, Finset.piecewise I x y ∈ s
α : Type u
β : Type v
γ : Type ?u.340703
δ : Type ?u.340706
ε : Type ?u.340709
ζ : Type ?u.340712
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.340723
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : DecidableEq ι
s : Set ((a : ι) → π a)
x y : (a : ι) → π a
hs : ∃ I t, (∀ (i : ι), t i ∈ 𝓝 (x i)) ∧ Set.pi (↑I) t ⊆ s
⊢ ∃ I, Finset.piecewise I x y ∈ s
rcases hs with ⟨I, t, htx, hts⟩
case intro.intro.intro
α : Type u
β : Type v
γ : Type ?u.340703
δ : Type ?u.340706
ε : Type ?u.340709
ζ : Type ?u.340712
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.340723
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : DecidableEq ι
s : Set ((a : ι) → π a)
x y : (a : ι) → π a
I : Finset ι
t : (i : ι) → Set (π i)
htx : ∀ (i : ι), t i ∈ 𝓝 (x i)
hts : Set.pi (↑I) t ⊆ s
i : ι
hi : i ∈ ↑I
⊢ Finset.piecewise I x y i ∈ t i
case intro.intro.intro
α : Type u
β : Type v
γ : Type ?u.340703
δ : Type ?u.340706
ε : Type ?u.340709
ζ : Type ?u.340712
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.340723
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : DecidableEq ι
s : Set ((a : ι) → π a)
x y : (a : ι) → π a
I : Finset ι
t : (i : ι) → Set (π i)
htx : ∀ (i : ι), t i ∈ 𝓝 (x i)
hts : Set.pi (↑I) t ⊆ s
⊢ ∃ I, Finset.piecewise I x y ∈ s
refine' ⟨I, hts fun i hi => _⟩
no goals
case intro.intro.intro
α : Type u
β : Type v
γ : Type ?u.340703
δ : Type ?u.340706
ε : Type ?u.340709
ζ : Type ?u.340712
ι : Type u_1
π : ι → Type u_2
κ : Type ?u.340723
inst✝² : TopologicalSpace α
inst✝¹ : (i : ι) → TopologicalSpace (π i)
f : α → (i : ι) → π i
inst✝ : DecidableEq ι
s : Set ((a : ι) → π a)
x y : (a : ι) → π a
I : Finset ι
t : (i : ι) → Set (π i)
htx : ∀ (i : ι), t i ∈ 𝓝 (x i)
hts : Set.pi (↑I) t ⊆ s
i : ι
hi : i ∈ ↑I
⊢ Finset.piecewise I x y i ∈ t i
simpa [Finset.mem_coe.1 hi] using mem_of_mem_nhds (htx i)