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 β
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
⊢ IsComplete (m '' s) ↔ IsComplete s
have 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
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 β
f : α → β
hf : IsUniformInducing f
⊢ CompleteSpace α ↔ IsComplete (range f)
have rw : IsComplete.{u} (α := α) univ ↔ IsComplete (range f)
Tactic: rw [completeSpace_iff_isComplete_univ, ← isComplete_image_iff hf, image_univ]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : IsUniformInducing f
rw : IsComplete.{u} (α := α) univ ↔ IsComplete (range f)
⊢ CompleteSpace α ↔ IsComplete (range f)
have rw₁ : IsComplete (f '' univ) ↔ IsComplete (range f)
Tactic: rw [completeSpace_iff_isComplete_univ, ← isComplete_image_iff hf, image_univ]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)
⊢ CompleteSpace α ↔ IsComplete (range f)
have rw₂ : IsComplete (range f) ↔ IsComplete (range f)
Tactic: rw [completeSpace_iff_isComplete_univ, ← isComplete_image_iff hf, image_univ]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : IsUniformInducing f
hsurj : Surjective f
⊢ CompleteSpace α ↔ CompleteSpace β
have rw : IsComplete (range f) ↔ CompleteSpace β
Tactic: rw [completeSpace_iff_isComplete_range hf, hsurj.range_eq, completeSpace_iff_isComplete_univ]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : IsUniformInducing f
hsurj : Surjective f
rw : IsComplete (range f) ↔ CompleteSpace β
⊢ CompleteSpace α ↔ CompleteSpace β
have rw₁ : IsComplete.{v} (α := β) univ ↔ CompleteSpace β
Tactic: rw [completeSpace_iff_isComplete_range hf, hsurj.range_eq, completeSpace_iff_isComplete_univ]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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 β
⊢ CompleteSpace α ↔ CompleteSpace β
have rw₂ : IsComplete.{v} (α := β) univ ↔ IsComplete.{v} (α := β) univ
Tactic: rw [completeSpace_iff_isComplete_range hf, hsurj.range_eq, completeSpace_iff_isComplete_univ]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
inst : UniformSpace α
s : Set α
⊢ CompleteSpace.{u} (↑s : Type u) ↔ IsComplete s
have rw : IsComplete.{u} (α := α) (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) ↔ IsComplete s
Tactic: rw [completeSpace_iff_isComplete_range isUniformEmbedding_subtype_val.isUniformInducing,
    Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
inst : UniformSpace α
s : Set α
rw : IsComplete.{u} (α := α) (range (ι := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))) ↔ IsComplete s
⊢ CompleteSpace.{u} (↑s : Type u) ↔ IsComplete s
have rw₁ : IsComplete s ↔ IsComplete s
Tactic: rw [completeSpace_iff_isComplete_range isUniformEmbedding_subtype_val.isUniformInducing,
    Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
⊢ (map f F).TotallyBounded ↔ F.TotallyBounded
have refine : ∀ (hs : (map f F).TotallyBounded), F.TotallyBounded
Tactic: refine ⟨fun hs ↦ ?_, fun h ↦ h.map hf.uniformContinuous⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
F : Filter α
hf : IsUniformInducing f
hs : (map f F).TotallyBounded
⊢ F.TotallyBounded
have simp_rw : ∀ i ∈ 𝓤 β, ∃ (t : Set α), t.Finite ∧ SetRel.preimage (Prod.map f f ⁻¹' id i) t ∈ F
Tactic: simp_rw [(hf.basis_uniformity (basis_sets _)).filter_totallyBounded_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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 ∈ 𝓤 β
⊢ ∃ (t_1 : Set α), t_1.Finite ∧ SetRel.preimage (Prod.map f f ⁻¹' id t) t_1 ∈ F
have 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
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⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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
⊢ ∃ (t_1 : Set α), t_1.Finite ∧ SetRel.preimage (Prod.map f f ⁻¹' id t) t_1 ∈ F
have right : SetRel.preimage (Prod.map f f ⁻¹' id t) u ∈ F
Tactic: use u, hfin
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (hypothesis)
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
⊢ SetRel.preimage (Prod.map f f ⁻¹' id t) u ∈ F
have h₁ : {a : β | ∃ x ∈ u, (a, f x) ∈ t} ∈ map f F
Tactic: simp_rw [SetRel.preimage, exists_mem_image] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
hf : IsUniformInducing f
⊢ TotallyBounded (f '' s) ↔ TotallyBounded s
have simp_rw : (𝓟 (f '' s)).TotallyBounded ↔ (𝓟 s).TotallyBounded
Tactic: simp_rw [← totallyBounded_principal_iff, ← map_principal, totallyBounded_map_iff hf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
hf : IsUniformInducing f
simp_rw : (𝓟 (f '' s)).TotallyBounded ↔ (𝓟 s).TotallyBounded
⊢ TotallyBounded (f '' s) ↔ TotallyBounded s
have simp_rw₁ : (map f (𝓟 s)).TotallyBounded ↔ (𝓟 s).TotallyBounded
Tactic: simp_rw [← totallyBounded_principal_iff, ← map_principal, totallyBounded_map_iff hf]
-- 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 γ
f : α → β
inst_3 : CompleteSpace α
inst_4 : CompleteSpace β
⊢ CompleteSpace (α ⊕ β)
have rw : IsComplete (α := α ⊕ β) (range Sum.inl ∪ range Sum.inr)
Tactic: rw [completeSpace_iff_isComplete_univ, ← range_inl_union_range_inr]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : DiscreteUniformity β
f : α → β
hf : IsUniformEmbedding f
⊢ DiscreteUniformity α
have simp_rw : 𝓤 α = 𝓟 SetRel.id
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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : DiscreteUniformity β
f : α → β
hf : IsUniformEmbedding f
simp_rw : 𝓤 α = 𝓟 SetRel.id
⊢ DiscreteUniformity α
have simp_rw₁ : Eq.{u + 1} (α := Filter (α × α)) (comap (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 β)) (𝓟 SetRel.id)
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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)
⊢ DiscreteUniformity α
have simp_rw₂ : Eq.{u + 1} (α := Filter (α × α)) (comap.{u, v} (β := β × β) (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓟 SetRel.id))
  (𝓟 SetRel.id)
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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)
⊢ DiscreteUniformity α
have simp_rw₃ : Eq.{u + 1} (α := Filter (α × α)) (𝓟 (preimage.{u, v} (β := β × β) (fun (x : α × α) ↦ (f x.1, f x.2)) SetRel.id))
  (𝓟 SetRel.id)
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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)
⊢ DiscreteUniformity α
have 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})
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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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})
⊢ DiscreteUniformity α
have simp_rw₅ : Eq.{u + 1} (α := Filter (α × α)) (𝓟 {a : α × α | f a.1 = f a.2}) (𝓟 {x : α × α | x.1 = x.2})
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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (hypothesis)
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
⊢ ∃ (c : γ), Tendsto f (comap e (𝓝 b)) (𝓝 c)
have de : IsDenseEmbedding e
Tactic: have de : IsDenseEmbedding e := he.isDenseEmbedding hd
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (hypothesis)
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
⊢ ∃ (c : γ), Tendsto f (comap e (𝓝 b)) (𝓝 c)
have de' : 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
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (hypothesis)
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)
⊢ ∃ (c : γ), Tendsto f (comap e (𝓝 b)) (𝓝 c)
have ue' : 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
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (hypothesis)
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)
⊢ ∃ (c : γ), Tendsto f (comap e (𝓝 b)) (𝓝 c)
have this : 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)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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 : γ), Tendsto f (comap e (𝓝 b)) (𝓝 c)
have 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)
Tactic: let ⟨c, hc⟩ := uniformly_extend_exists ue'.isUniformInducing de'.dense hf ⟨b, this⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (hypothesis)
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)
⊢ ∃ (c : γ), Tendsto f (comap e (𝓝 b)) (𝓝 c)
have hc₁ : 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
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)
have refine : range (ι := Subtype p) (Subtype.val (p := p)) ∈ comap e (𝓝 b)
Tactic: refine ⟨c, (tendsto_comap'_iff ?_).1 hc⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)
⊢ range (ι := Subtype p) (Subtype.val (p := p)) ∈ comap e (𝓝 b)
have rw : {x : α | p x} ∈ comap e (𝓝 b)
Tactic: rw [Subtype.range_coe_subtype]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)
⊢ e ⁻¹' closure[inst_1.toTopologicalSpace] (e '' s) ⊆ {x : α | p x}
have rwa : closure[inst.toTopologicalSpace] s ⊆ {x : α | p x}
Tactic: rwa [← de.isInducing.closure_eq_preimage_closure_image, hs.closure_eq]