[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
⊢ UniformInducing f ↔ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
[PROOFSTEP]
rw [uniformInducing_iff, UniformContinuous, tendsto_iff_comap, le_antisymm_iff, and_comm]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
⊢ 𝓤 α ≤ comap (fun x => (f x.fst, f x.snd)) (𝓤 β) ∧ comap (fun x => (f x.fst, f x.snd)) (𝓤 β) ≤ 𝓤 α ↔
    𝓤 α ≤ comap (fun x => (f x.fst, f x.snd)) (𝓤 β) ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
p' : ι' → Prop
s : ι → Set (α × α)
s' : ι' → Set (β × β)
h : HasBasis (𝓤 α) p s
h' : HasBasis (𝓤 β) p' s'
f : α → β
⊢ UniformInducing f ↔
    (∀ (i : ι'), p' i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
      ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
[PROOFSTEP]
simp [uniformInducing_iff', h.uniformContinuous_iff h', (h'.comap _).le_basis_iff h, subset_def]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
h : ∀ (s : Set (α × α)), s ∈ 𝓤 α ↔ ∃ t, t ∈ 𝓤 β ∧ ∀ (x y : α), (f x, f y) ∈ t → (x, y) ∈ s
⊢ comap (fun x => (f x.fst, f x.snd)) (𝓤 β) = 𝓤 α
[PROOFSTEP]
simp [eq_comm, Filter.ext_iff, subset_def, h]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ comap (fun x => (id x.fst, id x.snd)) (𝓤 α) = 𝓤 α
[PROOFSTEP]
rw [← Prod.map_def, Prod.map_id, comap_id]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : UniformInducing g
f : α → β
hf : UniformInducing f
⊢ comap (fun x => ((g ∘ f) x.fst, (g ∘ f) x.snd)) (𝓤 γ) = 𝓤 α
[PROOFSTEP]
rw [← hf.1, ← hg.1, comap_comap]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
g : β → γ
hg : UniformInducing g
f : α → β
hf : UniformInducing f
⊢ comap (fun x => ((g ∘ f) x.fst, (g ∘ f) x.snd)) (𝓤 γ) =
    comap ((fun x => (g x.fst, g x.snd)) ∘ fun x => (f x.fst, f x.snd)) (𝓤 γ)
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
hf : UniformInducing f
F : Filter α
⊢ Cauchy (map f F) ↔ Cauchy F
[PROOFSTEP]
simp only [Cauchy, map_neBot_iff, prod_map_map_eq, map_le_iff_le_comap, ← hf.comap_uniformity]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : UniformInducing (g ∘ f)
⊢ UniformInducing f
[PROOFSTEP]
refine' ⟨le_antisymm _ hf.le_comap⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : UniformInducing (g ∘ f)
⊢ comap (fun x => (f x.fst, f x.snd)) (𝓤 β) ≤ 𝓤 α
[PROOFSTEP]
rw [← hgf.1, ← Prod.map_def, ← Prod.map_def, ← Prod.map_comp_map f f g g, ← comap_comap]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hf : UniformContinuous f
hg : UniformContinuous g
hgf : UniformInducing (g ∘ f)
⊢ comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map f f) (comap (Prod.map g g) (𝓤 γ))
[PROOFSTEP]
exact comap_mono hg.le_comap
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hg : UniformInducing g
⊢ UniformContinuous f ↔ UniformContinuous (g ∘ f)
[PROOFSTEP]
dsimp only [UniformContinuous, Tendsto]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hg : UniformInducing g
⊢ map (fun x => (f x.fst, f x.snd)) (𝓤 α) ≤ 𝓤 β ↔ map (fun x => ((g ∘ f) x.fst, (g ∘ f) x.snd)) (𝓤 α) ≤ 𝓤 γ
[PROOFSTEP]
rw [← hg.comap_uniformity, ← map_le_iff_le_comap, Filter.map_map]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
g : β → γ
hg : UniformInducing g
⊢ map ((fun x => (g x.fst, g x.snd)) ∘ fun x => (f x.fst, f x.snd)) (𝓤 α) ≤ 𝓤 γ ↔
    map (fun x => ((g ∘ f) x.fst, (g ∘ f) x.snd)) (𝓤 α) ≤ 𝓤 γ
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
h : UniformInducing f
⊢ Inducing f
[PROOFSTEP]
obtain rfl := h.comap_uniformSpace
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
h : UniformInducing f
⊢ Inducing f
[PROOFSTEP]
exact inducing_induced f
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : UniformSpace γ
α' : Type u_1
β' : Type u_2
inst✝¹ : UniformSpace α'
inst✝ : UniformSpace β'
e₁ : α → α'
e₂ : β → β'
h₁ : UniformInducing e₁
h₂ : UniformInducing e₂
⊢ comap (fun x => ((e₁ x.fst.fst, e₂ x.fst.snd), e₁ x.snd.fst, e₂ x.snd.snd)) (𝓤 (α' × β')) = 𝓤 (α × β)
[PROOFSTEP]
simp [(· ∘ ·), uniformity_prod, ← h₁.1, ← h₂.1, comap_inf, comap_comap]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
⊢ UniformEmbedding f ↔ Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
[PROOFSTEP]
rw [uniformEmbedding_iff, and_comm, uniformInducing_iff']
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
p' : ι' → Prop
s : ι → Set (α × α)
s' : ι' → Set (β × β)
h : HasBasis (𝓤 α) p s
h' : HasBasis (𝓤 β) p' s'
f : α → β
⊢ UniformEmbedding f ↔
    Injective f ∧
      (∀ (i : ι'), p' i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
        ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
[PROOFSTEP]
rw [uniformEmbedding_iff, and_comm, h.uniformInducing_iff h']
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
p' : ι' → Prop
s : ι → Set (α × α)
s' : ι' → Set (β × β)
h : HasBasis (𝓤 α) p s
h' : HasBasis (𝓤 β) p' s'
f : α → β
⊢ UniformEmbedding f ↔
    Injective f ∧ UniformContinuous f ∧ ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
[PROOFSTEP]
simp only [h.uniformEmbedding_iff' h', h.uniformContinuous_iff h']
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s t : Set α
hst : s ⊆ t
⊢ comap (fun x => (inclusion hst x.fst, inclusion hst x.snd)) (𝓤 ↑t) = 𝓤 ↑s
[PROOFSTEP]
rw [uniformity_subtype, uniformity_subtype, comap_comap]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s t : Set α
hst : s ⊆ t
⊢ comap ((fun q => (↑q.fst, ↑q.snd)) ∘ fun x => (inclusion hst x.fst, inclusion hst x.snd)) (𝓤 α) =
    comap (fun q => (↑q.fst, ↑q.snd)) (𝓤 α)
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u
β✝ : Type v
γ : Type w
inst✝⁴ : UniformSpace α✝
inst✝³ : UniformSpace β✝
inst✝² : UniformSpace γ
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α ≃ β
h₁ : UniformContinuous ↑f
h₂ : UniformContinuous ↑f.symm
⊢ comap (Prod.map ↑f ↑f) (𝓤 β) ≤ 𝓤 α
[PROOFSTEP]
rwa [← Equiv.prodCongr_apply, ← map_equiv_symm]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
hs : s ∈ 𝓤 α
x : α × α
h : x ∈ Prod.map Sum.inl Sum.inl ⁻¹' (Prod.map Sum.inl Sum.inl '' s ∪ range (Prod.map Sum.inr Sum.inr))
⊢ x ∈ s
[PROOFSTEP]
simpa using h
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (β × β)
hs : s ∈ 𝓤 β
x : β × β
h : x ∈ Prod.map Sum.inr Sum.inr ⁻¹' (range (Prod.map Sum.inl Sum.inl) ∪ Prod.map Sum.inr Sum.inr '' s)
⊢ x ∈ s
[PROOFSTEP]
simpa using h
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => ¬(f x, f y) ∈ s
⊢ comap (Prod.map f f) (𝓤 β) = 𝓟 idRel
[PROOFSTEP]
refine' le_antisymm _ (@refl_le_uniformity α (UniformSpace.comap f _))
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => ¬(f x, f y) ∈ s
⊢ comap (Prod.map f f) (𝓤 β) ≤ 𝓟 idRel
[PROOFSTEP]
calc
  comap (Prod.map f f) (𝓤 β) ≤ comap (Prod.map f f) (𝓟 s) := comap_mono (le_principal_iff.2 hs)
  _ = 𝓟 (Prod.map f f ⁻¹' s) := comap_principal
  _ ≤ 𝓟 idRel := principal_mono.2 ?_
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => ¬(f x, f y) ∈ s
⊢ Prod.map f f ⁻¹' s ⊆ idRel
[PROOFSTEP]
rintro ⟨x, y⟩
[GOAL]
case mk
α✝ : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => ¬(f x, f y) ∈ s
x y : α
⊢ (x, y) ∈ Prod.map f f ⁻¹' s → (x, y) ∈ idRel
[PROOFSTEP]
simpa [not_imp_not] using @hf x y
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => ¬(f x, f y) ∈ s
⊢ UniformEmbedding f
[PROOFSTEP]
let _ : UniformSpace α := ⊥
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => ¬(f x, f y) ∈ s
x✝ : UniformSpace α := ⊥
⊢ UniformEmbedding f
[PROOFSTEP]
have := discreteTopology_bot α
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α✝
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => ¬(f x, f y) ∈ s
x✝ : UniformSpace α := ⊥
this : DiscreteTopology α
⊢ UniformEmbedding f
[PROOFSTEP]
exact UniformInducing.uniformEmbedding ⟨comap_uniformity_of_spaced_out hs hf⟩
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝⁵ : UniformSpace α✝
inst✝⁴ : UniformSpace β
inst✝³ : UniformSpace γ
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : DiscreteTopology α
inst✝ : SeparatedSpace β
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => ¬(f x, f y) ∈ s
⊢ ClosedEmbedding f
[PROOFSTEP]
rcases@DiscreteTopology.eq_bot α _ _ with rfl
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝⁴ : UniformSpace α✝
inst✝³ : UniformSpace β
inst✝² : UniformSpace γ
α : Type u_1
inst✝¹ : SeparatedSpace β
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => ¬(f x, f y) ∈ s
inst✝ : DiscreteTopology α
⊢ ClosedEmbedding f
[PROOFSTEP]
let _ : UniformSpace α := ⊥
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
inst✝⁴ : UniformSpace α✝
inst✝³ : UniformSpace β
inst✝² : UniformSpace γ
α : Type u_1
inst✝¹ : SeparatedSpace β
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun x y => ¬(f x, f y) ∈ s
inst✝ : DiscreteTopology α
x✝ : UniformSpace α := ⊥
⊢ ClosedEmbedding f
[PROOFSTEP]
exact { (uniformEmbedding_of_spaced_out hs hf).embedding with closed_range := isClosed_range_of_spaced_out hs hf }
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
e : α → β
b : β
he₁ : UniformInducing e
he₂ : DenseInducing e
hs : s ∈ 𝓤 α
⊢ ∃ a, closure (e '' {a' | (a, a') ∈ s}) ∈ 𝓝 b
[PROOFSTEP]
obtain ⟨U, ⟨hU, hUo, hsymm⟩, hs⟩ : ∃ U, (U ∈ 𝓤 β ∧ IsOpen U ∧ SymmetricRel U) ∧ Prod.map e e ⁻¹' U ⊆ s := by
  rwa [← he₁.comap_uniformity, (uniformity_hasBasis_open_symmetric.comap _).mem_iff] at hs 
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
e : α → β
b : β
he₁ : UniformInducing e
he₂ : DenseInducing e
hs : s ∈ 𝓤 α
⊢ ∃ U, (U ∈ 𝓤 β ∧ IsOpen U ∧ SymmetricRel U) ∧ Prod.map e e ⁻¹' U ⊆ s
[PROOFSTEP]
rwa [← he₁.comap_uniformity, (uniformity_hasBasis_open_symmetric.comap _).mem_iff] at hs 
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
e : α → β
b : β
he₁ : UniformInducing e
he₂ : DenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
⊢ ∃ a, closure (e '' {a' | (a, a') ∈ s}) ∈ 𝓝 b
[PROOFSTEP]
rcases he₂.dense.mem_nhds (UniformSpace.ball_mem_nhds b hU) with ⟨a, ha⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
e : α → β
b : β
he₁ : UniformInducing e
he₂ : DenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
⊢ ∃ a, closure (e '' {a' | (a, a') ∈ s}) ∈ 𝓝 b
[PROOFSTEP]
refine ⟨a, mem_of_superset ?_ (closure_mono <| image_subset _ <| ball_mono hs a)⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
e : α → β
b : β
he₁ : UniformInducing e
he₂ : DenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
⊢ closure (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)) ∈ 𝓝 b
[PROOFSTEP]
have ho : IsOpen (UniformSpace.ball (e a) U) := UniformSpace.isOpen_ball (e a) hUo
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
e : α → β
b : β
he₁ : UniformInducing e
he₂ : DenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen (UniformSpace.ball (e a) U)
⊢ closure (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)) ∈ 𝓝 b
[PROOFSTEP]
refine mem_of_superset (ho.mem_nhds <| (mem_ball_symmetry hsymm).2 ha) fun y hy => ?_
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
e : α → β
b : β
he₁ : UniformInducing e
he₂ : DenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen (UniformSpace.ball (e a) U)
y : β
hy : y ∈ UniformSpace.ball (e a) U
⊢ y ∈ closure (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U))
[PROOFSTEP]
refine mem_closure_iff_nhds.2 fun V hV => ?_
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
e : α → β
b : β
he₁ : UniformInducing e
he₂ : DenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen (UniformSpace.ball (e a) U)
y : β
hy : y ∈ UniformSpace.ball (e a) U
V : Set β
hV : V ∈ 𝓝 y
⊢ Set.Nonempty (V ∩ e '' UniformSpace.ball a (Prod.map e e ⁻¹' U))
[PROOFSTEP]
rcases he₂.dense.mem_nhds (inter_mem hV (ho.mem_nhds hy)) with ⟨x, hxV, hxU⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
e : α → β
b : β
he₁ : UniformInducing e
he₂ : DenseInducing e
hs✝ : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen U
hsymm : SymmetricRel U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen (UniformSpace.ball (e a) U)
y : β
hy : y ∈ UniformSpace.ball (e a) U
V : Set β
hV : V ∈ 𝓝 y
x : α
hxV : e x ∈ V
hxU : e x ∈ UniformSpace.ball (e a) U
⊢ Set.Nonempty (V ∩ e '' UniformSpace.ball a (Prod.map e e ⁻¹' U))
[PROOFSTEP]
exact ⟨e x, hxV, mem_image_of_mem e hxU⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : α → Prop
e : α → β
ue : UniformEmbedding e
de : DenseEmbedding e
⊢ comap (fun x => (DenseEmbedding.subtypeEmb p e x.fst, DenseEmbedding.subtypeEmb p e x.snd))
      (𝓤 { x // x ∈ closure (e '' {x | p x}) }) =
    𝓤 { x // p x }
[PROOFSTEP]
simp [comap_comap, (· ∘ ·), DenseEmbedding.subtypeEmb, uniformity_subtype, ue.comap_uniformity.symm]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
⊢ IsComplete s
[PROOFSTEP]
intro f hf hfs
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : f ≤ 𝓟 s
⊢ ∃ x, x ∈ s ∧ f ≤ 𝓝 x
[PROOFSTEP]
rw [le_principal_iff] at hfs 
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : s ∈ f
⊢ ∃ x, x ∈ s ∧ f ≤ 𝓝 x
[PROOFSTEP]
obtain ⟨_, ⟨x, hx, rfl⟩, hyf⟩ : ∃ y ∈ m '' s, map m f ≤ 𝓝 y
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : s ∈ f
⊢ ∃ y, y ∈ m '' s ∧ map m f ≤ 𝓝 y
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : s ∈ f
x : α
hx : x ∈ s
hyf : map m f ≤ 𝓝 (m x)
⊢ ∃ x, x ∈ s ∧ f ≤ 𝓝 x
[PROOFSTEP]
exact hs (f.map m) (hf.map hm.uniformContinuous) (le_principal_iff.2 (image_mem_map hfs))
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : s ∈ f
x : α
hx : x ∈ s
hyf : map m f ≤ 𝓝 (m x)
⊢ ∃ x, x ∈ s ∧ f ≤ 𝓝 x
[PROOFSTEP]
rw [map_le_iff_le_comap, ← nhds_induced, ← hm.inducing.induced] at hyf 
[GOAL]
case intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
hs : IsComplete (m '' s)
f : Filter α
hf : Cauchy f
hfs : s ∈ f
x : α
hx : x ∈ s
hyf : f ≤ 𝓝 x
⊢ ∃ x, x ∈ s ∧ f ≤ 𝓝 x
[PROOFSTEP]
exact ⟨x, hx, hyf⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set α
hs : IsComplete s
⊢ IsComplete (Subtype.val '' univ)
[PROOFSTEP]
simp [hs]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
⊢ IsComplete (m '' s) ↔ IsComplete s
[PROOFSTEP]
refine' ⟨isComplete_of_complete_image hm, fun c => _⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
⊢ IsComplete (m '' s)
[PROOFSTEP]
haveI : CompleteSpace s := c.completeSpace_coe
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
this : CompleteSpace ↑s
⊢ IsComplete (m '' s)
[PROOFSTEP]
set m' : s → β := m ∘ (↑)
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
this : CompleteSpace ↑s
m' : ↑s → β := m ∘ Subtype.val
⊢ IsComplete (m '' s)
[PROOFSTEP]
suffices IsComplete (range m') by rwa [range_comp, Subtype.range_coe] at this 
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
this✝ : CompleteSpace ↑s
m' : ↑s → β := m ∘ Subtype.val
this : IsComplete (range m')
⊢ IsComplete (m '' s)
[PROOFSTEP]
rwa [range_comp, Subtype.range_coe] at this 
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
this : CompleteSpace ↑s
m' : ↑s → β := m ∘ Subtype.val
⊢ IsComplete (range m')
[PROOFSTEP]
have hm' : UniformInducing m' := hm.comp uniformEmbedding_subtype_val.toUniformInducing
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
this : CompleteSpace ↑s
m' : ↑s → β := m ∘ Subtype.val
hm' : UniformInducing m'
⊢ IsComplete (range m')
[PROOFSTEP]
intro f hf hfm
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
this : CompleteSpace ↑s
m' : ↑s → β := m ∘ Subtype.val
hm' : UniformInducing m'
f : Filter β
hf : Cauchy f
hfm : f ≤ 𝓟 (range m')
⊢ ∃ x, x ∈ range m' ∧ f ≤ 𝓝 x
[PROOFSTEP]
rw [Filter.le_principal_iff] at hfm 
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
this : CompleteSpace ↑s
m' : ↑s → β := m ∘ Subtype.val
hm' : UniformInducing m'
f : Filter β
hf : Cauchy f
hfm : range m' ∈ f
⊢ ∃ x, x ∈ range m' ∧ f ≤ 𝓝 x
[PROOFSTEP]
have cf' : Cauchy (comap m' f) := hf.comap' hm'.comap_uniformity.le (NeBot.comap_of_range_mem hf.1 hfm)
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
this : CompleteSpace ↑s
m' : ↑s → β := m ∘ Subtype.val
hm' : UniformInducing m'
f : Filter β
hf : Cauchy f
hfm : range m' ∈ f
cf' : Cauchy (comap m' f)
⊢ ∃ x, x ∈ range m' ∧ f ≤ 𝓝 x
[PROOFSTEP]
rcases CompleteSpace.complete cf' with ⟨x, hx⟩
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
this : CompleteSpace ↑s
m' : ↑s → β := m ∘ Subtype.val
hm' : UniformInducing m'
f : Filter β
hf : Cauchy f
hfm : range m' ∈ f
cf' : Cauchy (comap m' f)
x : ↑s
hx : comap m' f ≤ 𝓝 x
⊢ ∃ x, x ∈ range m' ∧ f ≤ 𝓝 x
[PROOFSTEP]
rw [hm'.inducing.nhds_eq_comap, comap_le_comap_iff hfm] at hx 
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : α → β
s : Set α
hm : UniformInducing m
c : IsComplete s
this : CompleteSpace ↑s
m' : ↑s → β := m ∘ Subtype.val
hm' : UniformInducing m'
f : Filter β
hf : Cauchy f
hfm : range m' ∈ f
cf' : Cauchy (comap m' f)
x : ↑s
hx : f ≤ 𝓝 (m' x)
⊢ ∃ x, x ∈ range m' ∧ f ≤ 𝓝 x
[PROOFSTEP]
exact ⟨m' x, mem_range_self _, hx⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
hf : UniformInducing f
⊢ CompleteSpace α ↔ IsComplete (range f)
[PROOFSTEP]
rw [completeSpace_iff_isComplete_univ, ← isComplete_image_iff hf, image_univ]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
e : α ≃ β
he : UniformEmbedding ↑e
⊢ CompleteSpace α ↔ CompleteSpace β
[PROOFSTEP]
rw [completeSpace_iff_isComplete_range he.toUniformInducing, e.range_eq_univ, completeSpace_iff_isComplete_univ]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set α
⊢ IsComplete (range Subtype.val) ↔ IsComplete s
[PROOFSTEP]
rw [Subtype.range_coe]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
m : β → α
hm : UniformInducing m
dense : DenseRange m
h : ∀ (f : Filter β), Cauchy f → ∃ x, map m f ≤ 𝓝 x
f : Filter α
hf : Cauchy f
p : Set (α × α) → Set α → Set α := fun s t => {y | ∃ x, x ∈ t ∧ (x, y) ∈ s}
g : Filter α := Filter.lift (𝓤 α) fun s => Filter.lift' f (p s)
mp₀ : Monotone p
mp₁ : ∀ {s : Set (α × α)}, Monotone (p s)
this✝⁵ : f ≤ g
this✝⁴ : NeBot g
this✝³ : NeBot (comap m g)
this✝² : Cauchy g
this✝¹ : Cauchy (comap m g)
x : α
hx : map m (comap m g) ≤ 𝓝 x
this✝ : ClusterPt x (map m (comap m g))
this : ClusterPt x g
⊢ f ≤ g
[PROOFSTEP]
assumption
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ 𝓤 α
⊢ ∃ t_1, Set.Finite t_1 ∧ f ⁻¹' s ⊆ ⋃ (y : α) (_ : y ∈ t_1), {x | (x, y) ∈ t}
[PROOFSTEP]
rw [← hf.comap_uniformity] at ht 
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
⊢ ∃ t_1, Set.Finite t_1 ∧ f ⁻¹' s ⊆ ⋃ (y : α) (_ : y ∈ t_1), {x | (x, y) ∈ t}
[PROOFSTEP]
rcases mem_comap.2 ht with ⟨t', ht', ts⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
⊢ ∃ t_1, Set.Finite t_1 ∧ f ⁻¹' s ⊆ ⋃ (y : α) (_ : y ∈ t_1), {x | (x, y) ∈ t}
[PROOFSTEP]
rcases totallyBounded_iff_subset.1 (totallyBounded_subset (image_preimage_subset f s) hs) _ ht' with ⟨c, cs, hfc, hct⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
⊢ ∃ t_1, Set.Finite t_1 ∧ f ⁻¹' s ⊆ ⋃ (y : α) (_ : y ∈ t_1), {x | (x, y) ∈ t}
[PROOFSTEP]
refine' ⟨f ⁻¹' c, hfc.preimage (hf.inj.injOn _), fun x h => _⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
x : α
h : x ∈ f ⁻¹' s
⊢ x ∈ ⋃ (y : α) (_ : y ∈ f ⁻¹' c), {x | (x, y) ∈ t}
[PROOFSTEP]
have := hct (mem_image_of_mem f h)
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
x : α
h : x ∈ f ⁻¹' s
this : f x ∈ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
⊢ x ∈ ⋃ (y : α) (_ : y ∈ f ⁻¹' c), {x | (x, y) ∈ t}
[PROOFSTEP]
simp at this ⊢
[GOAL]
case intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
x : α
h : x ∈ f ⁻¹' s
this : ∃ i, i ∈ c ∧ (f x, i) ∈ t'
⊢ ∃ i, f i ∈ c ∧ (x, i) ∈ t
[PROOFSTEP]
rcases this with ⟨z, zc, zt⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
x : α
h : x ∈ f ⁻¹' s
z : β
zc : z ∈ c
zt : (f x, z) ∈ t'
⊢ ∃ i, f i ∈ c ∧ (x, i) ∈ t
[PROOFSTEP]
rcases cs zc with ⟨y, -, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : α → β
s : Set β
hf : UniformEmbedding f
hs : TotallyBounded s
t : Set (α × α)
ht : t ∈ comap (fun x => (f x.fst, f x.snd)) (𝓤 β)
t' : Set (β × β)
ht' : t' ∈ 𝓤 β
ts : (fun x => (f x.fst, f x.snd)) ⁻¹' t' ⊆ t
c : Set β
cs : c ⊆ f '' (f ⁻¹' s)
hfc : Set.Finite c
hct : f '' (f ⁻¹' s) ⊆ ⋃ (y : β) (_ : y ∈ c), {x | (x, y) ∈ t'}
x : α
h : x ∈ f ⁻¹' s
y : α
zc : f y ∈ c
zt : (f x, f y) ∈ t'
⊢ ∃ i, f i ∈ c ∧ (x, i) ∈ t
[PROOFSTEP]
exact ⟨y, zc, ts zt⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
⊢ CompleteSpace (α ⊕ β)
[PROOFSTEP]
rw [completeSpace_iff_isComplete_univ, ← range_inl_union_range_inr]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace α
inst✝ : CompleteSpace β
⊢ IsComplete (range Sum.inl ∪ range Sum.inr)
[PROOFSTEP]
exact
  uniformEmbedding_inl.toUniformInducing.isComplete_range.union uniformEmbedding_inr.toUniformInducing.isComplete_range
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
[PROOFSTEP]
have de : DenseEmbedding e := he.denseEmbedding hd
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
de : DenseEmbedding e
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
[PROOFSTEP]
have de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e) := de.subtype p
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
de : DenseEmbedding e
de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
[PROOFSTEP]
have ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e) := uniformEmbedding_subtypeEmb _ he de
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
de : DenseEmbedding e
de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)
ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
[PROOFSTEP]
have : b ∈ closure (e '' {x | p x}) := (closure_mono <| monotone_image <| hp) (mem_of_mem_nhds hb)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
de : DenseEmbedding e
de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)
ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)
this : b ∈ closure (e '' {x | p x})
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
[PROOFSTEP]
let ⟨c, hc⟩ := uniformly_extend_exists ue'.toUniformInducing de'.dense hf ⟨b, this⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
de : DenseEmbedding e
de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)
ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)
this : b ∈ closure (e '' {x | p x})
c : γ
hc : Tendsto (fun x => f ↑x) (comap (DenseEmbedding.subtypeEmb p e) (𝓝 { val := b, property := this })) (𝓝 c)
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
[PROOFSTEP]
replace hc : Tendsto (f ∘ Subtype.val) (((𝓝 b).comap e).comap Subtype.val) (𝓝 c) := by
  simpa only [nhds_subtype_eq_comap, comap_comap, DenseEmbedding.subtypeEmb_coe] using hc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
de : DenseEmbedding e
de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)
ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)
this : b ∈ closure (e '' {x | p x})
c : γ
hc : Tendsto (fun x => f ↑x) (comap (DenseEmbedding.subtypeEmb p e) (𝓝 { val := b, property := this })) (𝓝 c)
⊢ Tendsto (f ∘ Subtype.val) (comap Subtype.val (comap e (𝓝 b))) (𝓝 c)
[PROOFSTEP]
simpa only [nhds_subtype_eq_comap, comap_comap, DenseEmbedding.subtypeEmb_coe] using hc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
de : DenseEmbedding e
de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)
ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)
this : b ∈ closure (e '' {x | p x})
c : γ
hc : Tendsto (f ∘ Subtype.val) (comap Subtype.val (comap e (𝓝 b))) (𝓝 c)
⊢ ∃ c, Tendsto f (comap e (𝓝 b)) (𝓝 c)
[PROOFSTEP]
refine ⟨c, (tendsto_comap'_iff ?_).1 hc⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
de : DenseEmbedding e
de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)
ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)
this : b ∈ closure (e '' {x | p x})
c : γ
hc : Tendsto (f ∘ Subtype.val) (comap Subtype.val (comap e (𝓝 b))) (𝓝 c)
⊢ range Subtype.val ∈ comap e (𝓝 b)
[PROOFSTEP]
rw [Subtype.range_coe_subtype]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
de : DenseEmbedding e
de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)
ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)
this : b ∈ closure (e '' {x | p x})
c : γ
hc : Tendsto (f ∘ Subtype.val) (comap Subtype.val (comap e (𝓝 b))) (𝓝 c)
⊢ {x | p x} ∈ comap e (𝓝 b)
[PROOFSTEP]
exact ⟨_, hb, by rwa [← de.toInducing.closure_eq_preimage_closure_image, hs.closure_eq]⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e✝ : β → α
h_e : UniformInducing e✝
h_dense : DenseRange e✝
f✝ : β → γ
h_f : UniformContinuous f✝
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x => f ↑x
he : UniformEmbedding e
hd : ∀ (x : β), x ∈ closure (range e)
hb : closure (e '' s) ∈ 𝓝 b
hs : IsClosed s
hp : ∀ (x : α), x ∈ s → p x
de : DenseEmbedding e
de' : DenseEmbedding (DenseEmbedding.subtypeEmb p e)
ue' : UniformEmbedding (DenseEmbedding.subtypeEmb p e)
this : b ∈ closure (e '' {x | p x})
c : γ
hc : Tendsto (f ∘ Subtype.val) (comap Subtype.val (comap e (𝓝 b))) (𝓝 c)
⊢ e ⁻¹' closure (e '' s) ⊆ {x | p x}
[PROOFSTEP]
rwa [← de.toInducing.closure_eq_preimage_closure_image, hs.closure_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : UniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
a : α
⊢ Tendsto f (comap e (𝓝 a)) (𝓝 (DenseInducing.extend (_ : DenseInducing e) f a))
[PROOFSTEP]
simpa only [DenseInducing.extend] using tendsto_nhds_limUnder (uniformly_extend_exists h_e ‹_› h_f _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : UniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt :
  ∀ {a : α} {m : Set α},
    m ∈ 𝓝 a →
      ∃ c,
        c ∈ f '' (e ⁻¹' m) ∧
          (c, DenseInducing.extend (_ : DenseInducing e) f a) ∈ s ∧
            (DenseInducing.extend (_ : DenseInducing e) f a, c) ∈ s
this : Prod.map f f ⁻¹' s ∈ 𝓤 β
⊢ Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
[PROOFSTEP]
rwa [← h_e.comap_uniformity] at this 
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : UniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt :
  ∀ {a : α} {m : Set α},
    m ∈ 𝓝 a →
      ∃ c,
        c ∈ f '' (e ⁻¹' m) ∧
          (c, DenseInducing.extend (_ : DenseInducing e) f a) ∈ s ∧
            (DenseInducing.extend (_ : DenseInducing e) f a, c) ∈ s
this✝ : Prod.map f f ⁻¹' s ∈ 𝓤 β
this : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x✝ : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
⊢ (x₁, x₂) ∈
    Prod.map (DenseInducing.extend (_ : DenseInducing e) f) (DenseInducing.extend (_ : DenseInducing e) f) ⁻¹' d
[PROOFSTEP]
have : interior t ∈ 𝓝 (x₁, x₂) := isOpen_interior.mem_nhds hx_t
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : UniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt :
  ∀ {a : α} {m : Set α},
    m ∈ 𝓝 a →
      ∃ c,
        c ∈ f '' (e ⁻¹' m) ∧
          (c, DenseInducing.extend (_ : DenseInducing e) f a) ∈ s ∧
            (DenseInducing.extend (_ : DenseInducing e) f a, c) ∈ s
this✝¹ : Prod.map f f ⁻¹' s ∈ 𝓤 β
this✝ : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x✝ : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
this : interior t ∈ 𝓝 (x₁, x₂)
⊢ (x₁, x₂) ∈
    Prod.map (DenseInducing.extend (_ : DenseInducing e) f) (DenseInducing.extend (_ : DenseInducing e) f) ⁻¹' d
[PROOFSTEP]
let ⟨m₁, hm₁, m₂, hm₂, (hm : m₁ ×ˢ m₂ ⊆ interior t)⟩ := mem_nhds_prod_iff.mp this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : UniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt :
  ∀ {a : α} {m : Set α},
    m ∈ 𝓝 a →
      ∃ c,
        c ∈ f '' (e ⁻¹' m) ∧
          (c, DenseInducing.extend (_ : DenseInducing e) f a) ∈ s ∧
            (DenseInducing.extend (_ : DenseInducing e) f a, c) ∈ s
this✝¹ : Prod.map f f ⁻¹' s ∈ 𝓤 β
this✝ : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x✝ : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
this : interior t ∈ 𝓝 (x₁, x₂)
m₁ : Set α
hm₁ : m₁ ∈ 𝓝 x₁
m₂ : Set α
hm₂ : m₂ ∈ 𝓝 x₂
hm : m₁ ×ˢ m₂ ⊆ interior t
⊢ (x₁, x₂) ∈
    Prod.map (DenseInducing.extend (_ : DenseInducing e) f) (DenseInducing.extend (_ : DenseInducing e) f) ⁻¹' d
[PROOFSTEP]
obtain ⟨_, ⟨a, ha₁, rfl⟩, _, ha₂⟩ := h_pnt hm₁
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : UniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt :
  ∀ {a : α} {m : Set α},
    m ∈ 𝓝 a →
      ∃ c,
        c ∈ f '' (e ⁻¹' m) ∧
          (c, DenseInducing.extend (_ : DenseInducing e) f a) ∈ s ∧
            (DenseInducing.extend (_ : DenseInducing e) f a, c) ∈ s
this✝¹ : Prod.map f f ⁻¹' s ∈ 𝓤 β
this✝ : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x✝ : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
this : interior t ∈ 𝓝 (x₁, x₂)
m₁ : Set α
hm₁ : m₁ ∈ 𝓝 x₁
m₂ : Set α
hm₂ : m₂ ∈ 𝓝 x₂
hm : m₁ ×ˢ m₂ ⊆ interior t
a : β
ha₁ : a ∈ e ⁻¹' m₁
left✝ : (f a, DenseInducing.extend (_ : DenseInducing e) f x₁) ∈ s
ha₂ : (DenseInducing.extend (_ : DenseInducing e) f x₁, f a) ∈ s
⊢ (x₁, x₂) ∈
    Prod.map (DenseInducing.extend (_ : DenseInducing e) f) (DenseInducing.extend (_ : DenseInducing e) f) ⁻¹' d
[PROOFSTEP]
obtain ⟨_, ⟨b, hb₁, rfl⟩, hb₂, _⟩ := h_pnt hm₂
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : UniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt :
  ∀ {a : α} {m : Set α},
    m ∈ 𝓝 a →
      ∃ c,
        c ∈ f '' (e ⁻¹' m) ∧
          (c, DenseInducing.extend (_ : DenseInducing e) f a) ∈ s ∧
            (DenseInducing.extend (_ : DenseInducing e) f a, c) ∈ s
this✝¹ : Prod.map f f ⁻¹' s ∈ 𝓤 β
this✝ : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x✝ : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
this : interior t ∈ 𝓝 (x₁, x₂)
m₁ : Set α
hm₁ : m₁ ∈ 𝓝 x₁
m₂ : Set α
hm₂ : m₂ ∈ 𝓝 x₂
hm : m₁ ×ˢ m₂ ⊆ interior t
a : β
ha₁ : a ∈ e ⁻¹' m₁
left✝ : (f a, DenseInducing.extend (_ : DenseInducing e) f x₁) ∈ s
ha₂ : (DenseInducing.extend (_ : DenseInducing e) f x₁, f a) ∈ s
b : β
hb₁ : b ∈ e ⁻¹' m₂
hb₂ : (f b, DenseInducing.extend (_ : DenseInducing e) f x₂) ∈ s
right✝ : (DenseInducing.extend (_ : DenseInducing e) f x₂, f b) ∈ s
⊢ (x₁, x₂) ∈
    Prod.map (DenseInducing.extend (_ : DenseInducing e) f) (DenseInducing.extend (_ : DenseInducing e) f) ⁻¹' d
[PROOFSTEP]
have : Prod.map f f (a, b) ∈ s := ts <| mem_preimage.2 <| interior_subset (@hm (e a, e b) ⟨ha₁, hb₁⟩)
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : UniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt :
  ∀ {a : α} {m : Set α},
    m ∈ 𝓝 a →
      ∃ c,
        c ∈ f '' (e ⁻¹' m) ∧
          (c, DenseInducing.extend (_ : DenseInducing e) f a) ∈ s ∧
            (DenseInducing.extend (_ : DenseInducing e) f a, c) ∈ s
this✝² : Prod.map f f ⁻¹' s ∈ 𝓤 β
this✝¹ : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x✝ : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
this✝ : interior t ∈ 𝓝 (x₁, x₂)
m₁ : Set α
hm₁ : m₁ ∈ 𝓝 x₁
m₂ : Set α
hm₂ : m₂ ∈ 𝓝 x₂
hm : m₁ ×ˢ m₂ ⊆ interior t
a : β
ha₁ : a ∈ e ⁻¹' m₁
left✝ : (f a, DenseInducing.extend (_ : DenseInducing e) f x₁) ∈ s
ha₂ : (DenseInducing.extend (_ : DenseInducing e) f x₁, f a) ∈ s
b : β
hb₁ : b ∈ e ⁻¹' m₂
hb₂ : (f b, DenseInducing.extend (_ : DenseInducing e) f x₂) ∈ s
right✝ : (DenseInducing.extend (_ : DenseInducing e) f x₂, f b) ∈ s
this : Prod.map f f (a, b) ∈ s
⊢ (x₁, x₂) ∈
    Prod.map (DenseInducing.extend (_ : DenseInducing e) f) (DenseInducing.extend (_ : DenseInducing e) f) ⁻¹' d
[PROOFSTEP]
exact hs_comp ⟨f a, ha₂, ⟨f b, this, hb₂⟩⟩
