awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : MetricSpace Y
inst_3 : IsUltrametricDist Y
f g h : C(X, Y)
dist_triangle_max :
  ∀ (x : X), dist.{u_2} (α := Y) ((f : (a : X) → Y) x : Y) ((h : (a : X) → Y) x : Y) ≤ max (dist f g) (dist g h)
⊢ dist f h ≤ max (dist f g) (dist g h)

Tactic:
rw [ContinuousMap.dist_le (by positivity)]

Premises used: ContinuousMap.dist_le
-- Module: Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : MetricSpace Y
inst_3 : IsUltrametricDist Y
f g h : C(X, Y)
⊢ ∀ (x : X), dist.{u_2} (α := Y) ((f : (a : X) → Y) x : Y) ((h : (a : X) → Y) x : Y) ≤ max (dist f g) (dist g h)

Tactic:
fun x ↦ (dist_triangle_max (f x) (g x) (h x)).trans (max_le_max ?_ ?_)

Premises used: dist_triangle_max, max_le_max, LE.le.trans, DFunLike.coe
-- Module: Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : MetricSpace Y
inst_3 : IsUltrametricDist Y
f g h : C(X, Y)
dist_triangle_max : ∀ (x : X), dist.{u_2} (α := Y) ((f : (a : X) → Y) x : Y) ((g : (a : X) → Y) x : Y) ≤ dist f g
dist_triangle_max₁ : ∀ (x : X), dist.{u_2} (α := Y) ((g : (a : X) → Y) x : Y) ((h : (a : X) → Y) x : Y) ≤ dist g h
⊢ ∀ (x : X), dist.{u_2} (α := Y) ((f : (a : X) → Y) x : Y) ((h : (a : X) → Y) x : Y) ≤ max (dist f g) (dist g h)

Tactic:
refine fun x ↦ (dist_triangle_max (f x) (g x) (h x)).trans (max_le_max ?_ ?_)

Premises used: dist_triangle_max, max_le_max, LE.le.trans, DFunLike.coe
-- Module: Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : MetricSpace Y
inst_3 : IsUltrametricDist Y
f g h : C(X, Y)
x : X
⊢ dist.{u_2} (α := Y) ((f : (a : X) → Y) x : Y) ((g : (a : X) → Y) x : Y) ≤ dist f g

Tactic:
ContinuousMap.dist_apply_le_dist x

Premises used: ContinuousMap.dist_apply_le_dist
-- Module: Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : MetricSpace Y
inst_3 : IsUltrametricDist Y
f g h : C(X, Y)
x : X
⊢ dist.{u_2} (α := Y) ((f : (a : X) → Y) x : Y) ((g : (a : X) → Y) x : Y) ≤ dist f g

Tactic:
exact ContinuousMap.dist_apply_le_dist x

Premises used: ContinuousMap.dist_apply_le_dist
-- Module: Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : MetricSpace Y
inst_3 : IsUltrametricDist Y
f g h : C(X, Y)
x : X
⊢ dist.{u_2} (α := Y) ((g : (a : X) → Y) x : Y) ((h : (a : X) → Y) x : Y) ≤ dist g h

Tactic:
ContinuousMap.dist_apply_le_dist x

Premises used: ContinuousMap.dist_apply_le_dist
-- Module: Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : MetricSpace Y
inst_3 : IsUltrametricDist Y
f g h : C(X, Y)
x : X
⊢ dist.{u_2} (α := Y) ((g : (a : X) → Y) x : Y) ((h : (a : X) → Y) x : Y) ≤ dist g h

Tactic:
exact ContinuousMap.dist_apply_le_dist x

Premises used: ContinuousMap.dist_apply_le_dist
-- Module: Mathlib.Topology.MetricSpace.Ultra.Pi
Goal:
ι : Type u_1
X : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → PseudoMetricSpace (X i)
inst_2 : ∀ (i : ι), IsUltrametricDist.{u_2} (X i)
dist_triangle_max : ∀ (x y z : (i : ι) → X i), dist x z ≤ max (dist x y) (dist y z)
⊢ IsUltrametricDist ((i : ι) → X i)

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.Ultra.Pi
Goal:
ι : Type u_1
X : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → PseudoMetricSpace (X i)
inst_2 : ∀ (i : ι), IsUltrametricDist.{u_2} (X i)
f g h : (i : ι) → X i
dist_triangle_max :
  LE.le (α := NNReal) (Finset.sup Finset.univ fun (b : ι) ↦ nndist (f b) (h b))
    (Finset.sup.{0, u_1} (β := ι) Finset.univ ((fun (b : ι) ↦ nndist (f b) (g b)) ⊔ fun (b : ι) ↦ nndist (g b) (h b)))
