awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : T0Space α
f : α → β
hf : IsUniformInducing f
⊢ IsUniformEmbedding f

Tactic:
⟨hf, hf.isInducing.injective⟩

Premises used: IsUniformInducing.isInducing, Topology.IsInducing.injective, IsUniformEmbedding.mk
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : T0Space α
f : α → β
⊢ IsUniformEmbedding f ↔ IsUniformInducing f

Tactic:
⟨IsUniformEmbedding.isUniformInducing, IsUniformInducing.isUniformEmbedding⟩

Premises used: IsUniformEmbedding.isUniformInducing, Iff.intro, IsUniformInducing.isUniformEmbedding
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
β : Type v
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) (𝓤 β) = 𝓟 SetRel.id

Tactic:
le_antisymm ?_ (@refl_le_uniformity α (UniformSpace.comap f _))

Premises used: le_antisymm, refl_le_uniformity
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
β : Type v
inst : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun (x y : α) ↦ (f x, f y) ∉ s
refine : comap (Prod.map f f) (𝓤 β) ≤ 𝓟 SetRel.id
⊢ comap (Prod.map f f) (𝓤 β) = 𝓟 SetRel.id

Tactic:
refine le_antisymm ?_ (@refl_le_uniformity α (UniformSpace.comap f _))

Premises used: le_antisymm, refl_le_uniformity
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
β : Type v
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) (𝓤 β) ≤ comap (Prod.map f f) (𝓟 s)

Tactic:
comap_mono (le_principal_iff.2 hs)

Premises used: Iff.mpr, Filter.le_principal_iff, Filter.comap_mono
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
β : Type v
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) (𝓟 s) = 𝓟 (Prod.map f f ⁻¹' s)

Tactic:
comap_principal

Premises used: Filter.comap_principal
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
β : Type v
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) ≤ 𝓟 SetRel.id

Tactic:
principal_mono.2 ?_

Premises used: Iff.mpr, Filter.principal_mono
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
β : Type v
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 ⁻¹' s ⊆ SetRel.id
⊢ Filter.comap (Prod.map f f) (𝓤 β) ≤ 𝓟 SetRel.id

Tactic:
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
    _ ≤ 𝓟 SetRel.id := principal_mono.2 ?_

Premises used: Iff.mpr, SetRel.id, Filter.le_principal_iff, Filter.principal_mono, uniformity, Filter.comap_mono, Prod.map, Set.preimage, Filter.comap_principal, Filter.principal, Filter.comap
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
β : Type v
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 → Membership.mem (γ := Set (α × α)) SetRel.id (x, y)

Tactic:
simpa [not_imp_not] using @hf x y

Premises used: not_imp_not
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
β : Type v
inst : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun (x y : α) ↦ (f x, f y) ∉ s
x : UniformSpace α := ⊥
⊢ DiscreteTopology α

Tactic:
have := discreteTopology_bot α
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
β : Type v
inst : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun (x y : α) ↦ (f x, f y) ∉ s
x : UniformSpace α := ⊥
this : DiscreteTopology α
⊢ IsUniformEmbedding f

Tactic:
IsUniformInducing.isUniformEmbedding ⟨comap_uniformity_of_spaced_out hs hf⟩

Premises used: IsUniformInducing.mk, IsUniformInducing.isUniformEmbedding, comap_uniformity_of_spaced_out
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
β : Type v
inst : UniformSpace β
α : Type u_1
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun (x y : α) ↦ (f x, f y) ∉ s
x : UniformSpace α := ⊥
this : DiscreteTopology α
⊢ IsUniformEmbedding f

Tactic:
exact IsUniformInducing.isUniformEmbedding ⟨comap_uniformity_of_spaced_out hs hf⟩

Premises used: IsUniformInducing.mk, IsUniformInducing.isUniformEmbedding, comap_uniformity_of_spaced_out
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
h : IsUniformEmbedding f
hd : DenseRange f
⊢ IsDenseEmbedding f

Tactic:
{ h.isEmbedding with dense := hd }

Premises used: IsDenseEmbedding.mk, IsDenseInducing.mk, Topology.IsEmbedding.injective, Topology.IsEmbedding.toIsInducing, IsUniformEmbedding.isEmbedding
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
β : Type v
inst : UniformSpace β
α : Type u_1
inst_1 : TopologicalSpace α
inst_2 : DiscreteTopology α
inst_3 : T0Space β
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun (x y : α) ↦ (f x, f y) ∉ s
rcases : ∀ [DiscreteTopology α], IsClosedEmbedding f
⊢ IsClosedEmbedding f

