awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β
inst_3 : CompleteSpace α
s : Set α
hs : IsClosed[inst.toTopologicalSpace] s
⊢ CompleteSpace.{u} (↑s : Type u)

Tactic:
hs.isComplete.completeSpace_coe

Premises used: IsComplete.completeSpace_coe, IsClosed.isComplete
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
inst : UniformSpace α
⊢ CompleteSpace (ULift.{u_1, u} α) ↔ CompleteSpace α

Tactic:
IsUniformInducing.completeSpace_congr ⟨rfl⟩ ULift.down_surjective

Premises used: ULift.down_surjective, IsUniformInducing.mk, IsUniformInducing.completeSpace_congr, rfl
-- 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 (ULift.{u_1, u} α)

Tactic:
completeSpace_ulift_iff.2 ‹_›

Premises used: Iff.mpr, completeSpace_ulift_iff
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
m : β → α
hm : IsUniformInducing m
dense : DenseRange m
h : ∀ (f : Filter β), Cauchy f → ∃ (x : α), map m f ≤ 𝓝 x
f : Filter α
hf : Cauchy f
p : Set (α × α) → Set α → Set α := fun (s : Set (α × α)) (t : Set α) ↦ {y : α | ∃ x ∈ t, (x, y) ∈ s}
g : Filter α := (𝓤 α).lift fun (s : Set (α × α)) ↦ f.lift' (p s)
mp₀ : Monotone p
mp₁ : ∀ {s : Set (α × α)}, Monotone (p s)
this_1 : f ≤ g
this_2 : g.NeBot
this_3 : (comap m g).NeBot
this_4 : Cauchy g
this_5 : Cauchy (comap m g)
x : α
hx : map m (comap m g) ≤ 𝓝 x
this_6 : ClusterPt x (map m (comap m g))
this : ClusterPt x g
⊢ f ≤ g

Tactic:
assumption
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
⊢ (map f F).TotallyBounded ↔ F.TotallyBounded

Tactic:
⟨fun hs ↦ ?_, fun h ↦ h.map hf.uniformContinuous⟩

Premises used: Filter.TotallyBounded.map, Iff.intro, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
refine : ∀ (hs : (map f F).TotallyBounded), F.TotallyBounded
⊢ (map f F).TotallyBounded ↔ F.TotallyBounded

