awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
comap_uniformity :
  UniformSpace.comap
      (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β)
        ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ)))
      (uniformSpace α β 𝔖) =
    uniformSpace α γ 𝔖
⊢ Eq (α := Filter ((α →ᵤ[𝔖] γ) × (α →ᵤ[𝔖] γ))) (𝓤 (α →ᵤ[𝔖] γ)) (𝓤 (α →ᵤ[𝔖] γ))

Tactic:
congr
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
comap_uniformity :
  Eq (α := UniformSpace (α →ᵤ[𝔖] γ))
    (UniformSpace.comap
      (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β)
        ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ)))
      (uniformSpace α β 𝔖))
    (UniformSpace.comap (fun (x : α → γ) ↦ f ∘ x) (uniformSpace α β 𝔖))
⊢ UniformSpace.comap
      (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β)
        ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ)))
      (uniformSpace α β 𝔖) =
    uniformSpace α γ 𝔖

Tactic:
rw [← UniformSpace.ext hf, UniformOnFun.comap_eq]

Premises used: UniformSpace.ext, UniformOnFun.comap_eq
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : UniformSpace γ
f : γ → β
hf : 𝓤 γ = 𝓤 γ
⊢ Eq (α := UniformSpace (α →ᵤ[𝔖] γ))
    (UniformSpace.comap
      (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β)
        ((fun (x : α → γ) ↦ f ∘ x) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] γ) → α → γ)))
      (uniformSpace α β 𝔖))
    (UniformSpace.comap (fun (x : α → γ) ↦ f ∘ x) (uniformSpace α β 𝔖))

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : MapsTo (fun (x : Set γ) ↦ f '' x) 𝔗 𝔖
simp_rw :
  ∀ (i : Set γ) (i_1 : i ∈ 𝔗) (i_2 : Set (β × β)) (i_3 : i_2 ∈ 𝓤 β),
    Tendsto
      (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
        ((ofFun 𝔗 : (a : γ → β) → γ →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1 ∘ f),
          (ofFun 𝔗 : (a : γ → β) → γ →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2 ∘ f)))
      (⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V)) (𝓟 (UniformOnFun.gen 𝔗 i i_2))
⊢ UniformContinuous (β := γ →ᵤ[𝔗] β) fun (g : α →ᵤ[𝔖] β) ↦
    (ofFun 𝔗 : (a : γ → β) → γ →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g ∘ f)

Tactic:
simp_rw [UniformContinuous, UniformOnFun.uniformity_eq, tendsto_iInf]

Premises used: UniformContinuous, Filter.tendsto_iInf, UniformOnFun.uniformity_eq
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : MapsTo (fun (x : Set γ) ↦ f '' x) 𝔗 𝔖
⊢ ∀ (i : Set γ) (i_1 : i ∈ 𝔗) (i_2 : Set (β × β)) (i_3 : i_2 ∈ 𝓤 β),
    Tendsto
      (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
        ((ofFun 𝔗 : (a : γ → β) → γ →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1 ∘ f),
          (ofFun 𝔗 : (a : γ → β) → γ →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2 ∘ f)))
      (⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V)) (𝓟 (UniformOnFun.gen 𝔗 i i_2))

Tactic:
fun t ht V hV ↦ tendsto_iInf' (f '' t) <| tendsto_iInf' (hf ht) <|
    tendsto_iInf' V <| tendsto_iInf' hV ?_

Premises used: Filter.tendsto_iInf', Set.image
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : MapsTo (fun (x : Set γ) ↦ f '' x) 𝔗 𝔖
refine :
  ∀ (t : Set γ) (ht : t ∈ 𝔗) (V : Set (β × β)) (hV : V ∈ 𝓤 β),
    Tendsto
      (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
        ((ofFun 𝔗 : (a : γ → β) → γ →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1 ∘ f),
          (ofFun 𝔗 : (a : γ → β) → γ →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2 ∘ f)))
      (𝓟 (UniformOnFun.gen 𝔖 (f '' t) V)) (𝓟 (UniformOnFun.gen 𝔗 t V))
