awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
⊢ Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (⨅ (i : ι),
      UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ))
        (UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ UniformOnFun.{u_1, u_5} α (δ i) 𝔖) i)
          (uniformSpace α (δ i) 𝔖)))
    (⨅ (i : ι), uniformSpace α ((i : ι) → δ i) 𝔖)

Tactic:
iInf_congr fun i => ?_

Premises used: iInf_congr, UniformOnFun
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
comap_uniformity :
  ∀ (i : ι),
    Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
      (UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ))
        (UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ UniformOnFun.{u_1, u_5} α (δ i) 𝔖) i)
          (uniformSpace α (δ i) 𝔖)))
      (uniformSpace α ((i : ι) → δ i) 𝔖)
⊢ Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (⨅ (i : ι),
      UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ))
        (UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ UniformOnFun.{u_1, u_5} α (δ i) 𝔖) i)
          (uniformSpace α (δ i) 𝔖)))
    (⨅ (i : ι), uniformSpace α ((i : ι) → δ i) 𝔖)

Tactic:
refine iInf_congr fun i => ?_

Premises used: iInf_congr
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
i : ι
comap_uniformity :
  Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (UniformSpace.comap
        (Function.eval (β := fun (i : ι) ↦ UniformOnFun.{u_1, u_5} α (δ i) 𝔖) i ∘ Function.swap (φ := fun (a : α) ↦ δ))
        (uniformSpace α (δ i) 𝔖) :
      UniformSpace ((x : α) → (y : ι) → δ y))
    (UniformSpace.comap (β := α → δ i) (fun (x : α → (i : ι) → δ i) ↦ Function.eval (β := δ) i ∘ x)
        (uniformSpace α (δ i) 𝔖) :
      UniformSpace (α → (i : ι) → δ i))
⊢ Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (UniformSpace.comap (Function.swap (φ := fun (a : α) ↦ δ))
      (UniformSpace.comap (Function.eval (β := fun (i : ι) ↦ UniformOnFun.{u_1, u_5} α (δ i) 𝔖) i)
        (uniformSpace α (δ i) 𝔖)))
    (uniformSpace α ((i : ι) → δ i) 𝔖)

Tactic:
rw [← UniformSpace.comap_comap, UniformOnFun.comap_eq]

Premises used: UniformSpace.comap_comap, UniformOnFun.comap_eq
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
inst_1 : (i : ι) → UniformSpace (δ i)
i : ι
⊢ Eq (α := UniformSpace ((x : α) → (y : ι) → δ y))
    (UniformSpace.comap
        (Function.eval (β := fun (i : ι) ↦ UniformOnFun.{u_1, u_5} α (δ i) 𝔖) i ∘ Function.swap (φ := fun (a : α) ↦ δ))
        (uniformSpace α (δ i) 𝔖) :
      UniformSpace ((x : α) → (y : ι) → δ y))
    (UniformSpace.comap (β := α → δ i) (fun (x : α → (i : ι) → δ i) ↦ Function.eval (β := δ) i ∘ x)
        (uniformSpace α (δ i) 𝔖) :
      UniformSpace (α → (i : ι) → δ i))

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : TopologicalSpace α
h : IsCoherentWith 𝔖
⊢ IsClosed[topologicalSpace α β 𝔖]
    {f : α →ᵤ[𝔖] β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)}

Tactic:
isClosed_iff_forall_filter.2 fun f u _ hu huf ↦ h.continuous_iff.2 fun s hs ↦ ?_

Premises used: Iff.mpr, Topology.IsCoherentWith.continuous_iff, isClosed_iff_forall_filter
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : TopologicalSpace α
h : IsCoherentWith 𝔖
refine :
  ∀ (f : α →ᵤ[𝔖] β) (u : Filter (α →ᵤ[𝔖] β)),
    u.NeBot →
      ∀
        (hu :
          u ≤ 𝓟 {f : α →ᵤ[𝔖] β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)})
        (huf : u ≤ 𝓝 f) (s : Set α) (hs : s ∈ 𝔖),
        ContinuousOn.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) s
⊢ IsClosed[topologicalSpace α β 𝔖]
    {f : α →ᵤ[𝔖] β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)}

Tactic:
refine isClosed_iff_forall_filter.2 fun f u _ hu huf ↦ h.continuous_iff.2 fun s hs ↦ ?_

