awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
l : Filter ι
inst : l.NeBot
F : ι → β → α
f : β → α
h₁ : Tendsto F l (𝓝 f)
h₂ : UniformEquicontinuous F
⊢ UniformContinuous f
have rw : ∀ (h₁ : ∀ (x : β), Tendsto (fun (i : ι) ↦ F i x) l (𝓝 (f x))) (h₂ : UniformEquicontinuousOn F univ),
  UniformContinuousOn f univ
Tactic: rw [← uniformContinuousOn_univ, ← uniformEquicontinuousOn_univ, tendsto_pi_nhds] at *
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : Tendsto f (𝓝[s] x) (𝓝 z)
hs : ∀ y ∈ s, Tendsto (fun (x : ι) ↦ F x y) l (𝓝 (f y))
hx : x ∈ closure[tX] s
⊢ Tendsto (fun (x_1 : ι) ↦ F x_1 x) l (𝓝 z)
have rw : ∀ (hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id i} (f x))
  (hs : ∀ y ∈ s, Tendsto (fun (x : ι) ↦ F x y) l (𝓝 (f y))) (hx : x ∈ closure[tX] s),
  ∀ i ∈ 𝓤 α, ∀ᶠ (x_1 : ι) in l, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id i} (F x_1 x)
Tactic: rw [(nhds_basis_uniformity (𝓤 α).basis_sets).tendsto_right_iff] at hf ⊢
Cleared hypotheses: hf, hs, hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id i} (f x)
hs : ∀ y ∈ s, Tendsto (fun (x : ι) ↦ F x y) l (𝓝 (f y))
hx : x ∈ closure[tX] s
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ∀ᶠ (x_1 : ι) in l, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id U} (F x_1 x)
have rcases : ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVs : SetRel.IsSymm V) (hVU : (SetRel.comp V V).comp V ⊆ U),
  ∀ᶠ (x_1 : ι) in l, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id U} (F x_1 x)
Tactic: rcases comp_comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVs, hVU⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id i} (f x)
hs : ∀ y ∈ s, Tendsto (fun (x : ι) ↦ F x y) l (𝓝 (f y))
hx : x ∈ closure[tX] s
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
⊢ ∀ᶠ (x_1 : ι) in l, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id U} (F x_1 x)
have rw : ∀ (hx : (𝓝[s] x).NeBot) (U : Set (α × α)) (hU : U ∈ 𝓤 α) (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVs : SetRel.IsSymm V)
  (hVU : (SetRel.comp V V).comp V ⊆ U), ∀ᶠ (x_1 : ι) in l, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id U} (F x_1 x)