Tactic:
refine ⟨fun hs ↦ ?_, fun h ↦ h.map hf.uniformContinuous⟩
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
hs : (map f F).TotallyBounded
simp_rw : ∀ i ∈ 𝓤 β, ∃ (t : Set α), t.Finite ∧ SetRel.preimage (Prod.map f f ⁻¹' id i) t ∈ F
⊢ F.TotallyBounded

Tactic:
simp_rw [(hf.basis_uniformity (basis_sets _)).filter_totallyBounded_iff]

Premises used: Filter.HasBasis.filter_totallyBounded_iff, Filter.basis_sets, IsUniformInducing.basis_uniformity
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
hs : (map f F).TotallyBounded
t : Set (β × β)
ht : t ∈ 𝓤 β
rcases :
  ∀ (u : Set α) (hfin : u.Finite) (h : SetRel.preimage t (f '' u) ∈ map f F),
    ∃ (t_1 : Set α), t_1.Finite ∧ SetRel.preimage (Prod.map f f ⁻¹' id t) t_1 ∈ F
⊢ ∃ (t_1 : Set α), t_1.Finite ∧ SetRel.preimage (Prod.map f f ⁻¹' id t) t_1 ∈ F

Tactic:
rcases exists_subset_image_finite_and.1 (hs.exists_subset_of_mem (F.image_mem_map F.univ_mem) ht)
    with ⟨u, -, hfin, h⟩

Premises used: Filter.image_mem_map, Filter.TotallyBounded.exists_subset_of_mem, Iff.mp, Set.exists_subset_image_finite_and, Filter.univ_mem
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
hs : (map f F).TotallyBounded
t : Set (β × β)
ht : t ∈ 𝓤 β
u : Set α
hfin : u.Finite
h : SetRel.preimage t (f '' u) ∈ map f F
right : SetRel.preimage (Prod.map f f ⁻¹' id t) u ∈ F
⊢ ∃ (t_1 : Set α), t_1.Finite ∧ SetRel.preimage (Prod.map f f ⁻¹' id t) t_1 ∈ F

Tactic:
use u, hfin
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
hs : (map f F).TotallyBounded
t : Set (β × β)
ht : t ∈ 𝓤 β
u : Set α
hfin : u.Finite
h : SetRel.preimage t (f '' u) ∈ map f F
⊢ {a : β | ∃ x ∈ u, (a, f x) ∈ t} ∈ map f F

Tactic:
simp_rw [SetRel.preimage, exists_mem_image] at h

Premises used: Set.exists_mem_image, SetRel.preimage
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
hs : (map f F).TotallyBounded
t : Set (β × β)
ht : t ∈ 𝓤 β
u : Set α
hfin : u.Finite
h : {a : β | ∃ x ∈ u, (a, f x) ∈ t} ∈ map f F
⊢ SetRel.preimage (Prod.map f f ⁻¹' id t) u ∈ F

Tactic:
h

Premises used: Set.Mem, setOf, Prod.map, Set.preimage, SetRel.preimage
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
hs : (map f F).TotallyBounded
t : Set (β × β)
ht : t ∈ 𝓤 β
u : Set α
hfin : u.Finite
h : {a : β | ∃ x ∈ u, (a, f x) ∈ t} ∈ map f F
⊢ SetRel.preimage (Prod.map f f ⁻¹' id t) u ∈ F

Tactic:
exact h
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
hf : IsUniformInducing f
simp_rw : (𝓟 (f '' s)).TotallyBounded ↔ (𝓟 s).TotallyBounded
simp_rw₁ : (map f (𝓟 s)).TotallyBounded ↔ (𝓟 s).TotallyBounded
⊢ TotallyBounded (f '' s) ↔ TotallyBounded s

Tactic:
simp_rw [← totallyBounded_principal_iff, ← map_principal, totallyBounded_map_iff hf]

Premises used: Filter.totallyBounded_principal_iff, Filter.totallyBounded_map_iff, Filter.map_principal
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set β
hf : IsUniformInducing f
hs : TotallyBounded s
⊢ TotallyBounded (f ⁻¹' s)

Tactic:
(totallyBounded_image_iff hf).1 <| hs.subset <| image_preimage_subset ..

Premises used: TotallyBounded.subset, totallyBounded_image_iff, Set.image_preimage_subset, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
F : Filter β
hf : IsUniformInducing f
hF : F.TotallyBounded
⊢ (comap f F).TotallyBounded

Tactic:
(totallyBounded_map_iff hf).1 <| hF.mono map_comap_le

Premises used: Filter.TotallyBounded.mono, Iff.mp, Filter.totallyBounded_map_iff, Filter.map_comap_le
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β
inst_3 : CompleteSpace α
inst_4 : CompleteSpace β
rw : IsComplete (α := α ⊕ β) (range Sum.inl ∪ range Sum.inr)
⊢ CompleteSpace (α ⊕ β)

Tactic:
rw [completeSpace_iff_isComplete_univ, ← range_inl_union_range_inr]

Premises used: completeSpace_iff_isComplete_univ, Set.range_inl_union_range_inr
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β
inst_3 : CompleteSpace α
inst_4 : CompleteSpace β
⊢ IsComplete (α := α ⊕ β) (range Sum.inl ∪ range Sum.inr)

Tactic:
isUniformEmbedding_inl.isUniformInducing.isComplete_range.union
    isUniformEmbedding_inr.isUniformInducing.isComplete_range

Premises used: isUniformEmbedding_inl, IsComplete.union, IsUniformEmbedding.isUniformInducing, IsUniformInducing.isComplete_range, isUniformEmbedding_inr
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : α → β
inst_3 : CompleteSpace α
inst_4 : CompleteSpace β
⊢ IsComplete (α := α ⊕ β) (range Sum.inl ∪ range Sum.inr)

Tactic:
exact isUniformEmbedding_inl.isUniformInducing.isComplete_range.union
    isUniformEmbedding_inr.isUniformInducing.isComplete_range

Premises used: isUniformEmbedding_inl, IsComplete.union, IsUniformEmbedding.isUniformInducing, IsUniformInducing.isComplete_range, isUniformEmbedding_inr
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : DiscreteUniformity β
f : α → β
hf : IsUniformEmbedding f
simp_rw : 𝓤 α = 𝓟 SetRel.id
simp_rw₁ : Eq.{u + 1} (α := Filter (α × α)) (comap (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 β)) (𝓟 SetRel.id)
simp_rw₂ :
  Eq.{u + 1} (α := Filter (α × α)) (comap.{u, v} (β := β × β) (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓟 SetRel.id))
    (𝓟 SetRel.id)
simp_rw₃ :
  Eq.{u + 1} (α := Filter (α × α)) (𝓟 (preimage.{u, v} (β := β × β) (fun (x : α × α) ↦ (f x.1, f x.2)) SetRel.id))
    (𝓟 SetRel.id)
simp_rw₄ :
  Eq.{u + 1} (α := Filter (α × α))
    (𝓟 (preimage.{u, v} (β := β × β) (fun (x : α × α) ↦ (f x.1, f x.2)) {x : β × β | x.1 = x.2}))
    (𝓟 {x : α × α | x.1 = x.2})
simp_rw₅ : Eq.{u + 1} (α := Filter (α × α)) (𝓟 {a : α × α | f a.1 = f a.2}) (𝓟 {x : α × α | x.1 = x.2})
⊢ DiscreteUniformity α

Tactic:
simp_rw [discreteUniformity_iff_eq_principal_setRelId, ← hf.comap_uniformity,
    DiscreteUniformity.eq_principal_setRelId, comap_principal, SetRel.id, preimage_setOf_eq,
    hf.injective.eq_iff]

Premises used: IsUniformInducing.comap_uniformity, IsUniformEmbedding.injective, SetRel.id, Function.Injective.eq_iff, IsUniformEmbedding.toIsUniformInducing, discreteUniformity_iff_eq_principal_setRelId, Set.preimage_setOf_eq, DiscreteUniformity.eq_principal_setRelId, Filter.comap_principal
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
f : α → β
u : UniformSpace β
hf : Injective f
⊢ IsUniformEmbedding f

Tactic:
@IsUniformEmbedding.mk _ _ (UniformSpace.comap f u) _ _
    (@IsUniformInducing.mk _ _ (UniformSpace.comap f u) _ _ rfl) hf

Premises used: IsUniformEmbedding.mk, IsUniformInducing.mk, rfl
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
u : UniformSpace β
f : α → β
h : IsEmbedding f
⊢ IsUniformEmbedding f

Tactic:
let _ := h.comapUniformSpace f
  { comap_uniformity := rfl
    injective := h.injective }

Premises used: Topology.IsEmbedding.comapUniformSpace, IsUniformEmbedding.mk, IsUniformInducing.mk, Topology.IsEmbedding.injective, rfl
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
e : β → α
h_e : IsUniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst_3 : CompleteSpace γ
a : α
⊢ ∃ (c : γ), Tendsto f (comap e (𝓝 a)) (𝓝 c)

Tactic:
let de := h_e.isDenseInducing h_dense
  have : Cauchy (𝓝 a) := cauchy_nhds
  have : Cauchy (comap e (𝓝 a)) :=
    this.comap' (le_of_eq h_e.comap_uniformity) (de.comap_nhds_neBot _)
  have : Cauchy (map f (comap e (𝓝 a))) := this.map h_f
  CompleteSpace.complete this

Premises used: IsUniformInducing.comap_uniformity, IsDenseInducing.comap_nhds_neBot, Cauchy.comap', Cauchy.map, IsUniformInducing.isDenseInducing, Filter.Tendsto, CompleteSpace.complete, le_of_eq, cauchy_nhds
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous.{u_1, u_3} (β := γ) fun (x : Subtype p) ↦ f (↑x : α)
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst_1.toTopologicalSpace] (range e)
hb : closure[inst_1.toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
⊢ IsDenseEmbedding e

Tactic:
have de : IsDenseEmbedding e := he.isDenseEmbedding hd
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous.{u_1, u_3} (β := γ) fun (x : Subtype p) ↦ f (↑x : α)
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst_1.toTopologicalSpace] (range e)
hb : closure[inst_1.toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
de : IsDenseEmbedding e
⊢ IsDenseEmbedding (β := { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) })
    (IsDenseEmbedding.subtypeEmb p e)

Tactic:
have de' : IsDenseEmbedding (IsDenseEmbedding.subtypeEmb p e) := de.subtype p
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous.{u_1, u_3} (β := γ) fun (x : Subtype p) ↦ f (↑x : α)
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst_1.toTopologicalSpace] (range e)
hb : closure[inst_1.toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
de : IsDenseEmbedding e
de' :
  IsDenseEmbedding (β := { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) })
    (IsDenseEmbedding.subtypeEmb p e)
⊢ IsUniformEmbedding (β := { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) })
    (IsDenseEmbedding.subtypeEmb p e)

Tactic:
have ue' : IsUniformEmbedding (IsDenseEmbedding.subtypeEmb p e) :=
    isUniformEmbedding_subtypeEmb _ he de
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous.{u_1, u_3} (β := γ) fun (x : Subtype p) ↦ f (↑x : α)
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst_1.toTopologicalSpace] (range e)
hb : closure[inst_1.toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
de : IsDenseEmbedding e
de' :
  IsDenseEmbedding (β := { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) })
    (IsDenseEmbedding.subtypeEmb p e)
ue' :
  IsUniformEmbedding (β := { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) })
    (IsDenseEmbedding.subtypeEmb p e)
⊢ b ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x})

Tactic:
have : b ∈ closure (e '' { x | p x }) :=
    (closure_mono <| monotone_image <| hp) (mem_of_mem_nhds hb)
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous.{u_1, u_3} (β := γ) fun (x : Subtype p) ↦ f (↑x : α)
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst_1.toTopologicalSpace] (range e)
hb : closure[inst_1.toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
de : IsDenseEmbedding e
de' :
  IsDenseEmbedding (β := { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) })
    (IsDenseEmbedding.subtypeEmb p e)