Tactic:
rcases @DiscreteTopology.eq_bot α _ _ with rfl

Premises used: DiscreteTopology.eq_bot, rfl
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
β : Type v
inst : UniformSpace β
α : Type u_1
inst_1 : T0Space β
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun (x y : α) ↦ (f x, f y) ∉ s
inst_2 : DiscreteTopology α
x : UniformSpace α := ⊥
⊢ IsClosedEmbedding f

Tactic:
{ (isUniformEmbedding_of_spaced_out hs hf).isEmbedding with
      isClosed_range := isClosed_range_of_spaced_out hs hf }

Premises used: isUniformEmbedding_of_spaced_out, isClosed_range_of_spaced_out, IsUniformEmbedding.isEmbedding, Topology.IsClosedEmbedding.mk
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
β : Type v
inst : UniformSpace β
α : Type u_1
inst_1 : T0Space β
f : α → β
s : Set (β × β)
hs : s ∈ 𝓤 β
hf : Pairwise fun (x y : α) ↦ (f x, f y) ∉ s
inst_2 : DiscreteTopology α
x : UniformSpace α := ⊥
⊢ IsClosedEmbedding f

Tactic:
exact
    { (isUniformEmbedding_of_spaced_out hs hf).isEmbedding with
      isClosed_range := isClosed_range_of_spaced_out hs hf }

Premises used: isUniformEmbedding_of_spaced_out, IsUniformEmbedding.isEmbedding
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs : s ∈ 𝓤 α
rwa :
  ∀ (hs : Membership.mem (γ := Filter (α × α)) (comap (fun (x : α × α) ↦ (e x.1, e x.2)) (𝓤 β)) s),
    ∃ (U : Set (β × β)), (U ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] U ∧ SetRel.IsSymm U) ∧ Prod.map e e ⁻¹' U ⊆ s
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (hs :
      ∃ (i : SetRel β β),
        (i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i ∧ i.IsSymm) ∧ (fun (x : α × α) ↦ (e x.1, e x.2)) ⁻¹' id i ⊆ s),
    ∃ (U : Set (β × β)), (U ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] U ∧ SetRel.IsSymm U) ∧ Prod.map e e ⁻¹' U ⊆ s
⊢ ∃ (U : Set (β × β)), (U ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] U ∧ SetRel.IsSymm U) ∧ Prod.map e e ⁻¹' U ⊆ s

Tactic:
rwa [← he₁.comap_uniformity, (uniformity_hasBasis_open_symmetric.comap _).mem_iff] at hs

Premises used: IsUniformInducing.comap_uniformity, Filter.HasBasis.mem_iff, Filter.HasBasis.comap, uniformity_hasBasis_open_symmetric
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs : s ∈ 𝓤 α
obtain :
  ∀ (U : Set (β × β)) (hs : Prod.map e e ⁻¹' U ⊆ s) (hU : U ∈ 𝓤 β) (hUo : IsOpen[instTopologicalSpaceProd] U)
    (hsymm : SetRel.IsSymm U), ∃ (a : α), closure[inst_1.toTopologicalSpace] (e '' {a' : α | (a, a') ∈ s}) ∈ 𝓝 b
⊢ ∃ (a : α), closure[inst_1.toTopologicalSpace] (e '' {a' : α | (a, a') ∈ s}) ∈ 𝓝 b

Tactic:
obtain ⟨U, ⟨hU, hUo, hsymm⟩, hs⟩ :
    ∃ U, (U ∈ 𝓤 β ∧ IsOpen U ∧ SetRel.IsSymm U) ∧ Prod.map e e ⁻¹' U ⊆ s := by
      rwa [← he₁.comap_uniformity, (uniformity_hasBasis_open_symmetric.comap _).mem_iff] at hs

Premises used: Prod.map
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs_1 : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen[instTopologicalSpaceProd] U
hsymm : SetRel.IsSymm U
rcases :
  ∀ (a : α) (ha : e a ∈ UniformSpace.ball b U),
    ∃ (a : α), closure[inst_1.toTopologicalSpace] (e '' {a' : α | (a, a') ∈ s}) ∈ 𝓝 b
⊢ ∃ (a : α), closure[inst_1.toTopologicalSpace] (e '' {a' : α | (a, a') ∈ s}) ∈ 𝓝 b

Tactic:
rcases he₂.dense.mem_nhds (UniformSpace.ball_mem_nhds b hU) with ⟨a, ha⟩

