awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
⊢ U ∈ 𝓝ˢ K ↔ ∃ (i : ι), p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U
have mp : U ∈ 𝓝ˢ K → ∃ (i : ι), p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
mp : U ∈ 𝓝ˢ K → ∃ (i : ι), p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U
⊢ U ∈ 𝓝ˢ K ↔ ∃ (i : ι), p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U
have mpr : (∃ (i : ι), p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U) → U ∈ 𝓝ˢ K
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (hypothesis)
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
H : U ∈ 𝓝ˢ K
⊢ ∃ (i : ι), p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U
have HKU : K ⊆ ⋃ (x : Unit), interior U
Tactic: have HKU : K ⊆ ⋃ _ : Unit, interior U := by
        simpa only [iUnion_const, subset_interior_iff_mem_nhdsSet] using H
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
H : U ∈ 𝓝ˢ K
HKU : K ⊆ ⋃ (x : Unit), interior U
⊢ ∃ (i : ι), p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U
have mp : ∀ (i : ι) (hpi : p i) (hi : ⋃ x ∈ K, ball x (V i) ⊆ interior U), ∃ (i : ι), p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U
Tactic: obtain ⟨i, hpi, hi⟩ : ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ interior U := by
        simpa using hbasis.lebesgue_number_lemma hK (fun _ ↦ isOpen_interior) HKU
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
i : ι
hpi : p i
hi : ⋃ x ∈ K, ball x (V i) ⊆ U
⊢ U ∈ 𝓝ˢ K
have mpr : ∀ x ∈ K, ball x (V i) ∈ 𝓝 x
Tactic: refine mem_of_superset (bUnion_mem_nhdsSet fun x _ ↦ ?_) hi
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (hypothesis)
Goal:
α : Type ua
inst : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
⊢ ∃ V ∈ 𝓤 α, Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
have this : Bᶜ ∈ 𝓝ˢ A
Tactic: have : Bᶜ ∈ 𝓝ˢ A := hB.isOpen_compl.mem_nhdsSet.mpr h.le_compl_right
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (hypothesis)
Goal:
α : Type ua
inst : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
this : Bᶜ ∈ 𝓝ˢ A
⊢ ∃ V ∈ 𝓤 α, Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
have this₁ : ∃ i ∈ 𝓤 α, ⋃ x ∈ A, ball x (id i) ⊆ Bᶜ
Tactic: rw [(hA.nhdsSet_basis_uniformity (Filter.basis_sets _)).mem_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
inst : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
this : ∃ i ∈ 𝓤 α, ⋃ x ∈ A, ball x (id i) ⊆ Bᶜ
⊢ ∃ V ∈ 𝓤 α, Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
have rcases : ∀ (U : Set (α × α)) (hU : U ∈ 𝓤 α) (hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ),
  ∃ V ∈ 𝓤 α, Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
Tactic: rcases this with ⟨U, hU, hUAB⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
inst : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ
⊢ ∃ V ∈ 𝓤 α, Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
have rcases : ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVsymm : SetRel.IsSymm V) (hVU : V ○ V ⊆ U),
  ∃ V ∈ 𝓤 α, Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
Tactic: rcases comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVsymm, hVU⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
inst : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : V ○ V ⊆ U
⊢ ∃ V ∈ 𝓤 α, Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
have refine : ∀ (x : α), Membership.mem (γ := Set α) (⋃ x ∈ A, ball x V) x → x ∉ ⋃ x ∈ B, ball x V
Tactic: refine ⟨V, hV, Set.disjoint_left.mpr fun x => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
inst : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : V ○ V ⊆ U
x : α
⊢ Membership.mem (γ := Set α) (⋃ x ∈ A, ball x V) x → x ∉ ⋃ x ∈ B, ball x V
have simp : (∃ (i : α) (_ : i ∈ A), x ∈ ball i V) → ¬∃ (i : α) (_ : i ∈ B), x ∈ ball i V
Tactic: simp only [mem_iUnion₂]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
inst : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : V ○ V ⊆ U
x a : α
ha : a ∈ A
hxa : x ∈ ball a V
b : α
hb : b ∈ B
hxb : x ∈ ball b V
⊢ False
have rw : ∀ (hxa : a ∈ ball x V) (b : α) (hb : b ∈ B) (hxb : b ∈ ball x V), False
Tactic: rw [mem_ball_symmetry] at hxa hxb
Cleared hypotheses: hxa, b, hb, hxb
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : (𝓤 α).HasBasis p s
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
⊢ ∃ (i : ι), p i ∧ Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))
have rcases : ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVAB : Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)),
  ∃ (i : ι), p i ∧ Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))