ue' :
  IsUniformEmbedding (β := { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) })
    (IsDenseEmbedding.subtypeEmb p e)
this : b ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x})
let :
  ∀ (c : γ)
    (hc :
      Tendsto (fun (x : Subtype p) ↦ f (↑x : α))
        (comap (IsDenseEmbedding.subtypeEmb p e)
          (𝓝 (Subtype.mk (p := fun (x : β) ↦ x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x})) b this)))
        (𝓝 c)),
    ∃ (c : γ), Tendsto f (comap e (𝓝 b)) (𝓝 c)
⊢ ∃ (c : γ), Tendsto f (comap e (𝓝 b)) (𝓝 c)

Tactic:
let ⟨c, hc⟩ := uniformly_extend_exists ue'.isUniformInducing de'.dense hf ⟨b, this⟩
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous.{u_1, u_3} (β := γ) fun (x : Subtype p) ↦ f (↑x : α)
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst_1.toTopologicalSpace] (range e)
hb : closure[inst_1.toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
de : IsDenseEmbedding e
de' :
  IsDenseEmbedding (β := { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) })
    (IsDenseEmbedding.subtypeEmb p e)
ue' :
  IsUniformEmbedding (β := { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) })
    (IsDenseEmbedding.subtypeEmb p e)
this : b ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x})
c : γ
hc :
  Tendsto (fun (x : Subtype p) ↦ f (↑x : α))
    (comap (IsDenseEmbedding.subtypeEmb p e)
      (𝓝 (Subtype.mk (p := fun (x : β) ↦ x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x})) b this)))
    (𝓝 c)
