awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace β
inst_1 : BoundedSpace β
f g : α →ᵤ β
C : ℝ
hC : 0 ≤ C
simp_rw :
  (edist f g).toReal ≤ C ↔
    ∀ (x : α),
      (edist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β)).toReal ≤
        C
simp_rw₁ :
  edist f g ≤ ENNReal.ofReal C ↔
    ∀ (x : α),
      edist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β) ≤
        ENNReal.ofReal C
⊢ dist f g ≤ C ↔
    ∀ (x : α), dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β) ≤ C

Tactic:
simp_rw [dist_edist, ← ENNReal.le_ofReal_iff_toReal_le (edist_ne_top _ _) hC, edist_le]

Premises used: UniformFun.edist_le, ENNReal.le_ofReal_iff_toReal_le, edist_ne_top, dist_edist
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoMetricSpace β
inst_2 : BoundedSpace β
rw : Metric.ediam (X := α →ᵤ β) Set.univ < ∞
⊢ Bornology.IsBounded (α := α →ᵤ β) Set.univ

Tactic:
rw [Metric.isBounded_iff_ediam_ne_top, ← lt_top_iff_ne_top]

Premises used: Metric.isBounded_iff_ediam_ne_top, lt_top_iff_ne_top
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoMetricSpace β
inst_2 : BoundedSpace β
⊢ Metric.ediam (X := α →ᵤ β) Set.univ < ∞

Tactic:
lt_of_le_of_lt ?_ <| BoundedSpace.bounded_univ (α := β) |>.ediam_ne_top.lt_top

Premises used: lt_of_le_of_lt, BoundedSpace.bounded_univ, Bornology.IsBounded.ediam_ne_top, Ne.lt_top
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoMetricSpace β
inst_2 : BoundedSpace β
refine : Metric.ediam (X := α →ᵤ β) Set.univ ≤ Metric.ediam.{u_2} (X := β) Set.univ
⊢ Metric.ediam (X := α →ᵤ β) Set.univ < ∞

Tactic:
refine lt_of_le_of_lt ?_ <| BoundedSpace.bounded_univ (α := β) |>.ediam_ne_top.lt_top

Premises used: lt_of_le_of_lt, BoundedSpace.bounded_univ, Bornology.IsBounded.ediam_ne_top, Ne.lt_top
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoMetricSpace β
inst_2 : BoundedSpace β
simp :
  ∀ (x y : α →ᵤ β) (x_1 : α),
    edist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) x x_1 : β) ((toFun : (a : α →ᵤ β) → α → β) y x_1 : β) ≤
      Metric.ediam.{u_2} (X := β) Set.univ
⊢ Metric.ediam (X := α →ᵤ β) Set.univ ≤ Metric.ediam.{u_2} (X := β) Set.univ

Tactic:
simp only [Metric.ediam_le_iff, Set.mem_univ, edist_le, forall_const]

Premises used: UniformFun.edist_le, Set.mem_univ, forall_const, Metric.ediam_le_iff
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoMetricSpace β
inst_2 : BoundedSpace β
⊢ ∀ (x y : α →ᵤ β) (x_1 : α),
    edist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) x x_1 : β) ((toFun : (a : α →ᵤ β) → α → β) y x_1 : β) ≤
      Metric.ediam.{u_2} (X := β) Set.univ

Tactic:
fun f g x ↦ Metric.edist_le_ediam_of_mem (Set.mem_univ _) (Set.mem_univ _)

Premises used: Metric.edist_le_ediam_of_mem, UniformFun.toFun, Set.mem_univ, DFunLike.coe
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoMetricSpace β
inst_2 : BoundedSpace β
⊢ ∀ (x y : α →ᵤ β) (x_1 : α),
    edist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) x x_1 : β) ((toFun : (a : α →ᵤ β) → α → β) y x_1 : β) ≤
      Metric.ediam.{u_2} (X := β) Set.univ