Tactic: rw [mem_closure_iff_nhdsWithin_neBot] at hx
Cleared hypotheses: hx, U, hU, V, hV, hVs, hVU
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (hypothesis)
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id i} (f x)
hs : ∀ y ∈ s, Tendsto (fun (x : ι) ↦ F x y) l (𝓝 (f y))
hx : (𝓝[s] x).NeBot
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
⊢ ∀ᶠ (x_1 : ι) in l, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id U} (F x_1 x)
have this : ∀ᶠ (y : X) in 𝓝[s] x, y ∈ s ∧ (∀ (i : ι), (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V
Tactic: have : ∀ᶠ y in 𝓝[s] x, y ∈ s ∧ (∀ i, (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V :=
    eventually_mem_nhdsWithin.and <| ((hF V hV).filter_mono nhdsWithin_le_nhds).and (hf V hV)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id i} (f x)
hs : ∀ y ∈ s, Tendsto (fun (x : ι) ↦ F x y) l (𝓝 (f y))
hx : (𝓝[s] x).NeBot
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
this : ∀ᶠ (y : X) in 𝓝[s] x, y ∈ s ∧ (∀ (i : ι), (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V
⊢ ∀ᶠ (x_1 : ι) in l, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id U} (F x_1 x)
have rcases : ∀ (y : X) (hys : y ∈ s) (hFy : ∀ (i : ι), (F i x, F i y) ∈ V) (hfy : (f y, z) ∈ V),
  ∀ᶠ (x_1 : ι) in l, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id U} (F x_1 x)
Tactic: rcases this.exists with ⟨y, hys, hFy, hfy⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equicontinuity (goal)
Goal:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id i} (f x)
hs : ∀ y ∈ s, Tendsto (fun (x : ι) ↦ F x y) l (𝓝 (f y))
hx : (𝓝[s] x).NeBot
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
this : ∀ᶠ (y : X) in 𝓝[s] x, y ∈ s ∧ (∀ (i : ι), (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V
y : X
hys : y ∈ s
hFy : ∀ (i : ι), (F i x, F i y) ∈ V
hfy : (f y, z) ∈ V
⊢ ∀ᶠ (x_1 : ι) in l, Membership.mem (γ := Set α) {y : α | (y, z) ∈ id U} (F x_1 x)
have h : ∀ (i : ι) (hi : Membership.mem (γ := Set ι) ((fun (x : ι) ↦ F x y) ⁻¹' ball (f y) V) i), (F i x, z) ∈ id U
Tactic: filter_upwards [hs y hys (ball_mem_nhds _ hV)] with i hi
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equiv (goal)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
f : α ≃ᵤ β
g : β → α
hg : Function.RightInverse g (⇑f : (a : α) → β)
x : β
⊢ Eq.{u + 1} (α := α) ((f.symm : (a : β) → α) ((f : (a : α) → β) (g x) : β) : α) ((f.symm : (a : β) → α) x : α)
have rw : Eq.{u + 1} (α := α) ((f.symm : (a : β) → α) x : α) ((f.symm : (a : β) → α) x : α)
Tactic: rw [hg x]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equiv (goal)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
f : α → β
hf : IsUniformEmbedding f
⊢ UniformContinuous (Equiv.ofInjective f ⋯).invFun
have rw : UniformContinuous.{u_1, u_1} (α := (↑(range f) : Type u_1)) (Subtype.val (p := fun (x : β) ↦ x ∈ range f))
Tactic: rw [hf.isUniformInducing.uniformContinuous_iff, Equiv.invFun_as_coe,
      Equiv.self_comp_ofInjective_symm]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equiv (hypothesis)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
⊢ UniformContinuous (α := α) (Equiv.invFun Equiv.ulift)
have hf : IsUniformInducing (α := ULift.{v, u} α) (Equiv.toFun Equiv.ulift)
Tactic: have hf : IsUniformInducing (@Equiv.ulift.{v, u} α).toFun := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Equiv (goal)
Goal:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : UniformSpace δ
hf : IsUniformInducing (α := ULift.{v, u} α) (Equiv.toFun Equiv.ulift)
⊢ UniformContinuous (α := α) (Equiv.invFun Equiv.ulift)
have simp_rw : UniformContinuous.{u, u} (α := α) (Equiv.toFun Equiv.ulift ∘ Equiv.invFun Equiv.ulift)
Tactic: simp_rw [hf.uniformContinuous_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : CompactSpace α
f : α → β
h : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
⊢ map (Prod.map f f) (𝓤 α) = map (Prod.map f f) (𝓝ˢ (diagonal α))
have rw : map (Prod.map f f) (𝓤 α) = map (Prod.map f f) (𝓤 α)
Tactic: rw [nhdsSet_diagonal_eq_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
⊢ UniformContinuousOn f s
have rw : UniformContinuous (s.restrict (π := fun (a : α) ↦ β) f)
Tactic: rw [uniformContinuousOn_iff_restrict]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
⊢ UniformContinuous (s.restrict (π := fun (a : α) ↦ β) f)
have hs₁ : CompactSpace.{u_1} (↑s : Type u_1)
Tactic: rw [isCompact_iff_compactSpace] at hs
Cleared hypotheses: hs, hf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
s : Set α
f : α → β
hs : CompactSpace.{u_1} (↑s : Type u_1)
hf : ContinuousOn f s
⊢ UniformContinuous (s.restrict (π := fun (a : α) ↦ β) f)
have hf₁ : Continuous[instTopologicalSpaceSubtype, inst_1.toTopologicalSpace] (s.restrict (π := fun (a : α) ↦ β) f)
Tactic: rw [continuousOn_iff_continuous_restrict] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ a ∈ s, ContinuousAt f a
hr : r ∈ 𝓤 β
⊢ {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α
have obtain : ∀ (t : Set (β × β)) (ht : t ∈ 𝓤 β) (htsymm : SetRel.IsSymm t) (htr : SetRel.comp t t ⊆ r),
  {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α
Tactic: obtain ⟨t, ht, htsymm, htr⟩ := comp_symm_mem_uniformity_sets hr
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ a ∈ s, ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
⊢ {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α
have choose : ∀ (U : (a : α) → (ha : a ∈ s) → Set α) (hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a)
  (T : (a : α) → (ha : a ∈ s) → Set (α × α)) (hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α)
  (hb : ∀ (a : α) (ha : a ∈ s), ∀ a' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y : β | (f a, y) ∈ t}),
  {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α
Tactic: choose U hU T hT hb using fun a ha =>
    exists_mem_nhds_ball_subset_of_mem_nhds ((hf a ha).preimage_mem_nhds <| mem_nhds_left _ ht)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ a ∈ s, ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
U : (a : α) → (ha : a ∈ s) → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → (ha : a ∈ s) → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s), ∀ a' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y : β | (f a, y) ∈ t}
⊢ {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α
have obtain : ∀ (fs : Finset (↑s : Type u_1)) (hsU : s ⊆ ⋃ x ∈ fs, U (↑x : α) sorry), {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α
Tactic: obtain ⟨fs, hsU⟩ := hs.elim_nhds_subcover' U hU
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ a ∈ s, ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
U : (a : α) → (ha : a ∈ s) → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → (ha : a ∈ s) → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s), ∀ a' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y : β | (f a, y) ∈ t}
fs : Finset (↑s : Type u_1)
hsU : s ⊆ ⋃ x ∈ fs, U (↑x : α) ⋯
⊢ {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ 𝓤 α
have apply : Subset.{u_1} (α := Set (α × α)) (⋂ i ∈ fs, T (↑i : α) sorry) {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ r}
Tactic: apply mem_of_superset ((biInter_finset_mem fs).2 fun a _ => hT a a.2)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ a ∈ s, ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
U : (a : α) → (ha : a ∈ s) → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → (ha : a ∈ s) → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s), ∀ a' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y : β | (f a, y) ∈ t}
fs : Finset (↑s : Type u_1)
hsU : s ⊆ ⋃ x ∈ fs, U (↑x : α) ⋯
a₁ a₂ : α
h : Membership.mem (γ := Set (α × α)) (⋂ i ∈ fs, T (↑i : α) ⋯) (a₁, a₂)
h₁ : (a₁, a₂).1 ∈ s
⊢ (f (a₁, a₂).1, f (a₁, a₂).2) ∈ r
have obtain : ∀ (a : (↑s : Type u_1)) (ha : a ∈ fs) (haU : (a₁, a₂).1 ∈ U (↑a : α) sorry), (f (a₁, a₂).1, f (a₁, a₂).2) ∈ r
Tactic: obtain ⟨a, ha, haU⟩ := Set.mem_iUnion₂.1 (hsU h₁)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ a ∈ s, ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
U : (a : α) → (ha : a ∈ s) → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → (ha : a ∈ s) → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s), ∀ a' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y : β | (f a, y) ∈ t}
fs : Finset (↑s : Type u_1)
hsU : s ⊆ ⋃ x ∈ fs, U (↑x : α) ⋯
a₁ a₂ : α
h : Membership.mem (γ := Set (α × α)) (⋂ i ∈ fs, T (↑i : α) ⋯) (a₁, a₂)
h₁ : (a₁, a₂).1 ∈ s
a : (↑s : Type u_1)
ha : a ∈ fs
haU : (a₁, a₂).1 ∈ U (↑a : α) ⋯
⊢ (f (a₁, a₂).1, f (a₁, a₂).2) ∈ r
have a₃ : (f (a₁, a₂).1, f (a₁, a₂).2) ∈ SetRel.comp t t
Tactic: apply htr
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ a ∈ s, ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
U : (a : α) → (ha : a ∈ s) → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → (ha : a ∈ s) → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s), ∀ a' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y : β | (f a, y) ∈ t}
fs : Finset (↑s : Type u_1)
hsU : s ⊆ ⋃ x ∈ fs, U (↑x : α) ⋯
a₁ a₂ : α
h : Membership.mem (γ := Set (α × α)) (⋂ i ∈ fs, T (↑i : α) ⋯) (a₁, a₂)
h₁ : (a₁, a₂).1 ∈ s
a : (↑s : Type u_1)
ha : a ∈ fs
haU : (a₁, a₂).1 ∈ U (↑a : α) ⋯
⊢ (f (a₁, a₂).1, f (a₁, a₂).2) ∈ SetRel.comp t t
have a₃ : (a₁, a₂).1 ∈ ball (a₁, a₂).1 (T (↑a : α) sorry)
Tactic: refine ⟨f a, SetRel.symm t <| hb _ _ _ haU ?_, hb _ _ _ haU ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
r : Set (β × β)
s : Set α
hs : IsCompact s
f : α → β
hf : ∀ a ∈ s, ContinuousAt f a
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
U : (a : α) → (ha : a ∈ s) → Set α
hU : ∀ (a : α) (ha : a ∈ s), U a ha ∈ 𝓝 a
T : (a : α) → (ha : a ∈ s) → Set (α × α)
hT : ∀ (a : α) (ha : a ∈ s), T a ha ∈ 𝓤 α
hb : ∀ (a : α) (ha : a ∈ s), ∀ a' ∈ U a ha, ball a' (T a ha) ⊆ f ⁻¹' {y : β | (f a, y) ∈ t}
fs : Finset (↑s : Type u_1)
hsU : s ⊆ ⋃ x ∈ fs, U (↑x : α) ⋯
a₁ a₂ : α
h : Membership.mem (γ := Set (α × α)) (⋂ i ∈ fs, T (↑i : α) ⋯) (a₁, a₂)
h₁ : (a₁, a₂).1 ∈ s
a : (↑s : Type u_1)
ha : a ∈ fs
haU : (a₁, a₂).1 ∈ U (↑a : α) ⋯
a₃ : (a₁, a₂).1 ∈ ball (a₁, a₂).1 (T (↑a : α) ⋯)
⊢ (f (a₁, a₂).1, f (a₁, a₂).2) ∈ SetRel.comp t t
have a₄ : (a₁, a₂).2 ∈ ball (a₁, a₂).1 (T (↑a : α) sorry)
Tactic: refine ⟨f a, SetRel.symm t <| hb _ _ _ haU ?_, hb _ _ _ haU ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
⊢ {x : α × α | (f x.1, f x.2) ∈ r} ∈ 𝓤 α
have obtain : ∀ (t : Set (β × β)) (ht : t ∈ 𝓤 β) (htsymm : SetRel.IsSymm t) (htr : SetRel.comp t t ⊆ r),
  {x : α × α | (f x.1, f x.2) ∈ r} ∈ 𝓤 α
Tactic: obtain ⟨t, ht, htsymm, htr⟩ := comp_symm_mem_uniformity_sets hr
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
⊢ {x : α × α | (f x.1, f x.2) ∈ r} ∈ 𝓤 α
have obtain : ∀ (s : Set α) (hs : IsCompact s) (hst : sᶜ ⊆ f ⁻¹' {y : β | (x, y) ∈ t}), {x : α × α | (f x.1, f x.2) ∈ r} ∈ 𝓤 α
Tactic: obtain ⟨s, hs, hst⟩ := mem_cocompact.1 (hx <| mem_nhds_left _ ht)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y : β | (x, y) ∈ t}
⊢ {x : α × α | (f x.1, f x.2) ∈ r} ∈ 𝓤 α
have f₁ : Subset.{u_1} (α := Set (α × α)) (SetRel.symmetrize {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r})
  {x : α × α | (f x.1, f x.2) ∈ r}
Tactic: apply
      mem_of_superset
        (symmetrize_mem_uniformity <|
          (hs.uniformContinuousAt_of_continuousAt f fun _ _ => h_cont.continuousAt) <|
            symmetrize_mem_uniformity hr)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y : β | (x, y) ∈ t}
b₁ b₂ : α
h :
  Membership.mem (γ := Set (α × α)) (SetRel.symmetrize {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r})
    (b₁, b₂)
⊢ Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)
have pos : ∀ (h₁ : b₁ ∈ s), Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)
Tactic: by_cases h₁ : b₁ ∈ s
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y : β | (x, y) ∈ t}
b₁ b₂ : α
h :
  Membership.mem (γ := Set (α × α)) (SetRel.symmetrize {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r})
    (b₁, b₂)
pos : ∀ (h₁ : b₁ ∈ s), Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)
⊢ Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)
have neg : ∀ (h₁ : b₁ ∉ s), Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)
Tactic: by_cases h₁ : b₁ ∈ s
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y : β | (x, y) ∈ t}
b₁ b₂ : α
h :
  Membership.mem (γ := Set (α × α)) (SetRel.symmetrize {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r})
    (b₁, b₂)
h₁ : b₁ ∉ s
⊢ Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)
have pos : ∀ (h₂ : b₂ ∈ s), Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)
Tactic: by_cases h₂ : b₂ ∈ s
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y : β | (x, y) ∈ t}
b₁ b₂ : α
h :
  Membership.mem (γ := Set (α × α)) (SetRel.symmetrize {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r})
    (b₁, b₂)