⊢ dist f h ≤ max (dist f g) (dist g h)

Tactic:
simp only [dist_pi_def, ← NNReal.coe_max, NNReal.coe_le_coe, ← Finset.sup_sup]

Premises used: Finset.sup_sup, dist_pi_def, NNReal.coe_le_coe, NNReal.coe_max
-- Module: Mathlib.Topology.MetricSpace.Ultra.Pi
Goal:
ι : Type u_1
X : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → PseudoMetricSpace (X i)
inst_2 : ∀ (i : ι), IsUltrametricDist.{u_2} (X i)
f g h : (i : ι) → X i
⊢ LE.le (α := NNReal) (Finset.sup Finset.univ fun (b : ι) ↦ nndist (f b) (h b))
    (Finset.sup.{0, u_1} (β := ι) Finset.univ ((fun (b : ι) ↦ nndist (f b) (g b)) ⊔ fun (b : ι) ↦ nndist (g b) (h b)))

Tactic:
Finset.sup_mono_fun fun i _ ↦ IsUltrametricDist.dist_triangle_max (f i) (g i) (h i)

Premises used: IsUltrametricDist.dist_triangle_max, Finset.sup_mono_fun
-- Module: Mathlib.Topology.MetricSpace.Ultra.Pi
Goal:
ι : Type u_1
X : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → PseudoMetricSpace (X i)
inst_2 : ∀ (i : ι), IsUltrametricDist.{u_2} (X i)
f g h : (i : ι) → X i
⊢ LE.le (α := NNReal) (Finset.sup Finset.univ fun (b : ι) ↦ nndist (f b) (h b))
    (Finset.sup.{0, u_1} (β := ι) Finset.univ ((fun (b : ι) ↦ nndist (f b) (g b)) ⊔ fun (b : ι) ↦ nndist (g b) (h b)))

Tactic:
exact Finset.sup_mono_fun fun i _ ↦ IsUltrametricDist.dist_triangle_max (f i) (g i) (h i)
-- Module: Mathlib.Topology.MetricSpace.Ultra.TotallySeparated
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : IsUltrametricDist X
x y : X
h : x ≠ y
obtain : ∀ (r : ℝ) (hr : 0 < r) (hr' : r < dist x y), ∃ (U : Set X), IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ
⊢ ∃ (U : Set X), IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ

Tactic:
obtain ⟨r, hr, hr'⟩ := exists_between (dist_pos.mpr h)

Premises used: Iff.mpr, exists_between, dist_pos
-- Module: Mathlib.Topology.MetricSpace.Ultra.TotallySeparated
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : IsUltrametricDist X
x y : X
h : x ≠ y
r : ℝ
hr : 0 < r
hr' : r < dist x y
⊢ ∃ (U : Set X), IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ

Tactic:
⟨_, IsUltrametricDist.isClopen_ball x r, ?_, ?_⟩

Premises used: And.intro, Exists.intro, IsUltrametricDist.isClopen_ball
-- Module: Mathlib.Topology.MetricSpace.Ultra.TotallySeparated
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : IsUltrametricDist X
x y : X
h : x ≠ y
r : ℝ
hr : 0 < r
hr' : r < dist x y
refine_1 : x ∈ ball x r
refine_2 : y ∈ (ball x r)ᶜ
⊢ ∃ (U : Set X), IsClopen U ∧ x ∈ U ∧ y ∈ Uᶜ

Tactic:
refine ⟨_, IsUltrametricDist.isClopen_ball x r, ?_, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Ultra.TotallySeparated
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : IsUltrametricDist X
x y : X
h : x ≠ y
r : ℝ
hr : 0 < r
hr' : r < dist x y
⊢ x ∈ ball x r

Tactic:
simp only [mem_ball, dist_self, hr]

Premises used: Metric.mem_ball, dist_self
-- Module: Mathlib.Topology.MetricSpace.Ultra.TotallySeparated
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : IsUltrametricDist X
x y : X
h : x ≠ y
r : ℝ
hr : 0 < r
hr' : r < dist x y
⊢ y ∈ (ball x r)ᶜ

Tactic:
simp only [Set.mem_compl, mem_ball, dist_comm, not_lt, hr'.le]

Premises used: LT.lt.le, dist_comm, Metric.mem_ball, not_lt, Set.mem_compl
-- Module: Mathlib.Topology.MetricSpace.Ultra.TotallySeparated
Goal:
X : Type u_1
inst : MetricSpace X
inst_1 : IsUltrametricDist X
⊢ TotallyDisconnectedSpace X

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace β
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
inst : PseudoEMetricSpace β
f g : α →ᵤ β
C : ℝ≥0∞
⊢ edist f g ≤ C ↔
    ∀ (x : α),
      edist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β) ≤ C

Tactic:
iSup_le_iff

Premises used: iSup_le_iff
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
⊢ ∀ (x : α →ᵤ β), edist x x = 0

Tactic:
simp [edist_def]

Premises used: UniformFun.edist_def
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
⊢ ∀ (x y : α →ᵤ β), edist x y = edist y x

Tactic:
simp [edist_def, edist_comm]

Premises used: PseudoEMetricSpace.edist_comm, UniformFun.edist_def
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
this :
  Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β))
    (comap (β := ℝ≥0∞) (fun (x : (α →ᵤ β) × (α →ᵤ β)) ↦ edist x.1 x.2) (𝓝 0))
