awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
⊢ Eq (α := Set (α →ᵤ[{K : Set α | IsCompact K}] β)) (range (ι := C(α, β)) toUniformOnFunIsCompact)
    {f : α →ᵤ[{K : Set α | IsCompact K}] β | Continuous[inst, inst_1.toTopologicalSpace] f}

Tactic:
Set.ext fun f ↦ ⟨fun g ↦ g.choose_spec ▸ g.choose.2, fun hf ↦ ⟨⟨f, hf⟩, rfl⟩⟩

Premises used: Set.ext, Exists.choose_spec, ContinuousMap.mk, Eq.rec, ContinuousMap.continuous_toFun, Iff.intro, Exists.intro, Exists.choose, rfl
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
⊢ Eq (α := TopologicalSpace C(α, β)) compactOpen toTopologicalSpace

Tactic:
TopologicalSpace.ext_nhds fun f ↦ eq_of_forall_le_iff fun l ↦ ?_

Premises used: eq_of_forall_le_iff, TopologicalSpace.ext_nhds
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
refine : ∀ (f : C(α, β)) (l : Filter C(α, β)), l ≤ 𝓝 f ↔ l ≤ 𝓝 f
⊢ Eq (α := TopologicalSpace C(α, β)) compactOpen toTopologicalSpace

Tactic:
refine TopologicalSpace.ext_nhds fun f ↦ eq_of_forall_le_iff fun l ↦ ?_

Premises used: eq_of_forall_le_iff, TopologicalSpace.ext_nhds
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
K : Set α
V : Set (β × β)
f_1 f : C(α, β)
l : Filter C(α, β)
simp_rw :
  (∀ (K : Set α),
      IsCompact K →
        TendstoUniformlyOn (β := β) (fun (i : C(α, β)) (a : α) ↦ (id i : (a : α) → β) a) (⇑f : (a : α) → β) l K) ↔
    ∀ (s : Set α),
      Membership.mem (γ := Set (Set α)) {K : Set α | IsCompact K} s →
        TendstoUniformlyOn (β := β)
          ((⇑(UniformOnFun.toFun {K : Set α | IsCompact K}) : (a : α →ᵤ[{K : Set α | IsCompact K}] β) → α → β) ∘
            toUniformOnFunIsCompact ∘ id)
          ((UniformOnFun.toFun {K : Set α | IsCompact K} : (a : α →ᵤ[{K : Set α | IsCompact K}] β) → α → β)
            f.toUniformOnFunIsCompact)
          l s
⊢ l ≤ 𝓝 f ↔ l ≤ 𝓝 f

Tactic:
simp_rw [← tendsto_id', tendsto_iff_forall_isCompact_tendstoUniformlyOn,
      nhds_induced, tendsto_comap_iff, UniformOnFun.tendsto_iff_tendstoUniformlyOn]

Premises used: UniformOnFun.tendsto_iff_tendstoUniformlyOn, Filter.tendsto_id', Filter.tendsto_comap_iff, ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn, nhds_induced
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
K : Set α
V : Set (β × β)
f_1 f : C(α, β)
l : Filter C(α, β)
⊢ (∀ (K : Set α),
      IsCompact K →
        TendstoUniformlyOn (β := β) (fun (i : C(α, β)) (a : α) ↦ (id i : (a : α) → β) a) (⇑f : (a : α) → β) l K) ↔
    ∀ (s : Set α),
      Membership.mem (γ := Set (Set α)) {K : Set α | IsCompact K} s →
        TendstoUniformlyOn (β := β)
          ((⇑(UniformOnFun.toFun {K : Set α | IsCompact K}) : (a : α →ᵤ[{K : Set α | IsCompact K}] β) → α → β) ∘
            toUniformOnFunIsCompact ∘ id)
          ((UniformOnFun.toFun {K : Set α | IsCompact K} : (a : α →ᵤ[{K : Set α | IsCompact K}] β) → α → β)
            f.toUniformOnFunIsCompact)
          l s

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
X : Type u_1
inst_2 : TopologicalSpace X
f : X → C(α, β)
⊢ Continuous[inst_2, _] f ↔
    Continuous[inst_2, topologicalSpace α β {K : Set α | IsCompact K}] fun (x : X) ↦
      (ofFun {K : Set α | IsCompact K} : (a : α → β) → α →ᵤ[{K : Set α | IsCompact K}] β) (⇑(f x) : (a : α) → β)

