awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
x : α
r : ℝ
hr : 0 < r
K : ℝ
h : ∀ (y : α), dist y x < r → dist (f y) (f x) ≤ K * dist y x
⊢ ContinuousAt f x

Tactic:
tendsto_iff_dist_tendsto_zero.2 (squeeze_zero' (Eventually.of_forall fun _ => dist_nonneg)
    (mem_of_superset (ball_mem_nhds _ hr) h) ?_)

Premises used: Iff.mpr, ContinuousAt, dist_nonneg, Filter.Eventually.of_forall, Metric.ball_mem_nhds, tendsto_iff_dist_tendsto_zero, Filter.mem_of_superset, squeeze_zero'
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
x : α
r : ℝ
hr : 0 < r
K : ℝ
h : ∀ (y : α), dist y x < r → dist (f y) (f x) ≤ K * dist y x
refine : Tendsto (β := ℝ) (fun (a : α) ↦ K * dist a x) (nhds x) (nhds 0)
⊢ ContinuousAt f x

Tactic:
refine tendsto_iff_dist_tendsto_zero.2 (squeeze_zero' (Eventually.of_forall fun _ => dist_nonneg)
    (mem_of_superset (ball_mem_nhds _ hr) h) ?_)

Premises used: Iff.mpr, dist_nonneg, Filter.Eventually.of_forall, Metric.ball_mem_nhds, tendsto_iff_dist_tendsto_zero, Filter.mem_of_superset, squeeze_zero'
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
x : α
r : ℝ
hr : 0 < r
K : ℝ
h : ∀ (y : α), dist y x < r → dist (f y) (f x) ≤ K * dist y x
⊢ Continuous (Y := ℝ) fun (a : α) ↦ K * dist a x

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
x : α
r : ℝ
hr : 0 < r
K : ℝ
h : ∀ (y : α), dist y x < r → dist (f y) (f x) ≤ K * dist y x
⊢ K * dist x x = 0

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
x : α
r : ℝ
hr : 0 < r
K : ℝ
h : ∀ (y : α), dist y x < r → dist (f y) (f x) ≤ K * dist y x
⊢ Tendsto (β := ℝ) (fun (a : α) ↦ K * dist a x) (nhds x) (nhds 0)

Tactic:
exact Continuous.tendsto' (by fun_prop) x 0 (by simp)

Premises used: Continuous.tendsto', OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf : LocallyLipschitzOn s f
⊢ ContinuousOn f s

Tactic:
have hf' := hf.continuousOn
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf : LocallyLipschitzOn s f
hf' : ContinuousOn f s
x : α
hx : x ∈ s
let :
  ∀ (K : ℝ≥0) (t : Set α) (ht : t ∈ nhdsWithin x s) (hf : LipschitzOnWith K f t),
    ∃ ε > 0, ∃ (K : ℝ≥0), LipschitzOnWith K f (ball x ε ∩ s)
⊢ ∃ ε > 0, ∃ (K : ℝ≥0), LipschitzOnWith K f (ball x ε ∩ s)

