awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst_1 : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ (i : ι), s ⊆ t i
hb : (𝓤 β).HasBasis p V
⊢ 𝔖.Nonempty

Tactic:
have hne : 𝔖.Nonempty := (range_nonempty t).mono (range_subset_iff.2 ht)
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst_1 : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ (i : ι), s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
s₁ : Set α
hs₁ : s₁ ∈ 𝔖
s₂ : Set α
hs₂ : s₂ ∈ 𝔖
rcases :
  ∀ (i₁ : ι) (his₁ : s₁ ⊆ t i₁) (i₂ : ι) (his₂ : s₂ ⊆ t i₂),
    ∃ z ∈ 𝔖, (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s₁ z ∧ (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s₂ z
⊢ ∃ z ∈ 𝔖, (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s₁ z ∧ (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s₂ z

Tactic:
rcases hex s₁ hs₁, hex s₂ hs₂ with ⟨⟨i₁, his₁⟩, i₂, his₂⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst_1 : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ (i : ι), s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
s₁ : Set α
hs₁ : s₁ ∈ 𝔖
s₂ : Set α
hs₂ : s₂ ∈ 𝔖
i₁ : ι
his₁ : s₁ ⊆ t i₁
i₂ : ι
his₂ : s₂ ⊆ t i₂
rcases :
  ∀ (i : ι) (hi₁ : t i₁ ⊆ t i) (hi₂ : t i₂ ⊆ t i),
    ∃ z ∈ 𝔖, (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s₁ z ∧ (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s₂ z
⊢ ∃ z ∈ 𝔖, (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s₁ z ∧ (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s₂ z

Tactic:
rcases hdir i₁ i₂ with ⟨i, hi₁, hi₂⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst_1 : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ (i : ι), s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
s₁ : Set α
hs₁ : s₁ ∈ 𝔖
s₂ : Set α
hs₂ : s₂ ∈ 𝔖
i₁ : ι
his₁ : s₁ ⊆ t i₁
i₂ : ι
his₂ : s₂ ⊆ t i₂
i : ι
hi₁ : t i₁ ⊆ t i
hi₂ : t i₂ ⊆ t i
⊢ ∃ z ∈ 𝔖, (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s₁ z ∧ (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s₂ z

Tactic:
⟨t i, ht _, his₁.trans hi₁, his₂.trans hi₂⟩

Premises used: HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst_1 : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ (i : ι), s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
s₁ : Set α
hs₁ : s₁ ∈ 𝔖
s₂ : Set α
hs₂ : s₂ ∈ 𝔖
i₁ : ι
his₁ : s₁ ⊆ t i₁
i₂ : ι
his₂ : s₂ ⊆ t i₂
i : ι
hi₁ : t i₁ ⊆ t i
hi₂ : t i₂ ⊆ t i
⊢ ∃ z ∈ 𝔖, (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s₁ z ∧ (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s₂ z

Tactic:
exact ⟨t i, ht _, his₁.trans hi₁, his₂.trans hi₂⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst_1 : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ (i : ι), s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
⊢ DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖

Tactic:
have hd : DirectedOn (· ⊆ ·) 𝔖 := fun s₁ hs₁ s₂ hs₂ ↦ by
    rcases hex s₁ hs₁, hex s₂ hs₂ with ⟨⟨i₁, his₁⟩, i₂, his₂⟩
    rcases hdir i₁ i₂ with ⟨i, hi₁, hi₂⟩
    exact ⟨t i, ht _, his₁.trans hi₁, his₂.trans hi₂⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst_1 : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ (i : ι), s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
hd : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
⊢ HasBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (𝓤 (α →ᵤ[𝔖] β)) (fun (i : ι × ι') ↦ p i.2) fun (i : ι × ι') ↦
    UniformOnFun.gen 𝔖 (t i.1) (V i.2)

Tactic:
(UniformOnFun.hasBasis_uniformity_of_basis α β 𝔖 hne hd hb).to_hasBasis
    (fun ⟨s, i'⟩ ⟨hs, hi'⟩ ↦ ?_) fun ⟨i, i'⟩ hi' ↦ ⟨(t i, i'), ⟨ht i, hi'⟩, Subset.rfl⟩

Premises used: _private.0.UniformOnFun.hasBasis_uniformity_of_covering_of_basis.match_1, UniformOnFun.gen, Membership.mem, Exists, Prod.mk, HasSubset.Subset, Prod.fst, And, Set.Subset.rfl, And.intro, UniformOnFun.hasBasis_uniformity_of_basis, Exists.intro, _private.0.UniformOnFun.hasBasis_uniformity_of_covering_of_basis.match_2, _private.0.UniformOnFun.hasBasis_uniformity_of_covering_of_basis.match_3, Prod.snd, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst_1 : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ (i : ι), s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
hd : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
refine :
  ∀ (x : Prod.{u_1, u_6} (Set α) ι') (s : Set α) (i' : ι'),
    (s, i').1 ∈ 𝔖 ∧ p (s, i').2 →
      ∀ (hs : (s, i').1 ∈ 𝔖) (hi' : p (s, i').2),
        ∃ (i'_1 : ι × ι'),
          p i'_1.2 ∧ UniformOnFun.gen 𝔖 (t i'_1.1) (V i'_1.2) ⊆ UniformOnFun.gen 𝔖 (s, i').1 (V (s, i').2)
⊢ HasBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (𝓤 (α →ᵤ[𝔖] β)) (fun (i : ι × ι') ↦ p i.2) fun (i : ι × ι') ↦
    UniformOnFun.gen 𝔖 (t i.1) (V i.2)

Tactic:
refine (UniformOnFun.hasBasis_uniformity_of_basis α β 𝔖 hne hd hb).to_hasBasis
    (fun ⟨s, i'⟩ ⟨hs, hi'⟩ ↦ ?_) fun ⟨i, i'⟩ hi' ↦ ⟨(t i, i'), ⟨ht i, hi'⟩, Subset.rfl⟩

Premises used: _private.0.UniformOnFun.hasBasis_uniformity_of_covering_of_basis.match_1, UniformOnFun.gen, Exists, Prod.mk, HasSubset.Subset, Prod.fst, And, UniformOnFun.hasBasis_uniformity_of_basis, _private.0.UniformOnFun.hasBasis_uniformity_of_covering_of_basis.match_2, Prod.snd, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst_1 : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ (i : ι), s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
hd : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
x : Prod.{u_1, u_6} (Set α) ι'
s : Set α
i' : ι'
h : (s, i').1 ∈ 𝔖 ∧ p (s, i').2
hs : (s, i').1 ∈ 𝔖
hi' : p (s, i').2
rcases :
  ∀ (i : ι) (hi : s ⊆ t i),
    ∃ (i'_1 : ι × ι'), p i'_1.2 ∧ UniformOnFun.gen 𝔖 (t i'_1.1) (V i'_1.2) ⊆ UniformOnFun.gen 𝔖 (s, i').1 (V (s, i').2)
⊢ ∃ (i'_1 : ι × ι'), p i'_1.2 ∧ UniformOnFun.gen 𝔖 (t i'_1.1) (V i'_1.2) ⊆ UniformOnFun.gen 𝔖 (s, i').1 (V (s, i').2)

Tactic:
rcases hex s hs with ⟨i, hi⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst_1 : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ (i : ι), s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
hd : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
x : Prod.{u_1, u_6} (Set α) ι'
s : Set α
i' : ι'
h : (s, i').1 ∈ 𝔖 ∧ p (s, i').2
hs : (s, i').1 ∈ 𝔖
hi' : p (s, i').2
i : ι
hi : s ⊆ t i
⊢ ∃ (i'_1 : ι × ι'), p i'_1.2 ∧ UniformOnFun.gen 𝔖 (t i'_1.1) (V i'_1.2) ⊆ UniformOnFun.gen 𝔖 (s, i').1 (V (s, i').2)

Tactic:
⟨(i, i'), hi', UniformOnFun.gen_mono hi Subset.rfl⟩

Premises used: UniformOnFun.gen_mono, Prod.mk, Set.Subset.rfl, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
ι' : Type u_6
inst_1 : Nonempty ι
t : ι → Set α
p : ι' → Prop
V : ι' → Set (β × β)
ht : ∀ (i : ι), t i ∈ 𝔖
hdir : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) t
hex : ∀ s ∈ 𝔖, ∃ (i : ι), s ⊆ t i
hb : (𝓤 β).HasBasis p V
hne : 𝔖.Nonempty
hd : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
x : Prod.{u_1, u_6} (Set α) ι'
s : Set α
i' : ι'
h : (s, i').1 ∈ 𝔖 ∧ p (s, i').2
hs : (s, i').1 ∈ 𝔖
hi' : p (s, i').2
i : ι
hi : s ⊆ t i
⊢ ∃ (i'_1 : ι × ι'), p i'_1.2 ∧ UniformOnFun.gen 𝔖 (t i'_1.1) (V i'_1.2) ⊆ UniformOnFun.gen 𝔖 (s, i').1 (V (s, i').2)

Tactic:
exact ⟨(i, i'), hi', UniformOnFun.gen_mono hi Subset.rfl⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ (n : ι), s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
⊢ Nonempty ι

Tactic:
have := hb.nonempty
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ (n : ι), s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
this : Nonempty ι
⊢ HasAntitoneBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (𝓤 (α →ᵤ[𝔖] β)) fun (n : ι) ↦ UniformOnFun.gen 𝔖 (t n) (V n)

Tactic:
⟨(UniformOnFun.hasBasis_uniformity_of_covering_of_basis 𝔖
    ht hmono.directed_le hex hb.1).to_hasBasis ?_ fun i _ ↦ ⟨(i, i), trivial, Subset.rfl⟩, ?_⟩

Premises used: UniformOnFun.hasBasis_uniformity_of_covering_of_basis, trivial, Filter.HasAntitoneBasis.toHasBasis, Prod.mk, Filter.HasAntitoneBasis.mk, Set.Subset.rfl, And.intro, Exists.intro, Monotone.directed_le, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ (n : ι), s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
this : Nonempty ι
refine_1 :
  ∀ (i : ι × ι), True → ∃ (i' : ι), True ∧ UniformOnFun.gen 𝔖 (t i') (V i') ⊆ UniformOnFun.gen 𝔖 (t i.1) (V i.2)
refine_2 : Antitone (β := Set ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) fun (n : ι) ↦ UniformOnFun.gen 𝔖 (t n) (V n)
⊢ HasAntitoneBasis (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (𝓤 (α →ᵤ[𝔖] β)) fun (n : ι) ↦ UniformOnFun.gen 𝔖 (t n) (V n)

Tactic:
refine ⟨(UniformOnFun.hasBasis_uniformity_of_covering_of_basis 𝔖
    ht hmono.directed_le hex hb.1).to_hasBasis ?_ fun i _ ↦ ⟨(i, i), trivial, Subset.rfl⟩, ?_⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ (n : ι), s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
this : Nonempty ι
k l : ι
refine_1 :
  ∀ (n : ι) (hkn : k ≤ n) (hln : l ≤ n),
    ∃ (i' : ι), True ∧ UniformOnFun.gen 𝔖 (t i') (V i') ⊆ UniformOnFun.gen 𝔖 (t (k, l).1) (V (k, l).2)
⊢ ∃ (i' : ι), True ∧ UniformOnFun.gen 𝔖 (t i') (V i') ⊆ UniformOnFun.gen 𝔖 (t (k, l).1) (V (k, l).2)

Tactic:
rcases directed_of (· ≤ ·) k l with ⟨n, hkn, hln⟩

Premises used: LE.le, directed_of
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ (n : ι), s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
this : Nonempty ι
k l n : ι
hkn : k ≤ n
hln : l ≤ n
⊢ ∃ (i' : ι), True ∧ UniformOnFun.gen 𝔖 (t i') (V i') ⊆ UniformOnFun.gen 𝔖 (t (k, l).1) (V (k, l).2)

Tactic:
⟨n, trivial, UniformOnFun.gen_mono (hmono hkn) (hb.2 <| hln)⟩

Premises used: trivial, UniformOnFun.gen_mono, And.intro, Exists.intro, Filter.HasAntitoneBasis.antitone
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ (n : ι), s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
this : Nonempty ι
k l n : ι
hkn : k ≤ n
hln : l ≤ n
⊢ ∃ (i' : ι), True ∧ UniformOnFun.gen 𝔖 (t i') (V i') ⊆ UniformOnFun.gen 𝔖 (t (k, l).1) (V (k, l).2)

Tactic:
exact ⟨n, trivial, UniformOnFun.gen_mono (hmono hkn) (hb.2 <| hln)⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ (n : ι), s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
this : Nonempty ι
⊢ Antitone (β := Set ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) fun (n : ι) ↦ UniformOnFun.gen 𝔖 (t n) (V n)

Tactic:
fun k l h ↦ UniformOnFun.gen_mono (hmono h) (hb.2 h)

Premises used: UniformOnFun.gen_mono, Antitone, Filter.HasAntitoneBasis.antitone
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Type u_5
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
t : ι → Set α
V : ι → Set (β × β)
ht : ∀ (n : ι), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ (n : ι), s ⊆ t n
hb : (𝓤 β).HasAntitoneBasis V
this : Nonempty ι
⊢ Antitone (β := Set ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) fun (n : ι) ↦ UniformOnFun.gen 𝔖 (t n) (V n)

Tactic:
exact fun k l h ↦ UniformOnFun.gen_mono (hmono h) (hb.2 h)

Premises used: UniformOnFun.gen_mono, Filter.HasAntitoneBasis.antitone
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : (𝓤 β).IsCountablyGenerated
t : ℕ → Set α
ht : ∀ (n : ℕ), t n ∈ 𝔖
hmono : Monotone t
hex : ∀ s ∈ 𝔖, ∃ (n : ℕ), s ⊆ t n
⊢ IsCountablyGenerated (α := (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) (𝓤 (α →ᵤ[𝔖] β))

Tactic:
let ⟨_V, hV⟩ := exists_antitone_basis (𝓤 β)
  (UniformOnFun.hasAntitoneBasis_uniformity 𝔖 ht hmono hex hV).isCountablyGenerated

Premises used: Filter.HasAntitoneBasis.toHasBasis, uniformity, Filter.IsCountablyGenerated, _private.0.UniformOnFun.isCountablyGenerated_uniformity.match_1, UniformOnFun, Filter.exists_antitone_basis, UniformOnFun.hasAntitoneBasis_uniformity, Filter.HasBasis.isCountablyGenerated
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
f : α →ᵤ[𝔖] β
h : 𝔖.Nonempty
h' : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
⊢ (𝓝 f).HasBasis (fun (Si : Prod.{u_1, u_4} (Set α) ι) ↦ Si.1 ∈ 𝔖 ∧ p Si.2) fun (Si : Prod.{u_1, u_4} (Set α) ι) ↦
    {g : α →ᵤ[𝔖] β | (g, f) ∈ UniformOnFun.gen 𝔖 Si.1 (s Si.2)}

Tactic:
letI : UniformSpace (α → β) := UniformOnFun.uniformSpace α β 𝔖
  nhds_basis_uniformity (UniformOnFun.hasBasis_uniformity_of_basis α β 𝔖 h h' hb)

Premises used: Set.Mem, setOf, UniformOnFun.hasBasis_uniformity_of_basis, nhds_basis_uniformity
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
f : α →ᵤ[𝔖] β
h : 𝔖.Nonempty
h' : DirectedOn (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) 𝔖
⊢ (𝓝 f).HasBasis (fun (SV : Prod.{u_1, u_2} (Set α) (Set (β × β))) ↦ SV.1 ∈ 𝔖 ∧ SV.2 ∈ 𝓤 β)
    fun (SV : Prod.{u_1, u_2} (Set α) (Set (β × β))) ↦ {g : α →ᵤ[𝔖] β | (g, f) ∈ UniformOnFun.gen 𝔖 SV.1 SV.2}

Tactic:
UniformOnFun.hasBasis_nhds_of_basis α β 𝔖 f h h' (Filter.basis_sets _)

Premises used: Set.Mem, setOf, Filter.basis_sets, UniformOnFun.hasBasis_nhds_of_basis
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : UniformSpace β
𝔖 : Set (Set α)
h : s ∈ 𝔖
simp :
  LE.le (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (⨅ i ∈ 𝔖, 𝓤 (α →ᵤ[𝔖] β))
    (comap (β := UniformFun.{u_1, u_2} (↑s : Type u_1) β × UniformFun.{u_1, u_2} (↑s : Type u_1) β)
      (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
        (Function.comp (β := (↑s : Type u_1) → β)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
              (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
            (Function.comp (β := (a : α) → β) (s.restrict (π := fun (a : α) ↦ β))
                (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
              (α →ᵤ[𝔖] β) → (↑s : Type u_1) → β)
            x.1,
          Function.comp (β := (↑s : Type u_1) → β)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
              (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
            (Function.comp (β := (a : α) → β) (s.restrict (π := fun (a : α) ↦ β))
                (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
              (α →ᵤ[𝔖] β) → (↑s : Type u_1) → β)
            x.2))
      (𝓤 (UniformFun.{u_1, u_2} (↑s : Type u_1) β)))
⊢ LE.le (α := Filter (UniformFun.{u_1, u_2} (↑s : Type u_1) β × UniformFun.{u_1, u_2} (↑s : Type u_1) β))
    (map
      (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
        (Function.comp (β := (↑s : Type u_1) → β)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
              (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
            (Function.comp (β := (a : α) → β) (s.restrict (π := fun (a : α) ↦ β))
                (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
              (α →ᵤ[𝔖] β) → (↑s : Type u_1) → β)
            x.1,
          Function.comp (β := (↑s : Type u_1) → β)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
              (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
            (Function.comp (β := (a : α) → β) (s.restrict (π := fun (a : α) ↦ β))
                (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
              (α →ᵤ[𝔖] β) → (↑s : Type u_1) → β)
            x.2))
      (𝓤 (α →ᵤ[𝔖] β)))
    (𝓤 (UniformFun.{u_1, u_2} (↑s : Type u_1) β))

Tactic:
simp only [map_le_iff_le_comap, iInf_uniformity]

Premises used: iInf_uniformity, Filter.map_le_iff_le_comap
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : UniformSpace β
𝔖 : Set (Set α)
h : s ∈ 𝔖
⊢ LE.le (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (⨅ i ∈ 𝔖, 𝓤 (α →ᵤ[𝔖] β))
    (comap (β := UniformFun.{u_1, u_2} (↑s : Type u_1) β × UniformFun.{u_1, u_2} (↑s : Type u_1) β)
      (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
        (Function.comp (β := (↑s : Type u_1) → β)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
              (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
            (Function.comp (β := (a : α) → β) (s.restrict (π := fun (a : α) ↦ β))
                (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
              (α →ᵤ[𝔖] β) → (↑s : Type u_1) → β)
            x.1,
          Function.comp (β := (↑s : Type u_1) → β)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
              (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
            (Function.comp (β := (a : α) → β) (s.restrict (π := fun (a : α) ↦ β))
                (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
              (α →ᵤ[𝔖] β) → (↑s : Type u_1) → β)
            x.2))
      (𝓤 (UniformFun.{u_1, u_2} (↑s : Type u_1) β)))

Tactic:
iInf₂_le s h

Premises used: Set.Mem, iInf₂_le, setOf
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : UniformSpace β
𝔖 : Set (Set α)
h : s ∈ 𝔖
⊢ LE.le (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (⨅ i ∈ 𝔖, 𝓤 (α →ᵤ[𝔖] β))
    (comap (β := UniformFun.{u_1, u_2} (↑s : Type u_1) β × UniformFun.{u_1, u_2} (↑s : Type u_1) β)
      (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
        (Function.comp (β := (↑s : Type u_1) → β)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
              (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
            (Function.comp (β := (a : α) → β) (s.restrict (π := fun (a : α) ↦ β))
                (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
              (α →ᵤ[𝔖] β) → (↑s : Type u_1) → β)
            x.1,
          Function.comp (β := (↑s : Type u_1) → β)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
              (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
            (Function.comp (β := (a : α) → β) (s.restrict (π := fun (a : α) ↦ β))
                (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
              (α →ᵤ[𝔖] β) → (↑s : Type u_1) → β)
            x.2))
      (𝓤 (UniformFun.{u_1, u_2} (↑s : Type u_1) β)))

Tactic:
exact iInf₂_le s h

Premises used: iInf₂_le
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
⊢ IsUniformEmbedding (α := α →ᵤ[{s : Set α | s.Finite}] β) (β := α → β)
    (⇑(toFun {s : Set α | s.Finite}) : (a : α →ᵤ[{s : Set α | s.Finite}] β) → α → β)

Tactic:
⟨⟨?_⟩, Function.injective_id⟩

Premises used: Function.injective_id, IsUniformEmbedding.mk, IsUniformInducing.mk
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
refine :
  Eq (α := Filter ((α →ᵤ[{s : Set α | s.Finite}] β) × (α →ᵤ[{s : Set α | s.Finite}] β)))
    (comap (β := (α → β) × (α → β))
      (fun (x : (α →ᵤ[{s : Set α | s.Finite}] β) × (α →ᵤ[{s : Set α | s.Finite}] β)) ↦
        ((toFun {s : Set α | s.Finite} : (a : α →ᵤ[{s : Set α | s.Finite}] β) → α → β) x.1,
          (toFun {s : Set α | s.Finite} : (a : α →ᵤ[{s : Set α | s.Finite}] β) → α → β) x.2))
      (𝓤 (α → β)))
    (𝓤 (α →ᵤ[{s : Set α | s.Finite}] β))
⊢ IsUniformEmbedding (α := α →ᵤ[{s : Set α | s.Finite}] β) (β := α → β)
    (⇑(toFun {s : Set α | s.Finite}) : (a : α →ᵤ[{s : Set α | s.Finite}] β) → α → β)

Tactic:
refine ⟨⟨?_⟩, Function.injective_id⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
simp_rw :
  Eq (α := Filter ((α →ᵤ[{s : Set α | s.Finite}] β) × (α →ᵤ[{s : Set α | s.Finite}] β)))
    (⨅ (i : α),
      comap
        ((fun (a : ((i : α) → β) × ((i : α) → β)) ↦ (a.1 i, a.2 i)) ∘
          fun (x : (α →ᵤ[{s : Set α | s.Finite}] β) × (α →ᵤ[{s : Set α | s.Finite}] β)) ↦
          ((toFun {s : Set α | s.Finite} : (a : α →ᵤ[{s : Set α | s.Finite}] β) → α → β) x.1,
            (toFun {s : Set α | s.Finite} : (a : α →ᵤ[{s : Set α | s.Finite}] β) → α → β) x.2))
        (𝓤 β))
    (𝓤 (α →ᵤ[{s : Set α | s.Finite}] β))
⊢ Eq (α := Filter ((α →ᵤ[{s : Set α | s.Finite}] β) × (α →ᵤ[{s : Set α | s.Finite}] β)))
    (comap (β := (α → β) × (α → β))
      (fun (x : (α →ᵤ[{s : Set α | s.Finite}] β) × (α →ᵤ[{s : Set α | s.Finite}] β)) ↦
        ((toFun {s : Set α | s.Finite} : (a : α →ᵤ[{s : Set α | s.Finite}] β) → α → β) x.1,
          (toFun {s : Set α | s.Finite} : (a : α →ᵤ[{s : Set α | s.Finite}] β) → α → β) x.2))
      (𝓤 (α → β)))
    (𝓤 (α →ᵤ[{s : Set α | s.Finite}] β))

Tactic:
simp_rw [Pi.uniformity, comap_iInf, comap_comap]

Premises used: Filter.comap_iInf, Filter.comap_comap, Pi.uniformity