-- 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 :
  uniformSpace α β 𝔖 ≤
    UniformSpace.comap
      (Function.comp (β := δ₁ → β) (⇑(ofFun 𝔗₁) : (a : δ₁ → β) → δ₁ →ᵤ[𝔗₁] β)
        ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
      (uniformSpace δ₁ β 𝔗₁)
refine_2 :
  uniformSpace α β 𝔖 ≤
    UniformSpace.comap
      (Function.comp (β := δ₂ → β) (⇑(ofFun 𝔗₂) : (a : δ₂ → β) → δ₂ →ᵤ[𝔗₂] β)
        ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β)))
      (uniformSpace δ₂ β 𝔗₂)
refine_3 :
  ∀ (S : Set α) (hS : S ∈ 𝔖),
    LE.le (α := 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 δ₂ β 𝔗₂))
      (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 α β 𝔖 =
    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:
refine le_antisymm (le_inf ?_ ?_) (le_iInf₂ fun S hS ↦ ?_)

Premises used: le_inf, le_antisymm