awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
inst_1 : CompactSpace α
⊢ 𝓤 α = ⨆ (x : α), 𝓝 (x, x)

Tactic:
nhdsSet_diagonal_eq_uniformity.symm.trans (nhdsSet_diagonal _)

Premises used: nhdsSet_diagonal_eq_uniformity, nhdsSet_diagonal, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
γ : Type uc
t : TopologicalSpace γ
inst : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
⊢ u = u'

Tactic:
UniformSpace.ext ?_

Premises used: UniformSpace.ext
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
γ : Type uc
t : TopologicalSpace γ
inst : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
refine : 𝓤 γ = 𝓤 γ
⊢ u = u'

Tactic:
refine UniformSpace.ext ?_

Premises used: UniformSpace.ext
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
γ : Type uc
t : TopologicalSpace γ
inst : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
rwa rwa₁ rwa₂ rwa₃ : CompactSpace γ
⊢ CompactSpace γ

Tactic:
rwa [h]
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
γ : Type uc
t : TopologicalSpace γ
inst : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
⊢ CompactSpace γ

Tactic:
have : @CompactSpace γ u.toTopologicalSpace := by rwa [h]
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
γ : Type uc
t : TopologicalSpace γ
inst : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
this : CompactSpace γ
rwa rwa₁ rwa₂ rwa₃ : CompactSpace γ
⊢ CompactSpace γ

Tactic:
rwa [h']
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
γ : Type uc
t : TopologicalSpace γ
inst : CompactSpace γ
u u' : UniformSpace γ
h : toTopologicalSpace = t
h' : toTopologicalSpace = t
this : CompactSpace γ
⊢ CompactSpace γ

Tactic:
have : @CompactSpace γ u'.toTopologicalSpace := by rwa [h']
-- Module: Mathlib.Topology.UniformSpace.Compact
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))
rw₃ rw₄ : Eq.{uc + 1} (α := Filter (γ × γ)) (⨆ (x : γ), 𝓝 (x, x)) (⨆ (x : γ), 𝓝 (x, x))
⊢ 𝓤 γ = 𝓤 γ

Tactic:
rw [@compactSpace_uniformity _ u, compactSpace_uniformity, h, h']

Premises used: compactSpace_uniformity
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
β : Type ub
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : SetRel α β
hs : IsClosed s
t : Set β
ht : IsCompact t
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)ᶜ
⊢ IsClosed (s.preimage t)

Tactic:
rw [← isOpen_compl_iff, isOpen_iff_eventually] at hs ⊢

Premises used: isOpen_iff_eventually, isOpen_compl_iff
-- Module: Mathlib.Topology.UniformSpace.Compact
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
simp_rw : ∀ (x : α), (∀ x_1 ∈ t, (x, x_1) ∉ s) → ∀ᶠ (y : α) in nhds x, ∀ x ∈ t, (y, x) ∉ s
⊢ ∀ x ∈ (s.preimage t)ᶜ, ∀ᶠ (y : α) in nhds x, y ∈ (s.preimage t)ᶜ

Tactic:
simp_rw [Set.mem_compl_iff, SetRel.mem_preimage, not_exists, not_and]

Premises used: not_exists, SetRel.mem_preimage, not_and, Set.mem_compl_iff
-- Module: Mathlib.Topology.UniformSpace.Compact
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 : α), (∀ x_1 ∈ t, (x, x_1) ∉ s) → ∀ᶠ (y : α) in nhds x, ∀ x ∈ t, (y, x) ∉ s

Tactic:
fun y hy => ht.eventually_forall_of_forall_eventually fun x hx => hs _ <| hy _ hx

Premises used: Prod.mk, IsCompact.eventually_forall_of_forall_eventually
-- Module: Mathlib.Topology.UniformSpace.Compact
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 : α), (∀ x_1 ∈ t, (x, x_1) ∉ s) → ∀ᶠ (y : α) in nhds x, ∀ x ∈ t, (y, x) ∉ s

Tactic:
exact fun y hy => ht.eventually_forall_of_forall_eventually fun x hx => hs _ <| hy _ hx

Premises used: IsCompact.eventually_forall_of_forall_eventually
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
β : Type ub
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : SetRel α β
hs : IsClosed s
t : Set α
ht : IsCompact t
⊢ IsClosed (s.image t)

Tactic:
hs.relInv.relPreimage_of_isCompact ht

Premises used: IsClosed.relInv, Set.Mem, SetRel.inv, IsClosed.relPreimage_of_isCompact, setOf, Set.preimage, SetRel.image, Prod.swap
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
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
⊢ Tendsto F p (𝓝 f) ↔
    ∀ (K : Set α),
      IsCompact K →
        TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K

Tactic:
rw [tendsto_nhds_compactOpen]

Premises used: ContinuousMap.tendsto_nhds_compactOpen
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
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
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
⊢ (∀ (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
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
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
mp :
  TendstoLocallyUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
⊢ TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K

Tactic:
rw [← tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hK]

Premises used: tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
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 : α
mp :
  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) : β × β)
⊢ 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) : β × β)

Tactic:
_
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
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
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) : β × β)
⊢ ∃ 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⟩

Premises used: comp_open_symm_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
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
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) : β × β)
⊢ ∃ 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⟩

Premises used: mem_uniformity_isClosed
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
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 β)
⊢ s ∈ 𝓝[K] x

Tactic:
have hnhds : s ∈ 𝓝[K] x := inter_mem_nhdsWithin _ <| f.continuousAt _ (ball_mem_nhds _ hW)
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
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
⊢ IsCompact s