⊢ ∀ (i : Set γ) (i_1 : i ∈ 𝔗) (i_2 : Set (β × β)) (i_3 : i_2 ∈ 𝓤 β),
    Tendsto
      (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
        ((ofFun 𝔗 : (a : γ → β) → γ →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1 ∘ f),
          (ofFun 𝔗 : (a : γ → β) → γ →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2 ∘ f)))
      (⨅ s ∈ 𝔖, ⨅ V ∈ 𝓤 β, 𝓟 (UniformOnFun.gen 𝔖 s V)) (𝓟 (UniformOnFun.gen 𝔗 i i_2))

Tactic:
refine fun t ht V hV ↦ tendsto_iInf' (f '' t) <| tendsto_iInf' (hf ht) <|
    tendsto_iInf' V <| tendsto_iInf' hV ?_

Premises used: Filter.tendsto_iInf', Set.image
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
f : γ → α
hf : MapsTo (fun (x : Set γ) ↦ f '' x) 𝔗 𝔖
t : Set γ
ht : t ∈ 𝔗
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ Tendsto
    (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
      ((ofFun 𝔗 : (a : γ → β) → γ →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1 ∘ f),
        (ofFun 𝔗 : (a : γ → β) → γ →ᵤ[𝔗] β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2 ∘ f)))
    (𝓟 (UniformOnFun.gen 𝔖 (f '' t) V)) (𝓟 (UniformOnFun.gen 𝔗 t V))

Tactic:
simpa only [tendsto_principal_principal, UniformOnFun.gen] using fun _ ↦ forall_mem_image.1

Premises used: UniformOnFun.gen, Iff.mp, Set.forall_mem_image, Filter.tendsto_principal_principal
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s_1 : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
e : γ ≃ α
he : 𝔗 ⊆ image (⇑e : (a : γ) → α) ⁻¹' 𝔖
he' : 𝔖 ⊆ preimage (⇑e : (a : γ) → α) ⁻¹' 𝔗
s : Set α
hs : s ∈ 𝔖
change : (⇑e.symm : (a : α) → γ) '' s ∈ 𝔗
⊢ (fun (x : Set α) ↦ ((⇑e.symm : (a : α) → γ) '' x : Set γ)) s ∈ 𝔗

Tactic:
change e.symm '' s ∈ 𝔗

Premises used: Equiv.symm
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s_1 : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
e : γ ≃ α
he : 𝔗 ⊆ image (⇑e : (a : γ) → α) ⁻¹' 𝔖
he' : 𝔖 ⊆ preimage (⇑e : (a : γ) → α) ⁻¹' 𝔗
s : Set α
hs : s ∈ 𝔖
rw : (⇑e : (a : γ) → α) ⁻¹' s ∈ 𝔗
⊢ (⇑e.symm : (a : α) → γ) '' s ∈ 𝔗

Tactic:
rw [Equiv.image_symm_eq_preimage]

Premises used: Equiv.image_symm_eq_preimage
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s_1 : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
e : γ ≃ α
he : 𝔗 ⊆ image (⇑e : (a : γ) → α) ⁻¹' 𝔖
he' : 𝔖 ⊆ preimage (⇑e : (a : γ) → α) ⁻¹' 𝔗
s : Set α
hs : s ∈ 𝔖
⊢ (⇑e : (a : γ) → α) ⁻¹' s ∈ 𝔗

Tactic:
he' hs

Premises used: Set.Mem, setOf, Set.preimage
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s_1 : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
e : γ ≃ α
he : 𝔗 ⊆ image (⇑e : (a : γ) → α) ⁻¹' 𝔖
he' : 𝔖 ⊆ preimage (⇑e : (a : γ) → α) ⁻¹' 𝔗
s : Set α
hs : s ∈ 𝔖
⊢ (⇑e : (a : γ) → α) ⁻¹' s ∈ 𝔗

Tactic:
exact he' hs
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
obtain :
  ∀ (x : α) (hx : ¬f x = g x),
    ∃ (u : Set (α →ᵤ[𝔖] β)) (v : Set (α →ᵤ[𝔖] β)),
      IsOpen[topologicalSpace α β 𝔖] u ∧ IsOpen[topologicalSpace α β 𝔖] v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