⊢ Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β))
    (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : (α →ᵤ β) × (α →ᵤ β) | edist p.1 p.2 < ε})

Tactic:
simp [this, ENNReal.nhds_zero_basis.comap _ |>.eq_biInf, Set.Iio]

Premises used: Filter.HasBasis.eq_biInf, Filter.HasBasis.comap, ENNReal.nhds_zero_basis, Set.Iio
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
suffices :
  Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β))
    (comap (β := ℝ≥0∞) (fun (x : (α →ᵤ β) × (α →ᵤ β)) ↦ edist x.1 x.2) (𝓝 0))
⊢ Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β))
    (⨅ (ε : ℝ≥0∞), ⨅ (_ : ε > 0), 𝓟 {p : (α →ᵤ β) × (α →ᵤ β) | edist p.1 p.2 < ε})

Tactic:
suffices 𝓤 (α →ᵤ β) = comap (fun x ↦ edist x.1 x.2) (𝓝 0) by
      simp [this, ENNReal.nhds_zero_basis.comap _ |>.eq_biInf, Set.Iio]
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
rw :
  Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β))
    (⨅ (i : ℝ≥0∞), ⨅ (_ : 0 < i), 𝓟 ((fun (x : (α →ᵤ β) × (α →ᵤ β)) ↦ edist x.1 x.2) ⁻¹' Set.Iic i))
⊢ Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β))
    (comap (β := ℝ≥0∞) (fun (x : (α →ᵤ β) × (α →ᵤ β)) ↦ edist x.1 x.2) (𝓝 0))

Tactic:
rw [ENNReal.nhds_zero_basis_Iic.comap _ |>.eq_biInf]