Tactic:
isUniformEmbedding_toUniformOnFunIsCompact.isInducing.continuous_iff

Premises used: Topology.IsInducing.continuous_iff, IsUniformEmbedding.toIsUniformInducing, IsUniformInducing.isInducing, ContinuousMap.toUniformOnFunIsCompact, ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u_1
pi : ι → Prop
s : ι → Set (β × β)
h : (𝓤 β).HasBasis pi s
⊢ HasBasis (α := C(α, β) × C(α, β))
    (Filter.comap (β := (α →ᵤ[{K : Set α | IsCompact K}] β) × (α →ᵤ[{K : Set α | IsCompact K}] β))
      (fun (x : C(α, β) × C(α, β)) ↦ (x.1.toUniformOnFunIsCompact, x.2.toUniformOnFunIsCompact))
      (𝓤 (α →ᵤ[{K : Set α | IsCompact K}] β)))
    (fun (p : Prod.{u₁, u_1} (Set α) ι) ↦ IsCompact p.1 ∧ pi p.2) fun (p : Prod.{u₁, u_1} (Set α) ι) ↦
    {fg : C(α, β) × C(α, β) |
      ∀ x ∈ p.1, Membership.mem (α := β × β) (s p.2) (((fg.1 : (a : α) → β) x, (fg.2 : (a : α) → β) x) : β × β)}

Tactic:
.comap _ <| UniformOnFun.hasBasis_uniformity_of_basis _ _ {K | IsCompact K}
    ⟨∅, isCompact_empty⟩ (directedOn_of_sup_mem fun _ _ ↦ IsCompact.union) h

Premises used: UniformOnFun.gen, Set.Mem, setOf, directedOn_of_sup_mem, ContinuousMap.toUniformOnFunIsCompact, Filter.HasBasis.comap, Set.preimage, UniformOnFun.hasBasis_uniformity_of_basis, Exists.intro, IsCompact.union, EmptyCollection.emptyCollection, IsCompact, isCompact_empty
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u_1
pi : ι → Prop
s : ι → Set (β × β)
h : (𝓤 β).HasBasis pi s
⊢ HasBasis (α := C(α, β) × C(α, β))
    (Filter.comap (β := (α →ᵤ[{K : Set α | IsCompact K}] β) × (α →ᵤ[{K : Set α | IsCompact K}] β))
      (fun (x : C(α, β) × C(α, β)) ↦ (x.1.toUniformOnFunIsCompact, x.2.toUniformOnFunIsCompact))
      (𝓤 (α →ᵤ[{K : Set α | IsCompact K}] β)))
    (fun (p : Prod.{u₁, u_1} (Set α) ι) ↦ IsCompact p.1 ∧ pi p.2) fun (p : Prod.{u₁, u_1} (Set α) ι) ↦
    {fg : C(α, β) × C(α, β) |
      ∀ x ∈ p.1, Membership.mem (α := β × β) (s p.2) (((fg.1 : (a : α) → β) x, (fg.2 : (a : α) → β) x) : β × β)}

Tactic:
exact .comap _ <| UniformOnFun.hasBasis_uniformity_of_basis _ _ {K | IsCompact K}
    ⟨∅, isCompact_empty⟩ (directedOn_of_sup_mem fun _ _ ↦ IsCompact.union) h