⊢ ∃ (u : Set (α →ᵤ[𝔖] β)) (v : Set (α →ᵤ[𝔖] β)),
    IsOpen[topologicalSpace α β 𝔖] u ∧ IsOpen[topologicalSpace α β 𝔖] v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v

Tactic:
obtain ⟨x, hx⟩ := not_forall.mp (mt funext hfg)

Premises used: mt, funext, Iff.mp, Classical.not_forall
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
x : α
hx : ¬f x = g x
⊢ ∃ s ∈ 𝔖, x ∈ s

Tactic:
mem_sUnion.mp (h.symm ▸ True.intro)

Premises used: Eq.rec, Iff.mp, Set.mem_sUnion, Eq.symm, True.intro
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
x : α
hx : ¬f x = g x
obtain :
  ∀ (s : Set α) (hs : s ∈ 𝔖) (hxs : x ∈ s),
    ∃ (u : Set (α →ᵤ[𝔖] β)) (v : Set (α →ᵤ[𝔖] β)),
      IsOpen[topologicalSpace α β 𝔖] u ∧ IsOpen[topologicalSpace α β 𝔖] v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v
⊢ ∃ (u : Set (α →ᵤ[𝔖] β)) (v : Set (α →ᵤ[𝔖] β)),
    IsOpen[topologicalSpace α β 𝔖] u ∧ IsOpen[topologicalSpace α β 𝔖] v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v

Tactic:
obtain ⟨s, hs, hxs⟩ : ∃ s ∈ 𝔖, x ∈ s := mem_sUnion.mp (h.symm ▸ True.intro)

Premises used: Iff.mp, Set.mem_sUnion
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
x : α
hx : ¬f x = g x
s : Set α
hs : s ∈ 𝔖
hxs : x ∈ s
⊢ ∃ (u : Set (α →ᵤ[𝔖] β)) (v : Set (α →ᵤ[𝔖] β)),
    IsOpen[topologicalSpace α β 𝔖] u ∧ IsOpen[topologicalSpace α β 𝔖] v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v

Tactic:
separated_by_continuous (uniformContinuous_eval_of_mem β 𝔖 hxs hs).continuous hx

Premises used: separated_by_continuous, UniformContinuous.continuous, UniformOnFun.uniformContinuous_eval_of_mem
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : T2Space β
h : ⋃₀ 𝔖 = univ
f g : α →ᵤ[𝔖] β
hfg : f ≠ g
x : α
hx : ¬f x = g x
s : Set α
hs : s ∈ 𝔖
hxs : x ∈ s
⊢ ∃ (u : Set (α →ᵤ[𝔖] β)) (v : Set (α →ᵤ[𝔖] β)),
    IsOpen[topologicalSpace α β 𝔖] u ∧ IsOpen[topologicalSpace α β 𝔖] v ∧ f ∈ u ∧ g ∈ v ∧ Disjoint u v

Tactic:
exact separated_by_continuous (uniformContinuous_eval_of_mem β 𝔖 hxs hs).continuous hx

