-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformConvergenceTopology (goal)
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)))
⊢ Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (𝓤 (α →ᵤ[𝔖] β))
    (⨅ s ∈ 𝔖, ⨅ (i : ι), ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i)))
have 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) : β × β)})
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]