Premises used: setOf, directedOn_of_sup_mem, UniformOnFun.hasBasis_uniformity_of_basis, Exists.intro, IsCompact.union, EmptyCollection.emptyCollection, IsCompact, isCompact_empty
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
⊢ HasBasis (α := C(α, β) × C(α, β)) (𝓤 C(α, β))
    (fun (p : Prod.{u₁, u₂} (Set α) (Set (β × β))) ↦ IsCompact p.1 ∧ p.2 ∈ 𝓤 β)
    fun (p : Prod.{u₁, u₂} (Set α) (Set (β × β))) ↦
    {fg : C(α, β) × C(α, β) |
      ∀ x ∈ p.1, Membership.mem (α := β × β) p.2 (((fg.1 : (a : α) → β) x, (fg.2 : (a : α) → β) x) : β × β)}

Tactic:
(basis_sets _).compactConvergenceUniformity

Premises used: Set.Mem, setOf, Filter.basis_sets, Filter.HasBasis.compactConvergenceUniformity
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
X : Set (C(α, β) × C(α, β))
⊢ Membership.mem (γ := Filter (C(α, β) × C(α, β))) (𝓤 C(α, β)) X ↔
    ∃ (K : Set α) (V : Set (β × β)),
      IsCompact K ∧
        V ∈ 𝓤 β ∧
          {fg : C(α, β) × C(α, β) |
              ∀ x ∈ K, Membership.mem (α := β × β) V (((fg.1 : (a : α) → β) x, (fg.2 : (a : α) → β) x) : β × β)} ⊆
            X

Tactic:
simp [hasBasis_compactConvergenceUniformity.mem_iff, and_assoc]

Premises used: Filter.HasBasis.mem_iff, ContinuousMap.hasBasis_compactConvergenceUniformity, and_assoc
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u_1
p : ι → Prop
V : ι → Set (β × β)
K : CompactExhaustion α
hb : (𝓤 β).HasBasis p V
⊢ HasBasis (α := C(α, β) × C(α, β)) (𝓤 C(α, β)) (fun (i : ℕ × ι) ↦ p i.2) fun (i : ℕ × ι) ↦
    {fg : C(α, β) × C(α, β) |
      ∀ (x : α),
        Membership.mem (γ := Set α) ((K : (a : ℕ) → Set α) i.1 : Set α) x →
          Membership.mem (α := β × β) (V i.2) (((fg.1 : (a : α) → β) x, (fg.2 : (a : α) → β) x) : β × β)}

Tactic:
(UniformOnFun.hasBasis_uniformity_of_covering_of_basis {K | IsCompact K} K.isCompact
    (Monotone.directed_le K.subset) (fun _ ↦ K.exists_superset_of_isCompact) hb).comap _

Premises used: UniformOnFun.hasBasis_uniformity_of_covering_of_basis, UniformOnFun.gen, Set.Mem, uniformity, setOf, CompactExhaustion.subset, ContinuousMap.toUniformOnFunIsCompact, CompactExhaustion.isCompact, Filter.HasBasis.comap, Set.preimage, CompactExhaustion.exists_superset_of_isCompact, Monotone.directed_le, IsCompact, Filter.comap
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
V : ℕ → Set (β × β)
K : CompactExhaustion α
hb : (𝓤 β).HasAntitoneBasis V
⊢ HasAntitoneBasis (α := C(α, β) × C(α, β)) (𝓤 C(α, β)) fun (n : ℕ) ↦
    {fg : C(α, β) × C(α, β) |
      ∀ (x : α),
        Membership.mem (γ := Set α) ((K : (a : ℕ) → Set α) n : Set α) x →
          Membership.mem (α := β × β) (V n) (((fg.1 : (a : α) → β) x, (fg.2 : (a : α) → β) x) : β × β)}

Tactic:
(UniformOnFun.hasAntitoneBasis_uniformity {K | IsCompact K} K.isCompact
    K.subset (fun _ ↦ K.exists_superset_of_isCompact) hb).comap _

