awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
⊢ (⇑(toLocallyBoundedMap f hf) : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
⊢ comap f (cobounded β) ≤ cobounded α

Tactic:
(hf.toLocallyBoundedMap f).2

Premises used: Set.Mem, LocallyBoundedMap.comap_cobounded_le', setOf, LipschitzWith.toLocallyBoundedMap
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
s : Set α
hs : Bornology.IsBounded s
⊢ Bornology.IsBounded (f '' s)

Tactic:
hs.image (toLocallyBoundedMap f hf)

Premises used: Bornology.IsBounded.image, LipschitzWith.toLocallyBoundedMap
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
s : Set α
hs : Bornology.IsBounded s
⊢ Metric.diam (f '' s) ≤ (↑K : ℝ) * Metric.diam s

Tactic:
Metric.diam_le_of_forall_dist_le (mul_nonneg K.coe_nonneg Metric.diam_nonneg) <|
    forall_mem_image.2 fun _x hx =>
      forall_mem_image.2 fun _y hy => hf.dist_le_mul_of_le <| Metric.dist_le_diam_of_mem hs hx hy

Premises used: Iff.mpr, mul_nonneg, LipschitzWith.dist_le_mul_of_le, Metric.diam_nonneg, Metric.dist_le_diam_of_mem, NNReal.coe_nonneg, Metric.diam_le_of_forall_dist_le, Set.forall_mem_image
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
y : α
⊢ LipschitzWith (β := ℝ) 1 fun (x : α) ↦ dist x y

Tactic:
LipschitzWith.mk_one fun _ _ => dist_dist_dist_le_left _ _ _

Premises used: LipschitzWith.mk_one, dist_dist_dist_le_left
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
x : α
⊢ LipschitzWith 1 (dist x)

Tactic:
LipschitzWith.of_le_add fun _ _ => dist_triangle_right _ _ _

Premises used: LipschitzWith.of_le_add, dist_triangle_right
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
rw : LipschitzWith.{u, 0} (α := α × α) (HAdd.hAdd (α := ℝ≥0) 1 1) (uncurry dist)
⊢ LipschitzWith.{u, 0} (α := α × α) 2 (uncurry dist)

Tactic:
rw [← one_add_one_eq_two]

Premises used: one_add_one_eq_two
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ LipschitzWith.{u, 0} (α := α × α) (HAdd.hAdd (α := ℝ≥0) 1 1) (uncurry dist)

Tactic:
LipschitzWith.uncurry LipschitzWith.dist_left LipschitzWith.dist_right

Premises used: LipschitzWith.dist_left, LipschitzWith.uncurry, LipschitzWith.dist_right
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ LipschitzWith.{u, 0} (α := α × α) (HAdd.hAdd (α := ℝ≥0) 1 1) (uncurry dist)

Tactic:
exact LipschitzWith.uncurry LipschitzWith.dist_left LipschitzWith.dist_right

Premises used: LipschitzWith.dist_left, LipschitzWith.uncurry, LipschitzWith.dist_right
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
rw : dist (f^[n] x) ((f^[n] ∘ f) x) ≤ (↑K : ℝ) ^ n * dist x (f x)
⊢ dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * (↑K : ℝ) ^ n

Tactic:
rw [iterate_succ, mul_comm]

Premises used: Function.iterate_succ, mul_comm
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ dist (f^[n] x) ((f^[n] ∘ f) x) ≤ (↑K : ℝ) ^ n * dist x (f x)

Tactic:
simpa only [NNReal.coe_pow] using (hf.iterate n).dist_le_mul x (f x)

Premises used: LipschitzWith.dist_le_mul, LipschitzWith.iterate, NNReal.coe_pow
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
⊢ LipschitzWith (β := ℝ) 1 fun (p : ℝ × ℝ) ↦ max p.1 p.2

Tactic:
LipschitzWith.of_le_add fun _ _ => sub_le_iff_le_add'.1 <|
    (le_abs_self _).trans (abs_max_sub_max_le_max _ _ _ _)

Premises used: le_abs_self, LipschitzWith.of_le_add, HSub.hSub, abs_max_sub_max_le_max, Prod.fst, sub_le_iff_le_add', Max.max, Iff.mp, LE.le.trans, Prod.snd
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
⊢ LipschitzWith (β := ℝ) 1 fun (p : ℝ × ℝ) ↦ min p.1 p.2

Tactic:
LipschitzWith.of_le_add fun _ _ => sub_le_iff_le_add'.1 <|
    (le_abs_self _).trans (abs_min_sub_min_le_max _ _ _ _)

Premises used: le_abs_self, LipschitzWith.of_le_add, HSub.hSub, Prod.fst, sub_le_iff_le_add', Iff.mp, LE.le.trans, abs_min_sub_min_le_max, Prod.snd, Min.min
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
⊢ LipschitzWith 1 Real.toNNReal

Tactic:
lipschitzWith_iff_dist_le_mul.mpr (fun x y ↦ ?_)

Premises used: Iff.mpr, lipschitzWith_iff_dist_le_mul
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
refine : ∀ (x y : ℝ), dist x.toNNReal y.toNNReal ≤ (↑1 : ℝ) * dist x y
⊢ LipschitzWith 1 Real.toNNReal

Tactic:
refine lipschitzWith_iff_dist_le_mul.mpr (fun x y ↦ ?_)

Premises used: Iff.mpr, lipschitzWith_iff_dist_le_mul
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
x y : ℝ
⊢ dist x.toNNReal y.toNNReal ≤ (↑1 : ℝ) * dist x y

Tactic:
simpa only [NNReal.coe_one, dist_prod_same_right, one_mul, Real.dist_eq] using
    lipschitzWith_iff_dist_le_mul.mp lipschitzWith_max (x, 0) (y, 0)

Premises used: Prod.mk, dist_prod_same_right, lipschitzWith_iff_dist_le_mul, Real.dist_eq, Iff.mp, NNReal.coe_one, lipschitzWith_max, OfNat.ofNat, one_mul
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f g : α → ℝ
Kf Kg : ℝ≥0
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
⊢ LipschitzWith (β := ℝ) (max Kf Kg) fun (x : α) ↦ max (f x) (g x)

Tactic:
simpa only [(· ∘ ·), one_mul] using lipschitzWith_max.comp (hf.prodMk hg)

Premises used: Function.comp, LipschitzWith.prodMk, LipschitzWith.comp, lipschitzWith_max, one_mul
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f g : α → ℝ
Kf Kg : ℝ≥0
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
⊢ LipschitzWith (β := ℝ) (max Kf Kg) fun (x : α) ↦ min (f x) (g x)

Tactic:
simpa only [(· ∘ ·), one_mul] using lipschitzWith_min.comp (hf.prodMk hg)

Premises used: Function.comp, LipschitzWith.prodMk, LipschitzWith.comp, lipschitzWith_min, one_mul
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : α → ℝ
Kf : ℝ≥0
hf : LipschitzWith Kf f
a : ℝ
⊢ LipschitzWith (β := ℝ) Kf fun (x : α) ↦ max (f x) a

Tactic:
simpa using hf.max (LipschitzWith.const a)

Premises used: LipschitzWith.max, LipschitzWith.const
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : α → ℝ
Kf : ℝ≥0
hf : LipschitzWith Kf f
a : ℝ
⊢ LipschitzWith (β := ℝ) Kf fun (x : α) ↦ max a (f x)

Tactic:
simpa only [max_comm] using hf.max_const a

Premises used: LipschitzWith.max_const, max_comm
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : α → ℝ
Kf : ℝ≥0
hf : LipschitzWith Kf f
a : ℝ
⊢ LipschitzWith (β := ℝ) Kf fun (x : α) ↦ min (f x) a

Tactic:
simpa using hf.min (LipschitzWith.const a)

Premises used: LipschitzWith.min, LipschitzWith.const
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : α → ℝ
Kf : ℝ≥0
hf : LipschitzWith Kf f
a : ℝ
⊢ LipschitzWith (β := ℝ) Kf fun (x : α) ↦ min a (f x)

Tactic:
simpa only [min_comm] using hf.min_const a

Premises used: min_comm, LipschitzWith.min_const
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
a b : ℝ
h : a ≤ b
⊢ LipschitzWith 1 (projIcc a b h)

Tactic:
((LipschitzWith.id.const_min _).const_max _).subtype_mk _

Premises used: LipschitzWith.id, Set.projIcc, LipschitzWith.const_min, LipschitzWith.subtype_mk, LipschitzWith.const_max
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoMetricSpace X
inst_1 : PseudoMetricSpace Y
inst_2 : ProperSpace Y
f : X → Y
hf : IsProperMap f
K : ℝ≥0
hf' : LipschitzWith K f
⊢ ProperSpace X

Tactic:
⟨fun x r ↦ (hf.isCompact_preimage (isCompact_closedBall (f x) (K * r))).of_isClosed_subset
    Metric.isClosed_closedBall (hf'.mapsTo_closedBall x r).subset_preimage⟩

Premises used: HMul.hMul, Set.MapsTo.subset_preimage, Metric.isClosed_closedBall, IsProperMap.isCompact_preimage, IsCompact.of_isClosed_subset, ProperSpace.mk, ProperSpace.isCompact_closedBall, LipschitzWith.mapsTo_closedBall, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
s : Set α
f : α → β
K : ℝ
h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hbc : K ≤ (↑K.toNNReal : ℝ)
⊢ K * dist x y ≤ (↑K.toNNReal : ℝ) * dist x y

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
s : Set α
f : α → β
K : ℝ
h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ K ≤ (↑K.toNNReal : ℝ)

Tactic:
apply Real.le_coe_toNNReal

Premises used: Real.le_coe_toNNReal
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
s : Set α
f : α → β
h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ dist x y
⊢ ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ (↑1 : ℝ) * dist x y

Tactic:
simpa only [NNReal.coe_one, one_mul] using h

Premises used: NNReal.coe_one, one_mul
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
f : α → ℝ
K : ℝ
h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + K * dist x y
⊢ LipschitzOnWith K.toNNReal f s

Tactic:
have I : ∀ x ∈ s, ∀ y ∈ s, f x - f y ≤ K * dist x y := fun x hx y hy =>
    sub_le_iff_le_add'.2 (h x hx y hy)
  LipschitzOnWith.of_dist_le' fun x hx y hy =>
    abs_sub_le_iff.2 ⟨I x hx y hy, dist_comm y x ▸ I y hy x hx⟩

Premises used: Iff.mpr, abs_sub_le_iff, Eq.rec, dist_comm, sub_le_iff_le_add', And.intro, LipschitzOnWith.of_dist_le'
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
f : α → ℝ
K : ℝ≥0
h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + (↑K : ℝ) * dist x y
⊢ LipschitzOnWith K f s

Tactic:
simpa only [Real.toNNReal_coe] using LipschitzOnWith.of_le_add_mul' K h

Premises used: Real.toNNReal_coe, LipschitzOnWith.of_le_add_mul', NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
f : α → ℝ
h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + dist x y
⊢ ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + (↑1 : ℝ) * dist x y

Tactic:
simpa only [NNReal.coe_one, one_mul]

Premises used: NNReal.coe_one, one_mul
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
f : α → ℝ
K : ℝ≥0
h : LipschitzOnWith K f s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ f x ≤ f y + (↑K : ℝ) * dist x y

Tactic:
sub_le_iff_le_add'.1 <| le_trans (le_abs_self _) <| h.dist_le_mul x hx y hy

Premises used: le_abs_self, sub_le_iff_le_add', LipschitzOnWith.dist_le_mul, Iff.mp, le_trans
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
f : α → ℝ
K : ℝ≥0
⊢ LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + (↑K : ℝ) * dist x y

Tactic:
⟨LipschitzOnWith.le_add_mul, LipschitzOnWith.of_le_add_mul K⟩

Premises used: LipschitzOnWith.le_add_mul, Iff.intro, LipschitzOnWith.of_le_add_mul
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f : α → β → γ
K₁ K₂ : ℝ≥0
s : Set α
t : Set β
hs : Bornology.IsBounded s
ht : Bornology.IsBounded t
hf₁ : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K₁ (fun (a : α) ↦ f a b) s
hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t
⊢ Bornology.IsBounded (image2 f s t)

Tactic:
Metric.isBounded_iff_ediam_ne_top.2 <|
    ne_top_of_le_ne_top
      (ENNReal.add_ne_top.mpr
        ⟨ENNReal.mul_ne_top ENNReal.coe_ne_top hs.ediam_ne_top,
          ENNReal.mul_ne_top ENNReal.coe_ne_top ht.ediam_ne_top⟩)
      (ediam_image2_le _ _ _ hf₁ hf₂)

Premises used: Iff.mpr, Metric.isBounded_iff_ediam_ne_top, LipschitzOnWith.ediam_image2_le, Bornology.IsBounded.ediam_ne_top, ENNReal.mul_ne_top, ne_top_of_le_ne_top, And.intro, ENNReal.add_ne_top, ENNReal.coe_ne_top
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f g : α → ℝ
hf : LocallyLipschitz f
hg : LocallyLipschitz g
⊢ LocallyLipschitz (β := ℝ) fun (x : α) ↦ min (f x) (g x)

Tactic:
lipschitzWith_min.locallyLipschitz.comp (hf.prodMk hg)

Premises used: LocallyLipschitz.prodMk, LipschitzWith.locallyLipschitz, LocallyLipschitz.comp, lipschitzWith_min
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f g : α → ℝ
hf : LocallyLipschitz f
hg : LocallyLipschitz g
⊢ LocallyLipschitz (β := ℝ) fun (x : α) ↦ max (f x) (g x)

Tactic:
lipschitzWith_max.locallyLipschitz.comp (hf.prodMk hg)

Premises used: LocallyLipschitz.prodMk, LipschitzWith.locallyLipschitz, LocallyLipschitz.comp, lipschitzWith_max
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : α → ℝ
hf : LocallyLipschitz f
a : ℝ
⊢ LocallyLipschitz (β := ℝ) fun (x : α) ↦ max (f x) a

Tactic:
hf.max (LocallyLipschitz.const a)

Premises used: LocallyLipschitz.max, LocallyLipschitz.const
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : α → ℝ
hf : LocallyLipschitz f
a : ℝ
⊢ LocallyLipschitz (β := ℝ) fun (x : α) ↦ max a (f x)

Tactic:
simpa [max_comm] using (hf.max_const a)

Premises used: LocallyLipschitz.max_const, max_comm
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : α → ℝ
hf : LocallyLipschitz f
a : ℝ
⊢ LocallyLipschitz (β := ℝ) fun (x : α) ↦ min (f x) a

Tactic:
hf.min (LocallyLipschitz.const a)

Premises used: LocallyLipschitz.const, LocallyLipschitz.min
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : α → ℝ
hf : LocallyLipschitz f
a : ℝ
⊢ LocallyLipschitz (β := ℝ) fun (x : α) ↦ min a (f x)

Tactic:
simpa [min_comm] using (hf.min_const a)

Premises used: min_comm, LocallyLipschitz.min_const
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
inl : ∀ (hf : LipschitzOnWith K f ∅), ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn f g ∅
inr : ∀ (hs : s.Nonempty), ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn f g s
⊢ ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn f g s

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hs)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
K : ℝ≥0
hf : LipschitzOnWith K f ∅
⊢ ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn f g ∅

Tactic:
⟨fun _ => 0, (LipschitzWith.const _).weaken zero_le, eqOn_empty _ _⟩

Premises used: zero_le, And.intro, LipschitzWith.weaken, Exists.intro, LipschitzWith.const, OfNat.ofNat, Set.eqOn_empty
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
K : ℝ≥0
hf : LipschitzOnWith K f ∅
⊢ ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn f g ∅

Tactic:
exact ⟨fun _ => 0, (LipschitzWith.const _).weaken zero_le, eqOn_empty _ _⟩
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
⊢ Nonempty.{u + 1} (↑s : Type u)

Tactic:
simp only [hs, nonempty_coe_sort]

Premises used: Set.nonempty_coe_sort
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
⊢ Nonempty.{u + 1} (↑s : Type u)

Tactic:
have : Nonempty s := by simp only [hs, nonempty_coe_sort]
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
y : α
rcases :
  ∀ (z : α) (hz : z ∈ s), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
⊢ BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))