⊢ Tendsto (α := Subtype p) (f ∘ Subtype.val (p := p)) (comap (Subtype.val (p := p)) (comap e (𝓝 b))) (𝓝 c)

Tactic:
simpa only [nhds_subtype_eq_comap, comap_comap, IsDenseEmbedding.subtypeEmb_coe] using hc

Premises used: IsDenseEmbedding.subtypeEmb_coe, nhds_subtype_eq_comap, Filter.comap_comap
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous.{u_1, u_3} (β := γ) fun (x : Subtype p) ↦ f (↑x : α)
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst_1.toTopologicalSpace] (range e)
hb : closure[inst_1.toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
de : IsDenseEmbedding e
de' :
  IsDenseEmbedding (β := { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) })
    (IsDenseEmbedding.subtypeEmb p e)
ue' :
  IsUniformEmbedding (β := { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) })
    (IsDenseEmbedding.subtypeEmb p e)
this : b ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x})
c : γ
hc :
  Tendsto (fun (x : Subtype p) ↦ f (↑x : α))
    (comap (IsDenseEmbedding.subtypeEmb p e)
      (𝓝 (Subtype.mk (p := fun (x : β) ↦ x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x})) b this)))
    (𝓝 c)
⊢ Tendsto (α := Subtype p) (f ∘ Subtype.val (p := p)) (comap (Subtype.val (p := p)) (comap e (𝓝 b))) (𝓝 c)