Tactic:
exact fun f g x ↦ Metric.edist_le_ediam_of_mem (Set.mem_univ _) (Set.mem_univ _)

Premises used: Metric.edist_le_ediam_of_mem, Set.mem_univ
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace β
inst_1 : TopologicalSpace α
⊢ Isometry (α := α →ᵇ β) (β := α →ᵤ β)
    (Function.comp (β := α → β) (⇑ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (a : α) ↦ β)))

Tactic:
simp [Isometry, edist_def, edist_eq_iSup]

Premises used: UniformFun.edist_def, BoundedContinuousFunction.edist_eq_iSup, Isometry
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace β
inst_1 : TopologicalSpace α
inst_2 : CompactSpace α
⊢ Isometry (α := C(α, β)) (β := α →ᵤ β)
    (Function.comp (β := α → β) (⇑ofFun : (a : α → β) → α →ᵤ β) (DFunLike.coe (β := fun (a : α) ↦ β)))

Tactic:
isometry_ofFun_boundedContinuousFunction.comp <|
    ContinuousMap.isometryEquivBoundedOfCompact α β |>.isometry

Premises used: Isometry.comp, UniformFun.isometry_ofFun_boundedContinuousFunction, ContinuousMap.isometryEquivBoundedOfCompact, IsometryEquiv.isometry
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace β
inst_1 : TopologicalSpace α
inst_2 : CompactSpace α
f g : α →ᵤ β
hf : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((toFun : (a : α →ᵤ β) → α → β) f)
hg : Continuous[inst_1, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ((toFun : (a : α →ᵤ β) → α → β) g)
⊢ edist { toFun := (toFun : (a : α →ᵤ β) → α → β) f, continuous_toFun := hf : C(α, β) }
      { toFun := (toFun : (a : α →ᵤ β) → α → β) g, continuous_toFun := hg : C(α, β) } =
    edist f g

Tactic:
simp [← isometry_ofFun_continuousMap.edist_eq]

Premises used: Isometry.edist_eq, UniformFun.isometry_ofFun_continuousMap
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 : Set (Set α)
inst_1 : PseudoEMetricSpace β
f : γ → α →ᵤ[𝔖] β
K : Set α → ℝ≥0
h : ∀ s ∈ 𝔖, ∀ c ∈ s, LipschitzWith.{u_3, u_2} (β := β) (K s) fun (x : γ) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c
rw :
  ∀ s ∈ 𝔖,
    Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, UniformFun.topologicalSpace (↑s : Type u_1) β]
      (Function.comp (β := (↑s : Type u_1) → β)
        ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
          (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
        (Function.comp (β := α → β) (s.restrict (π := fun (a : α) ↦ β)) ((⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) ∘ f) :
          γ → (↑s : Type u_1) → β))
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, topologicalSpace α β 𝔖] f

Tactic:
rw [UniformOnFun.continuous_rng_iff]