Tactic:
rcases hs with ⟨z, hz⟩
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
y z : α
hz : z ∈ s
⊢ BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))

Tactic:
⟨f z - K * dist y z, ?_⟩

Premises used: HMul.hMul, HSub.hSub, Set.Nonempty, BddBelow, Exists.intro, Dist.dist, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
y z : α
hz : z ∈ s
refine :
  Membership.mem (γ := Set ℝ) (lowerBounds (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)))
    (f z - (↑K : ℝ) * dist y z)
⊢ BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))

Tactic:
refine ⟨f z - K * dist y z, ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
y z : α
hz : z ∈ s
t : (↑s : Type u)
rw : f z ≤ f (↑t : α) + (↑K : ℝ) * (dist y z + dist y (↑t : α))
⊢ f z - (↑K : ℝ) * dist y z ≤ f (↑t : α) + (↑K : ℝ) * dist y (↑t : α)

Tactic:
rw [sub_le_iff_le_add, add_assoc, ← mul_add, add_comm (dist y t)]

Premises used: add_assoc, sub_le_iff_le_add, add_comm, mul_add, Dist.dist, Subtype.val
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
y z : α
hz : z ∈ s
t : (↑s : Type u)
⊢ f z ≤ f (↑t : α) + (↑K : ℝ) * dist z (↑t : α)

