awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
rwa : closure[inst.toTopologicalSpace] s ⊆ {x : α | p x}
⊢ e ⁻¹' closure[inst_1.toTopologicalSpace] (e '' s) ⊆ {x : α | p x}
have rwa₁ : s ⊆ {x : α | p x}
Tactic: rwa [← de.isInducing.closure_eq_preimage_closure_image, hs.closure_eq]
-- 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 γ
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 ∈ 𝓤 β
⊢ Prod.map f f ⁻¹' s ∈ comap (Prod.map e e) (𝓤 α)
have 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) (𝓤 α)
Tactic: rwa [← h_e.comap_uniformity] at this
Cleared hypotheses: 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 γ
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
⊢ (x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d
have this₁ : interior t ∈ 𝓝 (x₁, x₂)
Tactic: have : interior t ∈ 𝓝 (x₁, x₂) := isOpen_interior.mem_nhds hx_t
-- 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 γ
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₂)
⊢ (x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d
have let : ∀ (m₁ : Set α) (hm₁ : m₁ ∈ 𝓝 x₁) (m₂ : Set α) (hm₂ : m₂ ∈ 𝓝 x₂) (hm : m₁ ×ˢ m₂ ⊆ interior t),
  (x₁, x₂) ∈ Prod.map (sorry.extend f) (sorry.extend f) ⁻¹' d
Tactic: let ⟨m₁, hm₁, m₂, hm₂, (hm : m₁ ×ˢ m₂ ⊆ interior t)⟩ := mem_nhds_prod_iff.mp this
-- 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 γ
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
⊢ (x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d
have obtain : ∀ (a : β) (ha₁ : a ∈ e ⁻¹' m₁),
  (f a, sorry.extend f x₁) ∈ s → ∀ (ha₂ : (sorry.extend f x₁, f a) ∈ s), (x₁, x₂) ∈ Prod.map (sorry.extend f) (sorry.extend f) ⁻¹' d
Tactic: obtain ⟨_, ⟨a, ha₁, rfl⟩, _, ha₂⟩ := h_pnt hm₁
-- 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 γ
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
⊢ (x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d
have obtain : ∀ (b : β) (hb₁ : b ∈ e ⁻¹' m₂) (hb₂ : (f b, sorry.extend f x₂) ∈ s),
  (sorry.extend f x₂, f b) ∈ s → (x₁, x₂) ∈ Prod.map (sorry.extend f) (sorry.extend f) ⁻¹' d
Tactic: obtain ⟨_, ⟨b, hb₁, rfl⟩, hb₂, _⟩ := h_pnt hm₂
-- 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 γ
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
⊢ (x₁, x₂) ∈ Prod.map (⋯.extend f) (⋯.extend f) ⁻¹' d
have this₁ : 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₁⟩)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (hypothesis)
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
⊢ IsUniformInducing (hid.extend f)
have this : CompleteSpace.{u_3} (↑(closure (range sf)) : Type u_3)
Tactic: have : CompleteSpace (closure (range sf)) :=
    isClosed_closure.isComplete.completeSpace_coe
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (hypothesis)
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 (hid.extend f)
have hgu : IsUniformInducing ff
Tactic: have hgu : IsUniformInducing ff :=
    (isUniformEmbedding_set_inclusion subset_closure).isUniformInducing.comp
      (SeparationQuotient.isUniformInducing_mk.comp h).rangeFactorization
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (hypothesis)
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
⊢ IsUniformInducing (hid.extend f)
have hgd : DenseRange ff
Tactic: have hgd : DenseRange ff :=
    ((denseRange_inclusion_iff subset_closure).2 subset_rfl).comp
      rangeFactorization_surjective.denseRange (continuous_inclusion subset_closure)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (hypothesis)
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
⊢ IsUniformInducing (hid.extend f)
have hg : IsDenseInducing ff
Tactic: have hg : IsDenseInducing ff := hgu.isDenseInducing hgd
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (hypothesis)
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
⊢ IsUniformInducing (hid.extend f)
have hfwd : UniformContinuous fwd
Tactic: have hfwd : UniformContinuous fwd :=
    uniformContinuous_uniformly_extend hi hid.dense hgu.uniformContinuous
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (hypothesis)
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
⊢ IsUniformInducing (hid.extend f)
have hg' : UniformContinuous (hg.extend i)
Tactic: have hg' : UniformContinuous (hg.extend i) :=
    uniformContinuous_uniformly_extend hgu hgd hi.uniformContinuous
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)
⊢ Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
have h₁ : ∀ (x : β), Eq (α := SeparationQuotient β) ((SeparationQuotient.mk ∘ hg.extend i ∘ fwd) x) (SeparationQuotient.mk x)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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 : β
⊢ Eq (α := SeparationQuotient β) ((SeparationQuotient.mk ∘ hg.extend i ∘ fwd) x) (SeparationQuotient.mk x)
have h₁ : IsClosed[inst_1.toTopologicalSpace]
  {x : β | Eq (α := SeparationQuotient β) ((SeparationQuotient.mk ∘ hg.extend i ∘ fwd) x) (SeparationQuotient.mk x)}
Tactic: induction x using isClosed_property hid.dense
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)}
⊢ Eq (α := SeparationQuotient β) ((SeparationQuotient.mk ∘ hg.extend i ∘ fwd) x) (SeparationQuotient.mk x)
have h₂ : ∀ (a : α),
  Eq (α := SeparationQuotient β) ((SeparationQuotient.mk ∘ hg.extend i ∘ fwd) (i a)) (SeparationQuotient.mk (i a))
Tactic: induction x using isClosed_property hid.dense
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (hypothesis)
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)
⊢ IsUniformInducing (hid.extend f)
have key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
Tactic: have key : SeparationQuotient.mk ∘ hg.extend i ∘ fwd = SeparationQuotient.mk := by
    ext x
    induction x using isClosed_property hid.dense
    · exact isClosed_eq (SeparationQuotient.continuous_mk.comp (hg'.comp hfwd).continuous)
        SeparationQuotient.continuous_mk
    · simpa [fwd, hid.extend_eq hgu.uniformContinuous.continuous]
        using hg.inseparable_extend hi.uniformContinuous.continuous.continuousAt
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
⊢ IsUniformInducing fwd
have refine : IsUniformInducing (β := SeparationQuotient β) ((SeparationQuotient.mk ∘ hg.extend i) ∘ fwd)
Tactic: refine IsUniformInducing.of_comp hfwd (SeparationQuotient.uniformContinuous_mk.comp hg') ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
⊢ IsUniformInducing (β := SeparationQuotient β) ((SeparationQuotient.mk ∘ hg.extend i) ∘ fwd)
have rw : IsUniformInducing.{u_2, u_2} (α := β) (β := SeparationQuotient β) SeparationQuotient.mk
Tactic: rw [Function.comp_assoc, key]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (hypothesis)
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)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
⊢ IsUniformInducing (hid.extend f)
have hfu : IsUniformInducing fwd
Tactic: have hfu : IsUniformInducing fwd := by
    refine IsUniformInducing.of_comp hfwd (SeparationQuotient.uniformContinuous_mk.comp hg') ?_
    rw [Function.comp_assoc, key]
    exact SeparationQuotient.isUniformInducing_mk
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
hfu : IsUniformInducing fwd
⊢ Subset (α := Set (SeparationQuotient γ)) (range (SeparationQuotient.mk ∘ hid.extend f))
    (closure (range (SeparationQuotient.mk ∘ f)))
have refine : Eq (α := Set (SeparationQuotient γ)) (SeparationQuotient.mk ∘ sorry.extend f '' range i) (range (SeparationQuotient.mk ∘ f))
Tactic: refine ((SeparationQuotient.continuous_mk.comp (uniformContinuous_uniformly_extend hi hid.dense
      h.uniformContinuous).continuous).range_subset_closure_image_dense hid.dense).trans
      (closure_mono (subset_of_eq ?_))
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformEmbedding (goal)
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)
key : Eq (α := β → SeparationQuotient β) (SeparationQuotient.mk ∘ hg.extend i ∘ fwd) SeparationQuotient.mk
hfu : IsUniformInducing fwd
⊢ Eq (α := Set (SeparationQuotient γ)) (SeparationQuotient.mk ∘ ⋯.extend f '' range i)
    (range (SeparationQuotient.mk ∘ f))
have rw : Eq (α := Set (SeparationQuotient γ)) (range ((SeparationQuotient.mk ∘ sorry.extend f) ∘ i))
  (range (SeparationQuotient.mk ∘ f))
Tactic: rw [← range_comp]