Premises used: Filter.HasBasis.eq_biInf, Filter.HasBasis.comap, ENNReal.nhds_zero_basis_Iic
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
rw :
  Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β)))
    (⨅ (i : ℝ≥0∞), ⨅ (_ : 0 < i), 𝓟 ((UniformFun.gen α β ∘ fun (ε : ℝ≥0∞) ↦ {p : β × β | edist p.1 p.2 ≤ ε}) i))
    (⨅ (i : ℝ≥0∞), ⨅ (_ : 0 < i), 𝓟 ((fun (x : (α →ᵤ β) × (α →ᵤ β)) ↦ edist x.1 x.2) ⁻¹' Set.Iic i))
⊢ Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β))) (𝓤 (α →ᵤ β))
    (⨅ (i : ℝ≥0∞), ⨅ (_ : 0 < i), 𝓟 ((fun (x : (α →ᵤ β) × (α →ᵤ β)) ↦ edist x.1 x.2) ⁻¹' Set.Iic i))

Tactic:
rw [UniformFun.hasBasis_uniformity_of_basis α β uniformity_basis_edist_le |>.eq_biInf]

Premises used: uniformity_basis_edist_le, Filter.HasBasis.eq_biInf, UniformFun.hasBasis_uniformity_of_basis
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
⊢ Eq (α := Filter ((α →ᵤ β) × (α →ᵤ β)))
    (⨅ (i : ℝ≥0∞), ⨅ (_ : 0 < i), 𝓟 ((UniformFun.gen α β ∘ fun (ε : ℝ≥0∞) ↦ {p : β × β | edist p.1 p.2 ≤ ε}) i))
    (⨅ (i : ℝ≥0∞), ⨅ (_ : 0 < i), 𝓟 ((fun (x : (α →ᵤ β) × (α →ᵤ β)) ↦ edist x.1 x.2) ⁻¹' Set.Iic i))

Tactic:
simp [UniformFun.gen, edist_le, Set.Iic]

Premises used: UniformFun.gen, UniformFun.edist_le, Set.Iic
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
f : γ → α →ᵤ β
K : ℝ≥0
⊢ LipschitzWith K f ↔
    ∀ (c : α), LipschitzWith.{u_3, u_2} (β := β) K fun (x : γ) ↦ (toFun : (a : α →ᵤ β) → α → β) (f x) c

Tactic:
simp [LipschitzWith, edist_le, forall_comm (α := α)]

Premises used: LipschitzWith, forall_comm, UniformFun.edist_le
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
f : γ → α → β
K : ℝ≥0
⊢ (LipschitzWith (β := α →ᵤ β) K fun (x : γ) ↦ (ofFun : (a : α → β) → α →ᵤ β) (f x)) ↔
    ∀ (c : α), LipschitzWith.{u_3, u_2} (β := β) K fun (x : γ) ↦ f x c

Tactic:
lipschitzWith_iff

Premises used: UniformFun.lipschitzWith_iff
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
h : ∀ (c : α), LipschitzWith K (f c)
rw :
  UniformContinuous (β := α →ᵤ β) ((⇑ofFun : (a : α → β) → α →ᵤ β) ∘ Function.swap (φ := fun (a : α) (a_1 : γ) ↦ β) f)
⊢ UniformEquicontinuous f

Tactic:
rw [uniformEquicontinuous_iff_uniformContinuous]

Premises used: uniformEquicontinuous_iff_uniformContinuous
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
h : ∀ (c : α), LipschitzWith K (f c)
⊢ LipschitzWith (β := α →ᵤ β) K fun (x : γ) ↦ (ofFun : (a : α → β) → α →ᵤ β) fun (c : α) ↦ f c x

Tactic:
rw [← lipschitzWith_ofFun_iff] at h

Premises used: UniformFun.lipschitzWith_ofFun_iff
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
h : LipschitzWith (β := α →ᵤ β) K fun (x : γ) ↦ (ofFun : (a : α → β) → α →ᵤ β) fun (c : α) ↦ f c x
⊢ UniformContinuous (β := α →ᵤ β) ((⇑ofFun : (a : α → β) → α →ᵤ β) ∘ Function.swap (φ := fun (a : α) (a_1 : γ) ↦ β) f)

Tactic:
h.uniformContinuous

Premises used: LipschitzWith.uniformContinuous
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
h : LipschitzWith (β := α →ᵤ β) K fun (x : γ) ↦ (ofFun : (a : α → β) → α →ᵤ β) fun (c : α) ↦ f c x
⊢ UniformContinuous (β := α →ᵤ β) ((⇑ofFun : (a : α → β) → α →ᵤ β) ∘ Function.swap (φ := fun (a : α) (a_1 : γ) ↦ β) f)

Tactic:
exact h.uniformContinuous

Premises used: LipschitzWith.uniformContinuous
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
f : γ → α →ᵤ β
K : ℝ≥0
s : Set γ
simp :
  (∀ (c : α),
      LipschitzWith.{u_3, u_2} (β := β) K fun (x : (↑s : Type u_3)) ↦ (toFun : (a : α →ᵤ β) → α → β) (f (↑x : γ)) c) ↔
    ∀ (c : α),
      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, UniformFun.lipschitzWith_iff
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
f : γ → α →ᵤ β
K : ℝ≥0
s : Set γ
⊢ (∀ (c : α),
      LipschitzWith.{u_3, u_2} (β := β) K fun (x : (↑s : Type u_3)) ↦ (toFun : (a : α →ᵤ β) → α → β) (f (↑x : γ)) c) ↔
    ∀ (c : α),
      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
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
f : γ → α → β
K : ℝ≥0
s : Set γ
⊢ LipschitzOnWith (β := α →ᵤ β) K (fun (x : γ) ↦ (ofFun : (a : α → β) → α →ᵤ β) (f x)) s ↔
    ∀ (c : α), LipschitzOnWith.{u_3, u_2} (β := β) K (fun (x : γ) ↦ f x c) s

Tactic:
lipschitzOnWith_iff

Premises used: UniformFun.lipschitzOnWith_iff
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
s : Set γ
h : ∀ (c : α), LipschitzOnWith K (f c) s
rw :
  UniformContinuousOn (β := α →ᵤ β) ((⇑ofFun : (a : α → β) → α →ᵤ β) ∘ Function.swap (φ := fun (a : α) (a_1 : γ) ↦ β) f)
    s
⊢ UniformEquicontinuousOn f s

Tactic:
rw [uniformEquicontinuousOn_iff_uniformContinuousOn]

Premises used: uniformEquicontinuousOn_iff_uniformContinuousOn
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
s : Set γ
h : ∀ (c : α), LipschitzOnWith K (f c) s
⊢ LipschitzOnWith (β := α →ᵤ β) K (fun (x : γ) ↦ (ofFun : (a : α → β) → α →ᵤ β) fun (c : α) ↦ f c x) s

Tactic:
rw [← lipschitzOnWith_ofFun_iff] at h

Premises used: UniformFun.lipschitzOnWith_ofFun_iff
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
s : Set γ
h : LipschitzOnWith (β := α →ᵤ β) K (fun (x : γ) ↦ (ofFun : (a : α → β) → α →ᵤ β) fun (c : α) ↦ f c x) s
⊢ UniformContinuousOn (β := α →ᵤ β) ((⇑ofFun : (a : α → β) → α →ᵤ β) ∘ Function.swap (φ := fun (a : α) (a_1 : γ) ↦ β) f)
    s

Tactic:
h.uniformContinuousOn

Premises used: LipschitzOnWith.uniformContinuousOn
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoEMetricSpace β
f : α → γ → β
K : ℝ≥0
s : Set γ
h : LipschitzOnWith (β := α →ᵤ β) K (fun (x : γ) ↦ (ofFun : (a : α → β) → α →ᵤ β) fun (c : α) ↦ f c x) s
⊢ UniformContinuousOn (β := α →ᵤ β) ((⇑ofFun : (a : α → β) → α →ᵤ β) ∘ Function.swap (φ := fun (a : α) (a_1 : γ) ↦ β) f)
    s

Tactic:
exact h.uniformContinuousOn

Premises used: LipschitzOnWith.uniformContinuousOn
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace β
f g : α →ᵤ β
x : α
⊢ edist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β) ≤ edist f g

Tactic:
edist_le.mp le_rfl x

Premises used: le_rfl, UniformFun.edist_le, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace β
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 using edist_eval_le

Premises used: UniformFun.edist_eval_le
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoMetricSpace β
inst_2 : BoundedSpace β
f g : α →ᵤ β
inl :
  IsEmpty α →
    edist f g =
      ENNReal.ofReal
        ((fun (f g : α →ᵤ β) ↦
            (⨆ (x : α),
                dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β) :
              ℝ))
          f g)
inr :
  Nonempty α →
    edist f g =
      ENNReal.ofReal
        ((fun (f g : α →ᵤ β) ↦
            (⨆ (x : α),
                dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β) :
              ℝ))
          f g)
⊢ edist f g =
    ENNReal.ofReal
      ((fun (f g : α →ᵤ β) ↦
          (⨆ (x : α),
              dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β) :
            ℝ))
        f g)

