awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ {x : α | p x} ∈ comap e (𝓝 b)

Tactic:
exact ⟨_, hb, by rwa [← de.isInducing.closure_eq_preimage_closure_image, hs.closure_eq]⟩
-- 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 : α
⊢ Tendsto f (comap e (𝓝 a)) (𝓝 (⋯.extend f a))

Tactic:
simpa only [IsDenseInducing.extend] using
    tendsto_nhds_limUnder (uniformly_extend_exists h_e ‹_› h_f _)

Premises used: tendsto_nhds_limUnder, uniformly_extend_exists, IsDenseInducing.extend
-- 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 γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt : ∀ {a : α} {m : Set α}, m ∈ 𝓝 a → ∃ c ∈ f '' e ⁻¹' m, (c, ⋯.extend f a) ∈ s ∧ (⋯.extend f a, c) ∈ s
this : Prod.map f f ⁻¹' s ∈ 𝓤 β
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : Membership.mem (γ := Filter (β × β)) (comap (fun (x : β × β) ↦ (e x.1, e x.2)) (𝓤 α)) (Prod.map f f ⁻¹' s)),
    Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
⊢ Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)

Tactic:
rwa [← h_e.comap_uniformity] at this

Premises used: IsUniformInducing.comap_uniformity
-- 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 γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt : ∀ {a : α} {m : Set α}, m ∈ 𝓝 a → ∃ c ∈ f '' e ⁻¹' m, (c, ⋯.extend f a) ∈ s ∧ (⋯.extend f a, c) ∈ s
this_1 : Prod.map f f ⁻¹' s ∈ 𝓤 β
this : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
⊢ interior t ∈ 𝓝 (x₁, x₂)

