-- Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
simp_rw :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (⨅ i ∈ 𝔖, 𝓤 (α →ᵤ[𝔖] β))
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)))
simp_rw₁ :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
    (⨅ i ∈ 𝔖,
      comap (β := UniformFun.{u_1, u_2} (↑i : Type u_1) β × UniformFun.{u_1, u_2} (↑i : Type u_1) β)
        (Prod.map
          (Function.comp (β := (↑i : Type u_1) → β)
            ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
              (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
            (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
              (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β))
          (Function.comp (β := (↑i : Type u_1) → β)
            ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
              (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
            (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
              (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β)))
        (𝓤 (UniformFun.{u_1, u_2} (↑i : Type u_1) β)))
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)))
simp_rw₂ :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
    (⨅ i ∈ 𝔖,
      comap (β := UniformFun.{u_1, u_2} (↑i : Type u_1) β × UniformFun.{u_1, u_2} (↑i : Type u_1) β)
        (Prod.map
          (Function.comp (β := (↑i : Type u_1) → β)
            ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
              (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
            (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
              (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β))
          (Function.comp (β := (↑i : Type u_1) → β)
            ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
              (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
            (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
              (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β)))
        (⨅ (i_1 : ι), ⨅ (_ : p i_1), 𝓟 ((UniformFun.gen (↑i : Type u_1) β ∘ V) i_1)))
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)))
simp_rw₃ :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
    (⨅ i ∈ 𝔖,
      ⨅ (i_1 : ι),
        ⨅ (_ : p i_1),
          comap (β := UniformFun.{u_1, u_2} (↑i : Type u_1) β × UniformFun.{u_1, u_2} (↑i : Type u_1) β)
            (Prod.map
              (Function.comp (β := (↑i : Type u_1) → β)
                ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                  (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                  (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β))
              (Function.comp (β := (↑i : Type u_1) → β)
                ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                  (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                  (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β)))
            (𝓟 ((UniformFun.gen (↑i : Type u_1) β ∘ V) i_1)))
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)))
simp_rw₄ :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
    (⨅ i ∈ 𝔖,
      ⨅ (i_1 : ι),
        ⨅ (_ : p i_1),
          𝓟
            (preimage (β := UniformFun.{u_1, u_2} (↑i : Type u_1) β × UniformFun.{u_1, u_2} (↑i : Type u_1) β)
              (Prod.map
                (Function.comp (β := (↑i : Type u_1) → β)
                  ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                    (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                  (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β))
                      (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                    (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β))
                (Function.comp (β := (↑i : Type u_1) → β)
                  ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                    (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                  (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β))
                      (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                    (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β)))
              ((UniformFun.gen (↑i : Type u_1) β ∘ V) i_1)))
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)))
simp_rw₅ :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
    (⨅ i ∈ 𝔖,
      ⨅ (i_1 : ι),
        ⨅ (_ : p i_1),
          𝓟
            (preimage (β := UniformFun.{u_1, u_2} (↑i : Type u_1) β × UniformFun.{u_1, u_2} (↑i : Type u_1) β)
              (Prod.map
                (Function.comp (β := (↑i : Type u_1) → β)
                  ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                    (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                  (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β))
                      (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                    (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β))
                (Function.comp (β := (↑i : Type u_1) → β)
                  ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                    (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                  (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β))
                      (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                    (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β)))
              (UniformFun.gen (↑i : Type u_1) β (V i_1))))
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)))
simp_rw₆ :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
    (⨅ i ∈ 𝔖,
      ⨅ (i_1 : ι),
        ⨅ (_ : p i_1),
          𝓟
            (preimage (β := UniformFun.{u_1, u_2} (↑i : Type u_1) β × UniformFun.{u_1, u_2} (↑i : Type u_1) β)
              (Prod.map
                (Function.comp (β := (↑i : Type u_1) → β)
                  ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                    (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                  (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β))
                      (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                    (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β))
                (Function.comp (β := (↑i : Type u_1) → β)
                  ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                    (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                  (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β))
                      (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                    (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β)))
              {uv : UniformFun.{u_1, u_2} (↑i : Type u_1) β × UniformFun.{u_1, u_2} (↑i : Type u_1) β |
                ∀ (x : (↑i : Type u_1)),
                  Membership.mem (α := β × β) (V i_1)
                    (((UniformFun.toFun : (a : (↑i : Type u_1) →ᵤ β) → (↑i : Type u_1) → β) uv.1 x,
                        (UniformFun.toFun : (a : (↑i : Type u_1) →ᵤ β) → (↑i : Type u_1) → β) uv.2 x) :
                      β × β)}))
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)))
simp_rw₇ :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
    (⨅ i ∈ 𝔖,
      ⨅ (i_1 : ι),
        ⨅ (_ : p i_1),
          𝓟
            (preimage (β := UniformFun.{u_1, u_2} (↑i : Type u_1) β × UniformFun.{u_1, u_2} (↑i : Type u_1) β)
              (Prod.map
                (Function.comp (β := (↑i : Type u_1) → β)
                  ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                    (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                  (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β))
                      (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                    (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β))
                (Function.comp (β := (↑i : Type u_1) → β)
                  ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                    (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                  (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β))
                      (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                    (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β)))
              {uv : UniformFun.{u_1, u_2} (↑i : Type u_1) β × UniformFun.{u_1, u_2} (↑i : Type u_1) β |
                ∀ (a : α) (b : a ∈ i),
                  Membership.mem (α := β × β) (V i_1)
                    (((UniformFun.toFun : (a : (↑i : Type u_1) →ᵤ β) → (↑i : Type u_1) → β) uv.1
                          (Subtype.mk (p := fun (a : α) ↦ a ∈ i) a b),
                        (UniformFun.toFun : (a : (↑i : Type u_1) →ᵤ β) → (↑i : Type u_1) → β) uv.2
                          (Subtype.mk (p := fun (a : α) ↦ a ∈ i) a b)) :
                      β × β)}))
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)))
simp_rw₈ :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
    (⨅ i ∈ 𝔖,
      ⨅ (i_1 : ι),
        ⨅ (_ : p i_1),
          𝓟
            (preimage (β := UniformFun.{u_1, u_2} (↑i : Type u_1) β × UniformFun.{u_1, u_2} (↑i : Type u_1) β)
              (Prod.map
                (Function.comp (β := (↑i : Type u_1) → β)
                  ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                    (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                  (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β))
                      (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                    (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β))
                (Function.comp (β := (↑i : Type u_1) → β)
                  ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                    (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                  (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β))
                      (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                    (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β)))
              {uv : UniformFun.{u_1, u_2} (↑i : Type u_1) β × UniformFun.{u_1, u_2} (↑i : Type u_1) β |
                ∀ (a : α) (b : a ∈ i),
                  Membership.mem (α := β × β) (V i_1)
                    (((UniformFun.toFun : (a : (↑i : Type u_1) →ᵤ β) → (↑i : Type u_1) → β) uv.1
                          (Subtype.mk (p := fun (a : α) ↦ a ∈ i) a b),
                        (UniformFun.toFun : (a : (↑i : Type u_1) →ᵤ β) → (↑i : Type u_1) → β) uv.2
                          (Subtype.mk (p := fun (a : α) ↦ a ∈ i) a b)) :
                      β × β)}))
    (⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {uv : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) uv.1 x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) uv.2 x) : β × β)})
