[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
s : Set α
a : α
di : DenseInducing i
hs : s ∈ 𝓝 a
⊢ closure (i '' s) ∈ 𝓝 (i a)
[PROOFSTEP]
rw [di.nhds_eq_comap a, ((nhds_basis_opens _).comap _).mem_iff] at hs 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
s : Set α
a : α
di : DenseInducing i
hs : ∃ i_1, (i a ∈ i_1 ∧ IsOpen i_1) ∧ i ⁻¹' i_1 ⊆ s
⊢ closure (i '' s) ∈ 𝓝 (i a)
[PROOFSTEP]
rcases hs with ⟨U, ⟨haU, hUo⟩, sub : i ⁻¹' U ⊆ s⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
s : Set α
a : α
di : DenseInducing i
U : Set β
sub : i ⁻¹' U ⊆ s
haU : i a ∈ U
hUo : IsOpen U
⊢ closure (i '' s) ∈ 𝓝 (i a)
[PROOFSTEP]
refine' mem_of_superset (hUo.mem_nhds haU) _
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
s : Set α
a : α
di : DenseInducing i
U : Set β
sub : i ⁻¹' U ⊆ s
haU : i a ∈ U
hUo : IsOpen U
⊢ U ⊆ closure (i '' s)
[PROOFSTEP]
calc
  U ⊆ closure (i '' (i ⁻¹' U)) := di.dense.subset_closure_image_preimage_of_isOpen hUo
  _ ⊆ closure (i '' s) := closure_mono (image_subset i sub)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di✝ di : DenseInducing i
s : Set α
⊢ Dense (i '' s) ↔ Dense s
[PROOFSTEP]
refine' ⟨fun H x => _, di.dense.dense_image di.continuous⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di✝ di : DenseInducing i
s : Set α
H : Dense (i '' s)
x : α
⊢ x ∈ closure s
[PROOFSTEP]
rw [di.toInducing.closure_eq_preimage_closure_image, H.closure_eq, preimage_univ]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
i : α → β
di✝ di : DenseInducing i
s : Set α
H : Dense (i '' s)
x : α
⊢ x ∈ univ
[PROOFSTEP]
trivial
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : T2Space β
di : DenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
⊢ interior s = ∅
[PROOFSTEP]
refine' eq_empty_iff_forall_not_mem.2 fun x hx => _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : T2Space β
di : DenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : x ∈ interior s
⊢ False
[PROOFSTEP]
rw [mem_interior_iff_mem_nhds] at hx 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : T2Space β
di : DenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
⊢ False
[PROOFSTEP]
have := di.closure_image_mem_nhds hx
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : T2Space β
di : DenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
this : closure (i '' s) ∈ 𝓝 (i x)
⊢ False
[PROOFSTEP]
rw [(hs.image di.continuous).isClosed.closure_eq] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : T2Space β
di : DenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
this : i '' s ∈ 𝓝 (i x)
⊢ False
[PROOFSTEP]
rcases hd.inter_nhds_nonempty this with ⟨y, hyi, hys⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : T2Space β
di : DenseInducing i
hd : Dense (range i)ᶜ
s : Set α
hs : IsCompact s
x : α
hx : s ∈ 𝓝 x
this : i '' s ∈ 𝓝 (i x)
y : β
hyi : y ∈ (range i)ᶜ
hys : y ∈ i '' s
⊢ False
[PROOFSTEP]
exact hyi (image_subset_range _ _ hys)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : DenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
[PROOFSTEP]
have lim1 : map g (comap g (𝓝 d)) ≤ 𝓝 d := map_comap_le
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : DenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map g (comap g (𝓝 d)) ≤ 𝓝 d
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
[PROOFSTEP]
replace lim1 : map h (map g (comap g (𝓝 d))) ≤ map h (𝓝 d) := map_mono lim1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : DenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map h (map g (comap g (𝓝 d))) ≤ map h (𝓝 d)
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
[PROOFSTEP]
rw [Filter.map_map, comm, ← Filter.map_map, map_le_iff_le_comap] at lim1 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : DenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
[PROOFSTEP]
have lim2 : comap i (map h (𝓝 d)) ≤ comap i (𝓝 (i a)) := comap_mono H
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : DenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))
lim2 : comap i (map h (𝓝 d)) ≤ comap i (𝓝 (i a))
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
[PROOFSTEP]
rw [← di.nhds_eq_comap] at lim2 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
d : δ
a : α
di : DenseInducing i
H : Tendsto h (𝓝 d) (𝓝 (i a))
comm : h ∘ g = i ∘ f
lim1 : map f (comap g (𝓝 d)) ≤ comap i (map h (𝓝 d))
lim2 : comap i (map h (𝓝 d)) ≤ 𝓝 a
⊢ Tendsto f (comap g (𝓝 d)) (𝓝 a)
[PROOFSTEP]
exact le_trans lim1 lim2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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
[PROOFSTEP]
rcases mem_closure_iff_nhds.1 (di.dense b) s hs with ⟨_, ⟨ha, a, rfl⟩⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
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
[PROOFSTEP]
exact ⟨a, ha⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
di : DenseInducing i
hf : ∀ (b : β), ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)
a : α
⊢ extend di f (i a) = f a
[PROOFSTEP]
rcases hf (i a) with ⟨b, hb⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
di : DenseInducing i
hf : ∀ (b : β), ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)
a : α
b : γ
hb : Tendsto f (comap i (𝓝 (i a))) (𝓝 b)
⊢ extend di f (i a) = f a
[PROOFSTEP]
refine' di.extend_eq_at' b _
[GOAL]
case intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
f : α → γ
di : DenseInducing i
hf : ∀ (b : β), ∃ c, Tendsto f (comap i (𝓝 b)) (𝓝 c)
a : α
b : γ
hb : Tendsto f (comap i (𝓝 (i a))) (𝓝 b)
⊢ Tendsto f (𝓝 a) (𝓝 b)
[PROOFSTEP]
rwa [← di.toInducing.nhds_eq_comap] at hb 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g✝ : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
b : β
f : α → γ
g : β → γ
di : DenseInducing i
hf : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) = f x
hg : ContinuousAt g b
⊢ extend di f b = g b
[PROOFSTEP]
refine' di.extend_eq_of_tendsto fun s hs => mem_map.2 _
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g✝ : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
b : β
f : α → γ
g : β → γ
di : DenseInducing i
hf : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) = f x
hg : ContinuousAt g b
s : Set γ
hs : s ∈ 𝓝 (g b)
⊢ f ⁻¹' s ∈ comap i (𝓝 b)
[PROOFSTEP]
suffices : ∀ᶠ x : α in comap i (𝓝 b), g (i x) ∈ s
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g✝ : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
b : β
f : α → γ
g : β → γ
di : DenseInducing i
hf : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) = f x
hg : ContinuousAt g b
s : Set γ
hs : s ∈ 𝓝 (g b)
this : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) ∈ s
⊢ f ⁻¹' s ∈ comap i (𝓝 b)
case this
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g✝ : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
b : β
f : α → γ
g : β → γ
di : DenseInducing i
hf : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) = f x
hg : ContinuousAt g b
s : Set γ
hs : s ∈ 𝓝 (g b)
⊢ ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) ∈ s
[PROOFSTEP]
exact hf.mp (this.mono fun x hgx hfx => hfx ▸ hgx)
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g✝ : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
b : β
f : α → γ
g : β → γ
di : DenseInducing i
hf : ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) = f x
hg : ContinuousAt g b
s : Set γ
hs : s ∈ 𝓝 (g b)
⊢ ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) ∈ s
[PROOFSTEP]
clear hf f
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f : γ → α
g✝ : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
b : β
g : β → γ
di : DenseInducing i
hg : ContinuousAt g b
s : Set γ
hs : s ∈ 𝓝 (g b)
⊢ ∀ᶠ (x : α) in comap i (𝓝 b), g (i x) ∈ s
[PROOFSTEP]
refine' eventually_comap.2 ((hg.eventually hs).mono _)
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f : γ → α
g✝ : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
b : β
g : β → γ
di : DenseInducing i
hg : ContinuousAt g b
s : Set γ
hs : s ∈ 𝓝 (g b)
⊢ ∀ (x : β), s (g x) → ∀ (a : α), i a = x → g (i a) ∈ s
[PROOFSTEP]
rintro _ hxs x rfl
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f : γ → α
g✝ : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T2Space γ
b : β
g : β → γ
di : DenseInducing i
hg : ContinuousAt g b
s : Set γ
hs : s ∈ 𝓝 (g b)
x : α
hxs : s (g (i x))
⊢ g (i x) ∈ s
[PROOFSTEP]
exact hxs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
⊢ ContinuousAt (extend di f) b
[PROOFSTEP]
set φ := di.extend f
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
⊢ ContinuousAt φ b
[PROOFSTEP]
haveI := di.comap_nhds_neBot
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
⊢ ContinuousAt φ b
[PROOFSTEP]
suffices ∀ V' ∈ 𝓝 (φ b), IsClosed V' → φ ⁻¹' V' ∈ 𝓝 b by
  simpa [ContinuousAt, (closed_nhds_basis (φ b)).tendsto_right_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this✝ : ∀ (b : β), NeBot (comap i (𝓝 b))
this : ∀ (V' : Set γ), V' ∈ 𝓝 (φ b) → IsClosed V' → φ ⁻¹' V' ∈ 𝓝 b
⊢ ContinuousAt φ b
[PROOFSTEP]
simpa [ContinuousAt, (closed_nhds_basis (φ b)).tendsto_right_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
⊢ ∀ (V' : Set γ), V' ∈ 𝓝 (φ b) → IsClosed V' → φ ⁻¹' V' ∈ 𝓝 b
[PROOFSTEP]
intro V' V'_in V'_closed
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
⊢ φ ⁻¹' V' ∈ 𝓝 b
[PROOFSTEP]
set V₁ := {x | Tendsto f (comap i <| 𝓝 x) (𝓝 <| φ x)}
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
⊢ φ ⁻¹' V' ∈ 𝓝 b
[PROOFSTEP]
have V₁_in : V₁ ∈ 𝓝 b := by
  filter_upwards [hf]
  rintro x ⟨c, hc⟩
  rwa [di.extend_eq_of_tendsto hc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
⊢ V₁ ∈ 𝓝 b
[PROOFSTEP]
filter_upwards [hf]
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
⊢ ∀ (a : β), (∃ c, Tendsto f (comap i (𝓝 a)) (𝓝 c)) → Tendsto f (comap i (𝓝 a)) (𝓝 (extend di f a))
[PROOFSTEP]
rintro x ⟨c, hc⟩
[GOAL]
case h.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
x : β
c : γ
hc : Tendsto f (comap i (𝓝 x)) (𝓝 c)
⊢ Tendsto f (comap i (𝓝 x)) (𝓝 (extend di f x))
[PROOFSTEP]
rwa [di.extend_eq_of_tendsto hc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
⊢ φ ⁻¹' V' ∈ 𝓝 b
[PROOFSTEP]
obtain ⟨V₂, V₂_in, V₂_op, hV₂⟩ : ∃ V₂ ∈ 𝓝 b, IsOpen V₂ ∧ ∀ x ∈ i ⁻¹' V₂, f x ∈ V' := by
  simpa [and_assoc] using ((nhds_basis_opens' b).comap i).tendsto_left_iff.mp (mem_of_mem_nhds V₁_in : b ∈ V₁) V' V'_in
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
⊢ ∃ V₂, V₂ ∈ 𝓝 b ∧ IsOpen V₂ ∧ ∀ (x : α), x ∈ i ⁻¹' V₂ → f x ∈ V'
[PROOFSTEP]
simpa [and_assoc] using ((nhds_basis_opens' b).comap i).tendsto_left_iff.mp (mem_of_mem_nhds V₁_in : b ∈ V₁) V' V'_in
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen V₂
hV₂ : ∀ (x : α), x ∈ i ⁻¹' V₂ → f x ∈ V'
⊢ φ ⁻¹' V' ∈ 𝓝 b
[PROOFSTEP]
suffices ∀ x ∈ V₁ ∩ V₂, φ x ∈ V' by filter_upwards [inter_mem V₁_in V₂_in] using this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this✝ : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen V₂
hV₂ : ∀ (x : α), x ∈ i ⁻¹' V₂ → f x ∈ V'
this : ∀ (x : β), x ∈ V₁ ∩ V₂ → φ x ∈ V'
⊢ φ ⁻¹' V' ∈ 𝓝 b
[PROOFSTEP]
filter_upwards [inter_mem V₁_in V₂_in] using this
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen V₂
hV₂ : ∀ (x : α), x ∈ i ⁻¹' V₂ → f x ∈ V'
⊢ ∀ (x : β), x ∈ V₁ ∩ V₂ → φ x ∈ V'
[PROOFSTEP]
rintro x ⟨x_in₁, x_in₂⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen V₂
hV₂ : ∀ (x : α), x ∈ i ⁻¹' V₂ → f x ∈ V'
x : β
x_in₁ : x ∈ V₁
x_in₂ : x ∈ V₂
⊢ φ x ∈ V'
[PROOFSTEP]
have hV₂x : V₂ ∈ 𝓝 x := IsOpen.mem_nhds V₂_op x_in₂
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen V₂
hV₂ : ∀ (x : α), x ∈ i ⁻¹' V₂ → f x ∈ V'
x : β
x_in₁ : x ∈ V₁
x_in₂ : x ∈ V₂
hV₂x : V₂ ∈ 𝓝 x
⊢ φ x ∈ V'
[PROOFSTEP]
apply V'_closed.mem_of_tendsto x_in₁
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen V₂
hV₂ : ∀ (x : α), x ∈ i ⁻¹' V₂ → f x ∈ V'
x : β
x_in₁ : x ∈ V₁
x_in₂ : x ∈ V₂
hV₂x : V₂ ∈ 𝓝 x
⊢ ∀ᶠ (x : α) in comap i (𝓝 x), f x ∈ V'
[PROOFSTEP]
use V₂
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
i : α → β
di✝ : DenseInducing i
inst✝² : TopologicalSpace δ
f✝ : γ → α
g : γ → δ
h : δ → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : DenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := extend di f
this : ∀ (b : β), NeBot (comap i (𝓝 b))
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
V₂ : Set β
V₂_in : V₂ ∈ 𝓝 b
V₂_op : IsOpen V₂
hV₂ : ∀ (x : α), x ∈ i ⁻¹' V₂ → f x ∈ V'
x : β
x_in₁ : x ∈ V₁
x_in₂ : x ∈ V₂
hV₂x : V₂ ∈ 𝓝 x
⊢ V₂ ∈ 𝓝 x ∧ i ⁻¹' V₂ ⊆ {x | (fun x => f x ∈ V') x}
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i✝ : α → β
di : DenseInducing i✝
inst✝¹ : TopologicalSpace δ
f : γ → α
g : γ → δ
h : δ → β
inst✝ : TopologicalSpace γ
i : α → β
c : Continuous i
dense : ∀ (x : β), x ∈ closure (range i)
H : ∀ (a : α) (s : Set α), s ∈ 𝓝 a → ∃ t, t ∈ 𝓝 (i a) ∧ ∀ (b : α), i b ∈ t → b ∈ s
a : α
⊢ comap i (𝓝 (i a)) ≤ 𝓝 a
[PROOFSTEP]
simpa [Filter.le_def] using H a
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : α → β
de : DenseEmbedding e
p : α → Prop
x✝ : { x // p x }
x : α
hx : p x
⊢ 𝓝 { val := x, property := hx } = comap (subtypeEmb p e) (𝓝 (subtypeEmb p e { val := x, property := hx }))
[PROOFSTEP]
simp [subtypeEmb, nhds_subtype_eq_comap, de.toInducing.nhds_eq_comap, comap_comap, (· ∘ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : α → β
de : DenseEmbedding e
p : α → Prop
⊢ closure (range (subtypeEmb p e)) = univ
[PROOFSTEP]
ext ⟨x, hx⟩
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : α → β
de : DenseEmbedding e
p : α → Prop
x : β
hx : x ∈ closure (e '' {x | p x})
⊢ { val := x, property := hx } ∈ closure (range (subtypeEmb p e)) ↔ { val := x, property := hx } ∈ univ
[PROOFSTEP]
rw [image_eq_range] at hx 
[GOAL]
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : α → β
de : DenseEmbedding e
p : α → Prop
x : β
hx✝ : x ∈ closure (e '' {x | p x})
hx : x ∈ closure (range fun x => e ↑x)
⊢ { val := x, property := hx✝ } ∈ closure (range (subtypeEmb p e)) ↔ { val := x, property := hx✝ } ∈ univ
[PROOFSTEP]
simpa [closure_subtype, ← range_comp, (· ∘ ·)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : HasBasis (𝓝 x) p s
f : α → β
hf : DenseInducing f
⊢ HasBasis (𝓝 (f x)) p fun i => closure (f '' s i)
[PROOFSTEP]
rw [Filter.hasBasis_iff] at h ⊢
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
⊢ ∀ (t : Set β), t ∈ 𝓝 (f x) ↔ ∃ i, p i ∧ closure (f '' s i) ⊆ t
[PROOFSTEP]
intro T
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
⊢ T ∈ 𝓝 (f x) ↔ ∃ i, p i ∧ closure (f '' s i) ⊆ T
[PROOFSTEP]
refine' ⟨fun hT => _, fun hT => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
⊢ ∃ i, p i ∧ closure (f '' s i) ⊆ T
[PROOFSTEP]
obtain ⟨T', hT₁, hT₂, hT₃⟩ := exists_mem_nhds_isClosed_subset hT
[GOAL]
case refine'_1.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed T'
hT₃ : T' ⊆ T
⊢ ∃ i, p i ∧ closure (f '' s i) ⊆ T
[PROOFSTEP]
have hT₄ : f ⁻¹' T' ∈ 𝓝 x := by
  rw [hf.toInducing.nhds_eq_comap x]
  exact ⟨T', hT₁, Subset.rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed T'
hT₃ : T' ⊆ T
⊢ f ⁻¹' T' ∈ 𝓝 x
[PROOFSTEP]
rw [hf.toInducing.nhds_eq_comap x]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed T'
hT₃ : T' ⊆ T
⊢ f ⁻¹' T' ∈ Filter.comap f (𝓝 (f x))
[PROOFSTEP]
exact ⟨T', hT₁, Subset.rfl⟩
[GOAL]
case refine'_1.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed T'
hT₃ : T' ⊆ T
hT₄ : f ⁻¹' T' ∈ 𝓝 x
⊢ ∃ i, p i ∧ closure (f '' s i) ⊆ T
[PROOFSTEP]
obtain ⟨i, hi, hi'⟩ := (h _).mp hT₄
[GOAL]
case refine'_1.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed T'
hT₃ : T' ⊆ T
hT₄ : f ⁻¹' T' ∈ 𝓝 x
i : ι
hi : p i
hi' : s i ⊆ f ⁻¹' T'
⊢ ∃ i, p i ∧ closure (f '' s i) ⊆ T
[PROOFSTEP]
exact
  ⟨i, hi,
    (closure_mono (image_subset f hi')).trans (Subset.trans (closure_minimal (image_preimage_subset _ _) hT₂) hT₃)⟩
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
hT : ∃ i, p i ∧ closure (f '' s i) ⊆ T
⊢ T ∈ 𝓝 (f x)
[PROOFSTEP]
obtain ⟨i, hi, hi'⟩ := hT
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure (f '' s i) ⊆ T
⊢ T ∈ 𝓝 (f x)
[PROOFSTEP]
suffices closure (f '' s i) ∈ 𝓝 (f x) by filter_upwards [this] using hi'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure (f '' s i) ⊆ T
this : closure (f '' s i) ∈ 𝓝 (f x)
⊢ T ∈ 𝓝 (f x)
[PROOFSTEP]
filter_upwards [this] using hi'
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : DenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure (f '' s i) ⊆ T
⊢ closure (f '' s i) ∈ 𝓝 (f x)
[PROOFSTEP]
replace h := (h (s i)).mpr ⟨i, hi, Subset.rfl⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : T3Space β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
f : α → β
hf : DenseInducing f
T : Set β
i : ι
hi : p i
hi' : closure (f '' s i) ⊆ T
h : s i ∈ 𝓝 x
⊢ closure (f '' s i) ∈ 𝓝 (f x)
[PROOFSTEP]
exact hf.closure_image_mem_nhds h
