case refine'_1
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : (⋃ (i : ι), U i) = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
hu : u ∈ ⋃ (i : ι), image Subtype.val '' b i
⊢ IsOpen u

case refine'_2
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : (⋃ (i : ι), U i) = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, (v ∈ ⋃ (i : ι), image Subtype.val '' b i) ∧ a ∈ v ∧ v ⊆ u
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : (⋃ (i : ι), U i) = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
⊢ IsTopologicalBasis (⋃ (i : ι), image Subtype.val '' b i)
refine' isTopologicalBasis_of_open_of_nhds (fun u hu => _) _
case refine'_1
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : (⋃ (i : ι), U i) = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
hu : ∃ i x, x ∈ b i ∧ Subtype.val '' x = u
⊢ IsOpen u
case refine'_1
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : (⋃ (i : ι), U i) = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
hu : u ∈ ⋃ (i : ι), image Subtype.val '' b i
⊢ IsOpen u
simp only [mem_iUnion, mem_image] at hu
case refine'_1.intro.intro.intro
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : (⋃ (i : ι), U i) = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
i : ι
s : Set { x // x ∈ U i }
sb : s ∈ b i
⊢ IsOpen (Subtype.val '' s)
case refine'_1
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : (⋃ (i : ι), U i) = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
hu : ∃ i x, x ∈ b i ∧ Subtype.val '' x = u
⊢ IsOpen u
rcases hu with ⟨i, s, sb, rfl⟩
no goals
case refine'_1.intro.intro.intro
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : (⋃ (i : ι), U i) = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
i : ι
s : Set { x // x ∈ U i }
sb : s ∈ b i
⊢ IsOpen (Subtype.val '' s)
exact (Uo i).isOpenMap_subtype_val _ ((hb i).isOpen sb)
case refine'_2
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : (⋃ (i : ι), U i) = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
a : α
u : Set α
ha : a ∈ u
uo : IsOpen u
⊢ ∃ v, (v ∈ ⋃ (i : ι), image Subtype.val '' b i) ∧ a ∈ v ∧ v ⊆ u
case refine'_2
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : (⋃ (i : ι), U i) = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, (v ∈ ⋃ (i : ι), image Subtype.val '' b i) ∧ a ∈ v ∧ v ⊆ u
intro a u ha uo
case refine'_2.intro
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : (⋃ (i : ι), U i) = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
a : α
u : Set α
ha : a ∈ u
uo : IsOpen u
i : ι
hi : a ∈ U i
⊢ ∃ v, (v ∈ ⋃ (i : ι), image Subtype.val '' b i) ∧ a ∈ v ∧ v ⊆ u
case refine'_2
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : (⋃ (i : ι), U i) = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
a : α
u : Set α
ha : a ∈ u
uo : IsOpen u
⊢ ∃ v, (v ∈ ⋃ (i : ι), image Subtype.val '' b i) ∧ a ∈ v ∧ v ⊆ u
rcases iUnion_eq_univ_iff.1 Uc a with ⟨i, hi⟩
case refine'_2.intro.intro
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : (⋃ (i : ι), U i) = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
uo : IsOpen u
i : ι
a : { x // x ∈ U i }
ha : ↑a ∈ u
⊢ ∃ v, (v ∈ ⋃ (i : ι), image Subtype.val '' b i) ∧ ↑a ∈ v ∧ v ⊆ u
case refine'_2.intro
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : (⋃ (i : ι), U i) = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
a : α
u : Set α
ha : a ∈ u
uo : IsOpen u
i : ι
hi : a ∈ U i
⊢ ∃ v, (v ∈ ⋃ (i : ι), image Subtype.val '' b i) ∧ a ∈ v ∧ v ⊆ u
lift a to ↥(U i) using hi
case refine'_2.intro.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : (⋃ (i : ι), U i) = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
uo : IsOpen u
i : ι
a : { x // x ∈ U i }
ha : ↑a ∈ u
v : Set ↑(U i)
hvb : v ∈ b i
hav : ?m.22393 ∈ v
hvu : v ⊆ Subtype.val ⁻¹' u
⊢ ∃ v, (v ∈ ⋃ (i : ι), image Subtype.val '' b i) ∧ ↑a ∈ v ∧ v ⊆ u
case refine'_2.intro.intro
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : (⋃ (i : ι), U i) = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
uo : IsOpen u
i : ι
a : { x // x ∈ U i }
ha : ↑a ∈ u
⊢ ∃ v, (v ∈ ⋃ (i : ι), image Subtype.val '' b i) ∧ ↑a ∈ v ∧ v ⊆ u
rcases(hb i).exists_subset_of_mem_open ha (uo.preimage continuous_subtype_val) with
  ⟨v, hvb, hav, hvu⟩
no goals
case refine'_2.intro.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
ι : Sort u_1
U : ι → Set α
Uo : ∀ (i : ι), IsOpen (U i)
Uc : (⋃ (i : ι), U i) = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
u : Set α
uo : IsOpen u
i : ι
a : { x // x ∈ U i }
ha : ↑a ∈ u
v : Set ↑(U i)
hvb : v ∈ b i
hav : ?m.22393 ∈ v
hvu : v ⊆ Subtype.val ⁻¹' u
⊢ ∃ v, (v ∈ ⋃ (i : ι), image Subtype.val '' b i) ∧ ↑a ∈ v ∧ v ⊆ u
exact ⟨(↑) '' v, mem_iUnion.2 ⟨i, mem_image_of_mem _ hvb⟩, mem_image_of_mem _ hav,
  image_subset_iff.2 hvu⟩