Tactic:
let ⟨K, t, ht, hf⟩ := hf hx
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf_1 : LocallyLipschitzOn s f
hf' : ContinuousOn f s
x : α
hx : x ∈ s
K : ℝ≥0
t : Set α
ht : t ∈ nhdsWithin x s
hf : LipschitzOnWith K f t
let : ∀ (ε : ℝ) (hε : ε > 0) (hε' : ball x ε ∩ s ⊆ t), ∃ ε > 0, ∃ (K : ℝ≥0), LipschitzOnWith K f (ball x ε ∩ s)
⊢ ∃ ε > 0, ∃ (K : ℝ≥0), LipschitzOnWith K f (ball x ε ∩ s)

Tactic:
let ⟨ε, hε, hε'⟩ := Metric.mem_nhdsWithin_iff.1 ht
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf_1 : LocallyLipschitzOn s f
hf' : ContinuousOn f s
x : α
hx : x ∈ s
K : ℝ≥0
t : Set α
ht : t ∈ nhdsWithin x s
hf : LipschitzOnWith K f t
ε : ℝ
hε : ε > 0
hε' : ball x ε ∩ s ⊆ t
⊢ ∃ ε > 0, ∃ (K : ℝ≥0), LipschitzOnWith K f (ball x ε ∩ s)

Tactic:
⟨ε, hε, K, hf.mono hε'⟩

Premises used: LipschitzOnWith.mono, And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf_1 : LocallyLipschitzOn s f
hf' : ContinuousOn f s
x : α
hx : x ∈ s
K : ℝ≥0
t : Set α
ht : t ∈ nhdsWithin x s
hf : LipschitzOnWith K f t
ε : ℝ
hε : ε > 0
hε' : ball x ε ∩ s ⊆ t
⊢ ∃ ε > 0, ∃ (K : ℝ≥0), LipschitzOnWith K f (ball x ε ∩ s)

Tactic:
exact ⟨ε, hε, K, hf.mono hε'⟩
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf : LocallyLipschitzOn s f
hf' : ContinuousOn f s
⊢ ∀ x ∈ s, ∃ ε > 0, ∃ (K : ℝ≥0), LipschitzOnWith K f (ball x ε ∩ s)

Tactic:
replace hf : ∀ x ∈ s, ∃ ε > 0, ∃ K, LipschitzOnWith K f (ball x ε ∩ s) := fun x hx ↦ by
    let ⟨K, t, ht, hf⟩ := hf hx
    let ⟨ε, hε, hε'⟩ := Metric.mem_nhdsWithin_iff.1 ht
    exact ⟨ε, hε, K, hf.mono hε'⟩
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
hf : ∀ x ∈ s, ∃ ε > 0, ∃ (K : ℝ≥0), LipschitzOnWith K f (ball x ε ∩ s)
choose :
  ∀ (ε : (x : α) → x ∈ s → ℝ) (hε : ∀ (x : α) (a : x ∈ s), ε x a > 0) (K : (x : α) → x ∈ s → ℝ≥0)
    (hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)), ∃ (K : ℝ≥0), LipschitzOnWith K f s
⊢ ∃ (K : ℝ≥0), LipschitzOnWith K f s

