-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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 ∈ 𝔖
⊢ 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) β))
have 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) β))
Tactic: simp_rw [this S hS, uniformSpace, UniformSpace.comap_iInf, UniformSpace.comap_inf,
      ← UniformSpace.comap_comap]