Tactic:
have hcomp : IsCompact s := hK.inter_right <| (isClosed_ball _ hWc).preimage f.continuous
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
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
⊢ 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
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
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 β)
right :
  ∀ᶠ (n : ι) in p,
    ∀ y ∈ s,
      Membership.mem (α := β × β) U
        (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)
⊢ ∃ t ∈ 𝓝[K] x,
    ∀ᶠ (n : ι) in p,
      ∀ y ∈ t,
        Membership.mem (α := β × β) U
          (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)

Tactic:
use s, hnhds
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
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 β)
⊢ ∀ᶠ (n : ι) in p,
    ∀ y ∈ s,
      Membership.mem (α := β × β) U
        (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)

Tactic:
(h s hcomp _ (isOpen_ball _ hVo) hmaps).mono fun g hg y hy ↦ ?_

Premises used: UniformSpace.isOpen_ball, Filter.Eventually.mono
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
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 β)
right :
  ∀ (g : ι)
    (hg : MapsTo.{u₁, u₂} (β := β) ((⇑(F g) : (a : α) → β) : (a : α) → β) s (ball ((f : (a : α) → β) x) V : Set β))
    (y : α) (hy : y ∈ s),
    Membership.mem (α := β × β) U
      (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) g y) : β × β)
⊢ ∀ᶠ (n : ι) in p,
    ∀ y ∈ s,
      Membership.mem (α := β × β) U
        (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)

Tactic:
refine (h s hcomp _ (isOpen_ball _ hVo) hmaps).mono fun g hg y hy ↦ ?_

Premises used: UniformSpace.isOpen_ball, Filter.Eventually.mono
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
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 β)
g : ι
hg : MapsTo.{u₁, u₂} (β := β) ((⇑(F g) : (a : α) → β) : (a : α) → β) s (ball ((f : (a : α) → β) x) V : Set β)
y : α
hy : y ∈ s
⊢ Membership.mem (α := β × β) U (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) g y) : β × β)

Tactic:
hVU ⟨f x, SetRel.symm V <| hmaps hy, hg hy⟩

Premises used: SetRel.symm, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
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 β)
g : ι
hg : MapsTo.{u₁, u₂} (β := β) ((⇑(F g) : (a : α) → β) : (a : α) → β) s (ball ((f : (a : α) → β) x) V : Set β)
y : α
hy : y ∈ s
⊢ Membership.mem (α := β × β) U (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) g y) : β × β)

Tactic:
exact hVU ⟨f x, SetRel.symm V <| hmaps hy, hg hy⟩
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen[inst_1.toTopologicalSpace] U
hf : MapsTo (⇑f : (a : α) → β) K U
mpr :
  ∀ (V : Set (β × β)) (hV : V ∈ 𝓤 β)
    (hVf : ∀ (x : β), Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' K) x → ball x V ⊆ U),
    ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U
⊢ ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U

Tactic:
rcases lebesgue_number_of_compact_open (hK.image (map_continuous f)) hU hf.image_subset
        with ⟨V, hV, -, hVf⟩

Premises used: lebesgue_number_of_compact_open, ContinuousMapClass.map_continuous, IsCompact.image, Set.MapsTo.image_subset
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen[inst_1.toTopologicalSpace] U
hf : MapsTo (⇑f : (a : α) → β) K U
V : Set (β × β)
hV : V ∈ 𝓤 β
hVf : ∀ (x : β), Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' K) x → ball x V ⊆ U
g : ι
hg : ∀ x ∈ K, Membership.mem (α := β × β) V (((f : (a : α) → β) x, (F g : (a : α) → β) x) : β × β)
x : α
hx : x ∈ K
⊢ Membership.mem (α := β) U ((F g : (a : α) → β) x : β)

Tactic:
hVf _ (mem_image_of_mem f hx) (hg x hx)

Premises used: Set.mem_image_of_mem, DFunLike.coe
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen[inst_1.toTopologicalSpace] U
hf : MapsTo (⇑f : (a : α) → β) K U
V : Set (β × β)
hV : V ∈ 𝓤 β
hVf : ∀ (x : β), Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' K) x → ball x V ⊆ U
h₁ :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι)
            {x : ι |
              (fun (n : ι) ↦
                  ∀ x ∈ K,
                    Membership.mem (α := β × β) V
                      (((f : (a : α) → β) x, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n x) : β × β))
                x}
            x →
          Membership.mem (γ := Set ι) {x : ι | (fun (a : ι) ↦ MapsTo (⇑(F a) : (a : α) → β) K U) x} x}
      a
h₂ :
  ∀ (a : ι),
    (∀ x ∈ K, Membership.mem (α := β × β) V (((f : (a : α) → β) x, (F a : (a : α) → β) x) : β × β)) →
      MapsTo (⇑(F a) : (a : α) → β) K U
h₃ :
  ∀ (g : ι) (hg : ∀ x ∈ K, Membership.mem (α := β × β) V (((f : (a : α) → β) x, (F g : (a : α) → β) x) : β × β)) ⦃x : α⦄
    (hx : x ∈ K), Membership.mem (α := β) U ((F g : (a : α) → β) x : β)
⊢ ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U

Tactic:
filter_upwards [h K hK V hV] with g hg x hx using hVf _ (mem_image_of_mem f hx) (hg x hx)
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : C(α, β)
⊢ Eq (α := α → β)
    ((UniformOnFun.toFun {K : Set α | IsCompact K} : (a : α →ᵤ[{K : Set α | IsCompact K}] β) → α → β)
        f.toUniformOnFunIsCompact :
      α → β)
    ((⇑f : (a : α) → β) : (a : α) → β)

Tactic:
rfl

Premises used: ContinuousMap.toUniformOnFunIsCompact, rfl