α : Type u_2
β : Type ?u.72956
γ : Type u_1
ι : Type u_3
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ (⨅ (s : Set α) (_ : s ∈ 𝔖) (i : ι), UniformSpace.comap (restrict s) (UniformFun.uniformSpace (↑s) γ)) =
    ⨅ (i : ι) (s : Set α) (_ : s ∈ 𝔖), UniformSpace.comap (restrict s) (UniformFun.uniformSpace (↑s) γ)
α : Type u_2
β : Type ?u.72956
γ : Type u_1
ι : Type u_3
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ uniformSpace α γ 𝔖 = ⨅ (i : ι), uniformSpace α γ 𝔖
simp_rw [UniformOnFun.uniformSpace, UniformFun.iInf_eq, UniformSpace.comap_iInf]
α : Type u_2
β : Type ?u.72956
γ : Type u_1
ι : Type u_3
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ (⨅ (s : Set α) (_ : s ∈ 𝔖) (i : ι), UniformSpace.comap (restrict s) (UniformFun.uniformSpace (↑s) γ)) =
    ⨅ (j : Set α) (i : ι) (_ : j ∈ 𝔖), UniformSpace.comap (restrict j) (UniformFun.uniformSpace (↑j) γ)
α : Type u_2
β : Type ?u.72956
γ : Type u_1
ι : Type u_3
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ (⨅ (s : Set α) (_ : s ∈ 𝔖) (i : ι), UniformSpace.comap (restrict s) (UniformFun.uniformSpace (↑s) γ)) =
    ⨅ (i : ι) (s : Set α) (_ : s ∈ 𝔖), UniformSpace.comap (restrict s) (UniformFun.uniformSpace (↑s) γ)
rw [iInf_comm]
no goals
α : Type u_2
β : Type ?u.72956
γ : Type u_1
ι : Type u_3
s s' : Set α
x : α
p : Filter ι
g : ι → α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ (⨅ (s : Set α) (_ : s ∈ 𝔖) (i : ι), UniformSpace.comap (restrict s) (UniformFun.uniformSpace (↑s) γ)) =
    ⨅ (j : Set α) (i : ι) (_ : j ∈ 𝔖), UniformSpace.comap (restrict j) (UniformFun.uniformSpace (↑j) γ)
exact iInf_congr fun s => iInf_comm