h₁ : b₁ ∉ s
pos : ∀ (h₂ : b₂ ∈ s), Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)
⊢ Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)
have neg : ∀ (h₂ : b₂ ∉ s), Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)
Tactic: by_cases h₂ : b₂ ∈ s
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
x : β
h_cont : Continuous[inst.toTopologicalSpace, inst_1.toTopologicalSpace] f
hx : Tendsto f (cocompact α) (𝓝 x)
r : Set (β × β)
hr : r ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : SetRel.IsSymm t
htr : SetRel.comp t t ⊆ r
s : Set α
hs : IsCompact s
hst : sᶜ ⊆ f ⁻¹' {y : β | (x, y) ∈ t}
b₁ b₂ : α
h :
  Membership.mem (γ := Set (α × α)) (SetRel.symmetrize {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ SetRel.symmetrize r})
    (b₁, b₂)
h₁ : b₁ ∉ s
h₂ : b₂ ∉ s
⊢ Membership.mem (γ := Set (α × α)) {x : α × α | (f x.1, f x.2) ∈ r} (b₁, b₂)
have neg : (f (b₁, b₂).1, f (b₁, b₂).2) ∈ SetRel.comp t t
Tactic: apply htr
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : LocallyCompactSpace α
inst_3 : CompactSpace β
inst_4 : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (SProd.sprod (β := Set β) U univ)
⊢ TendstoUniformly f (f x) (𝓝 x)
have rcases : ∀ (K : Set α) (hxK : K ∈ 𝓝 x) (hKU : K ⊆ U) (hK : IsCompact K), TendstoUniformly f (f x) (𝓝 x)
Tactic: rcases LocallyCompactSpace.local_compact_nhds _ _ hxU with ⟨K, hxK, hKU, hK⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.HeineCantor (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : LocallyCompactSpace α
inst_3 : CompactSpace β
inst_4 : UniformSpace γ
f : α → β → γ
x : α
U : Set α
hxU : U ∈ 𝓝 x
h : ContinuousOn (↿f) (SProd.sprod (β := Set β) U univ)
K : Set α
hxK : K ∈ 𝓝 x
hKU : K ⊆ U
hK : IsCompact K
⊢ TendstoUniformly f (f x) (𝓝 x)
have this : UniformContinuousOn (↿f) (SProd.sprod (β := Set β) K univ)
Tactic: have : UniformContinuousOn ↿f (K ×ˢ univ) :=
    IsCompact.uniformContinuousOn_of_continuous (hK.prod isCompact_univ)
      (h.mono <| prod_mono hKU Subset.rfl)