Tactic:
replace hc : Tendsto (f ∘ Subtype.val (p := p)) (((𝓝 b).comap e).comap Subtype.val) (𝓝 c) := by
    simpa only [nhds_subtype_eq_comap, comap_comap, IsDenseEmbedding.subtypeEmb_coe] using hc
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous.{u_1, u_3} (β := γ) fun (x : Subtype p) ↦ f (↑x : α)
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst_1.toTopologicalSpace] (range e)
hb : closure[inst_1.toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
de : IsDenseEmbedding e
de' :
  IsDenseEmbedding (β := { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) })
    (IsDenseEmbedding.subtypeEmb p e)
ue' :
  IsUniformEmbedding (β := { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) })
    (IsDenseEmbedding.subtypeEmb p e)
this : b ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x})
c : γ
hc : Tendsto (α := Subtype p) (f ∘ Subtype.val (p := p)) (comap (Subtype.val (p := p)) (comap e (𝓝 b))) (𝓝 c)
⊢ ∃ (c : γ), Tendsto f (comap e (𝓝 b)) (𝓝 c)

Tactic:
⟨c, (tendsto_comap'_iff ?_).1 hc⟩

Premises used: Filter.tendsto_comap'_iff, Exists.intro, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous.{u_1, u_3} (β := γ) fun (x : Subtype p) ↦ f (↑x : α)
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst_1.toTopologicalSpace] (range e)
hb : closure[inst_1.toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
de : IsDenseEmbedding e
de' :
  IsDenseEmbedding (β := { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) })
    (IsDenseEmbedding.subtypeEmb p e)
ue' :
  IsUniformEmbedding (β := { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) })
    (IsDenseEmbedding.subtypeEmb p e)
this : b ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x})
c : γ
hc : Tendsto (α := Subtype p) (f ∘ Subtype.val (p := p)) (comap (Subtype.val (p := p)) (comap e (𝓝 b))) (𝓝 c)
refine : range (ι := Subtype p) (Subtype.val (p := p)) ∈ comap e (𝓝 b)
⊢ ∃ (c : γ), Tendsto f (comap e (𝓝 b)) (𝓝 c)

Tactic:
refine ⟨c, (tendsto_comap'_iff ?_).1 hc⟩
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous.{u_1, u_3} (β := γ) fun (x : Subtype p) ↦ f (↑x : α)
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst_1.toTopologicalSpace] (range e)
hb : closure[inst_1.toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
de : IsDenseEmbedding e
de' :
  IsDenseEmbedding (β := { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) })
    (IsDenseEmbedding.subtypeEmb p e)
ue' :
  IsUniformEmbedding (β := { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) })
    (IsDenseEmbedding.subtypeEmb p e)
this : b ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x})
c : γ
hc : Tendsto (α := Subtype p) (f ∘ Subtype.val (p := p)) (comap (Subtype.val (p := p)) (comap e (𝓝 b))) (𝓝 c)
rw : {x : α | p x} ∈ comap e (𝓝 b)
⊢ range (ι := Subtype p) (Subtype.val (p := p)) ∈ comap e (𝓝 b)

Tactic:
rw [Subtype.range_coe_subtype]

Premises used: Subtype.range_coe_subtype
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous.{u_1, u_3} (β := γ) fun (x : Subtype p) ↦ f (↑x : α)
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst_1.toTopologicalSpace] (range e)
hb : closure[inst_1.toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
de : IsDenseEmbedding e
de' :
  IsDenseEmbedding (β := { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) })
    (IsDenseEmbedding.subtypeEmb p e)
ue' :
  IsUniformEmbedding (β := { x : β // x ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x}) })
    (IsDenseEmbedding.subtypeEmb p e)
this : b ∈ closure[inst_1.toTopologicalSpace] (e '' {x : α | p x})
c : γ
hc : Tendsto (α := Subtype p) (f ∘ Subtype.val (p := p)) (comap (Subtype.val (p := p)) (comap e (𝓝 b))) (𝓝 c)
rwa : closure[inst.toTopologicalSpace] s ⊆ {x : α | p x}
rwa₁ rwa₂ rwa₃ rwa₄ : s ⊆ {x : α | p x}
⊢ e ⁻¹' closure[inst_1.toTopologicalSpace] (e '' s) ⊆ {x : α | p x}

Tactic:
rwa [← de.isInducing.closure_eq_preimage_closure_image, hs.closure_eq]

Premises used: IsDenseEmbedding.toIsDenseInducing, IsClosed.closure_eq, IsDenseInducing.isInducing, Topology.IsInducing.closure_eq_preimage_closure_image