Premises used: UniformOnFun.gen, Filter.HasAntitoneBasis.comap, Set.Mem, uniformity, setOf, CompactExhaustion.subset, ContinuousMap.toUniformOnFunIsCompact, CompactExhaustion.isCompact, Set.preimage, CompactExhaustion.exists_superset_of_isCompact, UniformOnFun.hasAntitoneBasis_uniformity, IsCompact, Filter.comap
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
inst_2 : WeaklyLocallyCompactSpace α
inst_3 : SigmaCompactSpace α
inst_4 : (𝓤 β).IsCountablyGenerated
⊢ IsCountablyGenerated (α := C(α, β) × C(α, β)) (𝓤 C(α, β))

Tactic:
let ⟨_V, hV⟩ := exists_antitone_basis (𝓤 β)
  ((CompactExhaustion.choice α).hasAntitoneBasis_compactConvergenceUniformity
    hV).isCountablyGenerated

Premises used: Filter.HasAntitoneBasis.toHasBasis, ContinuousMap, uniformity, _private.0.ContinuousMap.instIsCountablyGeneratedProdUniformityOfWeaklyLocallyCompactSpaceOfSigmaCompactSpace.match_1, CompactExhaustion.choice, CompactExhaustion.hasAntitoneBasis_compactConvergenceUniformity, Filter.IsCountablyGenerated, Filter.exists_antitone_basis, Filter.HasBasis.isCountablyGenerated
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p
rw :
  ∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
⊢ Tendsto F p (𝓝 f)

Tactic:
rw [tendsto_iff_forall_isCompact_tendstoUniformlyOn]

Premises used: ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p
K : Set α
hK : IsCompact K
rw :
  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 β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p
K : Set α
hK : IsCompact K
⊢ TendstoLocallyUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K

Tactic:
h.tendstoLocallyUniformlyOn

Premises used: TendstoLocallyUniformly.tendstoLocallyUniformlyOn
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p
K : Set α
hK : IsCompact K
⊢ TendstoLocallyUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K

Tactic:
exact h.tendstoLocallyUniformlyOn

Premises used: TendstoLocallyUniformly.tendstoLocallyUniformlyOn
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst_2 : WeaklyLocallyCompactSpace α
⊢ Tendsto F p (𝓝 f) ↔
    TendstoLocallyUniformly.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p

Tactic:
⟨fun h V hV x ↦ ?_, tendsto_of_tendstoLocallyUniformly⟩

Premises used: Iff.intro, ContinuousMap.tendsto_of_tendstoLocallyUniformly
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst_2 : WeaklyLocallyCompactSpace α
refine :
  ∀ (h : Tendsto F p (𝓝 f)) (V : Set (β × β)) (hV : V ∈ 𝓤 β) (x : α),
    ∃ t ∈ 𝓝 x,
      ∀ᶠ (n : ι) in p,
        ∀ y ∈ t,
          Membership.mem (α := β × β) V
            (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)
⊢ Tendsto F p (𝓝 f) ↔
    TendstoLocallyUniformly.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p

Tactic:
refine ⟨fun h V hV x ↦ ?_, tendsto_of_tendstoLocallyUniformly⟩
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst_2 : WeaklyLocallyCompactSpace α
h : Tendsto F p (𝓝 f)
V : Set (β × β)
hV : V ∈ 𝓤 β
x : α
rw :
  ∀
    (h :
      ∀ (K : Set α),
        IsCompact K →
          TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K)
    (V : Set (β × β)) (hV : V ∈ 𝓤 β) (x : α),
    ∃ t ∈ 𝓝 x,
      ∀ᶠ (n : ι) in p,
        ∀ y ∈ t,
          Membership.mem (α := β × β) V
            (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)
⊢ ∃ t ∈ 𝓝 x,
    ∀ᶠ (n : ι) in p,
      ∀ y ∈ t,
        Membership.mem (α := β × β) V
          (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)

Tactic:
rw [tendsto_iff_forall_isCompact_tendstoUniformlyOn] at h

Premises used: ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst_2 : WeaklyLocallyCompactSpace α
h :
  ∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
