case mp
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
⊢ ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U

case mpr
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
⊢ IsBasis B
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
⊢ IsBasis B ↔ ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
constructor <;> intro h
case mp.mk
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
⊢ ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ { carrier := sU, is_open' := hU }
case mp
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
⊢ ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
rintro ⟨sU, hU⟩ x hx
case mp.mk.intro.intro.intro.intro
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
V : Opens α
H₁ : V ∈ B
H₂ : ↑V = sV
⊢ ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ { carrier := sU, is_open' := hU }
case mp.mk
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
⊢ ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ { carrier := sU, is_open' := hU }
rcases h.mem_nhds_iff.mp (IsOpen.mem_nhds hU hx) with ⟨sV, ⟨⟨V, H₁, H₂⟩, hsV⟩⟩
case mp.mk.intro.intro.intro.intro
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
V : Opens α
H₁ : V ∈ B
H₂ : ↑V = sV
⊢ x ∈ V ∧ V ≤ { carrier := sU, is_open' := hU }
case mp.mk.intro.intro.intro.intro
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
V : Opens α
H₁ : V ∈ B
H₂ : ↑V = sV
⊢ ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ { carrier := sU, is_open' := hU }
refine' ⟨V, H₁, _⟩
case mp.mk.intro.intro.intro.intro.mk
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
carrier✝ : Set α
is_open'✝ : IsOpen carrier✝
H₁ : { carrier := carrier✝, is_open' := is_open'✝ } ∈ B
H₂ : ↑{ carrier := carrier✝, is_open' := is_open'✝ } = sV
⊢ x ∈ { carrier := carrier✝, is_open' := is_open'✝ } ∧
    { carrier := carrier✝, is_open' := is_open'✝ } ≤ { carrier := sU, is_open' := hU }
case mp.mk.intro.intro.intro.intro
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
V : Opens α
H₁ : V ∈ B
H₂ : ↑V = sV
⊢ x ∈ V ∧ V ≤ { carrier := sU, is_open' := hU }
cases V
case mp.mk.intro.intro.intro.intro.mk
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
carrier✝ : Set α
is_open'✝ : IsOpen carrier✝
H₁ : { carrier := carrier✝, is_open' := is_open'✝ } ∈ B
H₂ : carrier✝ = sV
⊢ x ∈ { carrier := carrier✝, is_open' := is_open'✝ } ∧
    { carrier := carrier✝, is_open' := is_open'✝ } ≤ { carrier := sU, is_open' := hU }
case mp.mk.intro.intro.intro.intro.mk
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
carrier✝ : Set α
is_open'✝ : IsOpen carrier✝
H₁ : { carrier := carrier✝, is_open' := is_open'✝ } ∈ B
H₂ : ↑{ carrier := carrier✝, is_open' := is_open'✝ } = sV
⊢ x ∈ { carrier := carrier✝, is_open' := is_open'✝ } ∧
    { carrier := carrier✝, is_open' := is_open'✝ } ≤ { carrier := sU, is_open' := hU }
dsimp at H₂
case mp.mk.intro.intro.intro.intro.mk
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
carrier✝ : Set α
is_open'✝ : IsOpen carrier✝
H₁ : { carrier := carrier✝, is_open' := is_open'✝ } ∈ B
hsV : x ∈ carrier✝ ∧ carrier✝ ⊆ sU
⊢ x ∈ { carrier := carrier✝, is_open' := is_open'✝ } ∧
    { carrier := carrier✝, is_open' := is_open'✝ } ≤ { carrier := sU, is_open' := hU }
case mp.mk.intro.intro.intro.intro.mk
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
carrier✝ : Set α
is_open'✝ : IsOpen carrier✝
H₁ : { carrier := carrier✝, is_open' := is_open'✝ } ∈ B
H₂ : carrier✝ = sV
⊢ x ∈ { carrier := carrier✝, is_open' := is_open'✝ } ∧
    { carrier := carrier✝, is_open' := is_open'✝ } ≤ { carrier := sU, is_open' := hU }
subst H₂
no goals
case mp.mk.intro.intro.intro.intro.mk
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU }
carrier✝ : Set α
is_open'✝ : IsOpen carrier✝
H₁ : { carrier := carrier✝, is_open' := is_open'✝ } ∈ B
hsV : x ∈ carrier✝ ∧ carrier✝ ⊆ sU
⊢ x ∈ { carrier := carrier✝, is_open' := is_open'✝ } ∧
    { carrier := carrier✝, is_open' := is_open'✝ } ≤ { carrier := sU, is_open' := hU }
exact hsV
case mpr.refine'_1
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
⊢ ∀ (u : Set α), u ∈ SetLike.coe '' B → IsOpen u

case mpr.refine'_2
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ SetLike.coe '' B ∧ a ∈ v ∧ v ⊆ u
case mpr
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
⊢ IsBasis B
refine' isTopologicalBasis_of_open_of_nhds _ _
case mpr.refine'_1.intro.intro
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
U : Opens α
⊢ IsOpen ↑U
case mpr.refine'_1
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
⊢ ∀ (u : Set α), u ∈ SetLike.coe '' B → IsOpen u
rintro sU ⟨U, -, rfl⟩
no goals
case mpr.refine'_1.intro.intro
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
U : Opens α
⊢ IsOpen ↑U
exact U.2
case mpr.refine'_2
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
x : α
sU : Set α
hx : x ∈ sU
hsU : IsOpen sU
⊢ ∃ v, v ∈ SetLike.coe '' B ∧ x ∈ v ∧ v ⊆ sU
case mpr.refine'_2
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
⊢ ∀ (a : α) (u : Set α), a ∈ u → IsOpen u → ∃ v, v ∈ SetLike.coe '' B ∧ a ∈ v ∧ v ⊆ u
intro x sU hx hsU
case mpr.refine'_2.intro.intro
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
x : α
sU : Set α
hx : x ∈ sU
hsU : IsOpen sU
V : Opens α
hV : V ∈ B
H : x ∈ V ∧ V ≤ { carrier := sU, is_open' := hsU }
⊢ ∃ v, v ∈ SetLike.coe '' B ∧ x ∈ v ∧ v ⊆ sU
case mpr.refine'_2
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
x : α
sU : Set α
hx : x ∈ sU
hsU : IsOpen sU
⊢ ∃ v, v ∈ SetLike.coe '' B ∧ x ∈ v ∧ v ⊆ sU
rcases @h ⟨sU, hsU⟩ x hx with ⟨V, hV, H⟩
no goals
case mpr.refine'_2.intro.intro
ι : Type ?u.30155
α : Type u_1
β : Type ?u.30161
γ : Type ?u.30164
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U', U' ∈ B ∧ x ∈ U' ∧ U' ≤ U
x : α
sU : Set α
hx : x ∈ sU
hsU : IsOpen sU
V : Opens α
hV : V ∈ B
H : x ∈ V ∧ V ≤ { carrier := sU, is_open' := hsU }
⊢ ∃ v, v ∈ SetLike.coe '' B ∧ x ∈ v ∧ v ⊆ sU
exact ⟨V, ⟨V, hV, rfl⟩, H⟩