Tactic:
have : interior t ∈ 𝓝 (x₁, x₂) := isOpen_interior.mem_nhds hx_t
-- 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 γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt : ∀ {a : α} {m : Set α}, m ∈ 𝓝 a → ∃ c ∈ f '' e ⁻¹' m, (c, ⋯.extend f a) ∈ s ∧ (⋯.extend f a, c) ∈ s
this_1 : Prod.map f f ⁻¹' s ∈ 𝓤 β
this_2 : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
this : interior t ∈ 𝓝 (x₁, x₂)
let :
  ∀ (m₁ : Set α) (hm₁ : m₁ ∈ 𝓝 x₁) (m₂ : Set α) (hm₂ : m₂ ∈ 𝓝 x₂) (hm : m₁ ×ˢ m₂ ⊆ interior t),
    (x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d
⊢ (x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d

Tactic:
let ⟨m₁, hm₁, m₂, hm₂, (hm : m₁ ×ˢ m₂ ⊆ interior t)⟩ := mem_nhds_prod_iff.mp this
-- 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 γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt : ∀ {a : α} {m : Set α}, m ∈ 𝓝 a → ∃ c ∈ f '' e ⁻¹' m, (c, ⋯.extend f a) ∈ s ∧ (⋯.extend f a, c) ∈ s
this_1 : Prod.map f f ⁻¹' s ∈ 𝓤 β
this_2 : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
this : interior t ∈ 𝓝 (x₁, x₂)
m₁ : Set α
hm₁ : m₁ ∈ 𝓝 x₁
m₂ : Set α
hm₂ : m₂ ∈ 𝓝 x₂
hm : m₁ ×ˢ m₂ ⊆ interior t
obtain :
  ∀ (a : β) (ha₁ : a ∈ e ⁻¹' m₁),
    (f a, ⋯.extend f x₁) ∈ s → ∀ (ha₂ : (⋯.extend f x₁, f a) ∈ s), (x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d
⊢ (x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d

Tactic:
obtain ⟨_, ⟨a, ha₁, rfl⟩, _, ha₂⟩ := h_pnt hm₁

Premises used: 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 γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt : ∀ {a : α} {m : Set α}, m ∈ 𝓝 a → ∃ c ∈ f '' e ⁻¹' m, (c, ⋯.extend f a) ∈ s ∧ (⋯.extend f a, c) ∈ s
this_1 : Prod.map f f ⁻¹' s ∈ 𝓤 β
this_2 : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
this : interior t ∈ 𝓝 (x₁, x₂)
m₁ : Set α
hm₁ : m₁ ∈ 𝓝 x₁
m₂ : Set α
hm₂ : m₂ ∈ 𝓝 x₂
hm : m₁ ×ˢ m₂ ⊆ interior t
a : β
ha₁ : a ∈ e ⁻¹' m₁
left : (f a, ⋯.extend f x₁) ∈ s
ha₂ : (⋯.extend f x₁, f a) ∈ s
obtain :
  ∀ (b : β) (hb₁ : b ∈ e ⁻¹' m₂) (hb₂ : (f b, ⋯.extend f x₂) ∈ s),
    (⋯.extend f x₂, f b) ∈ s → (x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d
⊢ (x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d

Tactic:
obtain ⟨_, ⟨b, hb₁, rfl⟩, hb₂, _⟩ := h_pnt hm₂

Premises used: 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 γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt : ∀ {a : α} {m : Set α}, m ∈ 𝓝 a → ∃ c ∈ f '' e ⁻¹' m, (c, ⋯.extend f a) ∈ s ∧ (⋯.extend f a, c) ∈ s
this_1 : Prod.map f f ⁻¹' s ∈ 𝓤 β
this_2 : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
this : interior t ∈ 𝓝 (x₁, x₂)
m₁ : Set α
hm₁ : m₁ ∈ 𝓝 x₁
m₂ : Set α
hm₂ : m₂ ∈ 𝓝 x₂
hm : m₁ ×ˢ m₂ ⊆ interior t
a : β
ha₁ : a ∈ e ⁻¹' m₁
left : (f a, ⋯.extend f x₁) ∈ s
ha₂ : (⋯.extend f x₁, f a) ∈ s
b : β
hb₁ : b ∈ e ⁻¹' m₂
hb₂ : (f b, ⋯.extend f x₂) ∈ s
right : (⋯.extend f x₂, f b) ∈ s
⊢ Prod.map f f (a, b) ∈ s

Tactic:
have : Prod.map f f (a, b) ∈ s :=
        ts <| mem_preimage.2 <| interior_subset (@hm (e a, e b) ⟨ha₁, hb₁⟩)
-- 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 γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt : ∀ {a : α} {m : Set α}, m ∈ 𝓝 a → ∃ c ∈ f '' e ⁻¹' m, (c, ⋯.extend f a) ∈ s ∧ (⋯.extend f a, c) ∈ s
this_1 : Prod.map f f ⁻¹' s ∈ 𝓤 β
this_2 : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
this_3 : interior t ∈ 𝓝 (x₁, x₂)
m₁ : Set α
hm₁ : m₁ ∈ 𝓝 x₁
m₂ : Set α
hm₂ : m₂ ∈ 𝓝 x₂
hm : m₁ ×ˢ m₂ ⊆ interior t
a : β
ha₁ : a ∈ e ⁻¹' m₁
left : (f a, ⋯.extend f x₁) ∈ s
ha₂ : (⋯.extend f x₁, f a) ∈ s
b : β
hb₁ : b ∈ e ⁻¹' m₂
hb₂ : (f b, ⋯.extend f x₂) ∈ s
right : (⋯.extend f x₂, f b) ∈ s
this : Prod.map f f (a, b) ∈ s
⊢ (x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d

Tactic:
hs_comp ⟨f a, ha₂, ⟨f b, this, hb₂⟩⟩

Premises used: Set.Mem, setOf, Set.preimage, And.intro, Exists.intro
-- 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 γ
d : Set (γ × γ)
hd : d ∈ 𝓤 γ
s : Set (γ × γ)
hs : s ∈ 𝓤 γ
hs_comp : s ○ (s ○ s) ⊆ d
h_pnt : ∀ {a : α} {m : Set α}, m ∈ 𝓝 a → ∃ c ∈ f '' e ⁻¹' m, (c, ⋯.extend f a) ∈ s ∧ (⋯.extend f a, c) ∈ s
this_1 : Prod.map f f ⁻¹' s ∈ 𝓤 β
this_2 : Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
t : Set (α × α)
ht : t ∈ 𝓤 α
ts : Prod.map e e ⁻¹' t ⊆ Prod.map f f ⁻¹' s
x : α × α
x₁ x₂ : α
hx_t : (x₁, x₂) ∈ interior t
this_3 : interior t ∈ 𝓝 (x₁, x₂)
m₁ : Set α
hm₁ : m₁ ∈ 𝓝 x₁
m₂ : Set α
hm₂ : m₂ ∈ 𝓝 x₂
hm : m₁ ×ˢ m₂ ⊆ interior t
a : β
ha₁ : a ∈ e ⁻¹' m₁
left : (f a, ⋯.extend f x₁) ∈ s
ha₂ : (⋯.extend f x₁, f a) ∈ s
b : β
hb₁ : b ∈ e ⁻¹' m₂
hb₂ : (f b, ⋯.extend f x₂) ∈ s
right : (⋯.extend f x₂, f b) ∈ s
this : Prod.map f f (a, b) ∈ s
⊢ (x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d

Tactic:
exact hs_comp ⟨f a, ha₂, ⟨f b, this, hb₂⟩⟩

Premises used: And.intro, Exists.intro
-- 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 : T0Space γ
b : β
⊢ ⋯.extend f (e b) = f b

Tactic:
IsDenseInducing.extend_eq_at _ h_f.continuous.continuousAt

Premises used: UniformContinuous.continuous, Continuous.continuousAt, IsDenseInducing.extend_eq_at
-- 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 : β → γ
inst_3 : T0Space γ
g : α → γ
hg : ∀ (b : β), g (e b) = f b
hc : Continuous[inst.toTopologicalSpace, inst_2.toTopologicalSpace] g
⊢ ⋯.extend f = g

Tactic:
IsDenseInducing.extend_unique _ hg hc

Premises used: IsDenseInducing.extend_unique
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
⊢ IsUniformInducing.{u_1, u_1} (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
⟨uniformity_setCoe⟩

Premises used: uniformity_setCoe, IsUniformInducing.mk
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
⊢ UniformContinuous (rangeFactorization f) ↔ UniformContinuous f

Tactic:
(isUniformInducing_val _).uniformContinuous_iff

Premises used: IsUniformInducing.uniformContinuous_iff, isUniformInducing_val
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (Set.rangeFactorization f)

Tactic:
uniformContinuous_rangeFactorization_iff.mpr hf

Premises used: Iff.mpr, uniformContinuous_rangeFactorization_iff
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
⊢ IsUniformInducing (rangeFactorization f) ↔ IsUniformInducing f

Tactic:
(isUniformInducing_val (range f)).of_comp_iff.symm

Premises used: IsUniformInducing.of_comp_iff, isUniformInducing_val, Set.range, Iff.symm
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : IsUniformInducing f
⊢ IsUniformInducing (Set.rangeFactorization f)

Tactic:
isUniformInducing_rangeFactorization_iff.2 hf

Premises used: Iff.mpr, isUniformInducing_rangeFactorization_iff
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set α
f : (↑s : Type u_1) → β
inst_2 : CompleteSpace β
hs : Dense s
hf : UniformContinuous f
a : α
⊢ ∃ (b : β), Tendsto f (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 a)) (𝓝 b)

Tactic:
uniformly_extend_exists (isUniformInducing_val s) hs.denseRange_val hf a

Premises used: isUniformInducing_val, uniformly_extend_exists, Dense.denseRange_val
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set α
f : (↑s : Type u_1) → β
inst_2 : CompleteSpace β
hs : Dense s
hf : UniformContinuous f
a : α
⊢ Tendsto f (comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (𝓝 a)) (𝓝 (hs.extend (s := s) f a))

Tactic:
uniformly_extend_spec (isUniformInducing_val s) hs.denseRange_val hf a

Premises used: Dense.extend, isUniformInducing_val, Dense.denseRange_val, uniformly_extend_spec
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set α
f : (↑s : Type u_1) → β
inst_2 : CompleteSpace β
hs : Dense s
hf : UniformContinuous f
⊢ UniformContinuous (hs.extend (s := s) f)

Tactic:
uniformContinuous_uniformly_extend (isUniformInducing_val s) hs.denseRange_val hf

Premises used: uniformContinuous_uniformly_extend, Dense.extend, isUniformInducing_val, Dense.denseRange_val
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set α
f : (↑s : Type u_1) → β
inst_2 : T0Space β
hs : Dense s
hf : UniformContinuous f
x : (↑s : Type u_1)
⊢ hs.extend (s := s) f (↑x : α) = f x

Tactic:
IsDenseInducing.extend_eq_at _ hf.continuous.continuousAt

Premises used: Dense.extend, UniformContinuous.continuous, Continuous.continuousAt, IsDenseInducing.extend_eq_at
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
⊢ CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)

Tactic:
have : CompleteSpace (closure (range sf)) :=
    isClosed_closure.isComplete.completeSpace_coe
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
⊢ IsUniformInducing ff

Tactic:
have hgu : IsUniformInducing ff :=
    (isUniformEmbedding_set_inclusion subset_closure).isUniformInducing.comp
      (SeparationQuotient.isUniformInducing_mk.comp h).rangeFactorization
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
⊢ DenseRange ff

Tactic:
have hgd : DenseRange ff :=
    ((denseRange_inclusion_iff subset_closure).2 subset_rfl).comp
      rangeFactorization_surjective.denseRange (continuous_inclusion subset_closure)
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
⊢ IsDenseInducing ff

Tactic:
have hg : IsDenseInducing ff := hgu.isDenseInducing hgd
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
⊢ UniformContinuous fwd

Tactic:
have hfwd : UniformContinuous fwd :=
    uniformContinuous_uniformly_extend hi hid.dense hgu.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
⊢ UniformContinuous (hg.extend i)

Tactic:
have hg' : UniformContinuous (hg.extend i) :=
    uniformContinuous_uniformly_extend hgu hgd hi.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
h₁ : ∀ (x : β), Eq (α := SeparationQuotient β) ((SeparationQuotient.mk ∘ hg.extend i ∘ fwd) x) (SeparationQuotient.mk x)
⊢ Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk

Tactic:
ext x
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
x : β
h₁ :
  IsClosed[inst_1.toTopologicalSpace]
    {x : β | Eq (α := SeparationQuotient β) ((SeparationQuotient.mk ∘ hg.extend i ∘ fwd) x) (SeparationQuotient.mk x)}
h₂ :
  ∀ (a : α),
    Eq (α := SeparationQuotient β) ((SeparationQuotient.mk ∘ hg.extend i ∘ fwd) (i a)) (SeparationQuotient.mk (i a))
⊢ Eq (α := SeparationQuotient β) ((SeparationQuotient.mk ∘ hg.extend i ∘ fwd) x) (SeparationQuotient.mk x)

Tactic:
induction x using isClosed_property hid.dense

Premises used: IsDenseInducing.dense, isClosed_property
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
⊢ IsClosed[inst_1.toTopologicalSpace]
    {x : β | Eq (α := SeparationQuotient β) ((SeparationQuotient.mk ∘ hg.extend i ∘ fwd) x) (SeparationQuotient.mk x)}

Tactic:
isClosed_eq (SeparationQuotient.continuous_mk.comp (hg'.comp hfwd).continuous)
        SeparationQuotient.continuous_mk

Premises used: SeparationQuotient.continuous_mk, Continuous.comp, UniformContinuous.comp, UniformContinuous.continuous, isClosed_eq
-- Module: Mathlib.Topology.UniformSpace.UniformEmbedding
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
γ : Type u_3
inst_2 : UniformSpace γ
inst_3 : CompleteSpace β
inst_4 : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
ff : α → (↑(closure (range sf)) : Type u_3) :=
  inclusion (s := range sf) (t := closure (range sf)) ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : (b : β) → (↑(closure (range sf)) : Type u_3) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
⊢ IsClosed[inst_1.toTopologicalSpace]
    {x : β | Eq (α := SeparationQuotient β) ((SeparationQuotient.mk ∘ hg.extend i ∘ fwd) x) (SeparationQuotient.mk x)}

Tactic:
exact isClosed_eq (SeparationQuotient.continuous_mk.comp (hg'.comp hfwd).continuous)
        SeparationQuotient.continuous_mk

Premises used: SeparationQuotient.continuous_mk, Continuous.comp, UniformContinuous.comp, UniformContinuous.continuous, isClosed_eq