-- 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 ∈ 𝔖
refine_2 :
  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) β))
⊢ 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) β))

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

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