simp_rw₉ :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
    (⨅ i ∈ 𝔖,
      ⨅ (i_1 : ι),
        ⨅ (_ : p i_1),
          𝓟
            {a : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) |
              ∀ (a_1 : α) (b : a_1 ∈ i),
                Membership.mem (α := β × β) (V i_1)
                  (((UniformFun.toFun : (a : (↑i : Type u_1) →ᵤ β) → (↑i : Type u_1) → β)
                        (Prod.map
                            (Function.comp (β := (↑i : Type u_1) → β)
                              ((⇑UniformFun.ofFun :
                                  (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                                (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                              (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β))
                                  (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                                (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β))
                            (Function.comp (β := (↑i : Type u_1) → β)
                              ((⇑UniformFun.ofFun :
                                  (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                                (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                              (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β))
                                  (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                                (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β))
                            a).1
                        (Subtype.mk (p := fun (a : α) ↦ a ∈ i) a_1 b),
                      (UniformFun.toFun : (a : (↑i : Type u_1) →ᵤ β) → (↑i : Type u_1) → β)
                        (Prod.map
                            (Function.comp (β := (↑i : Type u_1) → β)
                              ((⇑UniformFun.ofFun :
                                  (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                                (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                              (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β))
                                  (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                                (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β))
                            (Function.comp (β := (↑i : Type u_1) → β)
                              ((⇑UniformFun.ofFun :
                                  (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                                (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                              (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β))
                                  (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                                (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β))
                            a).2
                        (Subtype.mk (p := fun (a : α) ↦ a ∈ i) a_1 b)) :
                    β × β)})
    (⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {uv : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) uv.1 x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) uv.2 x) : β × β)})
simp_rw₁₀ :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
    (⨅ i ∈ 𝔖,
      ⨅ (i_1 : ι),
        ⨅ (_ : p i_1),
          𝓟
            {a : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) |
              ∀ (a_1 : α) (b : a_1 ∈ i),
                Membership.mem (α := β × β) (V i_1)
                  (((UniformFun.toFun : (a : (↑i : Type u_1) →ᵤ β) → (↑i : Type u_1) → β)
                        (Function.comp (β := (↑i : Type u_1) → β)
                          ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                            (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                          (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β))
                              (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                            (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β)
                          a.1)
                        (Subtype.mk (p := fun (a : α) ↦ a ∈ i) a_1 b),
                      (UniformFun.toFun : (a : (↑i : Type u_1) →ᵤ β) → (↑i : Type u_1) → β)
                        (Prod.map
                            (Function.comp (β := (↑i : Type u_1) → β)
                              ((⇑UniformFun.ofFun :
                                  (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                                (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                              (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β))
                                  (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                                (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β))
                            (Function.comp (β := (↑i : Type u_1) → β)
                              ((⇑UniformFun.ofFun :
                                  (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                                (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                              (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β))
                                  (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                                (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β))
                            a).2
                        (Subtype.mk (p := fun (a : α) ↦ a ∈ i) a_1 b)) :
                    β × β)})
    (⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {uv : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) uv.1 x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) uv.2 x) : β × β)})
simp_rw₁₁ :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
    (⨅ i ∈ 𝔖,
      ⨅ (i_1 : ι),
        ⨅ (_ : p i_1),
          𝓟
            {a : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) |
              ∀ (a_1 : α) (b : a_1 ∈ i),
                Membership.mem (α := β × β) (V i_1)
                  (((UniformFun.toFun : (a : (↑i : Type u_1) →ᵤ β) → (↑i : Type u_1) → β)
                        (Function.comp (β := (↑i : Type u_1) → β)
                          ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                            (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                          (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β))
                              (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                            (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β)
                          a.1)
                        (Subtype.mk (p := fun (a : α) ↦ a ∈ i) a_1 b),
                      (UniformFun.toFun : (a : (↑i : Type u_1) →ᵤ β) → (↑i : Type u_1) → β)
                        (Function.comp (β := (↑i : Type u_1) → β)
                          ((⇑UniformFun.ofFun : (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β) :
                            (a : (↑i : Type u_1) → β) → UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                          (Function.comp (β := α → β) (i.restrict (π := fun (a : α) ↦ β))
                              (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
                            (α →ᵤ[𝔖] β) → (↑i : Type u_1) → β)
                          a.2)
                        (Subtype.mk (p := fun (a : α) ↦ a ∈ i) a_1 b)) :
                    β × β)})
    (⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {uv : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) uv.1 x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) uv.2 x) : β × β)})
simp_rw₁₂ :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
    (⨅ i ∈ 𝔖,
      ⨅ (i_1 : ι),
        ⨅ (_ : p i_1),
          𝓟
            {a : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) |
              ∀ (a_1 : α) (b : a_1 ∈ i),
                Membership.mem (α := β × β) (V i_1)
                  (((UniformFun.toFun : (a : (↑i : Type u_1) →ᵤ β) → (↑i : Type u_1) → β)
                        ((UniformFun.ofFun : (a : (↑i : Type u_1) → β) → (↑i : Type u_1) →ᵤ β)
                            (i.restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) a.1)) :
                          UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                        (Subtype.mk (p := fun (a : α) ↦ a ∈ i) a_1 b),
                      (UniformFun.toFun : (a : (↑i : Type u_1) →ᵤ β) → (↑i : Type u_1) → β)
                        ((UniformFun.ofFun : (a : (↑i : Type u_1) → β) → (↑i : Type u_1) →ᵤ β)
                            (i.restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) a.2)) :
                          UniformFun.{u_1, u_2} (↑i : Type u_1) β)
                        (Subtype.mk (p := fun (a : α) ↦ a ∈ i) a_1 b)) :
                    β × β)})
    (⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {uv : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) uv.1 x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) uv.2 x) : β × β)})
simp_rw₁₃ :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
    (⨅ i ∈ 𝔖,
      ⨅ (i_1 : ι),
        ⨅ (_ : p i_1),
          𝓟
            {a : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) |
              ∀ (a_1 : α) (b : a_1 ∈ i),
                Membership.mem (α := β × β) (V i_1)
                  ((i.restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) a.1)
                        (Subtype.mk (p := fun (a : α) ↦ a ∈ i) a_1 b),
                      i.restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) a.2)
                        (Subtype.mk (p := fun (a : α) ↦ a ∈ i) a_1 b)) :
                    β × β)})
    (⨅ s ∈ 𝔖,
      ⨅ (i : ι),
        ⨅ (_ : p i),
          𝓟
            {uv : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) |
              ∀ x ∈ s,
                Membership.mem (α := β × β) (V i)
                  (((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) uv.1 x, (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) uv.2 x) : β × β)})
⊢ Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (𝓤 (α →ᵤ[𝔖] β))
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)))

Tactic:
simp_rw [iInf_uniformity, uniformity_comap,
    (UniformFun.hasBasis_uniformity_of_basis _ _ h).eq_biInf, comap_iInf, comap_principal,
    Function.comp_apply, UniformFun.gen, Subtype.forall, UniformOnFun.gen, preimage_setOf_eq,
    Prod.map_fst, Prod.map_snd, Function.comp_apply, UniformFun.toFun_ofFun, restrict_apply]

Premises used: Prod.map_snd, Set.restrict_apply, UniformOnFun.gen, UniformFun.toFun_ofFun, Subtype.forall, UniformFun.gen, Filter.HasBasis.eq_biInf, UniformFun.hasBasis_uniformity_of_basis, iInf_uniformity, Filter.comap_iInf, Set.preimage_setOf_eq, Prod.map_fst, Filter.comap_principal, Function.comp_apply, uniformity_comap