-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
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 < ε})
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 < ε})
simp_rw₃ :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
    (⨅ (i : ℝ≥0∞),
      ⨅ (_ : i > 0),
        𝓟
          (Set.preimage (β :=
            ((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 < ε})
simp_rw₄ :
  Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β)))
    (⨅ (i : ℝ≥0∞),
      ⨅ (_ : i > 0),
        𝓟
          (Set.preimage (β :=
            ((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 (α := (s : (↑𝔖 : Type u_1)) → UniformFun.{u_1, u_2} (↑(↑s : Set α) : Type u_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 : α →ᵤ[𝔖] β) → α → β) p.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 : α →ᵤ[𝔖] β) → α → β) p.2))) <
              ε})
⊢ Eq (α := Filter ((α →ᵤ[𝔖] β) × (α →ᵤ[𝔖] β))) (𝓤 (α →ᵤ[𝔖] β))
    (⨅ (ε : ℝ≥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]

Premises used: IsUniformInducing.comap_uniformity, Filter.comap_iInf, Set.preimage_setOf_eq, UniformOnFun.edist_eq_pi_restrict, Filter.comap_principal, UniformOnFun.isUniformInducing_pi_restrict, PseudoEMetricSpace.uniformity_edist