Tactic:
cases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoMetricSpace β
inst_2 : BoundedSpace β
f g : α →ᵤ β
h : IsEmpty α
⊢ edist f g =
    ENNReal.ofReal
      ((fun (f g : α →ᵤ β) ↦
          (⨆ (x : α),
              dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β) :
            ℝ))
        f g)

Tactic:
simp [edist_def]

Premises used: UniformFun.edist_def
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoMetricSpace β
inst_2 : BoundedSpace β
f g : α →ᵤ β
h_1 : Nonempty α
h :
  Membership.mem (γ := Set ℝ)
    (upperBounds
      (Set.range fun (x : α) ↦
        dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β)))
    (Metric.ediam.{u_2} (X := β) Set.univ).toReal
⊢ BddAbove (α := ℝ)
    (Set.range fun (x : α) ↦
      dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β))

Tactic:
use (Metric.ediam (.univ : Set β)).toReal

Premises used: Set.univ, Metric.ediam, ENNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoMetricSpace β
inst_2 : BoundedSpace β
f g : α →ᵤ β
h : Nonempty α
⊢ Membership.mem (γ := Set ℝ)
    (upperBounds
      (Set.range fun (x : α) ↦
        dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β)))
    (Metric.ediam.{u_2} (X := β) Set.univ).toReal

