-- 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 φ₂
⊢ 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 φ₁
⊢ uniformSpace α β 𝔖 =
    UniformSpace.comap (⇑(ofFun 𝔗₁) ∘ (fun x => x ∘ φ₁) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₁ β 𝔗₁) ⊓
      UniformSpace.comap (⇑(ofFun 𝔗₂) ∘ (fun x => x ∘ φ₂) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₂ β 𝔗₂)

Proof state:
case refine_3
α : 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)) β)
S : Set α
hS : S ∈ 𝔖
⊢ (⨅ i ∈ 𝔗₁,
        UniformSpace.comap
          ((⇑UniformFun.ofFun ∘ i.restrict ∘ ⇑(toFun 𝔗₁)) ∘ ⇑(ofFun 𝔗₁) ∘ (fun x => x ∘ φ₁) ∘ ⇑(toFun 𝔖))
          (UniformFun.uniformSpace (↑i) β)) ⊓
      ⨅ i ∈ 𝔗₂,
        UniformSpace.comap
          ((⇑UniformFun.ofFun ∘ i.restrict ∘ ⇑(toFun 𝔗₂)) ∘ ⇑(ofFun 𝔗₂) ∘ (fun x => x ∘ φ₂) ∘ ⇑(toFun 𝔖))
          (UniformFun.uniformSpace (↑i) β) ≤
    UniformSpace.comap ((fun x => x ∘ ψ₁ S) ∘ ⇑UniformFun.ofFun ∘ S.restrict ∘ ⇑(toFun 𝔖))
        (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
      UniformSpace.comap ((fun x => x ∘ ψ₂ S) ∘ ⇑UniformFun.ofFun ∘ S.restrict ∘ ⇑(toFun 𝔖))
        (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)

Tactic:
exact inf_le_inf
  (iInf₂_le_of_le _ (h_preimage₁ hS) le_rfl)
  (iInf₂_le_of_le _ (h_preimage₂ hS) le_rfl)

Result:
no goals

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 ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      UniformSpace.comap (fun x => x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
        UniformSpace.comap (fun x => x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)

Tactic:
refine fun S hS ↦ UniformFun.uniformSpace_eq_inf_precomp_of_cover β _ _ ?_

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 φ₂
S : Set α
hS : S ∈ 𝔖
⊢ range (ψ₁ S) ∪ range (ψ₂ S) = univ

Proof state:
case refine_3
α : 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)) β)
S : Set α
hS : S ∈ 𝔖
⊢ UniformSpace.comap (⇑(ofFun 𝔗₁) ∘ (fun x => x ∘ φ₁) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₁ β 𝔗₁) ⊓
      UniformSpace.comap (⇑(ofFun 𝔗₂) ∘ (fun x => x ∘ φ₂) ∘ ⇑(toFun 𝔖)) (uniformSpace δ₂ β 𝔗₂) ≤
    UniformSpace.comap (⇑UniformFun.ofFun ∘ S.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑S) β)

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

Result:
case refine_3
α : 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)) β)
S : Set α
hS : S ∈ 𝔖
⊢ (⨅ i ∈ 𝔗₁,
        UniformSpace.comap
          ((⇑UniformFun.ofFun ∘ i.restrict ∘ ⇑(toFun 𝔗₁)) ∘ ⇑(ofFun 𝔗₁) ∘ (fun x => x ∘ φ₁) ∘ ⇑(toFun 𝔖))
          (UniformFun.uniformSpace (↑i) β)) ⊓
      ⨅ i ∈ 𝔗₂,
        UniformSpace.comap
          ((⇑UniformFun.ofFun ∘ i.restrict ∘ ⇑(toFun 𝔗₂)) ∘ ⇑(ofFun 𝔗₂) ∘ (fun x => x ∘ φ₂) ∘ ⇑(toFun 𝔖))
          (UniformFun.uniformSpace (↑i) β) ≤
    UniformSpace.comap ((fun x => x ∘ ψ₁ S) ∘ ⇑UniformFun.ofFun ∘ S.restrict ∘ ⇑(toFun 𝔖))
        (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
      UniformSpace.comap ((fun x => x ∘ ψ₂ S) ∘ ⇑UniformFun.ofFun ∘ S.restrict ∘ ⇑(toFun 𝔖))
        (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)