Tactic: rcases h.exists_uniform_thickening hA hB with ⟨V, hV, hVAB⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : (𝓤 α).HasBasis p s
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
V : Set (α × α)
hV : V ∈ 𝓤 α
hVAB : Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
⊢ ∃ (i : ι), p i ∧ Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))
have rcases : ∀ (i : ι) (hi : p i) (hiV : s i ⊆ V),
  ∃ (i : ι), p i ∧ Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))
Tactic: rcases hU.mem_iff.1 hV with ⟨i, hi, hiV⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
inst : UniformSpace α
inst_1 : CompactSpace α
⊢ 𝓝ˢ (diagonal α) = 𝓤 α
have refine : 𝓤 α ≤ 𝓝ˢ (diagonal α)
Tactic: refine nhdsSet_diagonal_le_uniformity.antisymm ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
inst : UniformSpace α
inst_1 : CompactSpace α
⊢ HasBasis (α := (α × α) × α × α) (𝓤 (α × α)) (fun (U : Set (α × α)) ↦ U ∈ 𝓤 α) fun (U : Set (α × α)) ↦
    (fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U
have rw : HasBasis (α := (α × α) × α × α) (Filter.comap (fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 α))
  (fun (U : Set (α × α)) ↦ U ∈ 𝓤 α) fun (U : Set (α × α)) ↦
  (fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U
Tactic: rw [uniformity_prod_eq_comap_prod]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (hypothesis)
Goal:
α : Type ua
inst : UniformSpace α
inst_1 : CompactSpace α
⊢ 𝓤 α ≤ 𝓝ˢ (diagonal α)
have this : HasBasis (α := (α × α) × α × α) (𝓤 (α × α)) (fun (U : Set (α × α)) ↦ U ∈ 𝓤 α) fun (U : Set (α × α)) ↦
  (fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U
Tactic: have :
    (𝓤 (α × α)).HasBasis (fun U => U ∈ 𝓤 α) fun U =>
      (fun p : (α × α) × α × α => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U := by
    rw [uniformity_prod_eq_comap_prod]
    exact (𝓤 α).basis_sets.prod_self.comap _
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
inst : UniformSpace α
inst_1 : CompactSpace α
this :
  HasBasis (α := (α × α) × α × α) (𝓤 (α × α)) (fun (U : Set (α × α)) ↦ U ∈ 𝓤 α) fun (U : Set (α × α)) ↦
    (fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U
⊢ 𝓤 α ≤ 𝓝ˢ (diagonal α)
have refine : ∀ (U : Set (α × α)) (hU : U ∈ 𝓤 α),
  ⋃ x ∈ diagonal α, ball x ((fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U) ∈ 𝓤 α
Tactic: refine (isCompact_diagonal.nhdsSet_basis_uniformity this).ge_iff.2 fun U hU => ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
γ : Type uc
t : TopologicalSpace γ
inst : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
⊢ u = u'
have refine : 𝓤 γ = 𝓤 γ
Tactic: refine UniformSpace.ext ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (hypothesis)
Goal:
γ : Type uc
t : TopologicalSpace γ
inst : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
⊢ 𝓤 γ = 𝓤 γ
have this : CompactSpace γ
Tactic: have : @CompactSpace γ u.toTopologicalSpace := by rwa [h]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (hypothesis)
Goal:
γ : Type uc
t : TopologicalSpace γ
inst : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
this : CompactSpace γ
⊢ 𝓤 γ = 𝓤 γ
have this₁ : CompactSpace γ
Tactic: have : @CompactSpace γ u'.toTopologicalSpace := by rwa [h']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
γ : Type uc
t : TopologicalSpace γ
inst : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
this_1 : CompactSpace γ
this : CompactSpace γ
⊢ 𝓤 γ = 𝓤 γ
have rw : ⨆ (x : γ), 𝓝 (x, x) = 𝓤 γ
Tactic: rw [@compactSpace_uniformity _ u, compactSpace_uniformity, h, h']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
γ : Type uc
t : TopologicalSpace γ
inst : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
this_1 : CompactSpace γ
this : CompactSpace γ
rw : ⨆ (x : γ), 𝓝 (x, x) = 𝓤 γ
⊢ 𝓤 γ = 𝓤 γ
have rw₁ : Eq.{uc + 1} (α := Filter (γ × γ)) (⨆ (x : γ), 𝓝 (x, x)) (⨆ (x : γ), 𝓝 (x, x))
Tactic: rw [@compactSpace_uniformity _ u, compactSpace_uniformity, h, h']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
γ : Type uc
t : TopologicalSpace γ
inst : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
this_1 : CompactSpace γ
this : CompactSpace γ
rw : ⨆ (x : γ), 𝓝 (x, x) = 𝓤 γ
rw₁ : Eq.{uc + 1} (α := Filter (γ × γ)) (⨆ (x : γ), 𝓝 (x, x)) (⨆ (x : γ), 𝓝 (x, x))
⊢ 𝓤 γ = 𝓤 γ
have rw₂ : Eq.{uc + 1} (α := Filter (γ × γ)) (⨆ (x : γ), 𝓝 (x, x)) (⨆ (x : γ), 𝓝 (x, x))
Tactic: rw [@compactSpace_uniformity _ u, compactSpace_uniformity, h, h']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
γ : Type uc
t : TopologicalSpace γ
inst : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
this_1 : CompactSpace γ
this : CompactSpace γ
rw : ⨆ (x : γ), 𝓝 (x, x) = 𝓤 γ
rw₁ : Eq.{uc + 1} (α := Filter (γ × γ)) (⨆ (x : γ), 𝓝 (x, x)) (⨆ (x : γ), 𝓝 (x, x))
rw₂ : Eq.{uc + 1} (α := Filter (γ × γ)) (⨆ (x : γ), 𝓝 (x, x)) (⨆ (x : γ), 𝓝 (x, x))
⊢ 𝓤 γ = 𝓤 γ
have rw₃ : Eq.{uc + 1} (α := Filter (γ × γ)) (⨆ (x : γ), 𝓝 (x, x)) (⨆ (x : γ), 𝓝 (x, x))
Tactic: rw [@compactSpace_uniformity _ u, compactSpace_uniformity, h, h']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
β : Type ub
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : SetRel α β
hs : IsClosed s
t : Set β
ht : IsCompact t
⊢ IsClosed (s.preimage t)
have rw : ∀ (hs : ∀ x ∈ sᶜ, ∀ᶠ (y : α × β) in nhds x, y ∈ sᶜ) {t : Set β} (ht : IsCompact t),
  ∀ x ∈ (s.preimage t)ᶜ, ∀ᶠ (y : α) in nhds x, y ∈ (s.preimage t)ᶜ
Tactic: rw [← isOpen_compl_iff, isOpen_iff_eventually] at hs ⊢
Cleared hypotheses: hs, t, ht
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
β : Type ub
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : SetRel α β
hs : ∀ x ∈ sᶜ, ∀ᶠ (y : α × β) in nhds x, y ∈ sᶜ
t : Set β
ht : IsCompact t
⊢ ∀ x ∈ (s.preimage t)ᶜ, ∀ᶠ (y : α) in nhds x, y ∈ (s.preimage t)ᶜ
have simp_rw : ∀ (x : α), (∀ x_1 ∈ t, (x, x_1) ∉ s) → ∀ᶠ (y : α) in nhds x, ∀ x ∈ t, (y, x) ∉ s
Tactic: simp_rw [Set.mem_compl_iff, SetRel.mem_preimage, not_exists, not_and]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
⊢ Tendsto F p (𝓝 f) ↔
    ∀ (K : Set α),
      IsCompact K →
        TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
have rw : (∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β),
        IsOpen[inst_1.toTopologicalSpace] U →
          MapsTo (⇑f : (a : α) → β) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U) ↔
  ∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
Tactic: rw [tendsto_nhds_compactOpen]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
⊢ (∀ (K : Set α),
      IsCompact K →
        ∀ (U : Set β),
          IsOpen[inst_1.toTopologicalSpace] U →
            MapsTo (⇑f : (a : α) → β) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U) ↔
    ∀ (K : Set α),
      IsCompact K →
        TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
have mp : (∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β),
        IsOpen[inst_1.toTopologicalSpace] U →
          MapsTo (⇑f : (a : α) → β) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U) →
  ∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
mp :
  (∀ (K : Set α),
      IsCompact K →
        ∀ (U : Set β),
          IsOpen[inst_1.toTopologicalSpace] U →
            MapsTo (⇑f : (a : α) → β) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U) →
    ∀ (K : Set α),
      IsCompact K →
        TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
⊢ (∀ (K : Set α),
      IsCompact K →
        ∀ (U : Set β),
          IsOpen[inst_1.toTopologicalSpace] U →
            MapsTo (⇑f : (a : α) → β) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U) ↔
    ∀ (K : Set α),
      IsCompact K →
        TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
have mpr : (∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K) →
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β),
        IsOpen[inst_1.toTopologicalSpace] U →
          MapsTo (⇑f : (a : α) → β) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β),
        IsOpen[inst_1.toTopologicalSpace] U →
          MapsTo (⇑f : (a : α) → β) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U
K : Set α
hK : IsCompact K
⊢ TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
have mp : TendstoLocallyUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
Tactic: rw [← tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hK]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β),
        IsOpen[inst_1.toTopologicalSpace] U →
          MapsTo (⇑f : (a : α) → β) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
h_1 : x ∈ K
⊢ ∃ t ∈ 𝓝[K] x,
    ∀ᶠ (n : ι) in p,
      ∀ y ∈ t,
        Membership.mem (α := β × β) U
          (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)
have mp : ∀ (V : Set (β × β)) (hV : V ∈ 𝓤 β) (hVo : IsOpen[instTopologicalSpaceProd] V) (hVsymm : SetRel.IsSymm V)
  (hVU : SetRel.comp V V ⊆ U),
  ∃ t ∈ 𝓝[K] x,
    ∀ᶠ (n : ι) in p,
      ∀ y ∈ t,
        Membership.mem (α := β × β) U
          (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)
Tactic: rcases comp_open_symm_mem_uniformity_sets hU with ⟨V, hV, hVo, hVsymm, hVU⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β),
        IsOpen[inst_1.toTopologicalSpace] U →
          MapsTo (⇑f : (a : α) → β) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
h_1 : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen[instTopologicalSpaceProd] V
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
⊢ ∃ t ∈ 𝓝[K] x,
    ∀ᶠ (n : ι) in p,
      ∀ y ∈ t,
        Membership.mem (α := β × β) U
          (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)
have mp : ∀ (W : Set (β × β)) (hW : W ∈ 𝓤 β) (hWc : IsClosed[instTopologicalSpaceProd] W) (hWU : W ⊆ V),
  ∃ t ∈ 𝓝[K] x,
    ∀ᶠ (n : ι) in p,
      ∀ y ∈ t,
        Membership.mem (α := β × β) U
          (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)
Tactic: rcases mem_uniformity_isClosed hV with ⟨W, hW, hWc, hWU⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (hypothesis)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β),
        IsOpen[inst_1.toTopologicalSpace] U →
          MapsTo (⇑f : (a : α) → β) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
h_1 : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen[instTopologicalSpaceProd] V
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
W : Set (β × β)
hW : W ∈ 𝓤 β
hWc : IsClosed[instTopologicalSpaceProd] W
hWU : W ⊆ V
s : Set α := K ∩ preimage.{u₁, u₂} (β := β) ((⇑f : (a : α) → β) : (a : α) → β) (ball ((f : (a : α) → β) x) W : Set β)
⊢ ∃ t ∈ 𝓝[K] x,
    ∀ᶠ (n : ι) in p,
      ∀ y ∈ t,
        Membership.mem (α := β × β) U
          (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)
have hnhds : s ∈ 𝓝[K] x
Tactic: have hnhds : s ∈ 𝓝[K] x := inter_mem_nhdsWithin _ <| f.continuousAt _ (ball_mem_nhds _ hW)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (hypothesis)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β),
        IsOpen[inst_1.toTopologicalSpace] U →
          MapsTo (⇑f : (a : α) → β) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
h_1 : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen[instTopologicalSpaceProd] V
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
W : Set (β × β)
hW : W ∈ 𝓤 β
hWc : IsClosed[instTopologicalSpaceProd] W
hWU : W ⊆ V
s : Set α := K ∩ preimage.{u₁, u₂} (β := β) ((⇑f : (a : α) → β) : (a : α) → β) (ball ((f : (a : α) → β) x) W : Set β)
hnhds : s ∈ 𝓝[K] x
⊢ ∃ t ∈ 𝓝[K] x,
    ∀ᶠ (n : ι) in p,
      ∀ y ∈ t,
        Membership.mem (α := β × β) U
          (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)
have hcomp : IsCompact s
Tactic: have hcomp : IsCompact s := hK.inter_right <| (isClosed_ball _ hWc).preimage f.continuous
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (hypothesis)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β),
        IsOpen[inst_1.toTopologicalSpace] U →
          MapsTo (⇑f : (a : α) → β) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