Tactic:
choose ε hε K hf using hf
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
⊢ ContinuousOn (Y := ℝ) (fun (y : α) ↦ dist (f x) (f y)) s

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
⊢ ContinuousOn (dist x) (s \ ball x (ε x hx))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
let :
  ∀ (K' : ℝ)
    (hK' :
      Membership.mem (γ := Set ℝ) (upperBounds ((fun (y : α) ↦ dist (f x) (f y) / dist x y) '' (s \ ball x (ε x hx))))
        K'),
    ∃ (K' : ℝ≥0), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑K' : ENNReal) * edist x y
⊢ ∃ (K' : ℝ≥0), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑K' : ENNReal) * edist x y

Tactic:
let ⟨K', hK'⟩ := (hs.diff isOpen_ball).bddAbove_image
      (f := fun y ↦ dist (f x) (f y) / dist x y) <| .div (.mono (by fun_prop) s.diff_subset)
        (by fun_prop) fun y hy ↦ ((hε x hx).trans_le <| not_lt.1 <| dist_comm x y ▸ hy.2).ne'
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
K' : ℝ
hK' :
  Membership.mem (γ := Set ℝ) (upperBounds ((fun (y : α) ↦ dist (f x) (f y) / dist x y) '' (s \ ball x (ε x hx)))) K'
⊢ ∃ (K' : ℝ≥0), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑K' : ENNReal) * edist x y

Tactic:
⟨.mk (K' ⊔ 0) le_sup_right, fun y hy ↦ ?_⟩

Premises used: NNReal.mk, le_sup_right, Max.max, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
K' : ℝ
hK' :
  Membership.mem (γ := Set ℝ) (upperBounds ((fun (y : α) ↦ dist (f x) (f y) / dist x y) '' (s \ ball x (ε x hx)))) K'
refine :
  ∀ (y : α) (hy : y ∈ s.diff (ball x (ε x hx))), edist (f x) (f y) ≤ (↑(NNReal.mk (max K' 0) ⋯) : ENNReal) * edist x y
⊢ ∃ (K' : ℝ≥0), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑K' : ENNReal) * edist x y

Tactic:
refine ⟨.mk (K' ⊔ 0) le_sup_right, fun y hy ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
K' : ℝ
hK' :
  Membership.mem (γ := Set ℝ) (upperBounds ((fun (y : α) ↦ dist (f x) (f y) / dist x y) '' (s \ ball x (ε x hx)))) K'
y : α
hy : y ∈ s.diff (ball x (ε x hx))
simp_rw : nndist (f x) (f y) ≤ NNReal.mk (max K' 0) ⋯ * nndist x y
⊢ edist (f x) (f y) ≤ (↑(NNReal.mk (max K' 0) ⋯) : ENNReal) * edist x y

Tactic:
simp_rw [edist_nndist, ← ENNReal.coe_mul, ENNReal.coe_le_coe]

Premises used: ENNReal.coe_le_coe, ENNReal.coe_mul, edist_nndist
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
K' : ℝ
hK' :
  Membership.mem (γ := Set ℝ) (upperBounds ((fun (y : α) ↦ dist (f x) (f y) / dist x y) '' (s \ ball x (ε x hx)))) K'
y : α
hy : y ∈ s.diff (ball x (ε x hx))
⊢ nndist (f x) (f y) ≤ NNReal.mk (max K' 0) ⋯ * nndist x y

Tactic:
(div_le_iff₀ ?_).1 ?_

Premises used: div_le_iff₀, Iff.mp
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
K' : ℝ
hK' :
  Membership.mem (γ := Set ℝ) (upperBounds ((fun (y : α) ↦ dist (f x) (f y) / dist x y) '' (s \ ball x (ε x hx)))) K'
y : α
hy : y ∈ s.diff (ball x (ε x hx))
refine_1 : 0 < nndist x y
refine_2 : nndist (f x) (f y) / nndist x y ≤ NNReal.mk (max K' 0) ⋯
⊢ nndist (f x) (f y) ≤ NNReal.mk (max K' 0) ⋯ * nndist x y

Tactic:
refine (div_le_iff₀ ?_).1 ?_

Premises used: div_le_iff₀, Iff.mp
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
K' : ℝ
hK' :
  Membership.mem (γ := Set ℝ) (upperBounds ((fun (y : α) ↦ dist (f x) (f y) / dist x y) '' (s \ ball x (ε x hx)))) K'
y : α
hy : y ∈ s.diff (ball x (ε x hx))
⊢ 0 < nndist x y

Tactic:
NNReal.coe_pos.1 <| coe_nndist x y ▸
        ((hε x hx).trans_le <| not_lt.1 <| dist_comm x y ▸ hy.2)

Premises used: coe_nndist, Eq.rec, dist_comm, not_lt, And.right, LT.lt.trans_le, Iff.mp, NNReal.coe_pos, Eq.symm
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
K' : ℝ
hK' :
  Membership.mem (γ := Set ℝ) (upperBounds ((fun (y : α) ↦ dist (f x) (f y) / dist x y) '' (s \ ball x (ε x hx)))) K'
y : α
hy : y ∈ s.diff (ball x (ε x hx))
⊢ 0 < nndist x y

Tactic:
exact NNReal.coe_pos.1 <| coe_nndist x y ▸
        ((hε x hx).trans_le <| not_lt.1 <| dist_comm x y ▸ hy.2)

Premises used: Iff.mp, NNReal.coe_pos
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
K' : ℝ
hK' :
  Membership.mem (γ := Set ℝ) (upperBounds ((fun (y : α) ↦ dist (f x) (f y) / dist x y) '' (s \ ball x (ε x hx)))) K'
y : α
hy : y ∈ s.diff (ball x (ε x hx))
⊢ nndist (f x) (f y) / nndist x y ≤ NNReal.mk (max K' 0) ⋯

Tactic:
simp [← NNReal.coe_le_coe, (mem_upperBounds.1 hK') _ <| mem_image_of_mem _ hy]

Premises used: Set.mem_image_of_mem, Iff.mp, NNReal.coe_le_coe, mem_upperBounds
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
⊢ ∀ (x : α) (hx : x ∈ s), ∃ (K' : ℝ≥0), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑K' : ENNReal) * edist x y

Tactic:
have (x) (hx : x ∈ s) : ∃ K' : ℝ≥0, ∀ y ∈ s.diff (ball x (ε x hx)),
      edist (f x) (f y) ≤ K' * edist x y := by
    let ⟨K', hK'⟩ := (hs.diff isOpen_ball).bddAbove_image
      (f := fun y ↦ dist (f x) (f y) / dist x y) <| .div (.mono (by fun_prop) s.diff_subset)
        (by fun_prop) fun y hy ↦ ((hε x hx).trans_le <| not_lt.1 <| dist_comm x y ▸ hy.2).ne'
    refine ⟨.mk (K' ⊔ 0) le_sup_right, fun y hy ↦ ?_⟩
    simp_rw [edist_nndist, ← ENNReal.coe_mul, ENNReal.coe_le_coe]
    refine (div_le_iff₀ ?_).1 ?_
    · exact NNReal.coe_pos.1 <| coe_nndist x y ▸
        ((hε x hx).trans_le <| not_lt.1 <| dist_comm x y ▸ hy.2)
    · simp [← NNReal.coe_le_coe, (mem_upperBounds.1 hK') _ <| mem_image_of_mem _ hy]
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
this :
  ∀ (x : α) (hx : x ∈ s), ∃ (K' : ℝ≥0), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑K' : ENNReal) * edist x y
choose :
  ∀ (K' : (x : α) → (hx : x ∈ s) → ℝ≥0)
    (hK' :
      ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y),
    ∃ (K : ℝ≥0), LipschitzOnWith K f s
⊢ ∃ (K : ℝ≥0), LipschitzOnWith K f s

Tactic:
choose K' hK' using this
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
obtain :
  ∀ (t : Finset (↑s : Type u_1)) (ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)),
    ∃ (K : ℝ≥0), LipschitzOnWith K f s
⊢ ∃ (K : ℝ≥0), LipschitzOnWith K f s

Tactic:
obtain ⟨t, ht⟩ := hs.elim_nhdsWithin_subcover' (fun x hx ↦ s ∩ ball x (ε x hx / 2))
    (fun x hx ↦ inter_mem_nhdsWithin s <| ball_mem_nhds x <| half_pos <| hε x hx)

Premises used: inter_mem_nhdsWithin, half_pos, HDiv.hDiv, Metric.ball, Inter.inter, Metric.ball_mem_nhds, IsCompact.elim_nhdsWithin_subcover', OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
h : LipschitzOnWith (t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) f s
⊢ ∃ (K : ℝ≥0), LipschitzOnWith K f s

Tactic:
use t.sup fun i ↦ K _ i.2 + 2 * K' _ i.2

Premises used: HMul.hMul, HAdd.hAdd, Finset.sup, OfNat.ofNat, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h :
  ∀ (z : (↑s : Type u_1)) (hz : z ∈ t) (hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)),
    edist (f x) (f y) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal) * edist x y
⊢ edist (f x) (f y) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal) * edist x y

Tactic:
let ⟨z, hz, hx'⟩ := mem_iUnion₂.1 <| ht hx
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
pos :
  ∀ (hy' : y ∈ ball (↑z : α) (ε (↑z : α) ⋯)),
    edist (f x) (f y) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal) * edist x y
neg :
  ∀ (hy' : y ∉ ball (↑z : α) (ε (↑z : α) ⋯)),
    edist (f x) (f y) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal) * edist x y
⊢ edist (f x) (f y) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal) * edist x y

Tactic:
by_cases hy' : y ∈ ball z.1 (ε _ z.2)

Premises used: Metric.ball, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
hy' : y ∈ ball (↑z : α) (ε (↑z : α) ⋯)
⊢ edist (f x) (f y) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal) * edist x y

Tactic:
(hf _ z.2 ⟨hx'.2.trans <| half_lt_self <| hε _ z.2, hx⟩ ⟨hy', hy⟩).trans <|
      mul_le_mul_of_nonneg_right ?_ zero_le

Premises used: half_lt_self, zero_le, mul_le_mul_of_nonneg_right, And.intro, LT.lt.trans, LE.le.trans, Subtype.property
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
hy' : y ∈ ball (↑z : α) (ε (↑z : α) ⋯)
pos : (↑(K (↑z : α) ⋯) : ENNReal) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal)
⊢ edist (f x) (f y) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal) * edist x y

Tactic:
refine (hf _ z.2 ⟨hx'.2.trans <| half_lt_self <| hε _ z.2, hx⟩ ⟨hy', hy⟩).trans <|
      mul_le_mul_of_nonneg_right ?_ zero_le

Premises used: half_lt_self, zero_le, mul_le_mul_of_nonneg_right, And.intro, LT.lt.trans, LE.le.trans, Subtype.property
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
hy' : y ∈ ball (↑z : α) (ε (↑z : α) ⋯)
⊢ (↑(K (↑z : α) ⋯) : ENNReal) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal)

Tactic:
ENNReal.coe_le_coe.2 <| t.le_sup_of_le hz <| le_self_add

Premises used: Iff.mpr, ENNReal.coe_le_coe, Finset.le_sup_of_le, le_self_add
-- Module: Mathlib.Topology.Algebra.MetricSpace.Lipschitz
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
hy' : y ∈ ball (↑z : α) (ε (↑z : α) ⋯)
⊢ (↑(K (↑z : α) ⋯) : ENNReal) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal)

Tactic:
exact ENNReal.coe_le_coe.2 <| t.le_sup_of_le hz <| le_self_add

Premises used: Iff.mpr, ENNReal.coe_le_coe, Finset.le_sup_of_le, le_self_add