∀ {ι : Type u_4} {β₁ : ι → Type u_5} {β₂ : ι → Type u_6} [inst : (i : ι) → UniformSpace (β₁ i)]
  [inst_1 : (i : ι) → UniformSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ᵤ β₂ i),
  (UniformEquiv.piCongrRight F).symm = UniformEquiv.piCongrRight fun i => (F i).symm