Tactic:
simp +contextual [mem_upperBounds, eq_comm (a := dist _ _), ← edist_dist,
          ← ENNReal.ofReal_le_iff_le_toReal BoundedSpace.bounded_univ.ediam_ne_top,
          Metric.edist_le_ediam_of_mem]

Premises used: ENNReal.ofReal_le_iff_le_toReal, BoundedSpace.bounded_univ, Metric.edist_le_ediam_of_mem, eq_comm, Bornology.IsBounded.ediam_ne_top, edist_dist, mem_upperBounds
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoMetricSpace β
inst_2 : BoundedSpace β
f g : α →ᵤ β
h : Nonempty α
⊢ BddAbove (α := ℝ)
    (Set.range fun (x : α) ↦
      dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β))

Tactic:
have : BddAbove <| .range fun x ↦ dist (toFun f x) (toFun g x) := by
        use (Metric.ediam (.univ : Set β)).toReal
        simp +contextual [mem_upperBounds, eq_comm (a := dist _ _), ← edist_dist,
          ← ENNReal.ofReal_le_iff_le_toReal BoundedSpace.bounded_univ.ediam_ne_top,
          Metric.edist_le_ediam_of_mem]
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoMetricSpace β
inst_2 : BoundedSpace β
f g : α →ᵤ β
h : Nonempty α
this :
  BddAbove (α := ℝ)
    (Set.range fun (x : α) ↦
      dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β))
r : ℝ≥0
⊢ edist f g ≤ (↑r : ℝ≥0∞) ↔
    ENNReal.ofReal
        ((fun (f g : α →ᵤ β) ↦
            (⨆ (x : α),
                dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β) :
              ℝ))
          f g) ≤
      (↑r : ℝ≥0∞)

Tactic:
simp [edist_def, ciSup_le_iff this]

Premises used: ciSup_le_iff, UniformFun.edist_def
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace γ
inst_1 : PseudoMetricSpace β
inst_2 : BoundedSpace β
f g : α →ᵤ β
h : Nonempty α
this :
  BddAbove (α := ℝ)
    (Set.range fun (x : α) ↦
      dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β))
⊢ edist f g =
    ENNReal.ofReal
      ((fun (f g : α →ᵤ β) ↦
          (⨆ (x : α),
              dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β) :
            ℝ))
        f g)

Tactic:
exact ENNReal.eq_of_forall_le_nnreal_iff fun r ↦ by simp [edist_def, ciSup_le_iff this]

Premises used: ENNReal.eq_of_forall_le_nnreal_iff
-- Module: Mathlib.Topology.MetricSpace.UniformConvergence
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace β
inst_1 : BoundedSpace β
f g : α →ᵤ β
⊢ dist f g =
    ⨆ (x : α), dist.{u_2} (α := β) ((toFun : (a : α →ᵤ β) → α → β) f x : β) ((toFun : (a : α →ᵤ β) → α → β) g x : β)

Tactic:
rfl

Premises used: rfl