Premises used: separated_by_continuous, UniformContinuous.continuous, UniformOnFun.uniformContinuous_eval_of_mem
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
rw :
  ∀ (i : (↑(⋃₀ 𝔖) : Type u_1)),
    UniformContinuous (β := β) fun (x : α →ᵤ[𝔖] β) ↦
      Function.comp (β := α → β) ((⋃₀ 𝔖).restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x i
⊢ UniformContinuous (α := α →ᵤ[𝔖] β) (β := (↑(⋃₀ 𝔖) : Type u_1) → β)
    (Function.comp (β := α → β) ((⋃₀ 𝔖).restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
      (α →ᵤ[𝔖] β) → (↑(⋃₀ 𝔖) : Type u_1) → β)

Tactic:
rw [uniformContinuous_pi]

Premises used: uniformContinuous_pi
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
x : α
hx : x ∈ ⋃₀ 𝔖
obtain :
  ∀ (s : Set α) (hs : s ∈ 𝔖) (hxs : x ∈ s),
    UniformContinuous (β := β) fun (x_1 : α →ᵤ[𝔖] β) ↦
      Function.comp (β := α → β) ((⋃₀ 𝔖).restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x_1
        (Subtype.mk (p := fun (x : α) ↦ x ∈ ⋃₀ 𝔖) x hx)
⊢ UniformContinuous (β := β) fun (x_1 : α →ᵤ[𝔖] β) ↦
    Function.comp (β := α → β) ((⋃₀ 𝔖).restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x_1
      (Subtype.mk (p := fun (x : α) ↦ x ∈ ⋃₀ 𝔖) x hx)

Tactic:
obtain ⟨s : Set α, hs : s ∈ 𝔖, hxs : x ∈ s⟩ := mem_sUnion.mpr hx

Premises used: Iff.mpr, Set.mem_sUnion, Set
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
x : α
hx : x ∈ ⋃₀ 𝔖
s : Set α
hs : s ∈ 𝔖
hxs : x ∈ s
⊢ UniformContinuous (β := β) fun (x_1 : α →ᵤ[𝔖] β) ↦
    Function.comp (β := α → β) ((⋃₀ 𝔖).restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x_1
      (Subtype.mk (p := fun (x : α) ↦ x ∈ ⋃₀ 𝔖) x hx)

Tactic:
uniformContinuous_eval_of_mem β 𝔖 hxs hs

Premises used: Set.restrict, UniformOnFun.uniformContinuous_eval_of_mem
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
x : α
hx : x ∈ ⋃₀ 𝔖
s : Set α
hs : s ∈ 𝔖
hxs : x ∈ s
⊢ UniformContinuous (β := β) fun (x_1 : α →ᵤ[𝔖] β) ↦
    Function.comp (β := α → β) ((⋃₀ 𝔖).restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) x_1
      (Subtype.mk (p := fun (x : α) ↦ x ∈ ⋃₀ 𝔖) x hx)

Tactic:
exact uniformContinuous_eval_of_mem β 𝔖 hxs hs

Premises used: UniformOnFun.uniformContinuous_eval_of_mem
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
simp_rw :
  ⨅ (i : Set α),
      ⨅ (x : i ∈ 𝔖),
        UniformSpace.comap (β := UniformFun.{u_1, u_2} (↑i : Type u_1) β)
          (Function.comp (β := (s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β)
              (Function.eval (β := fun (s : (↑𝔖 : Type u_1)) ↦ UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β)
                (Subtype.mk (p := fun (x : Set α) ↦ x ∈ 𝔖) i ⋯))
              fun (f : α →ᵤ[𝔖] β) (s : (↑𝔖 : Type u_1)) ↦
              (UniformFun.ofFun : (a : (↑(↑s : Set α) : Type u_1) → β) → (↑(↑s : Set α) : Type u_1) →ᵤ β)
                ((↑s : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)) :
            (α →ᵤ[𝔖] β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
          (UniformFun.uniformSpace (↑i : Type u_1) β : UniformSpace (UniformFun.{u_1, u_2} (↑i : Type u_1) β)) =
    uniformSpace α β 𝔖
⊢ IsUniformInducing (β := (s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β)
    fun (f : α →ᵤ[𝔖] β) (s : (↑𝔖 : Type u_1)) ↦
    (UniformFun.ofFun : (a : (↑(↑s : Set α) : Type u_1) → β) → (↑(↑s : Set α) : Type u_1) →ᵤ β)
      ((↑s : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f))

Tactic:
simp_rw [isUniformInducing_iff_uniformSpace, Pi.uniformSpace_eq, UniformSpace.comap_iInf,
    ← UniformSpace.comap_comap, iInf_subtype]

Premises used: Pi.uniformSpace_eq, iInf_subtype, isUniformInducing_iff_uniformSpace, UniformSpace.comap_comap, UniformSpace.comap_iInf
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
⊢ ⨅ (i : Set α),
      ⨅ (x : i ∈ 𝔖),
        UniformSpace.comap (β := UniformFun.{u_1, u_2} (↑i : Type u_1) β)
          (Function.comp (β := (s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β)
              (Function.eval (β := fun (s : (↑𝔖 : Type u_1)) ↦ UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β)
                (Subtype.mk (p := fun (x : Set α) ↦ x ∈ 𝔖) i ⋯))
              fun (f : α →ᵤ[𝔖] β) (s : (↑𝔖 : Type u_1)) ↦
              (UniformFun.ofFun : (a : (↑(↑s : Set α) : Type u_1) → β) → (↑(↑s : Set α) : Type u_1) →ᵤ β)
                ((↑s : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)) :
            (α →ᵤ[𝔖] β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
          (UniformFun.uniformSpace (↑i : Type u_1) β : UniformSpace (UniformFun.{u_1, u_2} (↑i : Type u_1) β)) =
    uniformSpace α β 𝔖

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
rw : ∀ (i : α), UniformContinuous (β := β) fun (x : α →ᵤ[𝔖] β) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x i
⊢ UniformContinuous (α := α →ᵤ[𝔖] β) (β := α → β) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)

Tactic:
rw [uniformContinuous_pi]

Premises used: uniformContinuous_pi
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
⊢ ∀ (i : α), UniformContinuous (β := β) fun (x : α →ᵤ[𝔖] β) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x i

Tactic:
uniformContinuous_eval h

Premises used: UniformOnFun.uniformContinuous_eval
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
h : ⋃₀ 𝔖 = univ
⊢ ∀ (i : α), UniformContinuous (β := β) fun (x : α →ᵤ[𝔖] β) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x i

Tactic:
exact uniformContinuous_eval h

Premises used: UniformOnFun.uniformContinuous_eval
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x
hc : ContinuousAt.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) x
rw :
  ∀ s ∈ 𝓤 β,
    ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x),
      Membership.mem (α := β × β) (SetRel.comp s s)
        (Function.comp (β := β) (Prod.mk ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f, x).1 (f, x).2))
            (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) a :
          β × β)
⊢ ContinuousAt (Y := β) (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) (f, x)

Tactic:
rw [ContinuousAt, nhds_eq_comap_uniformity, tendsto_comap_iff, ← lift'_comp_uniformity,
    tendsto_lift']

Premises used: Filter.tendsto_lift', ContinuousAt, Filter.tendsto_comap_iff, lift'_comp_uniformity, nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x
hc : ContinuousAt.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) x
U : Set (β × β)
hU : U ∈ 𝓤 β
rcases :
  ∀ (V : Set α) (hV : V ∈ 𝔖) (hVx : V ∈ 𝓝 x),
    ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x),
      Membership.mem (α := β × β) (SetRel.comp U U)
        (Function.comp (β := β) (Prod.mk ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f, x).1 (f, x).2))
            (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) a :
          β × β)
⊢ ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x),
    Membership.mem (α := β × β) (SetRel.comp U U)
      (Function.comp (β := β) (Prod.mk ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f, x).1 (f, x).2))
          (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) a :
        β × β)

Tactic:
rcases h𝔖 with ⟨V, hV, hVx⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
hc : ContinuousAt.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) x
U : Set (β × β)
hU : U ∈ 𝓤 β
V : Set α
hV : V ∈ 𝔖
hVx : V ∈ 𝓝 x
g : α →ᵤ[𝔖] β
y : α
h :
  ∀
    (hg :
      Membership.mem (γ := Set (α →ᵤ[𝔖] β))
        {g : α →ᵤ[𝔖] β |
          ∀ x ∈ V,
            Membership.mem (α := β × β) U
              (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
        (g, y).1)
    (hyV : (g, y).2 ∈ V)
    (hy :
      Membership.mem (γ := Set α)
        (preimage.{u_1, u_2} (β := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f : α → β)
          (UniformSpace.ball ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) U : Set β))
        (g, y).2),
    Membership.mem (α := β × β) (SetRel.comp U U)
      (Function.comp (β := β) (Prod.mk ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x))
          (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) (g, y) :
        β × β)