Tactic:
hf.le_add_mul hz t.2

Premises used: LipschitzOnWith.le_add_mul, Subtype.property
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
y z : α
hz : z ∈ s
t : (↑s : Type u)
bc : dist z (↑t : α) ≤ dist y z + dist y (↑t : α)
⊢ f (↑t : α) + (↑K : ℝ) * dist z (↑t : α) ≤ f (↑t : α) + (↑K : ℝ) * (dist y z + dist y (↑t : α))

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
y z : α
hz : z ∈ s
t : (↑s : Type u)
⊢ dist z (↑t : α) ≤ dist y z + dist y (↑t : α)

Tactic:
apply dist_triangle_left

Premises used: dist_triangle_left
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
y z : α
hz : z ∈ s
t : (↑s : Type u)
f₁ : f (↑t : α) + (↑K : ℝ) * dist z (↑t : α) ≤ f (↑t : α) + (↑K : ℝ) * (dist y z + dist y (↑t : α))
⊢ f z ≤ f (↑t : α) + (↑K : ℝ) * (dist y z + dist y (↑t : α))

Tactic:
calc
      f z ≤ f t + K * dist z t := hf.le_add_mul hz t.2
      _ ≤ f t + K * (dist y z + dist y t) := by gcongr; apply dist_triangle_left

