awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst_2 : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → ContinuousMap.{u_1, u₁} (δ i) α
h_proper : ∀ (i : ι), IsProperMap.{u_1, u₁} (X := δ i) (Y := α) (⇑(φ i) : (a : δ i) → α)
h_lf : LocallyFinite.{u₃, u₁} (X := α) fun (i : ι) ↦ range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
h_cover : Eq.{u₁ + 1} (α := Set α) (⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun (i : ι) ↦ {K : Set (δ i) | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ (⇑(φ i) : (a : δ i) → α) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ (⇑(φ i) : (a : δ i) → α) ⁻¹' x) 𝔖 (𝔗 i)
h_cover' : ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
⊢ Eq (α := UniformSpace C(α, β)) inferInstance
    (⨅ (i : ι),
      UniformSpace.comap (β := UniformOnFun.{u_1, u₂} (δ i) β {K : Set (δ i) | IsCompact K})
        (Function.comp (β := ContinuousMap.{u_1, u₂} (δ i) β) toUniformOnFunIsCompact fun (x : C(α, β)) ↦ x.comp (φ i))
        inferInstance)

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst_2 : CompleteSpace β
inst_3 : CompactlyCoherentSpace α
rw :
  CompleteSpace
    (↑{f : α →ᵤ[{K : Set α | IsCompact K}] β | Continuous[inst, inst_1.toTopologicalSpace] f} : Type (max u₁ u₂))
⊢ CompleteSpace C(α, β)

Tactic:
rw [completeSpace_iff_isComplete_range
    isUniformEmbedding_toUniformOnFunIsCompact.isUniformInducing,
    range_toUniformOnFunIsCompact, ← completeSpace_coe_iff_isComplete]

Premises used: IsUniformEmbedding.isUniformInducing, ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact, completeSpace_coe_iff_isComplete, ContinuousMap.range_toUniformOnFunIsCompact, completeSpace_iff_isComplete_range
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst_2 : CompleteSpace β
inst_3 : CompactlyCoherentSpace α
⊢ CompleteSpace
    (↑{f : α →ᵤ[{K : Set α | IsCompact K}] β | Continuous[inst, inst_1.toTopologicalSpace] f} : Type (max u₁ u₂))

Tactic:
(UniformOnFun.isClosed_setOf_continuous
    CompactlyCoherentSpace.isCoherentWith).completeSpace_coe

Premises used: Set.Mem, setOf, IsClosed.completeSpace_coe
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst_2 : CompleteSpace β
inst_3 : CompactlyCoherentSpace α
⊢ CompleteSpace
    (↑{f : α →ᵤ[{K : Set α | IsCompact K}] β | Continuous[inst, inst_1.toTopologicalSpace] f} : Type (max u₁ u₂))

Tactic:
exact (UniformOnFun.isClosed_setOf_continuous
    CompactlyCoherentSpace.isCoherentWith).completeSpace_coe

Premises used: IsClosed.completeSpace_coe
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
rcases :
  ∀ (f' : C(α, β)) (hf' : l ≤ 𝓝 f'),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
⊢ ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x

Tactic:
rcases CompleteSpace.complete hlc with ⟨f', hf'⟩

Premises used: CompleteSpace.complete
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
⊢ l.NeBot

Tactic:
have := hlc.1
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
x : α
hx : x ∈ s
⊢ Inseparable (f x) ((f' : (a : α) → β) x)

Tactic:
tendsto_nhds_unique_inseparable ?_ ((continuous_eval_const x).continuousAt.mono_left hf')

Premises used: tendsto_nhds_unique_inseparable, Continuous.continuousAt, ContinuousEvalConst.continuous_eval_const, Filter.Tendsto.mono_left
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
x : α
hx : x ∈ s
refine : Tendsto (fun (f : C(α, β)) ↦ (f : (a : α) → β) x) l (𝓝 (f x))
⊢ Inseparable (f x) ((f' : (a : α) → β) x)

Tactic:
refine tendsto_nhds_unique_inseparable ?_ ((continuous_eval_const x).continuousAt.mono_left hf')

Premises used: tendsto_nhds_unique_inseparable, Continuous.continuousAt, ContinuousEvalConst.continuous_eval_const, Filter.Tendsto.mono_left
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
x : α
hx : x ∈ s
⊢ Tendsto (fun (f : C(α, β)) ↦ (f : (a : α) → β) x) l (𝓝 (f x))

Tactic:
tendsto_const_nhds.congr' <| .filter_mono ?_ hlf

Premises used: Filter.EventuallyEq.filter_mono, tendsto_const_nhds, Filter.Tendsto.congr'
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
x : α
hx : x ∈ s
refine :
  EventuallyEq (β := β) (𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (fun (x_1 : C(α, β)) ↦ f x) fun (f : C(α, β)) ↦
    (f : (a : α) → β) x
⊢ Tendsto (fun (f : C(α, β)) ↦ (f : (a : α) → β) x) l (𝓝 (f x))

Tactic:
refine tendsto_const_nhds.congr' <| .filter_mono ?_ hlf

Premises used: tendsto_const_nhds, Filter.Tendsto.congr'
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
x : α
hx : x ∈ s
⊢ EventuallyEq (β := β) (𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (fun (x_1 : C(α, β)) ↦ f x) fun (f : C(α, β)) ↦
    (f : (a : α) → β) x

Tactic:
fun _ h ↦ (h hx).symm

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.EventuallyEq, Set.Subset, Eq.symm
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
x : α
hx : x ∈ s
⊢ EventuallyEq (β := β) (𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (fun (x_1 : C(α, β)) ↦ f x) fun (f : C(α, β)) ↦
    (f : (a : α) → β) x

Tactic:
exact fun _ h ↦ (h hx).symm
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
⊢ ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)

Tactic:
have H₁ : ∀ x ∈ s, Inseparable (f x) (f' x) := fun x hx ↦ by
    refine tendsto_nhds_unique_inseparable ?_ ((continuous_eval_const x).continuousAt.mono_left hf')
    refine tendsto_const_nhds.congr' <| .filter_mono ?_ hlf
    exact fun _ h ↦ (h hx).symm
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)
x : α
pos : ∀ (hx : x ∈ s), Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)
neg : ∀ (hx : x ∉ s), Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)
⊢ Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)
x : α
hx : x ∈ s
⊢ Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)

Tactic:
simp [hx, H₁, Inseparable.refl]

Premises used: Inseparable.refl
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)
x : α
hx : x ∉ s
⊢ Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)

Tactic:
simp [hx, H₁, Inseparable.refl]

Premises used: Inseparable.refl
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)
⊢ ∀ (x : α), Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)

Tactic:
have H₂ (x) : Inseparable (s.piecewise f f' x) (f' x) := by
    by_cases hx : x ∈ s <;> simp [hx, H₁, Inseparable.refl]
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)
H₂ : ∀ (x : α), Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)
g : C(α, β) := { toFun := s.piecewise (β := fun (a : α) ↦ β) f (⇑f' : (a : α) → β), continuous_toFun := ⋯ }
⊢ ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x

Tactic:
⟨g, Set.piecewise_eqOn _ _ _, hf'.trans_eq ?_⟩

Premises used: LE.le.trans_eq, Set.piecewise_eqOn, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)
H₂ : ∀ (x : α), Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)
g : C(α, β) := { toFun := s.piecewise (β := fun (a : α) ↦ β) f (⇑f' : (a : α) → β), continuous_toFun := ⋯ }
refine : 𝓝 f' = 𝓝 g
⊢ ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x

Tactic:
refine ⟨g, Set.piecewise_eqOn _ _ _, hf'.trans_eq ?_⟩
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)
H₂ : ∀ (x : α), Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)
g : C(α, β) := { toFun := s.piecewise (β := fun (a : α) ↦ β) f (⇑f' : (a : α) → β), continuous_toFun := ⋯ }
rwa : 𝓝 g = 𝓝 f'
rwa₁ : Inseparable g f'
rwa₂ : Inseparable (X := (a : α) → β) (⇑g : (a : α) → β) (⇑f' : (a : α) → β)
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (i : α), Inseparable.{u₂} (X := β) ((g : (a : α) → β) i : β) ((f' : (a : α) → β) i : β)
⊢ 𝓝 f' = 𝓝 g

Tactic:
rwa [eq_comm, ← Inseparable, ← inseparable_coe, inseparable_pi]

Premises used: inseparable_pi, ContinuousMap.inseparable_coe, eq_comm, Inseparable
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
intro intro₁ intro₂ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
intro₃ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (f' : C(α, β))
    (hf' : l ≤ 𝓝 f'),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
intro₄ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (f' : C(α, β))
    (hf' : l ≤ 𝓝 f') (this : l.NeBot),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
intro₅ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (f' : C(α, β))
    (hf' : l ≤ 𝓝 f') (this : l.NeBot) (H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
intro₆ intro₇ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (f' : C(α, β))
    (hf' : l ≤ 𝓝 f') (this : l.NeBot) (H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x))
    (H₂ : ∀ (x : α), Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
intro₈ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (f' : C(α, β))
    (hf' : l ≤ 𝓝 f') (this : l.NeBot) (H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x))
    (H₂ : ∀ (x : α), Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)),
    let g : C(α, β) := { toFun := s.piecewise (β := fun (a : α) ↦ β) f (⇑f' : (a : α) → β), continuous_toFun := ⋯ };
    𝓝 f' = 𝓝 g
⊢ IsComplete (α := C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}

Tactic:
classical
  intro l hlc hlf
  rcases CompleteSpace.complete hlc with ⟨f', hf'⟩
  have := hlc.1
  have H₁ : ∀ x ∈ s, Inseparable (f x) (f' x) := fun x hx ↦ by
    refine tendsto_nhds_unique_inseparable ?_ ((continuous_eval_const x).continuousAt.mono_left hf')
    refine tendsto_const_nhds.congr' <| .filter_mono ?_ hlf
    exact fun _ h ↦ (h hx).symm
  have H₂ (x) : Inseparable (s.piecewise f f' x) (f' x) := by
    by_cases hx : x ∈ s <;> simp [hx, H₁, Inseparable.refl]
  set g : C(α, β) :=
    ⟨s.piecewise f f', (continuous_congr_of_inseparable H₂).mpr <| map_continuous f'⟩
  refine ⟨g, Set.piecewise_eqOn _ _ _, hf'.trans_eq ?_⟩
  rwa [eq_comm, ← Inseparable, ← inseparable_coe, inseparable_pi]

Premises used: inseparable_pi, ContinuousMap.inseparable_coe, eq_comm, Inseparable
-- Module: Mathlib.Topology.UniformSpace.CompareReals
Goal:
h : ∀ (s : Set (ℚ × ℚ)), s ∈ uniformity ℚ ↔ s ∈ uniformity ℚ
⊢ Eq (α := UniformSpace ℚ) (AbsoluteValue.uniformSpace AbsoluteValue.abs) PseudoMetricSpace.toUniformSpace

Tactic:
ext s
-- Module: Mathlib.Topology.UniformSpace.CompareReals
Goal:
s : Set (ℚ × ℚ)
h :
  (∃ (i : ℚ), 0 < i ∧ {p : ℚ × ℚ | (AbsoluteValue.abs : (a : ℚ) → ℚ) (p.2 - p.1) < i} ⊆ s) ↔
    ∃ (i : ℚ), 0 < i ∧ {p : ℚ × ℚ | dist p.1 p.2 < (↑i : ℝ)} ⊆ s
⊢ s ∈ uniformity ℚ ↔ s ∈ uniformity ℚ

Tactic:
rw [(AbsoluteValue.hasBasis_uniformity _).mem_iff, Metric.uniformity_basis_dist_rat.mem_iff]

Premises used: Filter.HasBasis.mem_iff, Metric.uniformity_basis_dist_rat, AbsoluteValue.hasBasis_uniformity
-- Module: Mathlib.Topology.UniformSpace.CompareReals
Goal:
s : Set (ℚ × ℚ)
⊢ (∃ (i : ℚ), 0 < i ∧ {p : ℚ × ℚ | (AbsoluteValue.abs : (a : ℚ) → ℚ) (p.2 - p.1) < i} ⊆ s) ↔
    ∃ (i : ℚ), 0 < i ∧ {p : ℚ × ℚ | dist p.1 p.2 < (↑i : ℝ)} ⊆ s

Tactic:
simp only [Rat.dist_eq, AbsoluteValue.abs_apply, ← Rat.cast_sub, ← Rat.cast_abs, Rat.cast_lt,
    _root_.abs_sub_comm]

Premises used: Rat.dist_eq, AbsoluteValue.abs_apply, Rat.cast_lt, Rat.cast_abs, abs_sub_comm, Rat.cast_sub
-- Module: Mathlib.Topology.UniformSpace.CompareReals
Goal:
⊢ UniformSpace ℝ

Tactic:
infer_instance
-- Module: Mathlib.Topology.UniformSpace.CompareReals
Goal:
⊢ CompleteSpace ℝ

Tactic:
infer_instance
-- Module: Mathlib.Topology.UniformSpace.CompareReals
Goal:
⊢ T0Space ℝ

Tactic:
infer_instance
-- Module: Mathlib.Topology.UniformSpace.CompareReals
Goal:
rw : IsUniformInducing (β := ℝ) Rat.cast
⊢ IsUniformInducing (β := ℝ) Rat.cast

Tactic:
rw [Rat.uniformSpace_eq]

Premises used: Rat.uniformSpace_eq
-- Module: Mathlib.Topology.UniformSpace.CompareReals
Goal:
⊢ IsUniformInducing (β := ℝ) Rat.cast

Tactic:
Rat.isUniformEmbedding_coe_real.isUniformInducing

Premises used: IsUniformEmbedding.isUniformInducing, Rat.isUniformEmbedding_coe_real
-- Module: Mathlib.Topology.UniformSpace.CompareReals
Goal:
⊢ IsUniformInducing (β := ℝ) Rat.cast

Tactic:
exact Rat.isUniformEmbedding_coe_real.isUniformInducing

Premises used: IsUniformEmbedding.isUniformInducing, Rat.isUniformEmbedding_coe_real
-- Module: Mathlib.Topology.UniformSpace.CompareReals
Goal:
⊢ UniformContinuous (α := Bourbakiℝ) (β := ℝ) (⇑compareEquiv : (a : Bourbakiℝ) → ℝ)

Tactic:
bourbakiPkg.uniformContinuous_compareEquiv rationalCauSeqPkg

Premises used: CompareReals.Bourbakiℝ, AbstractCompletion.uniformContinuous_compareEquiv, CompareReals.bourbakiPkg, Quotient, SeparationQuotient, rationalCauSeqPkg, UniformSpace.Completion
-- Module: Mathlib.Topology.UniformSpace.CompareReals
Goal:
⊢ UniformContinuous (α := ℝ) (β := Bourbakiℝ) (⇑compareEquiv.symm : (a : ℝ) → Bourbakiℝ)

Tactic:
bourbakiPkg.uniformContinuous_compareEquiv_symm rationalCauSeqPkg

Premises used: CompareReals.Bourbakiℝ, CompareReals.bourbakiPkg, Quotient, SeparationQuotient, rationalCauSeqPkg, UniformSpace.Completion, AbstractCompletion.uniformContinuous_compareEquiv_symm
-- Module: Mathlib.Topology.UniformSpace.CompleteSeparated
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
⊢ Cauchy f

Tactic:
have : Cauchy f := cauchy_nhds.mono' ha inf_le_left
-- Module: Mathlib.Topology.UniformSpace.CompleteSeparated
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
this : Cauchy f
rcases : ∀ (y : α) (ys : y ∈ s) (fy : f ≤ 𝓝 y), a ∈ s
⊢ a ∈ s

Tactic:
rcases h f this inf_le_right with ⟨y, ys, fy⟩

Premises used: inf_le_right
-- Module: Mathlib.Topology.UniformSpace.CompleteSeparated
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
this : Cauchy f
y : α
ys : y ∈ s
fy : f ≤ 𝓝 y
rwa rwa₁ rwa₂ rwa₃ : y ∈ s
⊢ a ∈ s

Tactic:
rwa [(tendsto_nhds_unique' ha inf_le_left fy : a = y)]

Premises used: tendsto_nhds_unique', inf_le_left
-- Module: Mathlib.Topology.UniformSpace.CompleteSeparated
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace α
inst_3 : T0Space β
f : α → β
hf : IsUniformEmbedding f
⊢ IsClosedEmbedding f

Tactic:
⟨hf.isEmbedding, hf.isUniformInducing.isComplete_range.isClosed⟩

Premises used: IsComplete.isClosed, IsUniformEmbedding.isUniformInducing, IsUniformInducing.isComplete_range, IsUniformEmbedding.isEmbedding, Topology.IsClosedEmbedding.mk
-- Module: Mathlib.Topology.UniformSpace.CompleteSeparated
Goal:
α : Type u_1
inst : TopologicalSpace α
β : Type u_3
inst_1 : TopologicalSpace β
γ : Type u_4
inst_2 : UniformSpace γ
inst_3 : CompleteSpace γ
inst_4 : T0Space γ
e : α → β
f : α → γ
de : IsDenseInducing e
h : ∀ (b : β), Cauchy (map f (comap e (𝓝 b)))
⊢ Continuous[inst_1, inst_2.toTopologicalSpace] (de.extend f)

Tactic:
de.continuous_extend fun b => CompleteSpace.complete (h b)

Premises used: IsDenseInducing.continuous_extend, CompleteSpace.complete
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
β : Type v
γ : Type w
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : CauchyFilter α
⊢ (↑f : Filter α).NeBot

Tactic:
f.2.1

Premises used: And.left, Subtype.property
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
⊢ Monotone.{u, u} (α := SetRel α α) (β := SetRel (CauchyFilter α) (CauchyFilter α)) gen

Tactic:
monotone_setOf fun p => @Filter.monotone_mem _ (p.1.val ×ˢ p.2.val)

Premises used: Filter.monotone_mem, Set.monotone_setOf, CauchyFilter.gen
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
f : (s : SetRel α α) → Set (CauchyFilter α × CauchyFilter α) :=
  fun (s : SetRel α α) ↦ {p : CauchyFilter α × CauchyFilter α | s ∈ (↑p.2 : Filter α) ×ˢ (↑p.1 : Filter α)}
⊢ map Prod.swap
      ((𝓤 α).lift' fun (s : SetRel α α) ↦
        {p : CauchyFilter α × CauchyFilter α | s ∈ (↑p.1 : Filter α) ×ˢ (↑p.2 : Filter α)}) =
    (𝓤 α).lift' f

Tactic:
simp [f, map_lift'_eq, monotone_setOf, Filter.monotone_mem, Function.comp_def,
      image_swap_eq_preimage_swap]

Premises used: Set.image_swap_eq_preimage_swap, Filter.monotone_mem, Function.comp_def, Set.monotone_setOf, Filter.map_lift'_eq
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
f : (s : SetRel α α) → Set (CauchyFilter α × CauchyFilter α) :=
  fun (s : SetRel α α) ↦ {p : CauchyFilter α × CauchyFilter α | s ∈ (↑p.2 : Filter α) ×ˢ (↑p.1 : Filter α)}
⊢ map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f

Tactic:
have h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f := by
    delta gen
    simp [f, map_lift'_eq, monotone_setOf, Filter.monotone_mem, Function.comp_def,
      image_swap_eq_preimage_swap]
-- Module: Mathlib.Topology.UniformSpace.Completion
Goal:
α : Type u
inst : UniformSpace α
f : (s : SetRel α α) → Set (CauchyFilter α × CauchyFilter α) :=
  fun (s : SetRel α α) ↦ {p : CauchyFilter α × CauchyFilter α | s ∈ (↑p.2 : Filter α) ×ˢ (↑p.1 : Filter α)}
h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
⊢ ∀ (p : CauchyFilter α × CauchyFilter α),
    (↑p.2 : Filter α) ×ˢ (↑p.1 : Filter α) = map Prod.swap ((↑p.1 : Filter α) ×ˢ (↑p.2 : Filter α))

Tactic:
have h := fun p : CauchyFilter α × CauchyFilter α => @Filter.prod_comm _ _ p.2.val p.1.val