Premises used: UniformOnFun.continuous_rng_iff
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 : Set (Set α)
inst_1 : PseudoEMetricSpace β
f : γ → α →ᵤ[𝔖] β
K : Set α → ℝ≥0
h : ∀ s ∈ 𝔖, ∀ c ∈ s, LipschitzWith.{u_3, u_2} (β := β) (K s) fun (x : γ) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c
⊢ ∀ s ∈ 𝔖,
    Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, UniformFun.topologicalSpace (↑s : Type u_1) β]
      (Function.comp (β := (↑s : Type u_1) → β)
        ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
          (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
        (Function.comp (β := α → β) (s.restrict (π := fun (a : α) ↦ β)) ((⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) ∘ f) :
          γ → (↑s : Type u_1) → β))

Tactic:
fun s hs ↦ LipschitzWith.continuous (K := K s) ?_

Premises used: LipschitzWith.continuous
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 : Set (Set α)
inst_1 : PseudoEMetricSpace β
f : γ → α →ᵤ[𝔖] β
K : Set α → ℝ≥0
h : ∀ s ∈ 𝔖, ∀ c ∈ s, LipschitzWith.{u_3, u_2} (β := β) (K s) fun (x : γ) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c
refine :
  ∀ (s : Set α) (hs : s ∈ 𝔖),
    LipschitzWith (β := UniformFun.{u_1, u_2} (↑s : Type u_1) β) (K s)
      (Function.comp (β := (↑s : Type u_1) → β)
        ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
          (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
        (Function.comp (β := α → β) (s.restrict (π := fun (a : α) ↦ β)) ((⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) ∘ f) :
          γ → (↑s : Type u_1) → β))
⊢ ∀ s ∈ 𝔖,
    Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, UniformFun.topologicalSpace (↑s : Type u_1) β]
      (Function.comp (β := (↑s : Type u_1) → β)
        ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
          (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
        (Function.comp (β := α → β) (s.restrict (π := fun (a : α) ↦ β)) ((⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) ∘ f) :
          γ → (↑s : Type u_1) → β))

Tactic:
refine fun s hs ↦ LipschitzWith.continuous (K := K s) ?_

Premises used: LipschitzWith.continuous
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 : Set (Set α)
inst_1 : PseudoEMetricSpace β
f : γ → α →ᵤ[𝔖] β
K : Set α → ℝ≥0
h : ∀ s ∈ 𝔖, ∀ c ∈ s, LipschitzWith.{u_3, u_2} (β := β) (K s) fun (x : γ) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c
s : Set α
hs : s ∈ 𝔖
rw :
  ∀ (c : (↑s : Type u_1)),
    LipschitzWith.{u_3, u_2} (β := β) (K s) fun (x : γ) ↦
      (UniformFun.toFun : (a : (↑s : Type u_1) →ᵤ β) → (↑s : Type u_1) → β)
        (Function.comp (β := (↑s : Type u_1) → β)
          ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
            (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
          (Function.comp (β := α → β) (s.restrict (π := fun (a : α) ↦ β)) ((⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) ∘ f) :
            γ → (↑s : Type u_1) → β)
          x)
        c
⊢ LipschitzWith (β := UniformFun.{u_1, u_2} (↑s : Type u_1) β) (K s)
    (Function.comp (β := (↑s : Type u_1) → β)
      ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
        (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
      (Function.comp (β := α → β) (s.restrict (π := fun (a : α) ↦ β)) ((⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) ∘ f) :
        γ → (↑s : Type u_1) → β))

Tactic:
rw [UniformFun.lipschitzWith_iff]

Premises used: UniformFun.lipschitzWith_iff
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 : Set (Set α)
inst_1 : PseudoEMetricSpace β
f : γ → α →ᵤ[𝔖] β
K : Set α → ℝ≥0
h : ∀ s ∈ 𝔖, ∀ c ∈ s, LipschitzWith.{u_3, u_2} (β := β) (K s) fun (x : γ) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c
s : Set α
hs : s ∈ 𝔖
y : α
hy : y ∈ s
⊢ LipschitzWith.{u_3, u_2} (β := β) (K s) fun (x : γ) ↦
    (UniformFun.toFun : (a : (↑s : Type u_1) →ᵤ β) → (↑s : Type u_1) → β)
      (Function.comp (β := (↑s : Type u_1) → β)
        ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
          (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
        (Function.comp (β := α → β) (s.restrict (π := fun (a : α) ↦ β)) ((⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) ∘ f) :
          γ → (↑s : Type u_1) → β)
        x)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)

Tactic:
h s hs y hy

Premises used: Set.restrict
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
𝔖 : Set (Set α)
inst_1 : PseudoEMetricSpace β
f : γ → α →ᵤ[𝔖] β
K : Set α → ℝ≥0
h : ∀ s ∈ 𝔖, ∀ c ∈ s, LipschitzWith.{u_3, u_2} (β := β) (K s) fun (x : γ) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c
s : Set α
hs : s ∈ 𝔖
y : α
hy : y ∈ s
⊢ LipschitzWith.{u_3, u_2} (β := β) (K s) fun (x : γ) ↦
    (UniformFun.toFun : (a : (↑s : Type u_1) →ᵤ β) → (↑s : Type u_1) → β)
      (Function.comp (β := (↑s : Type u_1) → β)
        ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
          (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
        (Function.comp (β := α → β) (s.restrict (π := fun (a : α) ↦ β)) ((⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) ∘ f) :
          γ → (↑s : Type u_1) → β)
        x)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy)

Tactic:
exact h s hs y hy
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : PseudoEMetricSpace β
inst_1 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
f g : α →ᵤ[𝔖] β
⊢ edist f g =
    ⨆ x ∈ ⋃₀ 𝔖,
      edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x : β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : PseudoEMetricSpace β
inst_1 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
f g : α →ᵤ[𝔖] β
⊢ edist f g =
    ⨆ s ∈ 𝔖,
      ⨆ x ∈ s,
        edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x : β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x : β)

Tactic:
simp [edist_def, iSup_and, iSup_comm (ι := α)]

Premises used: iSup_comm, UniformOnFun.edist_def, iSup_and
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : PseudoEMetricSpace β
inst_1 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
f g : α →ᵤ[𝔖] β
⊢ edist f g =
    edist (α := UniformFun.{u_1, u_2} (↑(⋃₀ 𝔖) : Type u_1) β)
      ((UniformFun.ofFun : (a : (↑(⋃₀ 𝔖) : Type u_1) → β) → (↑(⋃₀ 𝔖) : Type u_1) →ᵤ β)
          ((⋃₀ 𝔖).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)) :
        UniformFun.{u_1, u_2} (↑(⋃₀ 𝔖) : Type u_1) β)
      ((UniformFun.ofFun : (a : (↑(⋃₀ 𝔖) : Type u_1) → β) → (↑(⋃₀ 𝔖) : Type u_1) →ᵤ β)
          ((⋃₀ 𝔖).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g)) :
        UniformFun.{u_1, u_2} (↑(⋃₀ 𝔖) : Type u_1) β)

Tactic:
iSup_subtype'

Premises used: iSup_subtype', Set.restrict
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : PseudoEMetricSpace β
inst_1 : Fintype (↑𝔖 : Type u_1)
f g : α →ᵤ[𝔖] β
simp_rw :
  Eq (α := ℝ≥0∞)
    (⨆ (x : Subtype (Membership.mem 𝔖)),
      ⨆ (x_1 : Subtype (Membership.mem (↑x : Set α))),
        edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f (↑x_1 : α) : β)
          ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g (↑x_1 : α) : β))
    (⨆ (b : (↑𝔖 : Type u_1)),
      edist (α := UniformFun.{u_1, u_2} (↑(↑b : Set α) : Type u_1) β)
        ((UniformFun.ofFun : (a : (↑(↑b : Set α) : Type u_1) → β) → (↑(↑b : Set α) : Type u_1) →ᵤ β)
            ((↑b : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)) :
          UniformFun.{u_1, u_2} (↑(↑b : Set α) : Type u_1) β)
        ((UniformFun.ofFun : (a : (↑(↑b : Set α) : Type u_1) → β) → (↑(↑b : Set α) : Type u_1) →ᵤ β)
            ((↑b : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g)) :
          UniformFun.{u_1, u_2} (↑(↑b : Set α) : Type u_1) β))