Premises used: UniformSpace.ball_mem_nhds, IsDenseInducing.dense, DenseRange.mem_nhds
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs_1 : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen[instTopologicalSpaceProd] U
hsymm : SetRel.IsSymm U
a : α
ha : e a ∈ UniformSpace.ball b U
⊢ ∃ (a : α), closure[inst_1.toTopologicalSpace] (e '' {a' : α | (a, a') ∈ s}) ∈ 𝓝 b

Tactic:
⟨a, mem_of_superset ?_ (closure_mono <| image_mono <| UniformSpace.ball_mono hs a)⟩

Premises used: Set.image_mono, UniformSpace.ball_mono, closure_mono, Exists.intro, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs_1 : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen[instTopologicalSpaceProd] U
hsymm : SetRel.IsSymm U
a : α
ha : e a ∈ UniformSpace.ball b U
refine : closure[inst_1.toTopologicalSpace] (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)) ∈ 𝓝 b
⊢ ∃ (a : α), closure[inst_1.toTopologicalSpace] (e '' {a' : α | (a, a') ∈ s}) ∈ 𝓝 b

Tactic:
refine ⟨a, mem_of_superset ?_ (closure_mono <| image_mono <| UniformSpace.ball_mono hs a)⟩
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs_1 : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen[instTopologicalSpaceProd] U
hsymm : SetRel.IsSymm U
a : α
ha : e a ∈ UniformSpace.ball b U
⊢ IsOpen[inst_1.toTopologicalSpace] (UniformSpace.ball (e a) U)

Tactic:
have ho : IsOpen (UniformSpace.ball (e a) U) := UniformSpace.isOpen_ball (e a) hUo
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs_1 : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen[instTopologicalSpaceProd] U
hsymm : SetRel.IsSymm U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen[inst_1.toTopologicalSpace] (UniformSpace.ball (e a) U)
⊢ closure[inst_1.toTopologicalSpace] (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)) ∈ 𝓝 b

Tactic:
mem_of_superset (ho.mem_nhds <| UniformSpace.mem_ball_symmetry.2 ha) fun y hy => ?_

Premises used: Iff.mpr, UniformSpace.mem_ball_symmetry, IsOpen.mem_nhds, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs_1 : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen[instTopologicalSpaceProd] U
hsymm : SetRel.IsSymm U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen[inst_1.toTopologicalSpace] (UniformSpace.ball (e a) U)
refine :
  ∀ (y : β) (hy : y ∈ UniformSpace.ball (e a) U),
    y ∈ closure[inst_1.toTopologicalSpace] (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U))
⊢ closure[inst_1.toTopologicalSpace] (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)) ∈ 𝓝 b

Tactic:
refine mem_of_superset (ho.mem_nhds <| UniformSpace.mem_ball_symmetry.2 ha) fun y hy => ?_

Premises used: Iff.mpr, UniformSpace.mem_ball_symmetry, IsOpen.mem_nhds, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs_1 : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen[instTopologicalSpaceProd] U
hsymm : SetRel.IsSymm U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen[inst_1.toTopologicalSpace] (UniformSpace.ball (e a) U)
y : β
hy : y ∈ UniformSpace.ball (e a) U
⊢ y ∈ closure[inst_1.toTopologicalSpace] (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U))

Tactic:
mem_closure_iff_nhds.2 fun V hV => ?_

Premises used: Iff.mpr, mem_closure_iff_nhds
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs_1 : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen[instTopologicalSpaceProd] U
hsymm : SetRel.IsSymm U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen[inst_1.toTopologicalSpace] (UniformSpace.ball (e a) U)
y : β
hy : y ∈ UniformSpace.ball (e a) U
refine : ∀ (V : Set β) (hV : V ∈ 𝓝 y), (V ∩ e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)).Nonempty
⊢ y ∈ closure[inst_1.toTopologicalSpace] (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U))

Tactic:
refine mem_closure_iff_nhds.2 fun V hV => ?_

Premises used: Iff.mpr, mem_closure_iff_nhds
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs_1 : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen[instTopologicalSpaceProd] U
hsymm : SetRel.IsSymm U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen[inst_1.toTopologicalSpace] (UniformSpace.ball (e a) U)
y : β
hy : y ∈ UniformSpace.ball (e a) U
V : Set β
hV : V ∈ 𝓝 y
rcases :
  ∀ (x : α) (hxV : e x ∈ V) (hxU : e x ∈ UniformSpace.ball (e a) U),
    (V ∩ e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)).Nonempty
⊢ (V ∩ e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)).Nonempty

Tactic:
rcases he₂.dense.mem_nhds (inter_mem hV (ho.mem_nhds hy)) with ⟨x, hxV, hxU⟩

