awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Ultrafilter (goal)
Goal:
X : Type u
x : X
inst : TopologicalSpace X
f : Filter X
simp_rw : (𝓝 x ⊓ f).NeBot ↔ ∃ (u : Ultrafilter X), (↑u : Filter X) ≤ f ∧ (↑u : Filter X) ≤ 𝓝 x
simp_rw₁ : (𝓝 x ⊓ f).NeBot ↔ ∃ (u : Ultrafilter X), (↑u : Filter X) ≤ f ⊓ 𝓝 x
⊢ ClusterPt x f ↔ ∃ (u : Ultrafilter X), (↑u : Filter X) ≤ f ∧ (↑u : Filter X) ≤ 𝓝 x
have simp_rw₂ : (𝓝 x ⊓ f).NeBot ↔ (f ⊓ 𝓝 x).NeBot
Tactic: simp_rw [ClusterPt, ← le_inf_iff, exists_ultrafilter_iff, inf_comm]
-- Lean 4 proof step from Mathlib.Topology.Ultrafilter (goal)
Goal:
X : Type u
α : Type u_1
x : X
inst : TopologicalSpace X
F : Filter α
u : α → X
⊢ MapClusterPt x F u ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
have simp_rw : ClusterPt x (map u F) ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
Tactic: simp_rw [MapClusterPt, ClusterPt, ← Filter.push_pull', map_neBot_iff, tendsto_iff_comap,
    ← le_inf_iff, exists_ultrafilter_iff, inf_comm]
-- Lean 4 proof step from Mathlib.Topology.Ultrafilter (goal)
Goal:
X : Type u
α : Type u_1
x : X
inst : TopologicalSpace X
F : Filter α
u : α → X
simp_rw : ClusterPt x (map u F) ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
⊢ MapClusterPt x F u ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
have simp_rw₁ : (𝓝 x ⊓ map u F).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
Tactic: simp_rw [MapClusterPt, ClusterPt, ← Filter.push_pull', map_neBot_iff, tendsto_iff_comap,
    ← le_inf_iff, exists_ultrafilter_iff, inf_comm]
-- Lean 4 proof step from Mathlib.Topology.Ultrafilter (goal)
Goal:
X : Type u
α : Type u_1
x : X
inst : TopologicalSpace X
F : Filter α
u : α → X
simp_rw : ClusterPt x (map u F) ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
simp_rw₁ : (𝓝 x ⊓ map u F).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
⊢ MapClusterPt x F u ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
have simp_rw₂ : (map u (comap u (𝓝 x) ⊓ F)).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
Tactic: simp_rw [MapClusterPt, ClusterPt, ← Filter.push_pull', map_neBot_iff, tendsto_iff_comap,
    ← le_inf_iff, exists_ultrafilter_iff, inf_comm]
-- Lean 4 proof step from Mathlib.Topology.Ultrafilter (goal)
Goal:
X : Type u
α : Type u_1
x : X
inst : TopologicalSpace X
F : Filter α
u : α → X
simp_rw : ClusterPt x (map u F) ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
simp_rw₁ : (𝓝 x ⊓ map u F).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
simp_rw₂ :
  (map u (comap u (𝓝 x) ⊓ F)).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
⊢ MapClusterPt x F u ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
have simp_rw₃ : (comap u (𝓝 x) ⊓ F).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
Tactic: simp_rw [MapClusterPt, ClusterPt, ← Filter.push_pull', map_neBot_iff, tendsto_iff_comap,
    ← le_inf_iff, exists_ultrafilter_iff, inf_comm]
-- Lean 4 proof step from Mathlib.Topology.Ultrafilter (goal)
Goal:
X : Type u
α : Type u_1
x : X
inst : TopologicalSpace X
F : Filter α
u : α → X
simp_rw : ClusterPt x (map u F) ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
simp_rw₁ : (𝓝 x ⊓ map u F).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
simp_rw₂ :
  (map u (comap u (𝓝 x) ⊓ F)).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
