case refine'_1
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
⊢ ∀ (u : Set ((i : ι) → X i)), u ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} → IsOpen u

case refine'_2
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
⊢ ∀ (a : (i : ι) → X i) (u : Set ((i : ι) → X i)),
    a ∈ u → IsOpen u → ∃ v, v ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} ∧ a ∈ v ∧ v ⊆ u
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
⊢ IsTopologicalBasis {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U}
refine' isTopologicalBasis_of_open_of_nhds _ _
case refine'_1.intro.intro.intro
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ IsOpen (Set.pi (↑F) U)
case refine'_1
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
⊢ ∀ (u : Set ((i : ι) → X i)), u ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} → IsOpen u
rintro _ ⟨U, F, h1, rfl⟩
case refine'_1.intro.intro.intro
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ ∀ (a : ι), a ∈ ↑F → IsOpen (U a)
case refine'_1.intro.intro.intro
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ IsOpen (Set.pi (↑F) U)
apply isOpen_set_pi F.finite_toSet
case refine'_1.intro.intro.intro
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
i : ι
hi : i ∈ ↑F
⊢ IsOpen (U i)
case refine'_1.intro.intro.intro
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
⊢ ∀ (a : ι), a ∈ ↑F → IsOpen (U a)
intro i hi
no goals
case refine'_1.intro.intro.intro
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
U : (i : ι) → Set (X i)
F : Finset ι
h1 : ∀ (i : ι), i ∈ F → U i ∈ T i
i : ι
hi : i ∈ ↑F
⊢ IsOpen (U i)
exact (cond i).isOpen (h1 i hi)
case refine'_2
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
a : (i : ι) → X i
U : Set ((i : ι) → X i)
ha : a ∈ U
hU : IsOpen U
⊢ ∃ v, v ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} ∧ a ∈ v ∧ v ⊆ U
case refine'_2
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
⊢ ∀ (a : (i : ι) → X i) (u : Set ((i : ι) → X i)),
    a ∈ u → IsOpen u → ∃ v, v ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} ∧ a ∈ v ∧ v ⊆ u
intro a U ha hU
case refine'_2.intro.intro.intro
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
a : (i : ι) → X i
U : Set ((i : ι) → X i)
ha : a ∈ U
hU : IsOpen U
I : Finset ι
t : (i : ι) → Set (X i)
hta : ∀ (i : ι), t i ∈ 𝓝 (a i)
htU : Set.pi (?m.30812 I t) t ⊆ U
⊢ ∃ v, v ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} ∧ a ∈ v ∧ v ⊆ U
case refine'_2
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
a : (i : ι) → X i
U : Set ((i : ι) → X i)
ha : a ∈ U
hU : IsOpen U
⊢ ∃ v, v ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} ∧ a ∈ v ∧ v ⊆ U
obtain ⟨I, t, hta, htU⟩ : ∃ (I : Finset ι) (t : ∀ i : ι, Set (X i)),
    (∀ i, t i ∈ 𝓝 (a i)) ∧ Set.pi (↑I) t ⊆ U := by
  rw [← Filter.mem_pi', ← nhds_pi]
  exact hU.mem_nhds ha
case refine'_2.intro.intro.intro
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
a : (i : ι) → X i
U : Set ((i : ι) → X i)
ha : a ∈ U
hU : IsOpen U
I : Finset ι
t : (i : ι) → Set (X i)
hta : ∀ (i : ι), t i ∈ 𝓝 (a i)
htU : Set.pi (↑I) t ⊆ U
this : ∀ (i : ι), ∃ V, V ∈ T i ∧ a i ∈ V ∧ V ⊆ t i
⊢ ∃ v, v ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} ∧ a ∈ v ∧ v ⊆ U
case refine'_2.intro.intro.intro
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
a : (i : ι) → X i
U : Set ((i : ι) → X i)
ha : a ∈ U
hU : IsOpen U
I : Finset ι
t : (i : ι) → Set (X i)
hta : ∀ (i : ι), t i ∈ 𝓝 (a i)
htU : Set.pi (?m.30812 I t) t ⊆ U
⊢ ∃ v, v ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} ∧ a ∈ v ∧ v ⊆ U
have : ∀ i, ∃ V ∈ T i, a i ∈ V ∧ V ⊆ t i := fun i => (cond i).mem_nhds_iff.1 (hta i)
case refine'_2.intro.intro.intro
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
a : (i : ι) → X i
U : Set ((i : ι) → X i)
ha : a ∈ U
hU : IsOpen U
I : Finset ι
t : (i : ι) → Set (X i)
hta : ∀ (i : ι), t i ∈ 𝓝 (a i)
htU : Set.pi (↑I) t ⊆ U
V : (i : ι) → Set (X i)
hVT : ∀ (i : ι), V i ∈ T i
haV : ∀ (i : ι), a i ∈ V i
hVt : ∀ (i : ι), V i ⊆ t i
⊢ ∃ v, v ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} ∧ a ∈ v ∧ v ⊆ U
case refine'_2.intro.intro.intro
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
a : (i : ι) → X i
U : Set ((i : ι) → X i)
ha : a ∈ U
hU : IsOpen U
I : Finset ι
t : (i : ι) → Set (X i)
hta : ∀ (i : ι), t i ∈ 𝓝 (a i)
htU : Set.pi (↑I) t ⊆ U
this : ∀ (i : ι), ∃ V, V ∈ T i ∧ a i ∈ V ∧ V ⊆ t i
⊢ ∃ v, v ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} ∧ a ∈ v ∧ v ⊆ U
choose V hVT haV hVt using this
no goals
case refine'_2.intro.intro.intro
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
a : (i : ι) → X i
U : Set ((i : ι) → X i)
ha : a ∈ U
hU : IsOpen U
I : Finset ι
t : (i : ι) → Set (X i)
hta : ∀ (i : ι), t i ∈ 𝓝 (a i)
htU : Set.pi (↑I) t ⊆ U
V : (i : ι) → Set (X i)
hVT : ∀ (i : ι), V i ∈ T i
haV : ∀ (i : ι), a i ∈ V i
hVt : ∀ (i : ι), V i ⊆ t i
⊢ ∃ v, v ∈ {S | ∃ U F, (∀ (i : ι), i ∈ F → U i ∈ T i) ∧ S = Set.pi (↑F) U} ∧ a ∈ v ∧ v ⊆ U
exact ⟨_, ⟨V, I, fun i _ => hVT i, rfl⟩, fun i _ => haV i, (pi_mono fun i _ => hVt i).trans htU⟩
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
a : (i : ι) → X i
U : Set ((i : ι) → X i)
ha : a ∈ U
hU : IsOpen U
⊢ U ∈ 𝓝 fun i => a i
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
a : (i : ι) → X i
U : Set ((i : ι) → X i)
ha : a ∈ U
hU : IsOpen U
⊢ ∃ I t, (∀ (i : ι), t i ∈ 𝓝 (a i)) ∧ Set.pi (↑I) t ⊆ U
rw [← Filter.mem_pi', ← nhds_pi]
no goals
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
a : (i : ι) → X i
U : Set ((i : ι) → X i)
ha : a ∈ U
hU : IsOpen U
⊢ U ∈ 𝓝 fun i => a i
exact hU.mem_nhds ha