⊢ (g, y) ∈
      SProd.sprod (α := Set (α →ᵤ[𝔖] β))
        {g : α →ᵤ[𝔖] β |
          ∀ x ∈ V,
            Membership.mem (α := β × β) U
              (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
        (V ∩
          preimage.{u_1, u_2} (β := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f : α → β)
            (UniformSpace.ball ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) U : Set β)) →
    Membership.mem (α := β × β) (SetRel.comp U U)
      (Function.comp (β := β) (Prod.mk ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x))
          (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) (g, y) :
        β × β)

Tactic:
⟨hg, hyV, hy⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
hc : ContinuousAt.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) x
U : Set (β × β)
hU : U ∈ 𝓤 β
V : Set α
hV : V ∈ 𝔖
hVx : V ∈ 𝓝 x
g : α →ᵤ[𝔖] β
y : α
hg :
  Membership.mem (γ := Set (α →ᵤ[𝔖] β))
    {g : α →ᵤ[𝔖] β |
      ∀ x ∈ V,
        Membership.mem (α := β × β) U
          (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x) : β × β)}
    (g, y).1
hyV : (g, y).2 ∈ V
hy :
  Membership.mem (γ := Set α)
    (preimage.{u_1, u_2} (β := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f : α → β)
      (UniformSpace.ball ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x) U : Set β))
    (g, y).2