⊢ edist f g =
    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 : α →ᵤ[𝔖] β) → α → β) f)))
      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 : α →ᵤ[𝔖] β) → α → β) g))

Tactic:
simp_rw [edist_def', iSup_subtype', edist_pi_def, Finset.sup_univ_eq_iSup]

Premises used: iSup_subtype', UniformOnFun.edist_def', edist_pi_def, Finset.sup_univ_eq_iSup
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : PseudoEMetricSpace β
inst_1 : Fintype (↑𝔖 : Type u_1)
f g : α →ᵤ[𝔖] β
⊢ Eq (α := ℝ≥0∞)
    (⨆ (x : Subtype (Membership.mem 𝔖)),
      ⨆ (x_1 : Subtype (Membership.mem (↑x : Set α))),
        edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f (↑x_1 : α) : β)
          ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g (↑x_1 : α) : β))
    (⨆ (b : (↑𝔖 : Type u_1)),
      edist (α := UniformFun.{u_1, u_2} (↑(↑b : Set α) : Type u_1) β)
        ((UniformFun.ofFun : (a : (↑(↑b : Set α) : Type u_1) → β) → (↑(↑b : Set α) : Type u_1) →ᵤ β)
            ((↑b : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f)) :
          UniformFun.{u_1, u_2} (↑(↑b : Set α) : Type u_1) β)
        ((UniformFun.ofFun : (a : (↑(↑b : Set α) : Type u_1) → β) → (↑(↑b : Set α) : Type u_1) →ᵤ β)
            ((↑b : Set α).restrict (π := fun (a : α) ↦ β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g)) :
          UniformFun.{u_1, u_2} (↑(↑b : Set α) : Type u_1) β))

