awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
h : IsUniformInducing f
⊢ IsInducing f
have obtain : ∀ (h : IsUniformInducing f), IsInducing f
Tactic: obtain rfl := h.comap_uniformSpace
Cleared hypotheses: inst, h
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
⊢ IsUniformEmbedding f ↔ Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
have rw : IsUniformInducing f ∧ Injective f ↔ Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
Tactic: rw [isUniformEmbedding_iff, and_comm, isUniformInducing_iff']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
rw : IsUniformInducing f ∧ Injective f ↔ Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
⊢ IsUniformEmbedding f ↔ Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
have rw₁ : Injective f ∧ IsUniformInducing f ↔ Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
Tactic: rw [isUniformEmbedding_iff, and_comm, isUniformInducing_iff']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
rw : IsUniformInducing f ∧ Injective f ↔ Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
rw₁ : Injective f ∧ IsUniformInducing f ↔ Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
⊢ IsUniformEmbedding f ↔ Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
have rw₂ : Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α ↔
  Injective f ∧ UniformContinuous f ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
Tactic: rw [isUniformEmbedding_iff, and_comm, isUniformInducing_iff']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
p' : ι' → Prop
s : ι → Set (α × α)
s' : ι' → Set (β × β)
h : (𝓤 α).HasBasis p s
h' : (𝓤 β).HasBasis p' s'
f : α → β
⊢ IsUniformEmbedding 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
have rw : IsUniformInducing f ∧ Injective 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
Tactic: rw [isUniformEmbedding_iff, and_comm, h.isUniformInducing_iff h']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
p' : ι' → Prop
s : ι → Set (α × α)
s' : ι' → Set (β × β)
h : (𝓤 α).HasBasis p s
h' : (𝓤 β).HasBasis p' s'
f : α → β
rw :
  IsUniformInducing f ∧ Injective 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
⊢ IsUniformEmbedding 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
have rw₁ : Injective f ∧ IsUniformInducing 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
Tactic: rw [isUniformEmbedding_iff, and_comm, h.isUniformInducing_iff h']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
p' : ι' → Prop
s : ι → Set (α × α)
s' : ι' → Set (β × β)
h : (𝓤 α).HasBasis p s
h' : (𝓤 β).HasBasis p' s'
f : α → β
rw :
  IsUniformInducing f ∧ Injective 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
rw₁ :
  Injective f ∧ IsUniformInducing 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
⊢ IsUniformEmbedding 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
have rw₂ : (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) ↔
  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
Tactic: rw [isUniformEmbedding_iff, and_comm, h.isUniformInducing_iff h']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
inst : UniformSpace α
s t : Set α
hst : s ⊆ t
⊢ Eq.{u + 1} (α := Filter ((↑s : Type u) × (↑s : Type u)))
    (comap (β := (↑t : Type u) × (↑t : Type u))
      (fun (x : (↑s : Type u) × (↑s : Type u)) ↦
        (inclusion (s := s) (t := t) hst x.1, inclusion (s := s) (t := t) hst x.2))
      (𝓤 (↑t : Type u)))
    (𝓤 (↑s : Type u))
have rw : Eq (α := Filter ((↑s : Type u) × (↑s : Type u)))
  (comap
    ((fun (q : { x : α // x ∈ t } × { x : α // x ∈ t }) ↦ ((↑q.1 : α), (↑q.2 : α))) ∘
      fun (x : (↑s : Type u) × (↑s : Type u)) ↦
      (inclusion (s := s) (t := t) hst x.1, inclusion (s := s) (t := t) hst x.2))
    (𝓤 α))
  (comap (fun (q : { x : α // x ∈ s } × { x : α // x ∈ s }) ↦ ((↑q.1 : α), (↑q.2 : α))) (𝓤 α))
Tactic: rw [uniformity_subtype, uniformity_subtype, comap_comap]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
g : β → γ
hg : IsUniformEmbedding g
f : α → β
⊢ IsUniformEmbedding (g ∘ f) ↔ IsUniformEmbedding f
have simp_rw : IsUniformInducing (g ∘ f) ∧ Injective (g ∘ f) ↔ IsUniformInducing f ∧ Injective f
Tactic: simp_rw [isUniformEmbedding_iff, hg.isUniformInducing.of_comp_iff, hg.injective.of_comp_iff f]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
g : β → γ
hg : IsUniformEmbedding g
f : α → β
simp_rw : IsUniformInducing (g ∘ f) ∧ Injective (g ∘ f) ↔ IsUniformInducing f ∧ Injective f
⊢ IsUniformEmbedding (g ∘ f) ↔ IsUniformEmbedding f
have simp_rw₁ : IsUniformInducing f ∧ Injective (g ∘ f) ↔ IsUniformInducing f ∧ Injective f
Tactic: simp_rw [isUniformEmbedding_iff, hg.isUniformInducing.of_comp_iff, hg.injective.of_comp_iff f]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α ≃ β
h₁ : UniformContinuous.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)
h₂ : UniformContinuous.{u_2, u_1} (α := β) (β := α) (⇑f.symm : (a : β) → α)
⊢ comap (Prod.map (⇑f : (a : α) → β) (⇑f : (a : α) → β)) (𝓤 β) ≤ 𝓤 α
have rwa : comap (⇑(f.prodCongr f) : (a : α × α) → β × β) (𝓤 β) ≤ 𝓤 α
Tactic: rwa [← Equiv.prodCongr_apply, ← map_equiv_symm]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α ≃ β
h₁ : UniformContinuous.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)
h₂ : UniformContinuous.{u_2, u_1} (α := β) (β := α) (⇑f.symm : (a : β) → α)
rwa : comap (⇑(f.prodCongr f) : (a : α × α) → β × β) (𝓤 β) ≤ 𝓤 α
⊢ comap (Prod.map (⇑f : (a : α) → β) (⇑f : (a : α) → β)) (𝓤 β) ≤ 𝓤 α
have rwa₁ : map (⇑(f.prodCongr f).symm : (a : β × β) → α × α) (𝓤 β) ≤ 𝓤 α
Tactic: rwa [← Equiv.prodCongr_apply, ← map_equiv_symm]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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
have refine : comap (Prod.map f f) (𝓤 β) ≤ 𝓟 SetRel.id
Tactic: refine le_antisymm ?_ (@refl_le_uniformity α (UniformSpace.comap f _))
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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
have comap : Prod.map f f ⁻¹' s ⊆ 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 ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (hypothesis)
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 α := ⊥
⊢ IsUniformEmbedding f
have this : DiscreteTopology α
Tactic: have := discreteTopology_bot α
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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
⊢ IsClosedEmbedding f
have rcases : ∀ [DiscreteTopology α], IsClosedEmbedding f
Tactic: rcases @DiscreteTopology.eq_bot α _ _ with rfl
Cleared hypotheses: inst_1, inst_2
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs : s ∈ 𝓤 α
⊢ ∃ (U : Set (β × β)), (U ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] U ∧ SetRel.IsSymm U) ∧ Prod.map e e ⁻¹' U ⊆ s
have 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
Tactic: rwa [← he₁.comap_uniformity, (uniformity_hasBasis_open_symmetric.comap _).mem_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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
⊢ ∃ (U : Set (β × β)), (U ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] U ∧ SetRel.IsSymm U) ∧ Prod.map e e ⁻¹' U ⊆ s
have 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
Tactic: rwa [← he₁.comap_uniformity, (uniformity_hasBasis_open_symmetric.comap _).mem_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set (α × α)
e : α → β
b : β
he₁ : IsUniformInducing e
he₂ : IsDenseInducing e
hs : s ∈ 𝓤 α
⊢ ∃ (a : α), closure[inst_1.toTopologicalSpace] (e '' {a' : α | (a, a') ∈ s}) ∈ 𝓝 b
have 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
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
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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 : α), closure[inst_1.toTopologicalSpace] (e '' {a' : α | (a, a') ∈ s}) ∈ 𝓝 b
have rcases : ∀ (a : α) (ha : e a ∈ UniformSpace.ball b U),
  ∃ (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⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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
have refine : closure[inst_1.toTopologicalSpace] (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)) ∈ 𝓝 b
Tactic: refine ⟨a, mem_of_superset ?_ (closure_mono <| image_mono <| UniformSpace.ball_mono hs a)⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (hypothesis)
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
⊢ closure[inst_1.toTopologicalSpace] (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)) ∈ 𝓝 b
have ho : IsOpen[inst_1.toTopologicalSpace] (UniformSpace.ball (e a) U)
Tactic: have ho : IsOpen (UniformSpace.ball (e a) U) := UniformSpace.isOpen_ball (e a) hUo
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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
have refine : ∀ (y : β) (hy : y ∈ UniformSpace.ball (e a) U),
  y ∈ closure[inst_1.toTopologicalSpace] (e '' UniformSpace.ball a (Prod.map e e ⁻¹' U))
Tactic: refine mem_of_superset (ho.mem_nhds <| UniformSpace.mem_ball_symmetry.2 ha) fun y hy => ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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))
have refine : ∀ (V : Set β) (hV : V ∈ 𝓝 y), (V ∩ e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)).Nonempty
Tactic: refine mem_closure_iff_nhds.2 fun V hV => ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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
⊢ (V ∩ e '' UniformSpace.ball a (Prod.map e e ⁻¹' U)).Nonempty
have 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
Tactic: rcases he₂.dense.mem_nhds (inter_mem hV (ho.mem_nhds hy)) with ⟨x, hxV, hxU⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (hypothesis)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
⊢ IsComplete (m '' s) ↔ IsComplete s
have fact1 : SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
Tactic: have fact1 : SurjOn (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 <| m '' s) := surjOn_image .. |>.filter_map_Iic
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (hypothesis)
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)))
⊢ IsComplete (m '' s) ↔ IsComplete s
have fact2 : MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
Tactic: have fact2 : MapsTo (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 <| m '' s) := mapsTo_image .. |>.filter_map_Iic
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)))
⊢ IsComplete (m '' s) ↔ IsComplete s
have simp_rw : (∀ (f : Filter β), Cauchy f → f ≤ 𝓟 (m '' s) → ∃ x ∈ m '' s, f ≤ 𝓝 x) ↔
  ∀ (f : Filter α), Cauchy f → f ≤ 𝓟 s → ∃ x ∈ s, f ≤ 𝓝 x
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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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
⊢ IsComplete (m '' s) ↔ IsComplete s
have simp_rw₁ : (∀ f ≤ 𝓟 (m '' s), Cauchy f → ∃ x ∈ m '' s, f ≤ 𝓝 x) ↔ ∀ f ≤ 𝓟 s, Cauchy f → ∃ x ∈ s, f ≤ 𝓝 x
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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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
⊢ IsComplete (m '' s) ↔ IsComplete s
have simp_rw₂ : (∀ f ∈ Iic (𝓟 (m '' s)), Cauchy f → ∃ x ∈ m '' s, f ≤ 𝓝 x) ↔ ∀ f ∈ Iic (𝓟 s), Cauchy f → ∃ x ∈ s, f ≤ 𝓝 x
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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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
⊢ IsComplete (m '' s) ↔ IsComplete s
have 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
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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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
⊢ IsComplete (m '' s) ↔ IsComplete s
have 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
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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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
⊢ IsComplete (m '' s) ↔ IsComplete s
have 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
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]