-- 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)))
⊢ 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) → β)))
            (UniformFun.gen (↑i : Type u_1) β (V i_1))))
  (⨅ 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]