-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem uniformSpace_eq_inf_precomp_of_cover {δ₁ δ₂ : Type*} (φ₁ : δ₁ → α) (φ₂ : δ₂ → α)
    (𝔗₁ : Set (Set δ₁)) (𝔗₂ : Set (Set δ₂))
    (h_image₁ : MapsTo (φ₁ '' ·) 𝔗₁ 𝔖) (h_image₂ : MapsTo (φ₂ '' ·) 𝔗₂ 𝔖)
    (h_preimage₁ : MapsTo (φ₁ ⁻¹' ·) 𝔖 𝔗₁) (h_preimage₂ : MapsTo (φ₂ ⁻¹' ·) 𝔖 𝔗₂)
    (h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂) :
    𝒱(α, β, 𝔖, _) =
      .comap (ofFun 𝔗₁ ∘ (· ∘ φ₁) ∘ toFun 𝔖) 𝒱(δ₁, β, 𝔗₁, _) ⊓
      .comap (ofFun 𝔗₂ ∘ (· ∘ φ₂) ∘ toFun 𝔖) 𝒱(δ₂, β, 𝔗₂, _)

Proof state:
α : 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 => φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x => φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x => φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x => φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S => S.restrictPreimage φ₁
⊢ uniformSpace α β 𝔖 =
    UniformSpace.comap (⇑(ofFun 𝔗₁) ∘ (fun x => x ∘ φ₁) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₁ β 𝔗₁) ⊓
      UniformSpace.comap (⇑(ofFun 𝔗₂) ∘ (fun x => x ∘ φ₂) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₂ β 𝔗₂)

Tactic:
set ψ₂ : Π S : Set α, φ₂ ⁻¹' S → S := fun S ↦ S.restrictPreimage φ₂

Result:
α : 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 => φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x => φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x => φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x => φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S => S.restrictPreimage φ₁
ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S => S.restrictPreimage φ₂
⊢ uniformSpace α β 𝔖 =
    UniformSpace.comap (⇑(ofFun 𝔗₁) ∘ (fun x => x ∘ φ₁) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₁ β 𝔗₁) ⊓
      UniformSpace.comap (⇑(ofFun 𝔗₂) ∘ (fun x => x ∘ φ₂) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₂ β 𝔗₂)

Proof state:
α : 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 => φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x => φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x => φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x => φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S => S.restrictPreimage φ₁
ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S => S.restrictPreimage φ₂
S : Set α
hS : S ∈ 𝔖
⊢ range (ψ₁ S) ∪ range (ψ₂ S) = univ

Tactic:
simpa only [← univ_subset_iff, ψ₁, ψ₂, range_restrictPreimage, ← preimage_union,
  ← image_subset_iff, image_univ, Subtype.range_val] using h_cover S hS

Result:
no goals

Proof state:
case refine_2
α : 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 => φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x => φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x => φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x => φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S => S.restrictPreimage φ₁
ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S => S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      UniformSpace.comap (fun x => x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
        UniformSpace.comap (fun x => x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)
⊢ UniformContinuous (⇑(ofFun 𝔗₂) ∘ (fun x => x ∘ φ₂) ∘ ⇑(toFun 𝔖))

Tactic:
exact UniformOnFun.precomp_uniformContinuous h_image₂

Result:
no goals

Proof state:
case refine_2
α : 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 => φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x => φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x => φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x => φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S => S.restrictPreimage φ₁
ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S => S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      UniformSpace.comap (fun x => x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
        UniformSpace.comap (fun x => x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)
⊢ uniformSpace α β 𝔖 ≤ UniformSpace.comap (⇑(ofFun 𝔗₂) ∘ (fun x => x ∘ φ₂) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₂ β 𝔗₂)

Tactic:
rw [← uniformContinuous_iff]

Result:
case refine_2
α : 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 => φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x => φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x => φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x => φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S => S.restrictPreimage φ₁
ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S => S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      UniformSpace.comap (fun x => x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
        UniformSpace.comap (fun x => x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)
⊢ UniformContinuous (⇑(ofFun 𝔗₂) ∘ (fun x => x ∘ φ₂) ∘ ⇑(toFun 𝔖))