-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem uniformSpace_eq_iInf_precomp_of_cover {δ : ι → Type*} (φ : Π i, δ i → α)
    (𝔗 : ∀ i, Set (Set (δ i))) (h_image : ∀ i, MapsTo (φ i '' ·) (𝔗 i) 𝔖)
    (h_preimage : ∀ i, MapsTo (φ i ⁻¹' ·) 𝔖 (𝔗 i))
    (h_cover : ∀ S ∈ 𝔖, ∃ I : Set ι, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)) :
    𝒱(α, β, 𝔖, _) = ⨅ i, .comap (ofFun (𝔗 i) ∘ (· ∘ φ i) ∘ toFun 𝔖) 𝒱(δ i, β, 𝔗 i, _)

Proof state:
α : 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 => φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x => φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i => S.restrictPreimage (φ i)
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      ⨅ i, UniformSpace.comap (fun x => x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)
⊢ uniformSpace α β 𝔖 =
    ⨅ i, UniformSpace.comap (⇑(ofFun (𝔗 i)) ∘ (fun x => x ∘ φ i) ∘ ⇑(toFun 𝔖)) (uniformSpace (δ i) β (𝔗 i))

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

Result:
case refine_1
α : 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 => φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x => φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i => S.restrictPreimage (φ i)
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      ⨅ i, UniformSpace.comap (fun x => x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)
i : ι
⊢ uniformSpace α β 𝔖 ≤
    UniformSpace.comap (⇑(ofFun (𝔗 i)) ∘ (fun x => x ∘ φ i) ∘ ⇑(toFun 𝔖)) (uniformSpace (δ i) β (𝔗 i))

case refine_2
α : 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 => φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x => φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i => S.restrictPreimage (φ i)
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      ⨅ i, UniformSpace.comap (fun x => x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)
S : Set α
hS : S ∈ 𝔖
⊢ ⨅ i, UniformSpace.comap (⇑(ofFun (𝔗 i)) ∘ (fun x => x ∘ φ i) ∘ ⇑(toFun 𝔖)) (uniformSpace (δ i) β (𝔗 i)) ≤
    UniformSpace.comap (⇑UniformFun.ofFun ∘ S.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑S) β)

Proof state:
case intro.intro
α : 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 => φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x => φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i => S.restrictPreimage (φ i)
S : Set α
hS : S ∈ 𝔖
I : Set ι
I_finite : I.Finite
I_cover : S ⊆ ⋃ i ∈ I, range (φ i)
⊢ UniformFun.uniformSpace (↑S) β =
    ⨅ i, UniformSpace.comap (fun x => x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)

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

Result:
case intro.intro
α : 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 => φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x => φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i => S.restrictPreimage (φ i)
S : Set α
hS : S ∈ 𝔖
I : Set ι
I_finite : I.Finite
I_cover : S ⊆ ⋃ i ∈ I, range (φ i)
⊢ ⋃ i ∈ I, range (ψ S i) = univ

Proof state:
case refine_1
α : 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 => φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x => φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i => S.restrictPreimage (φ i)
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      ⨅ i, UniformSpace.comap (fun x => x ∘ ψ S i) (UniformFun.uniformSpace (↑(φ i ⁻¹' S)) β)
i : ι
⊢ UniformContinuous (⇑(ofFun (𝔗 i)) ∘ (fun x => x ∘ φ i) ∘ ⇑(toFun 𝔖))

Tactic:
exact UniformOnFun.precomp_uniformContinuous (h_image i)

Result:
no goals

Proof state:
α : 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 => φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x => φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
⊢ uniformSpace α β 𝔖 =
    ⨅ i, UniformSpace.comap (⇑(ofFun (𝔗 i)) ∘ (fun x => x ∘ φ i) ∘ ⇑(toFun 𝔖)) (uniformSpace (δ i) β (𝔗 i))

Tactic:
set ψ : Π S : Set α, Π i : ι, (φ i) ⁻¹' S → S := fun S i ↦ S.restrictPreimage (φ i)

Result:
α : 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 => φ i '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x => φ i ⁻¹' x) 𝔖 (𝔗 i)
h_cover : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i)
ψ : (S : Set α) → (i : ι) → ↑(φ i ⁻¹' S) → ↑S := fun S i => S.restrictPreimage (φ i)
⊢ uniformSpace α β 𝔖 =
    ⨅ i, UniformSpace.comap (⇑(ofFun (𝔗 i)) ∘ (fun x => x ∘ φ i) ∘ ⇑(toFun 𝔖)) (uniformSpace (δ i) β (𝔗 i))