simp_rw₃ : (comap u (𝓝 x) ⊓ F).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
⊢ MapClusterPt x F u ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
have simp_rw₄ : (comap u (𝓝 x) ⊓ F).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ (↑U : Filter α) ≤ comap u (𝓝 x)
Tactic: simp_rw [MapClusterPt, ClusterPt, ← Filter.push_pull', map_neBot_iff, tendsto_iff_comap,
    ← le_inf_iff, exists_ultrafilter_iff, inf_comm]
-- Lean 4 proof step from Mathlib.Topology.Ultrafilter (goal)
Goal:
X : Type u
α : Type u_1
x : X
inst : TopologicalSpace X
F : Filter α
u : α → X
simp_rw : ClusterPt x (map u F) ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
simp_rw₁ : (𝓝 x ⊓ map u F).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
simp_rw₂ :
  (map u (comap u (𝓝 x) ⊓ F)).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
simp_rw₃ : (comap u (𝓝 x) ⊓ F).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
simp_rw₄ : (comap u (𝓝 x) ⊓ F).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ (↑U : Filter α) ≤ comap u (𝓝 x)
⊢ MapClusterPt x F u ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
have simp_rw₅ : (comap u (𝓝 x) ⊓ F).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ⊓ comap u (𝓝 x)
Tactic: simp_rw [MapClusterPt, ClusterPt, ← Filter.push_pull', map_neBot_iff, tendsto_iff_comap,
    ← le_inf_iff, exists_ultrafilter_iff, inf_comm]
-- Lean 4 proof step from Mathlib.Topology.Ultrafilter (goal)
Goal:
X : Type u
α : Type u_1
x : X
inst : TopologicalSpace X
F : Filter α
u : α → X
simp_rw : ClusterPt x (map u F) ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
simp_rw₁ : (𝓝 x ⊓ map u F).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
simp_rw₂ :
  (map u (comap u (𝓝 x) ⊓ F)).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
simp_rw₃ : (comap u (𝓝 x) ⊓ F).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
simp_rw₄ : (comap u (𝓝 x) ⊓ F).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ (↑U : Filter α) ≤ comap u (𝓝 x)
simp_rw₅ : (comap u (𝓝 x) ⊓ F).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ⊓ comap u (𝓝 x)
⊢ MapClusterPt x F u ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
have simp_rw₆ : (comap u (𝓝 x) ⊓ F).NeBot ↔ (F ⊓ comap u (𝓝 x)).NeBot
Tactic: simp_rw [MapClusterPt, ClusterPt, ← Filter.push_pull', map_neBot_iff, tendsto_iff_comap,
    ← le_inf_iff, exists_ultrafilter_iff, inf_comm]