Premises used: Iff.mpr, Topology.IsCoherentWith.continuous_iff, isClosed_iff_forall_filter
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : TopologicalSpace α
h : IsCoherentWith 𝔖
f : α →ᵤ[𝔖] β
u : Filter (α →ᵤ[𝔖] β)
h_1 : u.NeBot
hu : u ≤ 𝓟 {f : α →ᵤ[𝔖] β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)}
huf : u ≤ 𝓝 f
s : Set α
hs : s ∈ 𝔖
rw :
  ∀
    (huf :
      ∀ s ∈ 𝔖,
        TendstoUniformlyOn (β := β) ((⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) ∘ id)
          ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) u s)
    (s : Set α) (hs : s ∈ 𝔖), ContinuousOn.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) s
⊢ ContinuousOn.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) s

Tactic:
rw [← tendsto_id', UniformOnFun.tendsto_iff_tendstoUniformlyOn] at huf

Premises used: UniformOnFun.tendsto_iff_tendstoUniformlyOn, Filter.tendsto_id'
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : TopologicalSpace α
h : IsCoherentWith 𝔖
f : α →ᵤ[𝔖] β
u : Filter (α →ᵤ[𝔖] β)
h_1 : u.NeBot
hu : u ≤ 𝓟 {f : α →ᵤ[𝔖] β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)}
huf :
  ∀ s ∈ 𝔖,
    TendstoUniformlyOn (β := β) ((⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) ∘ id) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) u
      s
s : Set α
hs : s ∈ 𝔖
⊢ ContinuousOn.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) s

Tactic:
(huf s hs).continuousOn <| Eventually.frequently <| hu fun _ ↦ Continuous.continuousOn

Premises used: Continuous.continuousOn, Filter.Eventually.frequently, TendstoUniformlyOn.continuousOn
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
inst_1 : TopologicalSpace α
h : IsCoherentWith 𝔖
f : α →ᵤ[𝔖] β
u : Filter (α →ᵤ[𝔖] β)
h_1 : u.NeBot
hu : u ≤ 𝓟 {f : α →ᵤ[𝔖] β | Continuous[inst_1, inst.toTopologicalSpace] ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)}
huf :
  ∀ s ∈ 𝔖,
    TendstoUniformlyOn (β := β) ((⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) ∘ id) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) u
      s
s : Set α
hs : s ∈ 𝔖
⊢ ContinuousOn.{u_1, u_2} (Y := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f) s

Tactic:
exact (huf s hs).continuousOn <| Eventually.frequently <| hu fun _ ↦ Continuous.continuousOn