h_1 : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen[instTopologicalSpaceProd] V
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
W : Set (β × β)
hW : W ∈ 𝓤 β
hWc : IsClosed[instTopologicalSpaceProd] W
hWU : W ⊆ V
s : Set α := K ∩ preimage.{u₁, u₂} (β := β) ((⇑f : (a : α) → β) : (a : α) → β) (ball ((f : (a : α) → β) x) W : Set β)
hnhds : s ∈ 𝓝[K] x
hcomp : IsCompact s
⊢ ∃ t ∈ 𝓝[K] x,
    ∀ᶠ (n : ι) in p,
      ∀ y ∈ t,
        Membership.mem (α := β × β) U
          (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)
have hmaps : MapsTo.{u₁, u₂} (β := β) ((⇑f : (a : α) → β) : (a : α) → β) s (ball ((f : (a : α) → β) x) V : Set β)
Tactic: have hmaps : MapsTo f s (ball (f x) V) := fun x hx ↦ hWU hx.2
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β),
        IsOpen[inst_1.toTopologicalSpace] U →
          MapsTo (⇑f : (a : α) → β) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
h_1 : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen[instTopologicalSpaceProd] V
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
W : Set (β × β)
hW : W ∈ 𝓤 β
hWc : IsClosed[instTopologicalSpaceProd] W
hWU : W ⊆ V
s : Set α := K ∩ preimage.{u₁, u₂} (β := β) ((⇑f : (a : α) → β) : (a : α) → β) (ball ((f : (a : α) → β) x) W : Set β)
hnhds : s ∈ 𝓝[K] x
hcomp : IsCompact s
hmaps : MapsTo.{u₁, u₂} (β := β) ((⇑f : (a : α) → β) : (a : α) → β) s (ball ((f : (a : α) → β) x) V : Set β)
⊢ ∃ t ∈ 𝓝[K] x,
    ∀ᶠ (n : ι) in p,
      ∀ y ∈ t,
        Membership.mem (α := β × β) U
          (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)
have right : ∀ᶠ (n : ι) in p,
  ∀ y ∈ s,
    Membership.mem (α := β × β) U
      (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)
Tactic: use s, hnhds