α : Type u_1
β : Type u_3
γ : Type u_2
ι : Type ?u.75481
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : γ → β
⊢ (⨅ (s : Set α) (_ : s ∈ 𝔖), UniformSpace.comap ((fun x => f ∘ x) ∘ restrict s) (UniformFun.uniformSpace (↑s) β)) =
    ⨅ (i : Set α) (_ : i ∈ 𝔖), UniformSpace.comap (restrict i ∘ fun x => f ∘ x) (UniformFun.uniformSpace (↑i) β)
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Type ?u.75481
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : γ → β
⊢ uniformSpace α γ 𝔖 = UniformSpace.comap ((fun x x_1 => x ∘ x_1) f) (uniformSpace α β 𝔖)
simp_rw [UniformOnFun.uniformSpace, UniformSpace.comap_iInf, UniformFun.comap_eq, ←
  UniformSpace.comap_comap]
no goals
α : Type u_1
β : Type u_3
γ : Type u_2
ι : Type ?u.75481
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
f : γ → β
⊢ (⨅ (s : Set α) (_ : s ∈ 𝔖), UniformSpace.comap ((fun x => f ∘ x) ∘ restrict s) (UniformFun.uniformSpace (↑s) β)) =
    ⨅ (i : Set α) (_ : i ∈ 𝔖), UniformSpace.comap (restrict i ∘ fun x => f ∘ x) (UniformFun.uniformSpace (↑i) β)
rfl