Premises used: LipschitzOnWith.le_add_mul, HAdd.hAdd, Dist.dist, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
⊢ ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))

Tactic:
have B : ∀ y : α, BddBelow (range fun x : s => f x + K * dist y x) := fun y => by
    rcases hs with ⟨z, hz⟩
    refine ⟨f z - K * dist y z, ?_⟩
    rintro w ⟨t, rfl⟩
    dsimp
    rw [sub_le_iff_le_add, add_assoc, ← mul_add, add_comm (dist y t)]
    calc
      f z ≤ f t + K * dist z t := hf.le_add_mul hz t.2
      _ ≤ f t + K * (dist y z + dist y t) := by gcongr; apply dist_triangle_left
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
x : α
hx : x ∈ s
⊢ f x = g x

Tactic:
le_antisymm (le_ciInf fun y => hf.le_add_mul hx y.2) ?_

Premises used: LipschitzOnWith.le_add_mul, le_ciInf, le_antisymm, Subtype.property
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
x : α
hx : x ∈ s
refine : g x ≤ f x
⊢ f x = g x

Tactic:
refine le_antisymm (le_ciInf fun y => hf.le_add_mul hx y.2) ?_

Premises used: LipschitzOnWith.le_add_mul, le_ciInf, le_antisymm
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
x : α
hx : x ∈ s
⊢ g x ≤ f x

Tactic:
simpa only [add_zero, Subtype.coe_mk, mul_zero, dist_self] using ciInf_le (B x) ⟨x, hx⟩

Premises used: Subtype.coe_mk, MulZeroClass.mul_zero, Subtype.mk, dist_self, ciInf_le, add_zero
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
⊢ EqOn f g s

Tactic:
have E : EqOn f g s := fun x hx => by
    refine le_antisymm (le_ciInf fun y => hf.le_add_mul hx y.2) ?_
    simpa only [add_zero, Subtype.coe_mk, mul_zero, dist_self] using ciInf_le (B x) ⟨x, hx⟩
-- Module: Mathlib.Topology.MetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
E : EqOn f g s
⊢ ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn f g s

Tactic:
⟨g, LipschitzWith.of_le_add_mul K fun x y => ?_, E⟩

Premises used: LipschitzWith.of_le_add_mul, And.intro, Exists.intro