[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ map Prod.swap (Filter.lift' (𝓤 α) gen) ≤ Filter.lift' (𝓤 α) gen
[PROOFSTEP]
let f := fun s : Set (α × α) => {p : CauchyFilter α × CauchyFilter α | s ∈ (p.2.val ×ˢ p.1.val : Filter (α × α))}
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
⊢ map Prod.swap (Filter.lift' (𝓤 α) gen) ≤ Filter.lift' (𝓤 α) gen
[PROOFSTEP]
have h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f :=
  by
  delta gen
  simp [map_lift'_eq, monotone_setOf, Filter.monotone_mem, Function.comp, image_swap_eq_preimage_swap]
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
⊢ map Prod.swap (Filter.lift' (𝓤 α) gen) = Filter.lift' (𝓤 α) f
[PROOFSTEP]
delta gen
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
⊢ map Prod.swap (Filter.lift' (𝓤 α) fun s => {p | s ∈ ↑p.fst ×ˢ ↑p.snd}) = Filter.lift' (𝓤 α) f
[PROOFSTEP]
simp [map_lift'_eq, monotone_setOf, Filter.monotone_mem, Function.comp, image_swap_eq_preimage_swap]
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
h₁ : map Prod.swap (Filter.lift' (𝓤 α) gen) = Filter.lift' (𝓤 α) f
⊢ map Prod.swap (Filter.lift' (𝓤 α) gen) ≤ Filter.lift' (𝓤 α) gen
[PROOFSTEP]
have h₂ : (𝓤 α).lift' f ≤ (𝓤 α).lift' gen :=
  uniformity_lift_le_swap
    (monotone_principal.comp (monotone_setOf fun p => @Filter.monotone_mem _ (p.2.val ×ˢ p.1.val)))
    (by
      have h := fun p : CauchyFilter α × CauchyFilter α => @Filter.prod_comm _ _ p.2.val p.1.val
      simp [Function.comp, h, mem_map']
      exact le_rfl)
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
h₁ : map Prod.swap (Filter.lift' (𝓤 α) gen) = Filter.lift' (𝓤 α) f
⊢ (Filter.lift (𝓤 α) fun s => (𝓟 ∘ f) (Prod.swap ⁻¹' s)) ≤ Filter.lift' (𝓤 α) gen
[PROOFSTEP]
have h := fun p : CauchyFilter α × CauchyFilter α => @Filter.prod_comm _ _ p.2.val p.1.val
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
h₁ : map Prod.swap (Filter.lift' (𝓤 α) gen) = Filter.lift' (𝓤 α) f
h : ∀ (p : CauchyFilter α × CauchyFilter α), ↑p.snd ×ˢ ↑p.fst = map (fun p => (p.snd, p.fst)) (↑p.fst ×ˢ ↑p.snd)
⊢ (Filter.lift (𝓤 α) fun s => (𝓟 ∘ f) (Prod.swap ⁻¹' s)) ≤ Filter.lift' (𝓤 α) gen
[PROOFSTEP]
simp [Function.comp, h, mem_map']
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
h₁ : map Prod.swap (Filter.lift' (𝓤 α) gen) = Filter.lift' (𝓤 α) f
h : ∀ (p : CauchyFilter α × CauchyFilter α), ↑p.snd ×ˢ ↑p.fst = map (fun p => (p.snd, p.fst)) (↑p.fst ×ˢ ↑p.snd)
⊢ (Filter.lift (𝓤 α) fun s => 𝓟 {p | (fun p => (p.snd, p.fst)) ⁻¹' (Prod.swap ⁻¹' s) ∈ ↑p.fst ×ˢ ↑p.snd}) ≤
    Filter.lift' (𝓤 α) gen
[PROOFSTEP]
exact le_rfl
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Set (α × α) → Set (CauchyFilter α × CauchyFilter α) := fun s => {p | s ∈ ↑p.snd ×ˢ ↑p.fst}
h₁ : map Prod.swap (Filter.lift' (𝓤 α) gen) = Filter.lift' (𝓤 α) f
h₂ : Filter.lift' (𝓤 α) f ≤ Filter.lift' (𝓤 α) gen
⊢ map Prod.swap (Filter.lift' (𝓤 α) gen) ≤ Filter.lift' (𝓤 α) gen
[PROOFSTEP]
exact h₁.trans_le h₂
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ (Filter.lift' (Filter.lift' (𝓤 α) gen) fun s => s ○ s) = Filter.lift' (𝓤 α) fun s => gen s ○ gen s
[PROOFSTEP]
rw [lift'_lift'_assoc]
[GOAL]
case hg
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ Monotone gen
[PROOFSTEP]
exact monotone_gen
[GOAL]
case hh
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ Monotone fun s => s ○ s
[PROOFSTEP]
exact monotone_id.compRel monotone_id
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ (Filter.lift' (𝓤 α) fun s => gen (s ○ s)) = Filter.lift' (Filter.lift' (𝓤 α) fun s => s ○ s) gen
[PROOFSTEP]
rw [lift'_lift'_assoc]
[GOAL]
case hg
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ Monotone fun s => s ○ s
[PROOFSTEP]
exact monotone_id.compRel monotone_id
[GOAL]
case hh
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ Monotone gen
[PROOFSTEP]
exact monotone_gen
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (CauchyFilter α × CauchyFilter α)
⊢ s ∈ 𝓤 (CauchyFilter α) ↔ ∃ t, t ∈ 𝓤 α ∧ ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
[PROOFSTEP]
refine mem_uniformity.trans (exists_congr (fun t => and_congr_right_iff.mpr (fun _h => ?_)))
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (CauchyFilter α × CauchyFilter α)
t : Set (α × α)
_h : t ∈ 𝓤 α
⊢ gen t ⊆ s ↔ ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
[PROOFSTEP]
exact ⟨fun h _f _g ht => h ht, fun h _p hp => h _ _ hp⟩
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
s : Set (α × α)
x✝ : α × α
a₁ a₂ : α
⊢ (a₁, a₂) ∈ ((preimage fun x => (pureCauchy x.fst, pureCauchy x.snd)) ∘ gen) s ↔ (a₁, a₂) ∈ id s
[PROOFSTEP]
simp [preimage, gen, pureCauchy, prod_principal_principal]
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
this : (preimage fun x => (pureCauchy x.fst, pureCauchy x.snd)) ∘ gen = id
⊢ Filter.lift' (𝓤 α) ((preimage fun x => (pureCauchy x.fst, pureCauchy x.snd)) ∘ gen) = 𝓤 α
[PROOFSTEP]
simp [this]
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : CauchyFilter α
⊢ f ∈ closure (range pureCauchy)
[PROOFSTEP]
have h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y : α, (f, pureCauchy y) ∈ s := fun s hs =>
  let ⟨t'', ht''₁, (ht''₂ : gen t'' ⊆ s)⟩ := (mem_lift'_sets monotone_gen).mp hs
  let ⟨t', ht'₁, ht'₂⟩ := comp_mem_uniformity_sets ht''₁
  have : t' ∈ f.val ×ˢ f.val := f.property.right ht'₁
  let ⟨t, ht, (h : t ×ˢ t ⊆ t')⟩ := mem_prod_same_iff.mp this
  let ⟨x, (hx : x ∈ t)⟩ := f.property.left.nonempty_of_mem ht
  have : t'' ∈ f.val ×ˢ pure x :=
    mem_prod_iff.mpr
      ⟨t, ht, {y : α | (x, y) ∈ t'}, h <| mk_mem_prod hx hx, fun ⟨a, b⟩ ⟨(h₁ : a ∈ t), (h₂ : (x, b) ∈ t')⟩ =>
        ht'₂ <| prod_mk_mem_compRel (@h (a, x) ⟨h₁, hx⟩) h₂⟩
  ⟨x, ht''₂ <| by dsimp [gen]; exact this⟩
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : CauchyFilter α
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
t'' : Set (α × α)
ht''₁ : t'' ∈ 𝓤 α
ht''₂ : gen t'' ⊆ s
t' : Set (α × α)
ht'₁ : t' ∈ 𝓤 α
ht'₂ : t' ○ t' ⊆ t''
this✝ : t' ∈ ↑f ×ˢ ↑f
t : Set α
ht : t ∈ ↑f
h : t ×ˢ t ⊆ t'
x : α
hx : x ∈ t
this : t'' ∈ ↑f ×ˢ pure x
⊢ (f, pureCauchy x) ∈ gen t''
[PROOFSTEP]
dsimp [gen]
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : CauchyFilter α
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
t'' : Set (α × α)
ht''₁ : t'' ∈ 𝓤 α
ht''₂ : gen t'' ⊆ s
t' : Set (α × α)
ht'₁ : t' ∈ 𝓤 α
ht'₂ : t' ○ t' ⊆ t''
this✝ : t' ∈ ↑f ×ˢ ↑f
t : Set α
ht : t ∈ ↑f
h : t ×ˢ t ⊆ t'
x : α
hx : x ∈ t
this : t'' ∈ ↑f ×ˢ pure x
⊢ t'' ∈ ↑f ×ˢ ↑(pureCauchy x)
[PROOFSTEP]
exact this
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : CauchyFilter α
h_ex : ∀ (s : Set (CauchyFilter α × CauchyFilter α)), s ∈ 𝓤 (CauchyFilter α) → ∃ y, (f, pureCauchy y) ∈ s
⊢ f ∈ closure (range pureCauchy)
[PROOFSTEP]
simp only [closure_eq_cluster_pts, ClusterPt, nhds_eq_uniformity, lift'_inf_principal_eq,
  Set.inter_comm _ (range pureCauchy), mem_setOf_eq]
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : CauchyFilter α
h_ex : ∀ (s : Set (CauchyFilter α × CauchyFilter α)), s ∈ 𝓤 (CauchyFilter α) → ∃ y, (f, pureCauchy y) ∈ s
⊢ NeBot (Filter.lift' (𝓤 (CauchyFilter α)) fun t => range pureCauchy ∩ UniformSpace.ball f t)
[PROOFSTEP]
refine (lift'_neBot_iff ?_).mpr (fun s hs => ?_)
[GOAL]
case refine_1
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : CauchyFilter α
h_ex : ∀ (s : Set (CauchyFilter α × CauchyFilter α)), s ∈ 𝓤 (CauchyFilter α) → ∃ y, (f, pureCauchy y) ∈ s
⊢ Monotone fun t => range pureCauchy ∩ UniformSpace.ball f t
[PROOFSTEP]
refine monotone_const.inter ?_
[GOAL]
case refine_1
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : CauchyFilter α
h_ex : ∀ (s : Set (CauchyFilter α × CauchyFilter α)), s ∈ 𝓤 (CauchyFilter α) → ∃ y, (f, pureCauchy y) ∈ s
⊢ Monotone fun t => UniformSpace.ball f t
[PROOFSTEP]
simp_rw [UniformSpace.ball]
[GOAL]
case refine_1
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : CauchyFilter α
h_ex : ∀ (s : Set (CauchyFilter α × CauchyFilter α)), s ∈ 𝓤 (CauchyFilter α) → ∃ y, (f, pureCauchy y) ∈ s
⊢ Monotone fun t => Prod.mk f ⁻¹' t
[PROOFSTEP]
exact monotone_preimage
[GOAL]
case refine_2
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : CauchyFilter α
h_ex : ∀ (s : Set (CauchyFilter α × CauchyFilter α)), s ∈ 𝓤 (CauchyFilter α) → ∃ y, (f, pureCauchy y) ∈ s
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
⊢ Set.Nonempty (range pureCauchy ∩ UniformSpace.ball f s)
[PROOFSTEP]
let ⟨y, hy⟩ := h_ex s hs
[GOAL]
case refine_2
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : CauchyFilter α
h_ex : ∀ (s : Set (CauchyFilter α × CauchyFilter α)), s ∈ 𝓤 (CauchyFilter α) → ∃ y, (f, pureCauchy y) ∈ s
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
y : α
hy : (f, pureCauchy y) ∈ s
⊢ Set.Nonempty (range pureCauchy ∩ UniformSpace.ball f s)
[PROOFSTEP]
have : pureCauchy y ∈ range pureCauchy ∩ {y : CauchyFilter α | (f, y) ∈ s} := ⟨mem_range_self y, hy⟩
[GOAL]
case refine_2
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : CauchyFilter α
h_ex : ∀ (s : Set (CauchyFilter α × CauchyFilter α)), s ∈ 𝓤 (CauchyFilter α) → ∃ y, (f, pureCauchy y) ∈ s
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ 𝓤 (CauchyFilter α)
y : α
hy : (f, pureCauchy y) ∈ s
this : pureCauchy y ∈ range pureCauchy ∩ {y | (f, y) ∈ s}
⊢ Set.Nonempty (range pureCauchy ∩ UniformSpace.ball f s)
[PROOFSTEP]
exact ⟨_, this⟩
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ Nonempty (CauchyFilter α) ↔ Nonempty α
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ Nonempty (CauchyFilter α) → Nonempty α
[PROOFSTEP]
rintro ⟨c⟩
[GOAL]
case mpr
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
⊢ Nonempty α → Nonempty (CauchyFilter α)
[PROOFSTEP]
rintro ⟨c⟩
[GOAL]
case mp.intro
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
c : CauchyFilter α
⊢ Nonempty α
[PROOFSTEP]
have := eq_univ_iff_forall.1 denseEmbedding_pureCauchy.toDenseInducing.closure_range c
[GOAL]
case mp.intro
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
c : CauchyFilter α
this : c ∈ closure (range pureCauchy)
⊢ Nonempty α
[PROOFSTEP]
obtain ⟨_, ⟨_, a, _⟩⟩ := mem_closure_iff.1 this _ isOpen_univ trivial
[GOAL]
case mp.intro.intro.intro.intro
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
c : CauchyFilter α
this : c ∈ closure (range pureCauchy)
w✝ : CauchyFilter α
left✝ : w✝ ∈ univ
a : α
h✝ : pureCauchy a = w✝
⊢ Nonempty α
[PROOFSTEP]
exact ⟨a⟩
[GOAL]
case mpr.intro
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
c : α
⊢ Nonempty (CauchyFilter α)
[PROOFSTEP]
exact ⟨pureCauchy c⟩
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Filter α
hf : Cauchy f
f' : CauchyFilter α := { val := f, property := hf }
this : map pureCauchy f ≤ Filter.lift' (𝓤 (CauchyFilter α)) (preimage (Prod.mk f'))
⊢ map pureCauchy f ≤ 𝓝 f'
[PROOFSTEP]
simp [nhds_eq_uniformity]
[GOAL]
α : Type u
inst✝² : UniformSpace α
β : Type v
γ : Type w
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
f : Filter α
hf : Cauchy f
f' : CauchyFilter α := { val := f, property := hf }
this : map pureCauchy f ≤ Filter.lift' (𝓤 (CauchyFilter α)) (preimage (Prod.mk f'))
⊢ map pureCauchy f ≤ Filter.lift' (𝓤 (CauchyFilter α)) (UniformSpace.ball { val := f, property := hf })
[PROOFSTEP]
assumption
[GOAL]
α : Type u
inst✝³ : UniformSpace α
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
hf : UniformContinuous f
a : α
⊢ extend f (pureCauchy a) = f a
[PROOFSTEP]
rw [extend, if_pos hf]
[GOAL]
α : Type u
inst✝³ : UniformSpace α
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : SeparatedSpace β
f : α → β
hf : UniformContinuous f
a : α
⊢ DenseInducing.extend (_ : DenseInducing pureCauchy) f (pureCauchy a) = f a
[PROOFSTEP]
exact uniformly_extend_of_ind uniformInducing_pureCauchy denseRange_pureCauchy hf _
[GOAL]
α : Type u
inst✝³ : UniformSpace α
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace β
f : α → β
⊢ UniformContinuous (extend f)
[PROOFSTEP]
by_cases hf : UniformContinuous f
[GOAL]
case pos
α : Type u
inst✝³ : UniformSpace α
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (extend f)
[PROOFSTEP]
rw [extend, if_pos hf]
[GOAL]
case pos
α : Type u
inst✝³ : UniformSpace α
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (DenseInducing.extend (_ : DenseInducing pureCauchy) f)
[PROOFSTEP]
exact uniformContinuous_uniformly_extend uniformInducing_pureCauchy denseRange_pureCauchy hf
[GOAL]
case neg
α : Type u
inst✝³ : UniformSpace α
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous (extend f)
[PROOFSTEP]
rw [extend, if_neg hf]
[GOAL]
case neg
α : Type u
inst✝³ : UniformSpace α
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous fun x => f (Nonempty.some (_ : Nonempty α))
[PROOFSTEP]
exact uniformContinuous_of_const fun a _b => by congr
[GOAL]
α : Type u
inst✝³ : UniformSpace α
β : Type v
γ : Type w
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace β
f : α → β
hf : ¬UniformContinuous f
a _b : CauchyFilter α
⊢ f (Nonempty.some (_ : Nonempty α)) = f (Nonempty.some (_ : Nonempty α))
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
⊢ lim ↑f = lim ↑g ↔ (f, g) ∈ 𝓢 (CauchyFilter α)
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
⊢ lim ↑f = lim ↑g → (f, g) ∈ 𝓢 (CauchyFilter α)
[PROOFSTEP]
intro e s hs
[GOAL]
case mp
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
⊢ (f, g) ∈ s
[PROOFSTEP]
rcases CauchyFilter.mem_uniformity'.1 hs with ⟨t, tu, ts⟩
[GOAL]
case mp.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
⊢ (f, g) ∈ s
[PROOFSTEP]
apply ts
[GOAL]
case mp.intro.intro.a
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
⊢ t ∈ ↑f ×ˢ ↑g
[PROOFSTEP]
rcases comp_mem_uniformity_sets tu with ⟨d, du, dt⟩
[GOAL]
case mp.intro.intro.a.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
d : Set (α × α)
du : d ∈ 𝓤 α
dt : d ○ d ⊆ t
⊢ t ∈ ↑f ×ˢ ↑g
[PROOFSTEP]
refine'
  mem_prod_iff.2
    ⟨_, f.2.le_nhds_lim (mem_nhds_right (lim f.1) du), _, g.2.le_nhds_lim (mem_nhds_left (lim g.1) du), fun x h => _⟩
[GOAL]
case mp.intro.intro.a.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
d : Set (α × α)
du : d ∈ 𝓤 α
dt : d ○ d ⊆ t
x : α × α
h : x ∈ {x | (x, lim ↑f) ∈ d} ×ˢ {y | (lim ↑g, y) ∈ d}
⊢ x ∈ t
[PROOFSTEP]
cases' x with a b
[GOAL]
case mp.intro.intro.a.intro.intro.mk
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
d : Set (α × α)
du : d ∈ 𝓤 α
dt : d ○ d ⊆ t
a b : α
h : (a, b) ∈ {x | (x, lim ↑f) ∈ d} ×ˢ {y | (lim ↑g, y) ∈ d}
⊢ (a, b) ∈ t
[PROOFSTEP]
cases' h with h₁ h₂
[GOAL]
case mp.intro.intro.a.intro.intro.mk.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
d : Set (α × α)
du : d ∈ 𝓤 α
dt : d ○ d ⊆ t
a b : α
h₁ : (a, b).fst ∈ {x | (x, lim ↑f) ∈ d}
h₂ : (a, b).snd ∈ {y | (lim ↑g, y) ∈ d}
⊢ (a, b) ∈ t
[PROOFSTEP]
rw [← e] at h₂
[GOAL]
case mp.intro.intro.a.intro.intro.mk.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
e : lim ↑f = lim ↑g
s : Set (CauchyFilter α × CauchyFilter α)
hs : s ∈ (𝓤 (CauchyFilter α)).sets
t : Set (α × α)
tu : t ∈ 𝓤 α
ts : ∀ (f g : CauchyFilter α), t ∈ ↑f ×ˢ ↑g → (f, g) ∈ s
d : Set (α × α)
du : d ∈ 𝓤 α
dt : d ○ d ⊆ t
a b : α
h₁ : (a, b).fst ∈ {x | (x, lim ↑f) ∈ d}
h₂ : (a, b).snd ∈ {y | (lim ↑f, y) ∈ d}
⊢ (a, b) ∈ t
[PROOFSTEP]
exact dt ⟨_, h₁, h₂⟩
[GOAL]
case mpr
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
⊢ (f, g) ∈ 𝓢 (CauchyFilter α) → lim ↑f = lim ↑g
[PROOFSTEP]
intro H
[GOAL]
case mpr
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
H : (f, g) ∈ 𝓢 (CauchyFilter α)
⊢ lim ↑f = lim ↑g
[PROOFSTEP]
refine' separated_def.1 (by infer_instance) _ _ fun t tu => _
[GOAL]
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
H : (f, g) ∈ 𝓢 (CauchyFilter α)
⊢ SeparatedSpace α
[PROOFSTEP]
infer_instance
[GOAL]
case mpr
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
H : (f, g) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
⊢ (lim ↑f, lim ↑g) ∈ t
[PROOFSTEP]
rcases mem_uniformity_isClosed tu with ⟨d, du, dc, dt⟩
[GOAL]
case mpr.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f g : CauchyFilter α
H : (f, g) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
⊢ (lim ↑f, lim ↑g) ∈ t
[PROOFSTEP]
refine' H {p | (lim p.1.1, lim p.2.1) ∈ t} (CauchyFilter.mem_uniformity'.2 ⟨d, du, fun f g h => _⟩)
[GOAL]
case mpr.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h : d ∈ ↑f ×ˢ ↑g
⊢ (f, g) ∈ {p | (lim ↑p.fst, lim ↑p.snd) ∈ t}
[PROOFSTEP]
rcases mem_prod_iff.1 h with ⟨x, xf, y, yg, h⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h✝ : d ∈ ↑f ×ˢ ↑g
x : Set α
xf : x ∈ ↑f
y : Set α
yg : y ∈ ↑g
h : x ×ˢ y ⊆ d
⊢ (f, g) ∈ {p | (lim ↑p.fst, lim ↑p.snd) ∈ t}
[PROOFSTEP]
have limc : ∀ (f : CauchyFilter α), ∀ x ∈ f.1, lim f.1 ∈ closure x :=
  by
  intro f x xf
  rw [closure_eq_cluster_pts]
  exact f.2.1.mono (le_inf f.2.le_nhds_lim (le_principal_iff.2 xf))
[GOAL]
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h✝ : d ∈ ↑f ×ˢ ↑g
x : Set α
xf : x ∈ ↑f
y : Set α
yg : y ∈ ↑g
h : x ×ˢ y ⊆ d
⊢ ∀ (f : CauchyFilter α) (x : Set α), x ∈ ↑f → lim ↑f ∈ closure x
[PROOFSTEP]
intro f x xf
[GOAL]
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝¹ g✝ : CauchyFilter α
H : (f✝¹, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f✝ g : CauchyFilter α
h✝ : d ∈ ↑f✝ ×ˢ ↑g
x✝ : Set α
xf✝ : x✝ ∈ ↑f✝
y : Set α
yg : y ∈ ↑g
h : x✝ ×ˢ y ⊆ d
f : CauchyFilter α
x : Set α
xf : x ∈ ↑f
⊢ lim ↑f ∈ closure x
[PROOFSTEP]
rw [closure_eq_cluster_pts]
[GOAL]
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝¹ g✝ : CauchyFilter α
H : (f✝¹, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f✝ g : CauchyFilter α
h✝ : d ∈ ↑f✝ ×ˢ ↑g
x✝ : Set α
xf✝ : x✝ ∈ ↑f✝
y : Set α
yg : y ∈ ↑g
h : x✝ ×ˢ y ⊆ d
f : CauchyFilter α
x : Set α
xf : x ∈ ↑f
⊢ lim ↑f ∈ {a | ClusterPt a (𝓟 x)}
[PROOFSTEP]
exact f.2.1.mono (le_inf f.2.le_nhds_lim (le_principal_iff.2 xf))
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h✝ : d ∈ ↑f ×ˢ ↑g
x : Set α
xf : x ∈ ↑f
y : Set α
yg : y ∈ ↑g
h : x ×ˢ y ⊆ d
limc : ∀ (f : CauchyFilter α) (x : Set α), x ∈ ↑f → lim ↑f ∈ closure x
⊢ (f, g) ∈ {p | (lim ↑p.fst, lim ↑p.snd) ∈ t}
[PROOFSTEP]
have := dc.closure_subset_iff.2 h
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h✝ : d ∈ ↑f ×ˢ ↑g
x : Set α
xf : x ∈ ↑f
y : Set α
yg : y ∈ ↑g
h : x ×ˢ y ⊆ d
limc : ∀ (f : CauchyFilter α) (x : Set α), x ∈ ↑f → lim ↑f ∈ closure x
this : closure (x ×ˢ y) ⊆ d
⊢ (f, g) ∈ {p | (lim ↑p.fst, lim ↑p.snd) ∈ t}
[PROOFSTEP]
rw [closure_prod_eq] at this
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h✝ : d ∈ ↑f ×ˢ ↑g
x : Set α
xf : x ∈ ↑f
y : Set α
yg : y ∈ ↑g
h : x ×ˢ y ⊆ d
limc : ∀ (f : CauchyFilter α) (x : Set α), x ∈ ↑f → lim ↑f ∈ closure x
this : closure x ×ˢ closure y ⊆ d
⊢ (f, g) ∈ {p | (lim ↑p.fst, lim ↑p.snd) ∈ t}
[PROOFSTEP]
refine' dt (this ⟨_, _⟩)
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h✝ : d ∈ ↑f ×ˢ ↑g
x : Set α
xf : x ∈ ↑f
y : Set α
yg : y ∈ ↑g
h : x ×ˢ y ⊆ d
limc : ∀ (f : CauchyFilter α) (x : Set α), x ∈ ↑f → lim ↑f ∈ closure x
this : closure x ×ˢ closure y ⊆ d
⊢ (lim ↑(f, g).fst, lim ↑(f, g).snd).fst ∈ closure x
[PROOFSTEP]
dsimp
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h✝ : d ∈ ↑f ×ˢ ↑g
x : Set α
xf : x ∈ ↑f
y : Set α
yg : y ∈ ↑g
h : x ×ˢ y ⊆ d
limc : ∀ (f : CauchyFilter α) (x : Set α), x ∈ ↑f → lim ↑f ∈ closure x
this : closure x ×ˢ closure y ⊆ d
⊢ (lim ↑(f, g).fst, lim ↑(f, g).snd).snd ∈ closure y
[PROOFSTEP]
dsimp
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h✝ : d ∈ ↑f ×ˢ ↑g
x : Set α
xf : x ∈ ↑f
y : Set α
yg : y ∈ ↑g
h : x ×ˢ y ⊆ d
limc : ∀ (f : CauchyFilter α) (x : Set α), x ∈ ↑f → lim ↑f ∈ closure x
this : closure x ×ˢ closure y ⊆ d
⊢ lim ↑f ∈ closure x
[PROOFSTEP]
apply limc
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h✝ : d ∈ ↑f ×ˢ ↑g
x : Set α
xf : x ∈ ↑f
y : Set α
yg : y ∈ ↑g
h : x ×ˢ y ⊆ d
limc : ∀ (f : CauchyFilter α) (x : Set α), x ∈ ↑f → lim ↑f ∈ closure x
this : closure x ×ˢ closure y ⊆ d
⊢ lim ↑g ∈ closure y
[PROOFSTEP]
apply limc
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro.refine'_1.a
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h✝ : d ∈ ↑f ×ˢ ↑g
x : Set α
xf : x ∈ ↑f
y : Set α
yg : y ∈ ↑g
h : x ×ˢ y ⊆ d
limc : ∀ (f : CauchyFilter α) (x : Set α), x ∈ ↑f → lim ↑f ∈ closure x
this : closure x ×ˢ closure y ⊆ d
⊢ x ∈ ↑f
[PROOFSTEP]
assumption
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro.refine'_2.a
α : Type u_1
inst✝³ : Inhabited α
inst✝² : UniformSpace α
inst✝¹ : CompleteSpace α
inst✝ : SeparatedSpace α
f✝ g✝ : CauchyFilter α
H : (f✝, g✝) ∈ 𝓢 (CauchyFilter α)
t : Set (α × α)
tu : t ∈ 𝓤 α
d : Set (α × α)
du : d ∈ 𝓤 α
dc : IsClosed d
dt : d ⊆ t
f g : CauchyFilter α
h✝ : d ∈ ↑f ×ˢ ↑g
x : Set α
xf : x ∈ ↑f
y : Set α
yg : y ∈ ↑g
h : x ×ˢ y ⊆ d
limc : ∀ (f : CauchyFilter α) (x : Set α), x ∈ ↑f → lim ↑f ∈ closure x
this : closure x ×ˢ closure y ⊆ d
⊢ y ∈ ↑g
[PROOFSTEP]
assumption
[GOAL]
α : Type u_1
inst✝ : UniformSpace α
s : SeparatedSpace α
a b : α
h :
  (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) a =
    (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) b
⊢ a = b
[PROOFSTEP]
refine separated_def.1 s _ _ (fun s hs => ?_)
[GOAL]
α : Type u_1
inst✝ : UniformSpace α
s✝ : SeparatedSpace α
a b : α
h :
  (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) a =
    (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) b
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ (a, b) ∈ s
[PROOFSTEP]
rw [← (@uniformEmbedding_pureCauchy α _).comap_uniformity, Filter.mem_comap] at hs
[GOAL]
α : Type u_1
inst✝ : UniformSpace α
s✝ : SeparatedSpace α
a b : α
h :
  (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) a =
    (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) b
s : Set (α × α)
hs : ∃ t, t ∈ 𝓤 (CauchyFilter α) ∧ (fun x => (pureCauchy x.fst, pureCauchy x.snd)) ⁻¹' t ⊆ s
⊢ (a, b) ∈ s
[PROOFSTEP]
obtain ⟨t, ht, hts⟩ := hs
[GOAL]
case intro.intro
α : Type u_1
inst✝ : UniformSpace α
s✝ : SeparatedSpace α
a b : α
h :
  (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) a =
    (fun a => Quotient.mk (UniformSpace.separationSetoid (CauchyFilter α)) (pureCauchy a)) b
s : Set (α × α)
t : Set (CauchyFilter α × CauchyFilter α)
ht : t ∈ 𝓤 (CauchyFilter α)
hts : (fun x => (pureCauchy x.fst, pureCauchy x.snd)) ⁻¹' t ⊆ s
⊢ (a, b) ∈ s
[PROOFSTEP]
exact @hts (a, b) (Quotient.exact h t ht)
[GOAL]
α : Type u_1
inst✝² : UniformSpace α
β : Type u_2
inst✝¹ : UniformSpace β
γ : Type u_3
inst✝ : UniformSpace γ
h : CompleteSpace α
⊢ CompleteSpace (Quotient (separationSetoid α))
[PROOFSTEP]
constructor
[GOAL]
case complete
α : Type u_1
inst✝² : UniformSpace α
β : Type u_2
inst✝¹ : UniformSpace β
γ : Type u_3
inst✝ : UniformSpace γ
h : CompleteSpace α
⊢ ∀ {f : Filter (Quotient (separationSetoid α))}, Cauchy f → ∃ x, f ≤ 𝓝 x
[PROOFSTEP]
intro f hf
[GOAL]
case complete
α : Type u_1
inst✝² : UniformSpace α
β : Type u_2
inst✝¹ : UniformSpace β
γ : Type u_3
inst✝ : UniformSpace γ
h : CompleteSpace α
f : Filter (Quotient (separationSetoid α))
hf : Cauchy f
⊢ ∃ x, f ≤ 𝓝 x
[PROOFSTEP]
have : Cauchy (f.comap fun x => ⟦x⟧) :=
  hf.comap' comap_quotient_le_uniformity <| hf.left.comap_of_surj (surjective_quotient_mk _)
[GOAL]
case complete
α : Type u_1
inst✝² : UniformSpace α
β : Type u_2
inst✝¹ : UniformSpace β
γ : Type u_3
inst✝ : UniformSpace γ
h : CompleteSpace α
f : Filter (Quotient (separationSetoid α))
hf : Cauchy f
this : Cauchy (Filter.comap (fun x => Quotient.mk (separationSetoid α) x) f)
⊢ ∃ x, f ≤ 𝓝 x
[PROOFSTEP]
let ⟨x, (hx : (f.comap fun x => ⟦x⟧) ≤ 𝓝 x)⟩ := CompleteSpace.complete this
[GOAL]
case complete
α : Type u_1
inst✝² : UniformSpace α
β : Type u_2
inst✝¹ : UniformSpace β
γ : Type u_3
inst✝ : UniformSpace γ
h : CompleteSpace α
f : Filter (Quotient (separationSetoid α))
hf : Cauchy f
this : Cauchy (Filter.comap (fun x => Quotient.mk (separationSetoid α) x) f)
x : α
hx : Filter.comap (fun x => Quotient.mk (separationSetoid α) x) f ≤ 𝓝 x
⊢ ∃ x, f ≤ 𝓝 x
[PROOFSTEP]
exact ⟨⟦x⟧, (comap_le_comap_iff <| by simp).1 (hx.trans <| map_le_iff_le_comap.1 continuous_quotient_mk'.continuousAt)⟩
[GOAL]
α : Type u_1
inst✝² : UniformSpace α
β : Type u_2
inst✝¹ : UniformSpace β
γ : Type u_3
inst✝ : UniformSpace γ
h : CompleteSpace α
f : Filter (Quotient (separationSetoid α))
hf : Cauchy f
this : Cauchy (Filter.comap (fun x => Quotient.mk (separationSetoid α) x) f)
x : α
hx : Filter.comap (fun x => Quotient.mk (separationSetoid α) x) f ≤ 𝓝 x
⊢ (range fun x => Quotient.mk (separationSetoid α) x) ∈ f
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : UniformSpace α
β : Type u_2
inst✝¹ : UniformSpace β
γ : Type u_3
inst✝ : UniformSpace γ
⊢ Filter.comap (fun p => (↑α p.fst, ↑α p.snd)) (𝓤 (Completion α)) = 𝓤 α
[PROOFSTEP]
have :
  (fun x : α × α => ((x.1 : Completion α), (x.2 : Completion α))) =
    (fun x : CauchyFilter α × CauchyFilter α => (⟦x.1⟧, ⟦x.2⟧)) ∘ fun x : α × α => (pureCauchy x.1, pureCauchy x.2) :=
  by ext ⟨a, b⟩ <;> simp <;> rfl
[GOAL]
α : Type u_1
inst✝² : UniformSpace α
β : Type u_2
inst✝¹ : UniformSpace β
γ : Type u_3
inst✝ : UniformSpace γ
⊢ (fun x => (↑α x.fst, ↑α x.snd)) =
    (fun x =>
        (Quotient.mk (separationSetoid (CauchyFilter α)) x.fst,
          Quotient.mk (separationSetoid (CauchyFilter α)) x.snd)) ∘
      fun x => (pureCauchy x.fst, pureCauchy x.snd)
[PROOFSTEP]
ext ⟨a, b⟩
[GOAL]
case h.mk.h₁
α : Type u_1
inst✝² : UniformSpace α
β : Type u_2
inst✝¹ : UniformSpace β
γ : Type u_3
inst✝ : UniformSpace γ
a b : α
⊢ (↑α (a, b).fst, ↑α (a, b).snd).fst =
    (((fun x =>
            (Quotient.mk (separationSetoid (CauchyFilter α)) x.fst,
              Quotient.mk (separationSetoid (CauchyFilter α)) x.snd)) ∘
          fun x => (pureCauchy x.fst, pureCauchy x.snd))
        (a, b)).fst
[PROOFSTEP]
simp
[GOAL]
case h.mk.h₂
α : Type u_1
inst✝² : UniformSpace α
β : Type u_2
inst✝¹ : UniformSpace β
γ : Type u_3
inst✝ : UniformSpace γ
a b : α
⊢ (↑α (a, b).fst, ↑α (a, b).snd).snd =
    (((fun x =>
            (Quotient.mk (separationSetoid (CauchyFilter α)) x.fst,
              Quotient.mk (separationSetoid (CauchyFilter α)) x.snd)) ∘
          fun x => (pureCauchy x.fst, pureCauchy x.snd))
        (a, b)).snd
[PROOFSTEP]
simp
[GOAL]
case h.mk.h₁
α : Type u_1
inst✝² : UniformSpace α
β : Type u_2
inst✝¹ : UniformSpace β
γ : Type u_3
inst✝ : UniformSpace γ
a b : α
⊢ ↑α a = Quotient.mk (separationSetoid (CauchyFilter α)) (pureCauchy a)
[PROOFSTEP]
rfl
[GOAL]
case h.mk.h₂
α : Type u_1
inst✝² : UniformSpace α
β : Type u_2
inst✝¹ : UniformSpace β
γ : Type u_3
inst✝ : UniformSpace γ
a b : α
⊢ ↑α b = Quotient.mk (separationSetoid (CauchyFilter α)) (pureCauchy b)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝² : UniformSpace α
β : Type u_2
inst✝¹ : UniformSpace β
γ : Type u_3
inst✝ : UniformSpace γ
this :
  (fun x => (↑α x.fst, ↑α x.snd)) =
    (fun x =>
        (Quotient.mk (separationSetoid (CauchyFilter α)) x.fst,
          Quotient.mk (separationSetoid (CauchyFilter α)) x.snd)) ∘
      fun x => (pureCauchy x.fst, pureCauchy x.snd)
⊢ Filter.comap (fun p => (↑α p.fst, ↑α p.snd)) (𝓤 (Completion α)) = 𝓤 α
[PROOFSTEP]
rw [this, ← Filter.comap_comap]
[GOAL]
α : Type u_1
inst✝² : UniformSpace α
β : Type u_2
inst✝¹ : UniformSpace β
γ : Type u_3
inst✝ : UniformSpace γ
this :
  (fun x => (↑α x.fst, ↑α x.snd)) =
    (fun x =>
        (Quotient.mk (separationSetoid (CauchyFilter α)) x.fst,
          Quotient.mk (separationSetoid (CauchyFilter α)) x.snd)) ∘
      fun x => (pureCauchy x.fst, pureCauchy x.snd)
⊢ Filter.comap (fun x => (pureCauchy x.fst, pureCauchy x.snd))
      (Filter.comap
        (fun x =>
          (Quotient.mk (separationSetoid (CauchyFilter α)) x.fst,
            Quotient.mk (separationSetoid (CauchyFilter α)) x.snd))
        (𝓤 (Completion α))) =
    𝓤 α
[PROOFSTEP]
change Filter.comap _ (Filter.comap _ (𝓤 <| Quotient <| separationSetoid <| CauchyFilter α)) = 𝓤 α
[GOAL]
α : Type u_1
inst✝² : UniformSpace α
β : Type u_2
inst✝¹ : UniformSpace β
γ : Type u_3
inst✝ : UniformSpace γ
this :
  (fun x => (↑α x.fst, ↑α x.snd)) =
    (fun x =>
        (Quotient.mk (separationSetoid (CauchyFilter α)) x.fst,
          Quotient.mk (separationSetoid (CauchyFilter α)) x.snd)) ∘
      fun x => (pureCauchy x.fst, pureCauchy x.snd)
⊢ Filter.comap (fun x => (pureCauchy x.fst, pureCauchy x.snd))
      (Filter.comap
        (fun x =>
          (Quotient.mk (separationSetoid (CauchyFilter α)) x.fst,
            Quotient.mk (separationSetoid (CauchyFilter α)) x.snd))
        (𝓤 (Quotient (separationSetoid (CauchyFilter α))))) =
    𝓤 α
[PROOFSTEP]
rw [comap_quotient_eq_uniformity, uniformEmbedding_pureCauchy.comap_uniformity]
[GOAL]
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u_4
inst✝ : UniformSpace α
⊢ UniformSpace (Completion α)
[PROOFSTEP]
infer_instance
[GOAL]
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u_4
inst✝ : UniformSpace α
⊢ CompleteSpace (Completion α)
[PROOFSTEP]
infer_instance
[GOAL]
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u_4
inst✝ : UniformSpace α
⊢ SeparatedSpace (Completion α)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝⁴ : UniformSpace α
β : Type u_2
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
f✝ : α → β
inst✝¹ : CompleteSpace γ
inst✝ : SeparatedSpace γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
⊢ ∀ (a : α), (Completion.extension f ∘ Completion.map g) (↑α a) = Completion.extension (f ∘ g) (↑α a)
[PROOFSTEP]
intro a
[GOAL]
α : Type u_1
inst✝⁴ : UniformSpace α
β : Type u_2
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
f✝ : α → β
inst✝¹ : CompleteSpace γ
inst✝ : SeparatedSpace γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ (Completion.extension f ∘ Completion.map g) (↑α a) = Completion.extension (f ∘ g) (↑α a)
[PROOFSTEP]
rw [extension_coe (hf.comp hg), Function.comp_apply, map_coe hg, extension_coe hf, Function.comp_apply]
[GOAL]
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
⊢ Completion (SeparationQuotient α) ≃ Completion α
[PROOFSTEP]
refine' ⟨Completion.extension (SeparationQuotient.lift ((↑) : α → Completion α)), Completion.map Quotient.mk', _, _⟩
[GOAL]
case refine'_1
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
⊢ Function.LeftInverse (Completion.map Quotient.mk') (Completion.extension (SeparationQuotient.lift ↑α))
[PROOFSTEP]
intro a
[GOAL]
case refine'_1
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a : Completion (SeparationQuotient α)
⊢ Completion.map Quotient.mk' (Completion.extension (SeparationQuotient.lift ↑α) a) = a
[PROOFSTEP]
refine' induction_on a (isClosed_eq (continuous_map.comp continuous_extension) continuous_id) _
[GOAL]
case refine'_1
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a : Completion (SeparationQuotient α)
⊢ ∀ (a : SeparationQuotient α),
    Completion.map Quotient.mk' (Completion.extension (SeparationQuotient.lift ↑α) (↑(SeparationQuotient α) a)) =
      ↑(SeparationQuotient α) a
[PROOFSTEP]
rintro
  ⟨a⟩
      -- porting note: had to insert rewrites to switch between Quot.mk, Quotient.mk, Quotient.mk'
[GOAL]
case refine'_1.mk
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a✝¹ : Completion (SeparationQuotient α)
a✝ : SeparationQuotient α
a : α
⊢ Completion.map Quotient.mk'
      (Completion.extension (SeparationQuotient.lift ↑α) (↑(SeparationQuotient α) (Quot.mk Setoid.r a))) =
    ↑(SeparationQuotient α) (Quot.mk Setoid.r a)
[PROOFSTEP]
rw [← Quotient.mk, extension_coe (SeparationQuotient.uniformContinuous_lift _),
  SeparationQuotient.lift_mk (uniformContinuous_coe α), map_coe]
[GOAL]
case refine'_1.mk
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a✝¹ : Completion (SeparationQuotient α)
a✝ : SeparationQuotient α
a : α
⊢ ↑(SeparationQuotient α) (Quotient.mk' a) = ↑(SeparationQuotient α) (Quotient.mk (separationSetoid α) a)
[PROOFSTEP]
rfl
[GOAL]
case refine'_1.mk.hf
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a✝¹ : Completion (SeparationQuotient α)
a✝ : SeparationQuotient α
a : α
⊢ UniformContinuous Quotient.mk'
[PROOFSTEP]
exact uniformContinuous_quotient_mk
[GOAL]
case refine'_2
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
⊢ Function.RightInverse (Completion.map Quotient.mk') (Completion.extension (SeparationQuotient.lift ↑α))
[PROOFSTEP]
intro a
[GOAL]
case refine'_2
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a : Completion α
⊢ Completion.extension (SeparationQuotient.lift ↑α) (Completion.map Quotient.mk' a) = a
[PROOFSTEP]
refine' Completion.induction_on a (isClosed_eq (continuous_extension.comp continuous_map) continuous_id) fun a => _
[GOAL]
case refine'_2
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a✝ : Completion α
a : α
⊢ Completion.extension (SeparationQuotient.lift ↑α) (Completion.map Quotient.mk' (↑α a)) = ↑α a
[PROOFSTEP]
rw [map_coe]
  -- porting note: add SeparationQuotient.lift_mk' for Quotient.mk' ?
[GOAL]
case refine'_2
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a✝ : Completion α
a : α
⊢ Completion.extension (SeparationQuotient.lift ↑α) (↑(SeparationQuotient α) (Quotient.mk' a)) = ↑α a
[PROOFSTEP]
rw [extension_coe (SeparationQuotient.uniformContinuous_lift _), Quotient.mk',
  SeparationQuotient.lift_mk (uniformContinuous_coe α) _]
[GOAL]
case refine'_2.hf
α✝ : Type u_1
inst✝³ : UniformSpace α✝
β : Type u_2
inst✝² : UniformSpace β
γ : Type u_3
inst✝¹ : UniformSpace γ
α : Type u
inst✝ : UniformSpace α
a✝ : Completion α
a : α
⊢ UniformContinuous Quotient.mk'
[PROOFSTEP]
exact uniformContinuous_quotient_mk


[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
⊢ Isometry f ↔ ∀ (x y : α), nndist (f x) (f y) = nndist x y
[PROOFSTEP]
simp only [Isometry, edist_nndist, ENNReal.coe_eq_coe]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
⊢ Isometry f ↔ ∀ (x y : α), dist (f x) (f y) = dist x y
[PROOFSTEP]
simp only [isometry_iff_nndist_eq, ← coe_nndist, NNReal.coe_eq]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
x✝ y✝ z : α
s : Set α
h : Isometry f
x y : α
⊢ edist x y ≤ ↑1 * edist (f x) (f y)
[PROOFSTEP]
simp only [h x y, ENNReal.coe_one, one_mul, le_refl]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace γ
f : α → β
x✝ y✝ z : α
s : Set α
inst✝ : Subsingleton α
x y : α
⊢ edist (f x) (f y) = edist x y
[PROOFSTEP]
rw [Subsingleton.elim x y]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace γ
f : α → β
x✝ y✝ z : α
s : Set α
inst✝ : Subsingleton α
x y : α
⊢ edist (f y) (f y) = edist y y
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace γ
f✝ : α → β
x✝ y✝ z : α
s : Set α
δ : Type u_2
inst✝ : PseudoEMetricSpace δ
f : α → β
g : γ → δ
hf : Isometry f
hg : Isometry g
x y : α × γ
⊢ edist (Prod.map f g x) (Prod.map f g y) = edist x y
[PROOFSTEP]
simp only [Prod.edist_eq, hf.edist_eq, hg.edist_eq, Prod_map]
[GOAL]
ι✝ : Type u_1
α✝ : Type u
β✝ : Type v
γ : Type w
inst✝⁵ : PseudoEMetricSpace α✝
inst✝⁴ : PseudoEMetricSpace β✝
inst✝³ : PseudoEMetricSpace γ
f✝ : α✝ → β✝
x✝ y✝ z : α✝
s : Set α✝
ι : Type u_4
inst✝² : Fintype ι
α : ι → Type u_2
β : ι → Type u_3
inst✝¹ : (i : ι) → PseudoEMetricSpace (α i)
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : (i : ι) → α i → β i
hf : ∀ (i : ι), Isometry (f i)
x y : (i : ι) → α i
⊢ edist ((fun g i => f i (g i)) x) ((fun g i => f i (g i)) y) = edist x y
[PROOFSTEP]
simp only [edist_pi_def, (hf _).edist_eq]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f✝ : α → β
x✝ y✝ z : α
s : Set α
f : α → β
g : β → α
h : Isometry f
hg : Function.RightInverse g f
x y : β
⊢ edist (g x) (g y) = edist x y
[PROOFSTEP]
rw [← h, hg _, hg _]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
x✝ y z : α
s : Set α
h : Isometry f
x : α
r : ℝ≥0∞
⊢ f ⁻¹' EMetric.closedBall (f x) r = EMetric.closedBall x r
[PROOFSTEP]
ext y
[GOAL]
case h
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
x✝ y✝ z : α
s : Set α
h : Isometry f
x : α
r : ℝ≥0∞
y : α
⊢ y ∈ f ⁻¹' EMetric.closedBall (f x) r ↔ y ∈ EMetric.closedBall x r
[PROOFSTEP]
simp [h.edist_eq]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
x✝ y z : α
s : Set α
h : Isometry f
x : α
r : ℝ≥0∞
⊢ f ⁻¹' EMetric.ball (f x) r = EMetric.ball x r
[PROOFSTEP]
ext y
[GOAL]
case h
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
x✝ y✝ z : α
s : Set α
h : Isometry f
x : α
r : ℝ≥0∞
y : α
⊢ y ∈ f ⁻¹' EMetric.ball (f x) r ↔ y ∈ EMetric.ball x r
[PROOFSTEP]
simp [h.edist_eq]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
x y z : α
s✝ : Set α
hf : Isometry f
s : Set α
d : ℝ≥0∞
⊢ EMetric.diam (f '' s) ≤ d ↔ EMetric.diam s ≤ d
[PROOFSTEP]
simp only [EMetric.diam_le_iff, ball_image_iff, hf.edist_eq]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
x y z : α
s : Set α
hf : Isometry f
⊢ EMetric.diam (range f) = EMetric.diam univ
[PROOFSTEP]
rw [← image_univ]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
f : α → β
x y z : α
s : Set α
hf : Isometry f
⊢ EMetric.diam (f '' univ) = EMetric.diam univ
[PROOFSTEP]
exact hf.ediam_image univ
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
s : Set α
⊢ Metric.diam (f '' s) = Metric.diam s
[PROOFSTEP]
rw [Metric.diam, Metric.diam, hf.ediam_image]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
⊢ Metric.diam (range f) = Metric.diam univ
[PROOFSTEP]
rw [← image_univ]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
⊢ Metric.diam (f '' univ) = Metric.diam univ
[PROOFSTEP]
exact hf.diam_image univ
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
x : α
p : ℝ → Prop
⊢ f ⁻¹' {y | p (dist y (f x))} = {y | p (dist y x)}
[PROOFSTEP]
ext y
[GOAL]
case h
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
hf : Isometry f
x : α
p : ℝ → Prop
y : α
⊢ y ∈ f ⁻¹' {y | p (dist y (f x))} ↔ y ∈ {y | p (dist y x)}
[PROOFSTEP]
simp [hf.dist_eq]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
h : α ≃ᵢ β
⊢ EMetric.diam univ = EMetric.diam univ
[PROOFSTEP]
rw [← h.range_eq_univ, h.isometry.ediam_range]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
h : α ≃ᵢ β
s : Set β
⊢ EMetric.diam (↑h ⁻¹' s) = EMetric.diam s
[PROOFSTEP]
rw [← image_symm, ediam_image]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
⊢ ↑h ⁻¹' EMetric.ball x r = EMetric.ball (↑(IsometryEquiv.symm h) x) r
[PROOFSTEP]
rw [← h.isometry.preimage_emetric_ball (h.symm x) r, h.apply_symm_apply]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
⊢ ↑h ⁻¹' EMetric.closedBall x r = EMetric.closedBall (↑(IsometryEquiv.symm h) x) r
[PROOFSTEP]
rw [← h.isometry.preimage_emetric_closedBall (h.symm x) r, h.apply_symm_apply]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
h : α ≃ᵢ β
x : α
r : ℝ≥0∞
⊢ ↑h '' EMetric.ball x r = EMetric.ball (↑h x) r
[PROOFSTEP]
rw [← h.preimage_symm, h.symm.preimage_emetric_ball, symm_symm]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
h : α ≃ᵢ β
x : α
r : ℝ≥0∞
⊢ ↑h '' EMetric.closedBall x r = EMetric.closedBall (↑h x) r
[PROOFSTEP]
rw [← h.preimage_symm, h.symm.preimage_emetric_closedBall, symm_symm]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
e : α ≃ᵢ β
⊢ CompleteSpace α ↔ CompleteSpace β
[PROOFSTEP]
simp only [completeSpace_iff_isComplete_univ, ← e.range_eq_univ, ← image_univ,
  isComplete_image_iff e.isometry.uniformInducing]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝⁴ : PseudoEMetricSpace α
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
inst✝¹ : Unique ι
inst✝ : Fintype ι
x hx : ι → α
⊢ edist (Equiv.toFun (Equiv.funUnique ι α) x) (Equiv.toFun (Equiv.funUnique ι α) hx) = edist x hx
[PROOFSTEP]
simp [edist_pi_def, Finset.univ_unique, Finset.sup_singleton]
[GOAL]
ι : Type u_1
α✝ : Type u
β : Type v
γ : Type w
inst✝³ : PseudoEMetricSpace α✝
inst✝² : PseudoEMetricSpace β
inst✝¹ : PseudoEMetricSpace γ
α : Fin 2 → Type u_2
inst✝ : (i : Fin 2) → PseudoEMetricSpace (α i)
x hx : (i : Fin 2) → α i
⊢ edist (Equiv.toFun (piFinTwoEquiv α) x) (Equiv.toFun (piFinTwoEquiv α) hx) = edist x hx
[PROOFSTEP]
simp [edist_pi_def, Fin.univ_succ, Prod.edist_eq]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
s : Set β
⊢ Metric.diam (↑h ⁻¹' s) = Metric.diam s
[PROOFSTEP]
rw [← image_symm, diam_image]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h✝ h : α ≃ᵢ β
x : β
r : ℝ
⊢ ↑h ⁻¹' Metric.ball x r = Metric.ball (↑(IsometryEquiv.symm h) x) r
[PROOFSTEP]
rw [← h.isometry.preimage_ball (h.symm x) r, h.apply_symm_apply]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h✝ h : α ≃ᵢ β
x : β
r : ℝ
⊢ ↑h ⁻¹' Metric.sphere x r = Metric.sphere (↑(IsometryEquiv.symm h) x) r
[PROOFSTEP]
rw [← h.isometry.preimage_sphere (h.symm x) r, h.apply_symm_apply]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h✝ h : α ≃ᵢ β
x : β
r : ℝ
⊢ ↑h ⁻¹' Metric.closedBall x r = Metric.closedBall (↑(IsometryEquiv.symm h) x) r
[PROOFSTEP]
rw [← h.isometry.preimage_closedBall (h.symm x) r, h.apply_symm_apply]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h✝ h : α ≃ᵢ β
x : α
r : ℝ
⊢ ↑h '' Metric.ball x r = Metric.ball (↑h x) r
[PROOFSTEP]
rw [← h.preimage_symm, h.symm.preimage_ball, symm_symm]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h✝ h : α ≃ᵢ β
x : α
r : ℝ
⊢ ↑h '' Metric.sphere x r = Metric.sphere (↑h x) r
[PROOFSTEP]
rw [← h.preimage_symm, h.symm.preimage_sphere, symm_symm]
[GOAL]
ι : Type u_1
α : Type u
β : Type v
γ : Type w
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h✝ h : α ≃ᵢ β
x : α
r : ℝ
⊢ ↑h '' Metric.closedBall x r = Metric.closedBall (↑h x) r
[PROOFSTEP]
rw [← h.preimage_symm, h.symm.preimage_closedBall, symm_symm]