-- Lean 4 proof step from Mathlib.Topology.MetricSpace.UniformConvergence (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst_1 : PseudoEMetricSpace β
inst_2 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
x : Fintype (↑𝔖 : Type u_1) := Fintype.ofFinite (↑𝔖 : Type u_1)
simp_rw :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
    (comap (β :=
      ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β) ×
        ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β))
      (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
        (fun (s : (↑𝔖 : Type u_1)) ↦
          (UniformFun.ofFun : (a : (↑(↑s : Set α) : Type u_1) → β) → (↑(↑s : Set α) : Type u_1) →ᵤ β)
            ((↑s : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1)),
          fun (s : (↑𝔖 : Type u_1)) ↦
          (UniformFun.ofFun : (a : (↑(↑s : Set α) : Type u_1) → β) → (↑(↑s : Set α) : Type u_1) →ᵤ β)
            ((↑s : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2))))
      (𝓤 ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β)))
    (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) | edist p.1 p.2 < ε})
simp_rw₁ :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
    (comap (β :=
      ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β) ×
        ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β))
      (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
        (fun (s : (↑𝔖 : Type u_1)) ↦
          (UniformFun.ofFun : (a : (↑(↑s : Set α) : Type u_1) → β) → (↑(↑s : Set α) : Type u_1) →ᵤ β)
            ((↑s : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1)),
          fun (s : (↑𝔖 : Type u_1)) ↦
          (UniformFun.ofFun : (a : (↑(↑s : Set α) : Type u_1) → β) → (↑(↑s : Set α) : Type u_1) →ᵤ β)
            ((↑s : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2))))
      (⨅ (ε : ℝ≥0∞),
        ⨅ (_ : ε > 0),
          𝓟
            {p :
              ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β) ×
                ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β) |
              edist p.1 p.2 < ε}))
    (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) | edist p.1 p.2 < ε})
⊢ Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (𝓤 (α →ᵤ[𝔖] β))
    (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) | edist p.1 p.2 < ε})
have simp_rw₂ : Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
  (⨅ (i : ℝ≥0∞),
    ⨅ (_ : i > 0),
      comap (β :=
        ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β) ×
          ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β))
        (fun (x : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)) ↦
          (fun (s : (↑𝔖 : Type u_1)) ↦
            (UniformFun.ofFun : (a : (↑(↑s : Set α) : Type u_1) → β) → (↑(↑s : Set α) : Type u_1) →ᵤ β)
              ((↑s : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.1)),
            fun (s : (↑𝔖 : Type u_1)) ↦
            (UniformFun.ofFun : (a : (↑(↑s : Set α) : Type u_1) → β) → (↑(↑s : Set α) : Type u_1) →ᵤ β)
              ((↑s : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) x.2))))
        (𝓟
          {p :
            ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β) ×
              ((s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_1) β) |
            edist p.1 p.2 < i}))
  (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : (α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β) | edist p.1 p.2 < ε})
Tactic: simp_rw [← isUniformInducing_pi_restrict.comap_uniformity,
      PseudoEMetricSpace.uniformity_edist, comap_iInf, comap_principal, edist_eq_pi_restrict,
      Set.preimage_setOf_eq]