case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.5500
δ : Type ?u.5503
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
di : DenseInducing i
b : β
s : Set β
hs : s ∈ 𝓝 b
a : α
ha : i a ∈ s
⊢ ∃ a, i a ∈ s
α : Type u_1
β : Type u_2
γ : Type ?u.5500
δ : Type ?u.5503
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
di : DenseInducing i
b : β
s : Set β
hs : s ∈ 𝓝 b
⊢ ∃ a, i a ∈ s
rcases mem_closure_iff_nhds.1 (di.dense b) s hs with ⟨_, ⟨ha, a, rfl⟩⟩
no goals
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.5500
δ : Type ?u.5503
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
di : DenseInducing i
b : β
s : Set β
hs : s ∈ 𝓝 b
a : α
ha : i a ∈ s
⊢ ∃ a, i a ∈ s
exact ⟨a, ha⟩