Tactic:
rfl
-- 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 : α →ᵤ[𝔖] β
⊢ edist f f = 0

Tactic:
simp [edist_eq_restrict_sUnion]

Premises used: UniformOnFun.edist_eq_restrict_sUnion
-- 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 y : α →ᵤ[𝔖] β), edist x y = edist y x

Tactic:
simp [edist_eq_restrict_sUnion, edist_comm]

Premises used: PseudoEMetricSpace.edist_comm, UniformOnFun.edist_eq_restrict_sUnion
-- 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₁ f₂ f₃ : α →ᵤ[𝔖] β
⊢ edist f₁ f₃ ≤ edist f₁ f₂ + edist f₂ f₃

Tactic:
simp [edist_eq_restrict_sUnion, edist_triangle]

Premises used: UniformOnFun.edist_eq_restrict_sUnion, PseudoEMetricSpace.edist_triangle
-- 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
simp :
  (∀ (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
⊢ LipschitzWith K f ↔
    ∀ c ∈ ⋃₀ 𝔖, LipschitzWith.{u_3, u_2} (β := β) K fun (x : γ) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c

Tactic:
simp [LipschitzWith, edist_le]

Premises used: LipschitzWith, UniformOnFun.edist_le
-- 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
s : Set γ
simp :
  (∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          LipschitzWith.{u_3, u_2} (β := β) K fun (x : (↑s : Type u_3)) ↦
            (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f (↑x : γ)) c) ↔
    ∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          LipschitzWith.{u_3, u_2} (α := (↑s : Type u_3)) (β := β) K
            (s.restrict (π := fun (a : γ) ↦ β) fun (x : γ) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c)
⊢ LipschitzOnWith K f s ↔
    ∀ c ∈ ⋃₀ 𝔖, LipschitzOnWith.{u_3, u_2} (β := β) K (fun (x : γ) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c) s

Tactic:
simp [lipschitzOnWith_iff_restrict, lipschitzWith_iff]

Premises used: lipschitzOnWith_iff_restrict, UniformOnFun.lipschitzWith_iff
-- 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
s : Set γ
⊢ (∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          LipschitzWith.{u_3, u_2} (β := β) K fun (x : (↑s : Type u_3)) ↦
            (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f (↑x : γ)) c) ↔
    ∀ (c : α),
      ∀ x ∈ 𝔖,
        c ∈ x →
          LipschitzWith.{u_3, u_2} (α := (↑s : Type u_3)) (β := β) K
            (s.restrict (π := fun (a : γ) ↦ β) fun (x : γ) ↦ (toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) (f x) c)

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : PseudoEMetricSpace β
inst_1 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
f g : α →ᵤ[𝔖] β
x : α
hx : x ∈ ⋃₀ 𝔖
⊢ edist.{u_2} (α := β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x : β) ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) g x : β) ≤
    edist f g