Premises used: Filter.inter_mem, IsDenseInducing.dense, IsOpen.mem_nhds, DenseRange.mem_nhds
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs_1 : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen[instTopologicalSpaceProd] U
hsymm : SetRel.IsSymm U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen[inst_1.toTopologicalSpace] (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
⊢ (V ∩ e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)).Nonempty

Tactic:
⟨e x, hxV, mem_image_of_mem e hxU⟩

Premises used: Set.Nonempty, Set.mem_image_of_mem, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs_1 : s ∈ 𝓤 α
U : Set (β × β)
hs : Prod.map e e ⁻¹' U ⊆ s
hU : U ∈ 𝓤 β
hUo : IsOpen[instTopologicalSpaceProd] U
hsymm : SetRel.IsSymm U
a : α
ha : e a ∈ UniformSpace.ball b U
ho : IsOpen[inst_1.toTopologicalSpace] (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
⊢ (V ∩ e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)).Nonempty

Tactic:
exact ⟨e x, hxV, mem_image_of_mem e hxU⟩
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
p : α → Prop
e : α → β
ue : IsUniformEmbedding e
de : IsDenseEmbedding e
⊢ Eq.{u + 1} (α := Filter ({ x : α // p x } × { x : α // p x }))
    (comap.{u, v} (β :=
      { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) } ×
        { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) })
      (fun (x : { x : α // p x } × { x : α // p x }) ↦
        (IsDenseEmbedding.subtypeEmb p e x.1, IsDenseEmbedding.subtypeEmb p e x.2))
      (𝓤 { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) }))
    (𝓤 { x : α // p x })

Tactic:
simp [comap_comap, Function.comp_def, IsDenseEmbedding.subtypeEmb, uniformity_subtype,
        ue.comap_uniformity.symm]

Premises used: IsUniformInducing.comap_uniformity, IsUniformEmbedding.toIsUniformInducing, Function.comp_def, Filter.comap_comap, uniformity_subtype, Eq.symm, IsDenseEmbedding.subtypeEmb
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
⊢ SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))

Tactic:
have fact1 : SurjOn (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 <| m '' s) := surjOn_image .. |>.filter_map_Iic
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
fact1 : SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
⊢ MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))

Tactic:
have fact2 : MapsTo (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 <| m '' s) := mapsTo_image .. |>.filter_map_Iic
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
fact1 : SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
fact2 : MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
simp_rw :
  (∀ (f : Filter β), Cauchy f → f ≤ 𝓟 (m '' s) → ∃ x ∈ m '' s, f ≤ 𝓝 x) ↔
    ∀ (f : Filter α), Cauchy f → f ≤ 𝓟 s → ∃ x ∈ s, f ≤ 𝓝 x
simp_rw₁ : (∀ f ≤ 𝓟 (m '' s), Cauchy f → ∃ x ∈ m '' s, f ≤ 𝓝 x) ↔ ∀ f ≤ 𝓟 s, Cauchy f → ∃ x ∈ s, f ≤ 𝓝 x
simp_rw₂ : (∀ f ∈ Iic (𝓟 (m '' s)), Cauchy f → ∃ x ∈ m '' s, f ≤ 𝓝 x) ↔ ∀ f ∈ Iic (𝓟 s), Cauchy f → ∃ x ∈ s, f ≤ 𝓝 x
simp_rw₃ :
  (∀ x ∈ Iic (𝓟 s), Cauchy (map m x) → ∃ x_1 ∈ m '' s, map m x ≤ 𝓝 x_1) ↔ ∀ f ∈ Iic (𝓟 s), Cauchy f → ∃ x ∈ s, f ≤ 𝓝 x
simp_rw₄ : (∀ x ∈ Iic (𝓟 s), Cauchy x → ∃ x_1 ∈ m '' s, map m x ≤ 𝓝 x_1) ↔ ∀ f ∈ Iic (𝓟 s), Cauchy f → ∃ x ∈ s, f ≤ 𝓝 x
simp_rw₅ : (∀ x ∈ Iic (𝓟 s), Cauchy x → ∃ x_1 ∈ s, map m x ≤ 𝓝 (m x_1)) ↔ ∀ f ∈ Iic (𝓟 s), Cauchy f → ∃ x ∈ s, f ≤ 𝓝 x
simp_rw₆ :
  (∀ x ∈ Iic (𝓟 s), Cauchy x → ∃ x_1 ∈ s, x ≤ comap m (𝓝 (m x_1))) ↔ ∀ f ∈ Iic (𝓟 s), Cauchy f → ∃ x ∈ s, f ≤ 𝓝 x