V : Set (β × β)
hV : V ∈ 𝓤 β
x : α
obtain :
  ∀ (n : Set α) (hn₁ : IsCompact n) (hn₂ : n ∈ 𝓝 x),
    ∃ t ∈ 𝓝 x,
      ∀ᶠ (n : ι) in p,
        ∀ y ∈ t,
          Membership.mem (α := β × β) V
            (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)
⊢ ∃ t ∈ 𝓝 x,
    ∀ᶠ (n : ι) in p,
      ∀ y ∈ t,
        Membership.mem (α := β × β) V
          (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)

Tactic:
obtain ⟨n, hn₁, hn₂⟩ := exists_compact_mem_nhds x

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst_2 : WeaklyLocallyCompactSpace α
h :
  ∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
V : Set (β × β)
hV : V ∈ 𝓤 β
x : α
n : Set α
hn₁ : IsCompact n
hn₂ : n ∈ 𝓝 x
⊢ ∃ t ∈ 𝓝 x,
    ∀ᶠ (n : ι) in p,
      ∀ y ∈ t,
        Membership.mem (α := β × β) V
          (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)

Tactic:
⟨n, hn₂, h n hn₁ V hV⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst_2 : WeaklyLocallyCompactSpace α
h :
  ∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
V : Set (β × β)
hV : V ∈ 𝓤 β
x : α
n : Set α
hn₁ : IsCompact n
hn₂ : n ∈ 𝓝 x
⊢ ∃ t ∈ 𝓝 x,
    ∀ᶠ (n : ι) in p,
      ∀ y ∈ t,
        Membership.mem (α := β × β) V
          (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)

Tactic:
exact ⟨n, hn₂, h n hn₁ V hV⟩
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
δ : Type u_2
inst_2 : UniformSpace δ
g : C(β, δ)
hg : UniformContinuous.{u₂, u_2} (α := β) (β := δ) (⇑g : (a : β) → δ)
⊢ UniformContinuous (α := C(α, β)) g.comp

Tactic:
isUniformEmbedding_toUniformOnFunIsCompact.uniformContinuous_iff.mpr <|
    UniformOnFun.postcomp_uniformContinuous hg |>.comp
      isUniformEmbedding_toUniformOnFunIsCompact.uniformContinuous

Premises used: Iff.mpr, UniformOnFun.postcomp_uniformContinuous, IsUniformEmbedding.toIsUniformInducing, UniformContinuous.comp, IsUniformInducing.uniformContinuous_iff, ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
δ : Type u_2
inst_2 : UniformSpace δ
g : C(β, δ)
hg : IsUniformInducing.{u₂, u_2} (α := β) (β := δ) (⇑g : (a : β) → δ)
⊢ IsUniformInducing (α := C(α, β)) g.comp

Tactic:
isUniformEmbedding_toUniformOnFunIsCompact.isUniformInducing.of_comp_iff.mp <|
    UniformOnFun.postcomp_isUniformInducing hg |>.comp
      isUniformEmbedding_toUniformOnFunIsCompact.isUniformInducing

Premises used: IsUniformInducing.of_comp_iff, UniformOnFun.postcomp_isUniformInducing, IsUniformEmbedding.isUniformInducing, ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact, Iff.mp, IsUniformInducing.comp
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
δ : Type u_2
inst_2 : UniformSpace δ
g : C(β, δ)
hg : IsUniformEmbedding.{u₂, u_2} (α := β) (β := δ) (⇑g : (a : β) → δ)
⊢ IsUniformEmbedding (α := C(α, β)) g.comp

Tactic:
isUniformEmbedding_toUniformOnFunIsCompact.of_comp_iff.mp <|
    UniformOnFun.postcomp_isUniformEmbedding hg |>.comp
      isUniformEmbedding_toUniformOnFunIsCompact

Premises used: IsUniformEmbedding.comp, ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact, IsUniformEmbedding.of_comp_iff, Iff.mp, UniformOnFun.postcomp_isUniformEmbedding
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
γ : Type u_1
inst_2 : TopologicalSpace γ
g : C(α, γ)
⊢ UniformContinuous (β := C(α, β)) fun (f : C(γ, β)) ↦ f.comp g