Tactic:
edist_le.mp le_rfl x hx

Premises used: le_rfl, Iff.mp, UniformOnFun.edist_le
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : PseudoEMetricSpace β
inst_1 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
x : α
hx : x ∈ ⋃₀ 𝔖
f g : α →ᵤ[𝔖] β
⊢ edist.{u_2} (α := β) ((fun (f : α →ᵤ[𝔖] β) ↦ ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x : β)) f)
      ((fun (f : α →ᵤ[𝔖] β) ↦ ((toFun 𝔖 : (a : α →ᵤ[𝔖] β) → α → β) f x : β)) g) ≤
    (↑1 : ℝ≥0∞) * edist f g

Tactic:
simpa only [ENNReal.coe_one, one_mul] using edist_eval_le hx

Premises used: UniformOnFun.edist_eval_le, ENNReal.coe_one, one_mul
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : PseudoEMetricSpace β
inst_1 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
⊢ LipschitzWith (α := α →ᵤ β) (β := α →ᵤ[𝔖] β) 1
    (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β) (⇑UniformFun.toFun : (a : α →ᵤ β) → α → β))

Tactic:
lipschitzWith_iff.mpr fun _ _ ↦ UniformFun.lipschitzWith_eval _

Premises used: Iff.mpr, UniformOnFun.lipschitzWith_iff, UniformFun.lipschitzWith_eval
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 𝔗 : Set (Set α)
inst : PseudoEMetricSpace β
inst_1 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
inst_2 : Finite.{u_1 + 1} (↑𝔗 : Type u_1)
h : ⋃₀ 𝔖 ⊆ ⋃₀ 𝔗
⊢ LipschitzWith (α := α →ᵤ[𝔗] β) (β := α →ᵤ[𝔖] β) 1
    (Function.comp (β := α → β) (⇑(ofFun 𝔖) : (a : α → β) → α →ᵤ[𝔖] β) (⇑(toFun 𝔗) : (a : α →ᵤ[𝔗] β) → α → β))

Tactic:
lipschitzWith_iff.mpr fun _x hx ↦ lipschitzWith_eval (h hx)

Premises used: Iff.mpr, UniformOnFun.lipschitzWith_iff, UniformOnFun.lipschitzWith_eval
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
𝔖 : Set (Set α)
inst : PseudoEMetricSpace β
inst_1 : Finite.{u_1 + 1} (↑𝔖 : Type u_1)
s : Set α
hs : s ∈ 𝔖
⊢ LipschitzWith (α := α →ᵤ[𝔖] β) (β := UniformFun.{u_1, u_2} (↑s : Type u_1) β) 1
    (Function.comp (β := (↑s : Type u_1) → β)
      ((⇑UniformFun.ofFun : (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β) :
        (a : (↑s : Type u_1) → β) → UniformFun.{u_1, u_2} (↑s : Type u_1) β)
      (Function.comp (β := α → β) (s.restrict (π := fun (a : α) ↦ β)) (⇑(toFun 𝔖) : (a : α →ᵤ[𝔖] β) → α → β) :
        (α →ᵤ[𝔖] β) → (↑s : Type u_1) → β))

Tactic:
UniformFun.lipschitzWith_iff.mpr fun x ↦ lipschitzWith_eval ⟨s, hs, x.2⟩

Premises used: Iff.mpr, UniformOnFun.lipschitzWith_eval, UniformFun.lipschitzWith_iff, And.intro, Exists.intro, Subtype.property