⊢ Membership.mem (α := β × β) (SetRel.comp U U)
    (Function.comp (β := β) (Prod.mk ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x))
        (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2) (g, y) :
      β × β)

Tactic:
⟨toFun 𝔖 f y, hy, hg y hyV⟩

Premises used: Set.Mem, setOf, UniformOnFun.toFun, SetRel.comp, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : TopologicalSpace α
h𝔖 : ∀ (x : α), ∃ V ∈ 𝔖, V ∈ 𝓝 x
⊢ ContinuousOn (Y := β) (fun (fx : (α →ᵤ[𝔖] β) × α) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1 fx.2)
    {fx : (α →ᵤ[𝔖] β) × α | ContinuousAt.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) fx.1) fx.2}

Tactic:
fun (_f, x) hc ↦
  (UniformOnFun.continuousAt_eval₂ (h𝔖 x) hc).continuousWithinAt

Premises used: ContinuousWithinAt, ContinuousAt, setOf, ContinuousAt.continuousWithinAt, UniformOnFun.toFun, Prod.fst, ContinuousOn, _private.0.UniformOnFun.continuousOn_eval₂.match_1, UniformOnFun.continuousAt_eval₂, Prod.snd, DFunLike.coe
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
F : ι → α →ᵤ[𝔖] β
f : α →ᵤ[𝔖] β
⊢ Tendsto F p (𝓝 f) ↔
    ∀ s ∈ 𝔖,
      TendstoUniformlyOn.{u_1, u_2, u_4} (β := β) ((⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) ∘ F)
        ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) p s

Tactic:
simp only [UniformOnFun.nhds_eq, tendsto_iInf, tendsto_principal, TendstoUniformlyOn,
    Function.comp_apply, mem_setOf]

Premises used: Filter.tendsto_principal, Set.mem_setOf, TendstoUniformlyOn, Filter.tendsto_iInf, Function.comp_apply, UniformOnFun.nhds_eq
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
X : Type u_5
inst_1 : TopologicalSpace X
f : X → α →ᵤ[𝔖] β
⊢ Continuous[inst_1, topologicalSpace α β 𝔖] f ↔
    ∀ s ∈ 𝔖,
      Continuous[inst_1, UniformFun.topologicalSpace (↑s : Type u_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 (β := α → β) (s.restrict (π := fun (a : α) ↦ β)) ((⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) ∘ f) :
            X → (↑s : Type u_1) → β))

Tactic:
simp only [continuous_iff_continuousAt, ContinuousAt,
    UniformOnFun.tendsto_iff_tendstoUniformlyOn, UniformFun.tendsto_iff_tendstoUniformly,
    tendstoUniformlyOn_iff_tendstoUniformly_comp_coe, @forall_comm X,
    Function.comp_def, restrict_eq, UniformFun.toFun_ofFun]

Premises used: UniformFun.toFun_ofFun, ContinuousAt, UniformOnFun.tendsto_iff_tendstoUniformlyOn, UniformFun.tendsto_iff_tendstoUniformly, forall_comm, Function.comp_def, tendstoUniformlyOn_iff_tendstoUniformly_comp_coe, Set.restrict_eq, continuous_iff_continuousAt