Premises used: Continuous.continuousOn, Filter.Eventually.frequently, TendstoUniformlyOn.continuousOn
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → (↑(φ₁ ⁻¹' S) : Type u_5) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → (↑(φ₂ ⁻¹' S) : Type u_6) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₂
⊢ ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (UniformSpace.comap (β := (↑(φ₁ ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₁ S)
          (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S) : Type u_5) β) ⊓
        UniformSpace.comap (β := (↑(φ₂ ⁻¹' S) : Type u_6) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₂ S)
          (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S) : Type u_6) β))

Tactic:
fun S hS ↦ UniformFun.uniformSpace_eq_inf_precomp_of_cover β _ _ ?_

Premises used: Set.Mem, setOf, UniformFun, UniformFun.uniformSpace_eq_inf_precomp_of_cover
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → (↑(φ₁ ⁻¹' S) : Type u_5) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → (↑(φ₂ ⁻¹' S) : Type u_6) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₂
refine : ∀ (S : Set α) (hS : S ∈ 𝔖), range (ψ₁ S) ∪ range (ψ₂ S) = univ
⊢ ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (UniformSpace.comap (β := (↑(φ₁ ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₁ S)
          (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S) : Type u_5) β) ⊓
        UniformSpace.comap (β := (↑(φ₂ ⁻¹' S) : Type u_6) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₂ S)
          (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S) : Type u_6) β))

Tactic:
refine fun S hS ↦ UniformFun.uniformSpace_eq_inf_precomp_of_cover β _ _ ?_

Premises used: UniformFun.uniformSpace_eq_inf_precomp_of_cover
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → (↑(φ₁ ⁻¹' S) : Type u_5) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → (↑(φ₂ ⁻¹' S) : Type u_6) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₂
S : Set α
hS : S ∈ 𝔖
⊢ range (ψ₁ S) ∪ range (ψ₂ S) = univ

Tactic:
simpa only [← univ_subset_iff, ψ₁, ψ₂, range_restrictPreimage, ← preimage_union,
      ← image_subset_iff, image_univ, Subtype.range_val] using h_cover S hS

Premises used: Set.univ_subset_iff, Set.image_univ, Set.range_restrictPreimage, Subtype.range_val, Set.preimage_union, Set.image_subset_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → (↑(φ₁ ⁻¹' S) : Type u_5) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → (↑(φ₂ ⁻¹' S) : Type u_6) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₂
⊢ ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (UniformSpace.comap (β := (↑(φ₁ ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₁ S)
          (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S) : Type u_5) β) ⊓
        UniformSpace.comap (β := (↑(φ₂ ⁻¹' S) : Type u_6) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₂ S)
          (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S) : Type u_6) β))

Tactic:
have : ∀ S ∈ 𝔖, 𝒰(S, β, _) = .comap (· ∘ ψ₁ S) 𝒰(_, β, _) ⊓ .comap (· ∘ ψ₂ S) 𝒰(_, β, _) := by
    refine fun S hS ↦ UniformFun.uniformSpace_eq_inf_precomp_of_cover β _ _ ?_
    simpa only [← univ_subset_iff, ψ₁, ψ₂, range_restrictPreimage, ← preimage_union,
      ← image_subset_iff, image_univ, Subtype.range_val] using h_cover S hS
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → (↑(φ₁ ⁻¹' S) : Type u_5) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → (↑(φ₂ ⁻¹' S) : Type u_6) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (UniformSpace.comap (β := (↑(φ₁ ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₁ S)
          (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S) : Type u_5) β) ⊓
        UniformSpace.comap (β := (↑(φ₂ ⁻¹' S) : Type u_6) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₂ S)
          (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S) : Type u_6) β))
⊢ uniformSpace α β 𝔖 =
    UniformSpace.comap
        (Function.comp (β := δ₁ → β) (⇑(ofFun 𝔗₁) : (a : δ₁ → β) → δ₁ →ᵤ[𝔗₁] β)
          ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
        (uniformSpace δ₁ β 𝔗₁) ⊓
      UniformSpace.comap
        (Function.comp (β := δ₂ → β) (⇑(ofFun 𝔗₂) : (a : δ₂ → β) → δ₂ →ᵤ[𝔗₂] β)
          ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
        (uniformSpace δ₂ β 𝔗₂)

Tactic:
le_antisymm (le_inf ?_ ?_) (le_iInf₂ fun S hS ↦ ?_)

Premises used: le_inf, le_iInf₂, le_antisymm
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → (↑(φ₁ ⁻¹' S) : Type u_5) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → (↑(φ₂ ⁻¹' S) : Type u_6) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (UniformSpace.comap (β := (↑(φ₁ ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₁ S)
          (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S) : Type u_5) β) ⊓
        UniformSpace.comap (β := (↑(φ₂ ⁻¹' S) : Type u_6) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₂ S)
          (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S) : Type u_6) β))
refine_1 :
  UniformContinuous (α := α →ᵤ[𝔖] β) (β := δ₁ →ᵤ[𝔗₁] β)
    (Function.comp (β := δ₁ → β) (⇑(ofFun 𝔗₁) : (a : δ₁ → β) → δ₁ →ᵤ[𝔗₁] β)
      ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
⊢ uniformSpace α β 𝔖 ≤
    UniformSpace.comap
      (Function.comp (β := δ₁ → β) (⇑(ofFun 𝔗₁) : (a : δ₁ → β) → δ₁ →ᵤ[𝔗₁] β)
        ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
      (uniformSpace δ₁ β 𝔗₁)

Tactic:
rw [← uniformContinuous_iff]

Premises used: uniformContinuous_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → (↑(φ₁ ⁻¹' S) : Type u_5) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → (↑(φ₂ ⁻¹' S) : Type u_6) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (UniformSpace.comap (β := (↑(φ₁ ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₁ S)
          (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S) : Type u_5) β) ⊓
        UniformSpace.comap (β := (↑(φ₂ ⁻¹' S) : Type u_6) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₂ S)
          (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S) : Type u_6) β))
⊢ UniformContinuous (α := α →ᵤ[𝔖] β) (β := δ₁ →ᵤ[𝔗₁] β)
    (Function.comp (β := δ₁ → β) (⇑(ofFun 𝔗₁) : (a : δ₁ → β) → δ₁ →ᵤ[𝔗₁] β)
      ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))

Tactic:
UniformOnFun.precomp_uniformContinuous h_image₁

Premises used: UniformOnFun.precomp_uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → (↑(φ₁ ⁻¹' S) : Type u_5) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → (↑(φ₂ ⁻¹' S) : Type u_6) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (UniformSpace.comap (β := (↑(φ₁ ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₁ S)
          (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S) : Type u_5) β) ⊓
        UniformSpace.comap (β := (↑(φ₂ ⁻¹' S) : Type u_6) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₂ S)
          (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S) : Type u_6) β))
⊢ UniformContinuous (α := α →ᵤ[𝔖] β) (β := δ₁ →ᵤ[𝔗₁] β)
    (Function.comp (β := δ₁ → β) (⇑(ofFun 𝔗₁) : (a : δ₁ → β) → δ₁ →ᵤ[𝔗₁] β)
      ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))

Tactic:
exact UniformOnFun.precomp_uniformContinuous h_image₁

Premises used: UniformOnFun.precomp_uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → (↑(φ₁ ⁻¹' S) : Type u_5) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → (↑(φ₂ ⁻¹' S) : Type u_6) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (UniformSpace.comap (β := (↑(φ₁ ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₁ S)
          (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S) : Type u_5) β) ⊓
        UniformSpace.comap (β := (↑(φ₂ ⁻¹' S) : Type u_6) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₂ S)
          (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S) : Type u_6) β))
refine_2 :
  UniformContinuous (α := α →ᵤ[𝔖] β) (β := δ₂ →ᵤ[𝔗₂] β)
    (Function.comp (β := δ₂ → β) (⇑(ofFun 𝔗₂) : (a : δ₂ → β) → δ₂ →ᵤ[𝔗₂] β)
      ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
⊢ uniformSpace α β 𝔖 ≤
    UniformSpace.comap
      (Function.comp (β := δ₂ → β) (⇑(ofFun 𝔗₂) : (a : δ₂ → β) → δ₂ →ᵤ[𝔗₂] β)
        ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
      (uniformSpace δ₂ β 𝔗₂)

Tactic:
rw [← uniformContinuous_iff]

Premises used: uniformContinuous_iff
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → (↑(φ₁ ⁻¹' S) : Type u_5) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → (↑(φ₂ ⁻¹' S) : Type u_6) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (UniformSpace.comap (β := (↑(φ₁ ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₁ S)
          (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S) : Type u_5) β) ⊓
        UniformSpace.comap (β := (↑(φ₂ ⁻¹' S) : Type u_6) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₂ S)
          (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S) : Type u_6) β))
⊢ UniformContinuous (α := α →ᵤ[𝔖] β) (β := δ₂ →ᵤ[𝔗₂] β)
    (Function.comp (β := δ₂ → β) (⇑(ofFun 𝔗₂) : (a : δ₂ → β) → δ₂ →ᵤ[𝔗₂] β)
      ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))

Tactic:
UniformOnFun.precomp_uniformContinuous h_image₂

Premises used: UniformOnFun.precomp_uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → (↑(φ₁ ⁻¹' S) : Type u_5) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → (↑(φ₂ ⁻¹' S) : Type u_6) → (↑S : Type u_1) := fun (S : Set α) ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (UniformSpace.comap (β := (↑(φ₁ ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₁ S)
          (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S) : Type u_5) β) ⊓
        UniformSpace.comap (β := (↑(φ₂ ⁻¹' S) : Type u_6) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₂ S)
          (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S) : Type u_6) β))
⊢ UniformContinuous (α := α →ᵤ[𝔖] β) (β := δ₂ →ᵤ[𝔗₂] β)
    (Function.comp (β := δ₂ → β) (⇑(ofFun 𝔗₂) : (a : δ₂ → β) → δ₂ →ᵤ[𝔗₂] β)
      ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))

Tactic:
exact UniformOnFun.precomp_uniformContinuous h_image₂

Premises used: UniformOnFun.precomp_uniformContinuous