Tactic:
isUniformEmbedding_toUniformOnFunIsCompact.uniformContinuous_iff.mpr <|
    UniformOnFun.precomp_uniformContinuous (fun _ hK ↦ hK.image g.continuous) |>.comp
      isUniformEmbedding_toUniformOnFunIsCompact.uniformContinuous

Premises used: Iff.mpr, IsUniformEmbedding.toIsUniformInducing, UniformContinuous.comp, IsUniformInducing.uniformContinuous_iff, ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact, UniformOnFun.precomp_uniformContinuous, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompactSpace α
⊢ HasBasis (α := C(α, β) × C(α, β)) (𝓤 C(α, β)) (fun (V : Set (β × β)) ↦ V ∈ 𝓤 β) fun (V : Set (β × β)) ↦
    {fg : C(α, β) × C(α, β) |
      ∀ (x : α), Membership.mem (α := β × β) V (((fg.1 : (a : α) → β) x, (fg.2 : (a : α) → β) x) : β × β)}

Tactic:
hasBasis_compactConvergenceUniformity.to_hasBasis
    (fun p hp => ⟨p.2, hp.2, fun _fg hfg x _hx => hfg x⟩) fun V hV ↦
    ⟨⟨univ, V⟩, ⟨isCompact_univ, hV⟩, fun _fg hfg x => hfg x (mem_univ x)⟩

Premises used: Set.univ, ContinuousMap.hasBasis_compactConvergenceUniformity, Prod.mk, And.right, isCompact_univ, And.intro, Exists.intro, Set.mem_univ, Prod.snd, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompactSpace α
ι : Sort u_1
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
⊢ HasBasis (α := C(α, β) × C(α, β)) (𝓤 C(α, β)) p fun (i : ι) ↦
    {fg : C(α, β) × C(α, β) |
      ∀ (x : α), Membership.mem (α := β × β) (V i) (((fg.1 : (a : α) → β) x, (fg.2 : (a : α) → β) x) : β × β)}

Tactic:
hasBasis_compactConvergenceUniformity_of_compact.to_hasBasis
    (fun _U hU ↦ (h.mem_iff.mp hU).imp fun _i ⟨hpi, hi⟩ ↦ ⟨hpi, fun _ h a ↦ hi <| h a⟩)
    fun i hi ↦ ⟨V i, h.mem_of_mem hi, .rfl⟩

Premises used: Filter.HasBasis.mem_iff, Exists.imp, Set.Subset.rfl, And.intro, Exists.intro, Iff.mp, ContinuousMap.hasBasis_compactConvergenceUniformity_of_compact, Filter.HasBasis.to_hasBasis, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst_2 : CompactSpace α
⊢ Tendsto F p (𝓝 f) ↔
    TendstoUniformly.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p

Tactic:
simp [isUniformEmbedding_uniformFunOfFun.isInducing.tendsto_nhds_iff,
    UniformFun.tendsto_iff_tendstoUniformly, Function.comp_def]

Premises used: UniformFun.tendsto_iff_tendstoUniformly, IsUniformEmbedding.toIsUniformInducing, IsUniformInducing.isInducing, Topology.IsInducing.tendsto_nhds_iff, Function.comp_def, ContinuousMap.isUniformEmbedding_uniformFunOfFun
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompactSpace α
X : Type u_1
inst_3 : TopologicalSpace X
f : X → C(α, β)
⊢ Continuous[inst_3, _] f ↔
    Continuous[inst_3, topologicalSpace α β] fun (x : X) ↦ (ofFun : (a : α → β) → α →ᵤ β) (⇑(f x) : (a : α) → β)

Tactic:
isUniformEmbedding_uniformFunOfFun.isInducing.continuous_iff

Premises used: Topology.IsInducing.continuous_iff, IsUniformEmbedding.toIsUniformInducing, IsUniformInducing.isInducing, ContinuousMap.isUniformEmbedding_uniformFunOfFun