-- Lean 4 proof step from Mathlib.Topology.Ultrafilter (goal)
Goal:
X : Type u
s : Set X
inst : TopologicalSpace X
⊢ IsOpen[inst] s ↔ ∀ x ∈ s, ∀ (l : Ultrafilter X), (↑l : Filter X) ≤ 𝓝 x → s ∈ l
have simp_rw : (∀ x ∈ s, s ∈ 𝓝 x) ↔ ∀ x ∈ s, ∀ (l : Ultrafilter X), (↑l : Filter X) ≤ 𝓝 x → s ∈ l
Tactic: simp_rw [isOpen_iff_mem_nhds, ← mem_iff_ultrafilter]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.AbstractCompletion (goal)
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
x : α
⊢ Inseparable (pkg.extend f (pkg.coe x)) (f x)
have rw : Inseparable (sorry.extend f (pkg.coe x)) (f x)
Tactic: rw [extend_def _ hf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.AbstractCompletion (goal)
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : T2Space β
hf : UniformContinuous f
a : α
⊢ pkg.extend f (pkg.coe a) = f a
have rw : sorry.extend f (pkg.coe a) = f a
Tactic: rw [pkg.extend_def hf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.AbstractCompletion (goal)
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
⊢ UniformContinuous (pkg.extend f)
have pos : ∀ (hf : UniformContinuous f), UniformContinuous (pkg.extend f)
Tactic: by_cases hf : UniformContinuous f
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.AbstractCompletion (goal)
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
pos : ∀ (hf : UniformContinuous f), UniformContinuous (pkg.extend f)
⊢ UniformContinuous (pkg.extend f)
have neg : ∀ (hf : ¬UniformContinuous f), UniformContinuous (pkg.extend f)
Tactic: by_cases hf : UniformContinuous f
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.AbstractCompletion (goal)
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
hf : UniformContinuous f
⊢ UniformContinuous (pkg.extend f)
have pos : UniformContinuous (sorry.extend f)
Tactic: rw [pkg.extend_def hf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.AbstractCompletion (goal)
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
hf : ¬UniformContinuous f
⊢ UniformContinuous (if UniformContinuous f then ⋯.extend f else fun (x : pkg.space) ↦ f (⋯.some x))
have neg : UniformContinuous.{vα, uβ} (β := β) fun (x : pkg.space) ↦ f (sorry.some x)
Tactic: rw [if_neg hf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.AbstractCompletion (goal)
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
h : IsUniformInducing f
⊢ IsUniformInducing (pkg.extend f)
have rw : IsUniformInducing (sorry.extend f)
Tactic: rw [extend_def _ h.uniformContinuous]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.AbstractCompletion (goal)
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
f : α → β
inst_2 : CompleteSpace β
inst_3 : T0Space β
hf : UniformContinuous f
g : pkg.space → β
hg : UniformContinuous g
h : ∀ (a : α), f a = g (pkg.coe a)
⊢ pkg.extend f = g
have apply : ∀ (a : α), pkg.extend f (pkg.coe a) = g (pkg.coe a)
Tactic: apply pkg.funext pkg.continuous_extend hg.continuous
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.AbstractCompletion (goal)
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
⊢ pkg.extend (pkg'.coe ∘ f) (pkg.coe a) = g (pkg.coe a)
have simp_rw : pkg.extend (fun (x : α) ↦ (g ∘ pkg.coe) x) (pkg.coe a) = (g ∘ pkg.coe) a
Tactic: simp_rw [Function.comp_def, h, ← comp_apply (f := g)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.AbstractCompletion (goal)
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
f : α → β
g : pkg.space → pkg'.space
hg : UniformContinuous g
h : ∀ (a : α), pkg'.coe (f a) = g (pkg.coe a)
a : α
⊢ pkg.extend (fun (x : α) ↦ (g ∘ pkg.coe) x) (pkg.coe a) = (g ∘ pkg.coe) a
have rw : (g ∘ pkg.coe) a = (g ∘ pkg.coe) a
Tactic: rw [pkg.extend_coe (hg.comp pkg.uniformContinuous_coe)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.AbstractCompletion (goal)
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst_2 : UniformSpace γ
inst_3 : CompleteSpace γ
inst_4 : T0Space γ
f : β → γ
g : α → β
hf : UniformContinuous f
hg : UniformContinuous g
a : α
⊢ (pkg'.extend f ∘ pkg.map pkg' g) (pkg.coe a) = pkg.extend (f ∘ g) (pkg.coe a)
have rw : f (g a) = (f ∘ g) a
Tactic: rw [pkg.extend_coe (hf.comp hg), comp_apply, pkg.map_coe pkg' hg, pkg'.extend_coe hf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.AbstractCompletion (hypothesis)
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
⊢ pkg.compare pkg' ∘ pkg'.compare pkg = id
have uc : UniformContinuous (pkg.compare pkg')
Tactic: have uc := pkg.uniformContinuous_compare pkg'
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.AbstractCompletion (hypothesis)
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
uc : UniformContinuous (pkg.compare pkg')
⊢ pkg.compare pkg' ∘ pkg'.compare pkg = id
have uc' : UniformContinuous (pkg'.compare pkg)
Tactic: have uc' := pkg'.uniformContinuous_compare pkg
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.AbstractCompletion (goal)
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
⊢ pkg.compare pkg' ∘ pkg'.compare pkg = id
have apply : ∀ (a : α), (pkg.compare pkg' ∘ pkg'.compare pkg) (pkg'.coe a) = id (pkg'.coe a)
Tactic: apply pkg'.funext (uc.comp uc').continuous continuous_id
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.AbstractCompletion (goal)
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
uc : UniformContinuous (pkg.compare pkg')
uc' : UniformContinuous (pkg'.compare pkg)
a : α
⊢ (pkg.compare pkg' ∘ pkg'.compare pkg) (pkg'.coe a) = id (pkg'.coe a)
have rw : pkg'.coe a = id (pkg'.coe a)
Tactic: rw [comp_apply, pkg'.compare_coe pkg, pkg.compare_coe pkg']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.AbstractCompletion (hypothesis)
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
γ : Type uγ
inst_1 : TopologicalSpace γ
inst_2 : T3Space γ
f : α → γ
cont_f : Continuous[inst.toTopologicalSpace, inst_1] f
x : UniformSpace pkg'.space := pkg'.uniformStruct
x_1 : UniformSpace pkg.space := pkg.uniformStruct
h : ∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))
⊢ ⋯.extend f ∘ pkg'.compare pkg = ⋯.extend f
have this : ∀ (x : α), (sorry.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x
Tactic: have (x : α) : (pkg.isDenseInducing.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x := by
    simp only [Function.comp_apply, compare_coe, IsDenseInducing.extend_eq _ cont_f]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.AbstractCompletion (goal)
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
γ : Type uγ
inst_1 : TopologicalSpace γ
inst_2 : T3Space γ
f : α → γ
cont_f : Continuous[inst.toTopologicalSpace, inst_1] f
x : UniformSpace pkg'.space := pkg'.uniformStruct
x_1 : UniformSpace pkg.space := pkg.uniformStruct
h : ∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))
this : ∀ (x : α), (⋯.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x
⊢ ⋯.extend f ∘ pkg'.compare pkg = ⋯.extend f
have apply : Continuous[_, inst_1] (sorry.extend f)
Tactic: apply (IsDenseInducing.extend_unique (AbstractCompletion.isDenseInducing _) this
    (Continuous.comp _ (uniformContinuous_compare pkg' pkg).continuous)).symm
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.AbstractCompletion (goal)
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
γ : Type uγ
inst_1 : TopologicalSpace γ
inst_2 : T3Space γ
f : α → γ
cont_f : Continuous[inst.toTopologicalSpace, inst_1] f
x : UniformSpace pkg'.space := pkg'.uniformStruct
x_1 : UniformSpace pkg.space := pkg.uniformStruct
h : ∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))
this : ∀ (x : α), (⋯.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x
⊢ Continuous[_, inst_1] (⋯.extend f)
have hf : ∀ (b : pkg.space), ∃ (c : γ), Tendsto f (comap pkg.coe (𝓝 b)) (𝓝 c)
Tactic: apply IsDenseInducing.continuous_extend
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.AbstractCompletion (goal)
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst_2 : UniformSpace γ
f : α → β → γ
inst_3 : CompleteSpace γ
⊢ UniformContinuous₂ (pkg.extend₂ pkg' f)
have rw : UniformContinuous ((pkg.prod pkg').extend (uncurry f))
Tactic: rw [uniformContinuous₂_def, AbstractCompletion.extend₂, uncurry_curry]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
⊢ UniformSpace.comap F (UniformFun.uniformSpace X α) = UniformSpace.comap F (Pi.uniformSpace fun (i : X) ↦ α)
have refine : UniformSpace.comap F (Pi.uniformSpace fun (i : X) ↦ α) ≤ UniformSpace.comap F (UniformFun.uniformSpace X α)
Tactic: refine le_antisymm (UniformSpace.comap_mono UniformFun.uniformContinuous_toFun) ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
⊢ UniformSpace.comap F (Pi.uniformSpace fun (i : X) ↦ α) ≤ UniformSpace.comap F (UniformFun.uniformSpace X α)
have simp_rw : ⨅ (i : X), comap (fun (x : ι × ι) ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α) ≤
  comap (Prod.map F F) (𝓤 (X → α))
Tactic: simp_rw [UniformSpace.comap, UniformSpace.le_def, uniformity_comap, Pi.uniformity,
    Filter.comap_iInf, comap_comap, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
⊢ ⨅ (i : X), comap (fun (x : ι × ι) ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α) ≤
    comap (Prod.map F F) (𝓤 (X → α))
have refine : ∀ i' ∈ 𝓤 α,
  Membership.mem (γ := Filter (ι × ι))
    (⨅ (i : X), comap (fun (x : ι × ι) ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α))
    (Prod.map F F ⁻¹' UniformFun.gen X α i')
Tactic: refine ((UniformFun.hasBasis_uniformity X α).comap (Prod.map F F)).ge_iff.mpr ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ Membership.mem (γ := Filter (ι × ι))
    (⨅ (i : X), comap (fun (x : ι × ι) ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α))
    (Prod.map F F ⁻¹' UniformFun.gen X α U)
have rcases : ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (Vsymm : SetRel.IsSymm V) (hVU : (SetRel.comp V V).comp V ⊆ U),
  Membership.mem (γ := Filter (ι × ι))
    (⨅ (i : X), comap (fun (x : ι × ι) ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α))
    (Prod.map F F ⁻¹' UniformFun.gen X α U)
Tactic: rcases comp_comp_symm_mem_uniformity_sets hU with ⟨V, hV, Vsymm, hVU⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : (x : X) → Set X := fun (x : X) ↦ {y : X | ∀ (i : ι), (F i x, F i y) ∈ V}
⊢ Membership.mem (γ := Filter (ι × ι))
    (⨅ (i : X), comap (fun (x : ι × ι) ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α))
    (Prod.map F F ⁻¹' UniformFun.gen X α U)
have rcases : ∀ (A : Finset X) (Acover : Eq.{u_2 + 1} (α := Set X) (⋃ x ∈ A, Ω x) ⊤),
  Membership.mem (γ := Filter (ι × ι))
    (⨅ (i : X), comap (fun (x : ι × ι) ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α))
    (Prod.map F F ⁻¹' UniformFun.gen X α U)
Tactic: rcases CompactSpace.elim_nhds_subcover Ω (fun x ↦ F_eqcont x V hV) with ⟨A, Acover⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : (x : X) → Set X := fun (x : X) ↦ {y : X | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : Eq.{u_2 + 1} (α := Set X) (⋃ x ∈ A, Ω x) ⊤
i j : ι
hij : Membership.mem (γ := Set (ι × ι)) (⋂ a ∈ A, {ij : ι × ι | (F ij.1 a, F ij.2 a) ∈ V}) (i, j)
x : X
⊢ Membership.mem (α := α × α) U
    (((UniformFun.toFun : (a : X →ᵤ α) → X → α) (Prod.map F F (i, j)).1 x,
        (UniformFun.toFun : (a : X →ᵤ α) → X → α) (Prod.map F F (i, j)).2 x) :
      α × α)
have rw : ∀
  (hij :
    ∀ (i_1 : X) (j_1 : i_1 ∈ A), Membership.mem (γ := Set (ι × ι)) {ij : ι × ι | (F ij.1 i_1, F ij.2 i_1) ∈ V} (i, j))
  (x : X),
  Membership.mem (α := α × α) U
    (((UniformFun.toFun : (a : X →ᵤ α) → X → α) (Prod.map F F (i, j)).1 x,
        (UniformFun.toFun : (a : X →ᵤ α) → X → α) (Prod.map F F (i, j)).2 x) :
      α × α)
Tactic: rw [mem_iInter₂] at hij
Cleared hypotheses: hij, x
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : (x : X) → Set X := fun (x : X) ↦ {y : X | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : Eq.{u_2 + 1} (α := Set X) (⋃ x ∈ A, Ω x) ⊤
i j : ι
hij : ∀ (i_1 : X) (j_1 : i_1 ∈ A), Membership.mem (γ := Set (ι × ι)) {ij : ι × ι | (F ij.1 i_1, F ij.2 i_1) ∈ V} (i, j)
x : X
⊢ Membership.mem (α := α × α) U
    (((UniformFun.toFun : (a : X →ᵤ α) → X → α) (Prod.map F F (i, j)).1 x,
        (UniformFun.toFun : (a : X →ᵤ α) → X → α) (Prod.map F F (i, j)).2 x) :
      α × α)
have rcases : ∀ (a : X) (ha : a ∈ A) (hax : x ∈ Ω a),
  Membership.mem (α := α × α) U
    (((UniformFun.toFun : (a : X →ᵤ α) → X → α) (Prod.map F F (i, j)).1 x,
        (UniformFun.toFun : (a : X →ᵤ α) → X → α) (Prod.map F F (i, j)).2 x) :
      α × α)
Tactic: rcases mem_iUnion₂.mp (Acover.symm.subset <| mem_univ x) with ⟨a, ha, hax⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : (x : X) → Set X := fun (x : X) ↦ {y : X | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : Eq.{u_2 + 1} (α := Set X) (⋃ x ∈ A, Ω x) ⊤
⊢ Membership.mem (γ := Filter (ι × ι))
    (⨅ (i : X), comap (fun (x : ι × ι) ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α))
    (Prod.map F F ⁻¹' UniformFun.gen X α U)
have this : ⋂ a ∈ A, {ij : ι × ι | (F ij.1 a, F ij.2 a) ∈ V} ⊆ Prod.map F F ⁻¹' UniformFun.gen X α U
Tactic: have : (⋂ a ∈ A, {ij : ι × ι | (F ij.1 a, F ij.2 a) ∈ V}) ⊆
      (Prod.map F F) ⁻¹' UniformFun.gen X α U := by
    -- Given `(i, j) ∈ ⋂ a ∈ A, 𝐒(V, a)` and `x : X`, we have to prove that `(F i x, F j x) ∈ U`.
    rintro ⟨i, j⟩ hij x
    rw [mem_iInter₂] at hij
    -- We know that `x ∈ Ω a` for some `a ∈ A`, so that both `(F i x, F i a)` and `(F j a, F j x)`
    -- are in `V`.
    rcases mem_iUnion₂.mp (Acover.symm.subset <| mem_univ x) with ⟨a, ha, hax⟩
    -- Since `(i, j) ∈ 𝐒(V, a)` we also have `(F i a, F j a) ∈ V`, and finally we get
    -- `(F i x, F j x) ∈ V ○ V ○ V ⊆ U`.
    exact hVU <| SetRel.prodMk_mem_comp (SetRel.prodMk_mem_comp (SetRel.symm V <| hax i) (hij a ha))
      (hax j)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : UniformSpace ι
inst_3 : CompactSpace X
F_eqcont : Equicontinuous F
⊢ IsUniformInducing (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F) ↔ IsUniformInducing F
have rw : UniformSpace.comap ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F) (UniformFun.uniformSpace X α) = inst_2 ↔
  UniformSpace.comap F (UniformFun.uniformSpace X α) = inst_2
Tactic: rw [isUniformInducing_iff_uniformSpace, isUniformInducing_iff_uniformSpace,
      ← F_eqcont.comap_uniformFun_eq]