-- 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)
f : γ → α →ᵤ[𝔖] β
K : ℝ≥0
mp :
  (∀ (x y : γ) (x_1 : α),
      ∀ x_2 ∈ 𝔖,
        x_1 ∈ x_2 →
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
            (↑K : ℝ≥0∞) * edist x y) →
    ∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          ∀ (x y : γ),
            edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
              (↑K : ℝ≥0∞) * edist x y
mpr :
  (∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          ∀ (x y : γ),
            edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
              (↑K : ℝ≥0∞) * edist x y) →
    ∀ (x y : γ) (x_1 : α),
      ∀ x_2 ∈ 𝔖,
        x_1 ∈ x_2 →
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
            (↑K : ℝ≥0∞) * edist x y
mp₁ mp₂ mp₃ :
  (∀ (x y : γ) (x_1 : α),
      ∀ x_2 ∈ 𝔖,
        x_1 ∈ x_2 →
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
            (↑K : ℝ≥0∞) * edist x y) →
    ∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          ∀ (x y : γ),
            edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
              (↑K : ℝ≥0∞) * edist x y
mpr₁ mpr₂ mpr₃ :
  (∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          ∀ (x y : γ),
            edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
              (↑K : ℝ≥0∞) * edist x y) →
    ∀ (x y : γ) (x_1 : α),
      ∀ x_2 ∈ 𝔖,
        x_1 ∈ x_2 →
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
            (↑K : ℝ≥0∞) * edist x y
mp₄ mp₅ mp₆ :
  (∀ (x y : γ) (x_1 : α),
      ∀ x_2 ∈ 𝔖,
        x_1 ∈ x_2 →
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
            (↑K : ℝ≥0∞) * edist x y) →
    ∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          ∀ (x y : γ),
            edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
              (↑K : ℝ≥0∞) * edist x y
mpr₄ mpr₅ mpr₆ :
  (∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          ∀ (x y : γ),
            edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
              (↑K : ℝ≥0∞) * edist x y) →
    ∀ (x y : γ) (x_1 : α),
      ∀ x_2 ∈ 𝔖,
        x_1 ∈ x_2 →
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
            (↑K : ℝ≥0∞) * edist x y
mp₇ mp₈ mp₉ :
  (∀ (x y : γ) (x_1 : α),
      ∀ x_2 ∈ 𝔖,
        x_1 ∈ x_2 →
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
            (↑K : ℝ≥0∞) * edist x y) →
    ∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          ∀ (x y : γ),
            edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
              (↑K : ℝ≥0∞) * edist x y
mpr₇ mpr₈ mpr₉ :
  (∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          ∀ (x y : γ),
            edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
              (↑K : ℝ≥0∞) * edist x y) →
    ∀ (x y : γ) (x_1 : α),
      ∀ x_2 ∈ 𝔖,
        x_1 ∈ x_2 →
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
            (↑K : ℝ≥0∞) * edist x y
mp₁₀ mp₁₁ mp₁₂ :
  (∀ (x y : γ) (x_1 : α),
      ∀ x_2 ∈ 𝔖,
        x_1 ∈ x_2 →
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
            (↑K : ℝ≥0∞) * edist x y) →
    ∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          ∀ (x y : γ),
            edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
              (↑K : ℝ≥0∞) * edist x y
mpr₁₀ mpr₁₁ mpr₁₂ :
  (∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          ∀ (x y : γ),
            edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
              (↑K : ℝ≥0∞) * edist x y) →
    ∀ (x y : γ) (x_1 : α),
      ∀ x_2 ∈ 𝔖,
        x_1 ∈ x_2 →
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
            (↑K : ℝ≥0∞) * edist x y
mp₁₃ mp₁₄ mp₁₅ :
  (∀ (x y : γ) (x_1 : α),
      ∀ x_2 ∈ 𝔖,
        x_1 ∈ x_2 →
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
            (↑K : ℝ≥0∞) * edist x y) →
    ∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          ∀ (x y : γ),
            edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
              (↑K : ℝ≥0∞) * edist x y
mpr₁₃ mpr₁₄ mpr₁₅ :
  (∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          ∀ (x y : γ),
            edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
              (↑K : ℝ≥0∞) * edist x y) →
    ∀ (x y : γ) (x_1 : α),
      ∀ x_2 ∈ 𝔖,
        x_1 ∈ x_2 →
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
            (↑K : ℝ≥0∞) * edist x y
mp₁₆ mp₁₇ :
  (∀ (x y : γ) (x_1 : α),
      ∀ x_2 ∈ 𝔖,
        x_1 ∈ x_2 →
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
            (↑K : ℝ≥0∞) * edist x y) →
    ∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          ∀ (x y : γ),
            edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
              (↑K : ℝ≥0∞) * edist x y
mpr₁₆ mpr₁₇ :
  (∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          ∀ (x y : γ),
            edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
              (↑K : ℝ≥0∞) * edist x y) →
    ∀ (x y : γ) (x_1 : α),
      ∀ x_2 ∈ 𝔖,
        x_1 ∈ x_2 →
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
            (↑K : ℝ≥0∞) * edist x y
⊢ (∀ (x y : γ) (x_1 : α),
      ∀ x_2 ∈ 𝔖,
        x_1 ∈ x_2 →
          edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) x_1 : β)
              ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) x_1 : β) ≤
            (↑K : ℝ≥0∞) * edist x y) ↔
    ∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          ∀ (x y : γ),
            edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c : β)
                ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f y) c : β) ≤
              (↑K : ℝ≥0∞) * edist x y

Tactic:
tauto