-- 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) β))
S : Set α
hS : S ∈ 𝔖
refine_3 :
  LE.le (α := UniformSpace (α →ᵤ[𝔖] β))
    ((⨅ i ∈ 𝔗₁,
        UniformSpace.comap (β := UniformFun.{u_5, u_2} (↑i : Type u_5) β)
          (Function.comp (β := δ₁ →ᵤ[𝔗₁] β)
            (Function.comp (β := (↑i : Type u_5) → β)
              ((⇑UniformFun.ofFun : (a : (↑i : Type u_5) → β) → UniformFun.{u_5, u_2} (↑i : Type u_5) β) :
                (a : (↑i : Type u_5) → β) → UniformFun.{u_5, u_2} (↑i : Type u_5) β)
              (Function.comp (β := δ₁ → β) (i.restrict (π := fun (a : δ₁) ↦ β))
                  (⇑(toFun 𝔗₁) : (a : δ₁ →ᵤ[𝔗₁] β) → δ₁ → β) :
                (δ₁ →ᵤ[𝔗₁] β) → (↑i : Type u_5) → β))
            (Function.comp (β := δ₁ → β) (⇑(ofFun 𝔗₁) : (a : δ₁ → β) → δ₁ →ᵤ[𝔗₁] β)
              ((fun (x : α → β) ↦ x ∘ φ₁) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β))))
          (UniformFun.uniformSpace (↑i : Type u_5) β)) ⊓
      ⨅ i ∈ 𝔗₂,
        UniformSpace.comap (β := UniformFun.{u_6, u_2} (↑i : Type u_6) β)
          (Function.comp (β := δ₂ →ᵤ[𝔗₂] β)
            (Function.comp (β := (↑i : Type u_6) → β)
              ((⇑UniformFun.ofFun : (a : (↑i : Type u_6) → β) → UniformFun.{u_6, u_2} (↑i : Type u_6) β) :
                (a : (↑i : Type u_6) → β) → UniformFun.{u_6, u_2} (↑i : Type u_6) β)
              (Function.comp (β := δ₂ → β) (i.restrict (π := fun (a : δ₂) ↦ β))
                  (⇑(toFun 𝔗₂) : (a : δ₂ →ᵤ[𝔗₂] β) → δ₂ → β) :
                (δ₂ →ᵤ[𝔗₂] β) → (↑i : Type u_6) → β))
            (Function.comp (β := δ₂ → β) (⇑(ofFun 𝔗₂) : (a : δ₂ → β) → δ₂ →ᵤ[𝔗₂] β)
              ((fun (x : α → β) ↦ x ∘ φ₂) ∘ (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β))))
          (UniformFun.uniformSpace (↑i : Type u_6) β))
    (UniformSpace.comap (β := (↑(φ₁ ⁻¹' S) : Type u_5) → β)
        ((fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₁ S) ∘
          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_5) β) ⊓
      UniformSpace.comap (β := (↑(φ₂ ⁻¹' S) : Type u_6) → β)
        ((fun (x : UniformFun.{u_1, u_2} (↑S : Type u_1) β) ↦ x ∘ ψ₂ S) ∘
          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_6) β))
⊢ 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) β))

Tactic:
simp_rw [this S hS, uniformSpace, UniformSpace.comap_iInf, UniformSpace.comap_inf,
      ← UniformSpace.comap_comap]

Premises used: UniformOnFun.uniformSpace, UniformSpace.comap_inf, UniformSpace.comap_comap, UniformSpace.comap_iInf