⊢ IsComplete (m '' s) ↔ IsComplete s

Tactic:
simp_rw [IsComplete, imp.swap (a := Cauchy _), ← mem_Iic (b := 𝓟 _), fact1.forall fact2,
    hm.cauchy_map_iff, exists_mem_image, map_le_iff_le_comap, hm.isInducing.nhds_eq_comap]

Premises used: Topology.IsInducing.nhds_eq_comap, IsComplete, IsUniformInducing.isInducing, Set.SurjOn.forall, Filter.map_le_iff_le_comap, Set.mem_Iic, Set.exists_mem_image, imp.swap, IsUniformInducing.cauchy_map_iff
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
hf : IsUniformInducing f
⊢ IsComplete (f '' s) ↔ IsComplete s

Tactic:
isComplete_image_iff hf

Premises used: isComplete_image_iff
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
hf : IsUniformEmbedding f
⊢ IsComplete (f '' s) ↔ IsComplete s

Tactic:
hf.isUniformInducing.isComplete_iff

Premises used: IsUniformEmbedding.isUniformInducing, IsUniformInducing.isComplete_iff
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
inst : UniformSpace α
p : α → Prop
s : Set { x : α // p x }
⊢ IsComplete s ↔ IsComplete (val (p := fun (x : α) ↦ p x) '' s)

Tactic:
isUniformEmbedding_subtype_val.isComplete_iff.symm

Premises used: IsUniformEmbedding.isComplete_iff, Iff.symm, isUniformEmbedding_subtype_val
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : IsUniformInducing f
rw : IsComplete.{u} (α := α) univ ↔ IsComplete (range f)
rw₁ : IsComplete (f '' univ) ↔ IsComplete (range f)
rw₂ rw₃ : IsComplete (range f) ↔ IsComplete (range f)
⊢ CompleteSpace α ↔ IsComplete (range f)

Tactic:
rw [completeSpace_iff_isComplete_univ, ← isComplete_image_iff hf, image_univ]

Premises used: Set.image_univ, completeSpace_iff_isComplete_univ, isComplete_image_iff
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace α
hf : IsUniformInducing f
⊢ IsComplete (range f)

Tactic:
(completeSpace_iff_isComplete_range hf).1 ‹_›

Premises used: Iff.mp, completeSpace_iff_isComplete_range
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : IsUniformInducing f
hsurj : Surjective f
rw : IsComplete (range f) ↔ CompleteSpace β
rw₁ : IsComplete.{v} (α := β) univ ↔ CompleteSpace β
rw₂ rw₃ : IsComplete.{v} (α := β) univ ↔ IsComplete.{v} (α := β) univ
⊢ CompleteSpace α ↔ CompleteSpace β

Tactic:
rw [completeSpace_iff_isComplete_range hf, hsurj.range_eq, completeSpace_iff_isComplete_univ]

Premises used: completeSpace_iff_isComplete_univ, Function.Surjective.range_eq, completeSpace_iff_isComplete_range
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
inst : UniformSpace α
⊢ CompleteSpace.{u} (SeparationQuotient α) ↔ CompleteSpace α

Tactic:
.symm <| isUniformInducing_mk.completeSpace_congr surjective_mk

Premises used: SeparationQuotient.isUniformInducing_mk, SeparationQuotient.surjective_mk, IsUniformInducing.completeSpace_congr, Iff.symm
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β
inst_3 : CompleteSpace α
⊢ CompleteSpace.{u} (SeparationQuotient α)

Tactic:
completeSpace_iff.2 ‹_›

Premises used: Iff.mpr, SeparationQuotient.completeSpace_iff
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
e : α ≃ β
he : IsUniformEmbedding.{u, v} (α := α) (β := β) (⇑e : (a : α) → β)
⊢ CompleteSpace α ↔ CompleteSpace β

Tactic:
he.completeSpace_congr e.surjective

Premises used: IsUniformEmbedding.toIsUniformInducing, Equiv.surjective, IsUniformInducing.completeSpace_congr
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
inst : UniformSpace α
s : Set α
rw : IsComplete.{u} (α := α) (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) ↔ IsComplete s
rw₁ rw₂ : IsComplete s ↔ IsComplete s
⊢ CompleteSpace.{u} (↑s : Type u) ↔ IsComplete s

Tactic:
rw [completeSpace_iff_isComplete_range isUniformEmbedding_subtype_val.isUniformInducing,
    Subtype.range_coe]

Premises used: IsUniformEmbedding.isUniformInducing, Subtype.range_coe, completeSpace_iff_isComplete_range, isUniformEmbedding_subtype_val