awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → (↑(φ i ⁻¹' S) : Type u_5) → (↑S : Type u_1) :=
  fun (S : Set α) (i : ι) ↦ S.restrictPreimage (φ i)
S : Set α
hS : S ∈ 𝔖
rcases :
  ∀ (I : Set ι) (I_finite : I.Finite) (I_cover : S ⊆ ⋃ i ∈ I, range (φ i)),
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (⨅ (i : ι),
        UniformSpace.comap (β := (↑(φ i ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ S i)
          (UniformFun.uniformSpace (↑(φ i ⁻¹' S) : Type u_5) β))
⊢ Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
    (⨅ (i : ι),
      UniformSpace.comap (β := (↑(φ i ⁻¹' S) : Type u_5) → β)
        (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ S i)
        (UniformFun.uniformSpace (↑(φ i ⁻¹' S) : Type u_5) β))

Tactic:
rcases h_cover S hS with ⟨I, I_finite, I_cover⟩
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → (↑(φ i ⁻¹' S) : Type u_5) → (↑S : Type u_1) :=
  fun (S : Set α) (i : ι) ↦ S.restrictPreimage (φ i)
S : Set α
hS : S ∈ 𝔖
I : Set ι
I_finite : I.Finite
I_cover : S ⊆ ⋃ i ∈ I, range (φ i)
⊢ Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
    (⨅ (i : ι),
      UniformSpace.comap (β := (↑(φ i ⁻¹' S) : Type u_5) → β)
        (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ S i)
        (UniformFun.uniformSpace (↑(φ i ⁻¹' S) : Type u_5) β))

Tactic:
UniformFun.uniformSpace_eq_iInf_precomp_of_cover β _ ⟨I, I_finite, ?_⟩

Premises used: UniformFun.uniformSpace_eq_iInf_precomp_of_cover, UniformFun, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → (↑(φ i ⁻¹' S) : Type u_5) → (↑S : Type u_1) :=
  fun (S : Set α) (i : ι) ↦ S.restrictPreimage (φ i)
S : Set α
hS : S ∈ 𝔖
I : Set ι
I_finite : I.Finite
I_cover : S ⊆ ⋃ i ∈ I, range (φ i)
refine : Eq.{u_1 + 1} (α := Set (↑S : Type u_1)) (⋃ i ∈ I, range (ψ S i)) univ
⊢ Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
    (⨅ (i : ι),
      UniformSpace.comap (β := (↑(φ i ⁻¹' S) : Type u_5) → β)
        (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ S i)
        (UniformFun.uniformSpace (↑(φ i ⁻¹' S) : Type u_5) β))

Tactic:
refine UniformFun.uniformSpace_eq_iInf_precomp_of_cover β _ ⟨I, I_finite, ?_⟩

Premises used: UniformFun.uniformSpace_eq_iInf_precomp_of_cover, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → (↑(φ i ⁻¹' S) : Type u_5) → (↑S : Type u_1) :=
  fun (S : Set α) (i : ι) ↦ S.restrictPreimage (φ i)
S : Set α
hS : S ∈ 𝔖
I : Set ι
I_finite : I.Finite
I_cover : S ⊆ ⋃ i ∈ I, range (φ i)
⊢ Eq.{u_1 + 1} (α := Set (↑S : Type u_1)) (⋃ i ∈ I, range (ψ S i)) univ

Tactic:
simpa only [← univ_subset_iff, ψ, range_restrictPreimage, ← preimage_iUnion₂,
      ← image_subset_iff, image_univ, Subtype.range_val] using I_cover

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

Tactic:
have : ∀ S ∈ 𝔖, 𝒰(S, β, _) = ⨅ i, .comap (· ∘ ψ S i) 𝒰(_, β, _) := fun S hS ↦ by
    rcases h_cover S hS with ⟨I, I_finite, I_cover⟩
    refine UniformFun.uniformSpace_eq_iInf_precomp_of_cover β _ ⟨I, I_finite, ?_⟩
    simpa only [← univ_subset_iff, ψ, range_restrictPreimage, ← preimage_iUnion₂,
      ← image_subset_iff, image_univ, Subtype.range_val] using I_cover
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → (↑(φ i ⁻¹' S) : Type u_5) → (↑S : Type u_1) :=
  fun (S : Set α) (i : ι) ↦ S.restrictPreimage (φ i)
this :
  ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (⨅ (i : ι),
        UniformSpace.comap (β := (↑(φ i ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ S i)
          (UniformFun.uniformSpace (↑(φ i ⁻¹' S) : Type u_5) β))
⊢ uniformSpace α β 𝔖 =
    ⨅ (i : ι),
      UniformSpace.comap
        (Function.comp (β := δ i → β) (⇑(ofFun (𝔗 i)) : (a : δ i → β) → δ i →ᵤ[𝔗 i] β)
          ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
        (uniformSpace (δ i) β (𝔗 i))

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

Premises used: le_iInf, le_iInf₂, le_antisymm
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → (↑(φ i ⁻¹' S) : Type u_5) → (↑S : Type u_1) :=
  fun (S : Set α) (i : ι) ↦ S.restrictPreimage (φ i)
this :
  ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (⨅ (i : ι),
        UniformSpace.comap (β := (↑(φ i ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ S i)
          (UniformFun.uniformSpace (↑(φ i ⁻¹' S) : Type u_5) β))
refine_1 :
  ∀ (i : ι),
    uniformSpace α β 𝔖 ≤
      UniformSpace.comap
        (Function.comp (β := δ i → β) (⇑(ofFun (𝔗 i)) : (a : δ i → β) → δ i →ᵤ[𝔗 i] β)
          ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
        (uniformSpace (δ i) β (𝔗 i))
refine_2 :
  ∀ (S : Set α) (hS : S ∈ 𝔖),
    LE.le (α := UniformSpace (α →ᵤ[𝔖] β))
      (⨅ (i : ι),
        UniformSpace.comap
          (Function.comp (β := δ i → β) (⇑(ofFun (𝔗 i)) : (a : δ i → β) → δ i →ᵤ[𝔗 i] β)
            ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
          (uniformSpace (δ i) β (𝔗 i)))
      (UniformSpace.comap (β := UniformFun.{u_1, u_2} (↑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 : α →ᵤ[𝔖] β) → α → β) :
            (α →ᵤ[𝔖] β) → (↑S : Type u_1) → β))
        (UniformFun.uniformSpace (↑S : Type u_1) β))
⊢ uniformSpace α β 𝔖 =
    ⨅ (i : ι),
      UniformSpace.comap
        (Function.comp (β := δ i → β) (⇑(ofFun (𝔗 i)) : (a : δ i → β) → δ i →ᵤ[𝔗 i] β)
          ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
        (uniformSpace (δ i) β (𝔗 i))

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

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

Tactic:
rw [← uniformContinuous_iff]

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

Tactic:
UniformOnFun.precomp_uniformContinuous (h_image i)

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

Tactic:
exact UniformOnFun.precomp_uniformContinuous (h_image i)

Premises used: UniformOnFun.precomp_uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → (↑(φ i ⁻¹' S) : Type u_5) → (↑S : Type u_1) :=
  fun (S : Set α) (i : ι) ↦ S.restrictPreimage (φ i)
this :
  ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (⨅ (i : ι),
        UniformSpace.comap (β := (↑(φ i ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ S i)
          (UniformFun.uniformSpace (↑(φ i ⁻¹' S) : Type u_5) β))
S : Set α
hS : S ∈ 𝔖
⊢ LE.le (α := UniformSpace (α →ᵤ[𝔖] β))
    (⨅ (i : ι),
      ⨅ i_1 ∈ 𝔗 i,
        UniformSpace.comap (β := UniformFun.{u_5, u_2} (↑i_1 : Type u_5) β)
          (Function.comp (β := δ i →ᵤ[𝔗 i] β)
            (Function.comp (β := (↑i_1 : Type u_5) → β)
              ((⇑UniformFun.ofFun : (a : (↑i_1 : Type u_5) → β) → UniformFun.{u_5, u_2} (↑i_1 : Type u_5) β) :
                (a : (↑i_1 : Type u_5) → β) → UniformFun.{u_5, u_2} (↑i_1 : Type u_5) β)
              (Function.comp (β := δ i → β) (i_1.restrict (π := fun (a : δ i) ↦ β))
                  (⇑(toFun (𝔗 i)) : (a : δ i →ᵤ[𝔗 i] β) → δ i → β) :
                (δ i →ᵤ[𝔗 i] β) → (↑i_1 : Type u_5) → β))
            (Function.comp (β := δ i → β) (⇑(ofFun (𝔗 i)) : (a : δ i → β) → δ i →ᵤ[𝔗 i] β)
              ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β))))
          (UniformFun.uniformSpace (↑i_1 : Type u_5) β))
    (⨅ (i : ι),
      UniformSpace.comap (β := (↑(φ i ⁻¹' S) : Type u_5) → β)
        ((fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ S i) ∘
          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 : α →ᵤ[𝔖] β) → α → β) :
              (α →ᵤ[𝔖] β) → (↑S : Type u_1) → β))
        (UniformFun.uniformSpace (↑(φ i ⁻¹' S) : Type u_5) β))

Tactic:
iInf_mono fun i ↦ iInf₂_le_of_le _ (h_preimage i hS) le_rfl

Premises used: le_rfl, Set.Mem, setOf, iInf₂_le_of_le, iInf_mono, Set.preimage
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
ι : Type u_4
inst : UniformSpace β
𝔖 : Set (Set α)
δ : ι → Type u_5
φ : (i : ι) → δ i → α
𝔗 : (i : ι) → Set (Set (δ i))
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → (↑(φ i ⁻¹' S) : Type u_5) → (↑S : Type u_1) :=
  fun (S : Set α) (i : ι) ↦ S.restrictPreimage (φ i)
this :
  ∀ S ∈ 𝔖,
    Eq (α := UniformSpace (UniformFun.{u_1, u_2} (↑S : Type u_1) β)) (UniformFun.uniformSpace (↑S : Type u_1) β)
      (⨅ (i : ι),
        UniformSpace.comap (β := (↑(φ i ⁻¹' S) : Type u_5) → β)
          (fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ S i)
          (UniformFun.uniformSpace (↑(φ i ⁻¹' S) : Type u_5) β))
S : Set α
hS : S ∈ 𝔖
⊢ LE.le (α := UniformSpace (α →ᵤ[𝔖] β))
    (⨅ (i : ι),
      ⨅ i_1 ∈ 𝔗 i,
        UniformSpace.comap (β := UniformFun.{u_5, u_2} (↑i_1 : Type u_5) β)
          (Function.comp (β := δ i →ᵤ[𝔗 i] β)
            (Function.comp (β := (↑i_1 : Type u_5) → β)
              ((⇑UniformFun.ofFun : (a : (↑i_1 : Type u_5) → β) → UniformFun.{u_5, u_2} (↑i_1 : Type u_5) β) :
                (a : (↑i_1 : Type u_5) → β) → UniformFun.{u_5, u_2} (↑i_1 : Type u_5) β)
              (Function.comp (β := δ i → β) (i_1.restrict (π := fun (a : δ i) ↦ β))
                  (⇑(toFun (𝔗 i)) : (a : δ i →ᵤ[𝔗 i] β) → δ i → β) :
                (δ i →ᵤ[𝔗 i] β) → (↑i_1 : Type u_5) → β))
            (Function.comp (β := δ i → β) (⇑(ofFun (𝔗 i)) : (a : δ i → β) → δ i →ᵤ[𝔗 i] β)
              ((fun (x : α → β) ↦ x ∘ φ i) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β))))
          (UniformFun.uniformSpace (↑i_1 : Type u_5) β))
    (⨅ (i : ι),
      UniformSpace.comap (β := (↑(φ i ⁻¹' S) : Type u_5) → β)
        ((fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ S i) ∘
          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 : α →ᵤ[𝔖] β) → α → β) :
              (α →ᵤ[𝔖] β) → (↑S : Type u_1) → β))
        (UniformFun.uniformSpace (↑(φ i ⁻¹' S) : Type u_5) β))

Tactic:
exact iInf_mono fun i ↦ iInf₂_le_of_le _ (h_preimage i hS) le_rfl

Premises used: le_rfl, iInf₂_le_of_le, iInf_mono, Set.preimage
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
inst_1 : CompleteSpace β
⊢ CompleteSpace (α →ᵤ β)

Tactic:
(UniformOnFun.uniformEquivUniformFun β {univ} (mem_singleton _)).completeSpace_iff.1 inferInstance

Premises used: Set.mem_singleton, Set.univ, inferInstance, UniformOnFun.uniformEquivUniformFun, UniformEquiv.completeSpace_iff, Iff.mp, Singleton.singleton
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF : ∀ (i : ι) (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
⊢ UniformContinuous (s.restrict (π := fun (a : β) ↦ γ) g)

Tactic:
rw [uniformContinuousOn_iff_restrict] at hg

Premises used: uniformContinuousOn_iff_restrict
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF : ∀ (i : ι) (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
hg₁ : UniformContinuous (s.restrict (π := fun (a : β) ↦ γ) g)
⊢ TendstoUniformly F f p

Tactic:
rw [uniformContinuousOn_iff_restrict] at hg

Premises used: uniformContinuousOn_iff_restrict
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF : ∀ (i : ι) (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuous (s.restrict (π := fun (a : β) ↦ γ) g)
h : TendstoUniformly F f p
⊢ ∀ (i : ι) (i_1 : α), F i i_1 ∈ s

Tactic:
hF
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF : ∀ (i : ι) (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuous (s.restrict (π := fun (a : β) ↦ γ) g)
h : TendstoUniformly F f p
lift :
  ∀ (F' : (i : ι) → α → (↑s : Type u_2)) (hF' : (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) = F)
    (comp_tendstoUniformly :
      ∀ (hF : ∀ (i : ι) (x : α), (↑(F' i x) : β) ∈ s) (hf : ∀ (x : α), f x ∈ s) (hg : UniformContinuousOn g s)
        (h : TendstoUniformly (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) f p),
        TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β)) (fun (x : α) ↦ g (f x)) p)
    (h : TendstoUniformly (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) f p),
    TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β)) (fun (x : α) ↦ g (f x)) p
⊢ TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (F i x)) (fun (x : α) ↦ g (f x)) p

Tactic:
lift F to ι → α → s using hF with F' hF'
-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst : UniformSpace β
inst_1 : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuous (s.restrict (π := fun (a : β) ↦ γ) g)
F' : (i : ι) → α → (↑s : Type u_2)
hF' : (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) = F
comp_tendstoUniformly :
  ∀ (hF : ∀ (i : ι) (x : α), (↑(F' i x) : β) ∈ s) (hf : ∀ (x : α), f x ∈ s) (hg : UniformContinuousOn g s)
    (h : TendstoUniformly (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) f p),
    TendstoUniformly.{u_1, u_3, u_4} (β := γ) (fun (i : ι) (x : α) ↦ g (↑(F' i x) : β)) (fun (x : α) ↦ g (f x)) p
h : TendstoUniformly (fun (i : ι) (i_1 : α) ↦ (↑(F' i i_1) : β)) f p
⊢ ∀ (i : α), f i ∈ s

Tactic:
hf