awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
⊢ LocallyLipschitzOn univ f ↔ LocallyLipschitz f

Tactic:
simp [LocallyLipschitzOn, LocallyLipschitz]

Premises used: LocallyLipschitz, LocallyLipschitzOn
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
s : Set α
f : α → β
h : LocallyLipschitz f
⊢ LocallyLipschitzOn s f

Tactic:
(locallyLipschitzOn_univ.2 h).mono s.subset_univ

Premises used: Iff.mpr, locallyLipschitzOn_univ, Set.subset_univ, LocallyLipschitzOn.mono
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
⊢ LipschitzOnWith K f s ↔ LipschitzWith K (s.restrict (π := fun (a : α) ↦ β) f)

Tactic:
simp [LipschitzOnWith, LipschitzWith]

Premises used: LipschitzWith, LipschitzOnWith
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
t : Set (↑s : Type u)
⊢ LipschitzOnWith K (s.restrict (π := fun (a : α) ↦ β) f) t ↔
    LipschitzOnWith K f (s ∩ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)

Tactic:
simp [LipschitzOnWith]

Premises used: LipschitzOnWith
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
s : Set α
f : α → β
simp :
  (∀ (x : (↑s : Type u)), ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] (↑x : α), LipschitzOnWith K f t) ↔
    ∀ (x : (↑s : Type u)),
      ∃ (K : ℝ≥0) (t : Set (↑s : Type u)),
        (∃ t_1 ∈ 𝓝[s] (↑x : α), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t_1 ⊆ t) ∧
          LipschitzOnWith K f (s ∩ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
⊢ LocallyLipschitzOn s f ↔ LocallyLipschitz (s.restrict (π := fun (a : α) ↦ β) f)

Tactic:
simp only [LocallyLipschitzOn, LocallyLipschitz, SetCoe.forall',
    lipschitzOnWith_restrict,
    nhds_subtype_eq_comap_nhdsWithin, mem_comap]

Premises used: LocallyLipschitz, Filter.mem_comap, nhds_subtype_eq_comap_nhdsWithin, lipschitzOnWith_restrict, LocallyLipschitzOn, SetCoe.forall'
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
s : Set α
f : α → β
a :
  ∀ (x : (↑s : Type u)) (K : ℝ≥0),
    (∃ t ∈ 𝓝[s] (↑x : α), LipschitzOnWith K f t) ↔
      ∃ (t : Set (↑s : Type u)),
        (∃ t_1 ∈ 𝓝[s] (↑x : α), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t_1 ⊆ t) ∧
          LipschitzOnWith K f (s ∩ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
⊢ (∀ (x : (↑s : Type u)), ∃ (K : ℝ≥0), ∃ t ∈ 𝓝[s] (↑x : α), LipschitzOnWith K f t) ↔
    ∀ (x : (↑s : Type u)),
      ∃ (K : ℝ≥0) (t : Set (↑s : Type u)),
        (∃ t_1 ∈ 𝓝[s] (↑x : α), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t_1 ⊆ t) ∧
          LipschitzOnWith K f (s ∩ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)

Tactic:
congr! with x K
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
s : Set α
f : α → β
x : (↑s : Type u)
K : ℝ≥0
a :
  (∃ t ∈ 𝓝[s] (↑x : α), LipschitzOnWith K f t) →
    ∃ (t : Set (↑s : Type u)),
      (∃ t_1 ∈ 𝓝[s] (↑x : α), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t_1 ⊆ t) ∧
        LipschitzOnWith K f (s ∩ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
a₁ :
  (∃ (t : Set (↑s : Type u)),
      (∃ t_1 ∈ 𝓝[s] (↑x : α), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t_1 ⊆ t) ∧
        LipschitzOnWith K f (s ∩ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)) →
    ∃ t ∈ 𝓝[s] (↑x : α), LipschitzOnWith K f t
⊢ (∃ t ∈ 𝓝[s] (↑x : α), LipschitzOnWith K f t) ↔
    ∃ (t : Set (↑s : Type u)),
      (∃ t_1 ∈ 𝓝[s] (↑x : α), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t_1 ⊆ t) ∧
        LipschitzOnWith K f (s ∩ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)

Tactic:
constructor
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
s : Set α
f : α → β
x : (↑s : Type u)
K : ℝ≥0
t : Set α
ht : t ∈ 𝓝[s] (↑x : α)
hft : LipschitzOnWith K f t
⊢ ∃ (t : Set (↑s : Type u)),
    (∃ t_1 ∈ 𝓝[s] (↑x : α), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t_1 ⊆ t) ∧
      LipschitzOnWith K f (s ∩ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)

Tactic:
⟨_, ⟨t, ht, Subset.rfl⟩, hft.mono <| inter_subset_right.trans <| image_preimage_subset ..⟩

Premises used: LipschitzOnWith.mono, HasSubset.Subset.trans, Set.Subset.rfl, And.intro, Set.image_preimage_subset, Exists.intro, Set.inter_subset_right
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
s : Set α
f : α → β
x : (↑s : Type u)
K : ℝ≥0
t : Set α
ht : t ∈ 𝓝[s] (↑x : α)
hft : LipschitzOnWith K f t
⊢ ∃ (t : Set (↑s : Type u)),
    (∃ t_1 ∈ 𝓝[s] (↑x : α), Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t_1 ⊆ t) ∧
      LipschitzOnWith K f (s ∩ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)

Tactic:
exact ⟨_, ⟨t, ht, Subset.rfl⟩, hft.mono <| inter_subset_right.trans <| image_preimage_subset ..⟩
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
s : Set α
f : α → β
x : (↑s : Type u)
K : ℝ≥0
t : Set (↑s : Type u)
hft : LipschitzOnWith K f (s ∩ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
u : Set α
hu : u ∈ 𝓝[s] (↑x : α)
hut : Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u ⊆ t
⊢ ∃ t ∈ 𝓝[s] (↑x : α), LipschitzOnWith K f t

Tactic:
⟨s ∩ u, Filter.inter_mem self_mem_nhdsWithin hu,
      hft.mono fun x hx ↦ ⟨hx.1, ⟨x, hx.1⟩, hut hx.2, rfl⟩⟩

Premises used: LipschitzOnWith.mono, Filter.inter_mem, Subtype.mk, Inter.inter, And.right, self_mem_nhdsWithin, And.left, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
s : Set α
f : α → β
x : (↑s : Type u)
K : ℝ≥0
t : Set (↑s : Type u)
hft : LipschitzOnWith K f (s ∩ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
u : Set α
hu : u ∈ 𝓝[s] (↑x : α)
hut : Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u ⊆ t
⊢ ∃ t ∈ 𝓝[s] (↑x : α), LipschitzOnWith K f t

Tactic:
exact ⟨s ∩ u, Filter.inter_mem self_mem_nhdsWithin hu,
      hft.mono fun x hx ↦ ⟨hx.1, ⟨x, hx.1⟩, hut hx.2, rfl⟩⟩
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
t : Set β
h : MapsTo f s t
⊢ LipschitzOnWith K f s ↔ LipschitzWith K (restrict f s t h)

Tactic:
_root_.lipschitzOnWith_iff_restrict

Premises used: Subtype.map, LipschitzWith, lipschitzOnWith_iff_restrict, Set.restrict, Set.MapsTo.restrict
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
s : Set α
h : LipschitzWith K f
⊢ LipschitzOnWith K f s

Tactic:
fun x _ y _ => h x y

Premises used: LipschitzOnWith
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
h : LipschitzWith K f
x y : α
⊢ edist (f x) (f y) ≤ (↑K : ℝ≥0∞) * edist x y

Tactic:
h x y
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ≥0∞
h : LipschitzWith K f
hr : edist x y ≤ r
⊢ edist (f x) (f y) ≤ (↑K : ℝ≥0∞) * r

Tactic:
(h x y).trans <| mul_right_mono hr

Premises used: mul_right_mono, LE.le.trans
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ≥0∞
h : LipschitzWith K f
hK : K ≠ 0
hr : edist x y < r
grw : (↑K : ℝ≥0∞) * edist x y < (↑K : ℝ≥0∞) * r
⊢ edist (f x) (f y) < (↑K : ℝ≥0∞) * r

Tactic:
grw [h x y]
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ≥0∞
h : LipschitzWith K f
hK : K ≠ 0
hr : edist x y < r
hinf : (↑K : ℝ≥0∞) ≠ ∞
⊢ (↑K : ℝ≥0∞) * edist x y < (↑K : ℝ≥0∞) * r

Tactic:
gcongr
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ≥0∞
h : LipschitzWith K f
hK : K ≠ 0
hr : edist x y < r
⊢ (↑K : ℝ≥0∞) ≠ ∞

Tactic:
simp
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
h : LipschitzWith K f
x : α
r : ℝ≥0∞
⊢ MapsTo f (closedEBall x r) (closedEBall (f x) ((↑K : ℝ≥0∞) * r))

Tactic:
fun _y hy => h.edist_le_mul_of_le hy

Premises used: Set.Mem, setOf, LipschitzWith.edist_le_mul_of_le, Set.MapsTo, Metric.closedEBall
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
h : LipschitzWith K f
hK : K ≠ 0
x : α
r : ℝ≥0∞
⊢ MapsTo f (eball x r) (eball (f x) ((↑K : ℝ≥0∞) * r))

Tactic:
fun _y hy => h.edist_lt_mul_of_lt hK hy

Premises used: Set.Mem, setOf, Metric.eball, Set.MapsTo, LipschitzWith.edist_lt_mul_of_lt
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
x y : α
h : edist x y ≠ ∞
⊢ (↑K : ℝ≥0∞) * edist x y < ∞

Tactic:
finiteness
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
h : LipschitzWith K f
x y : α
rw : edist (f x) (f y) / (↑K : ℝ≥0∞) ≤ edist x y
⊢ (↑K : ℝ≥0∞)⁻¹ * edist (f x) (f y) ≤ edist x y

Tactic:
rw [mul_comm, ← div_eq_mul_inv]

Premises used: div_eq_mul_inv, mul_comm
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
h : LipschitzWith K f
x y : α
⊢ edist (f x) (f y) / (↑K : ℝ≥0∞) ≤ edist x y

Tactic:
ENNReal.div_le_of_le_mul' (h x y)

Premises used: ENNReal.div_le_of_le_mul'
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
h : LipschitzWith K f
x y : α
⊢ edist (f x) (f y) / (↑K : ℝ≥0∞) ≤ edist x y

Tactic:
exact ENNReal.div_le_of_le_mul' (h x y)

Premises used: ENNReal.div_le_of_le_mul'
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
h : ∀ (x y : α), edist (f x) (f y) ≤ edist x y
x y : α
⊢ edist (f x) (f y) ≤ (↑1 : ℝ≥0∞) * edist x y

Tactic:
simp only [ENNReal.coe_one, one_mul, h]

Premises used: ENNReal.coe_one, one_mul
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
K' : ℝ≥0
h : K ≤ K'
⊢ LipschitzWith K' f

Tactic:
fun x y => le_trans (hf x y) <| mul_left_mono (ENNReal.coe_le_coe.2 h)

Premises used: Iff.mpr, LipschitzWith, ENNReal.coe_le_coe, mul_left_mono, le_trans
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
s : Set α
h : ∀ x ∈ f '' s, ∀ y ∈ f '' s, edist x y ≤ (↑K : ℝ≥0∞) * ediam s
⊢ ediam (f '' s) ≤ (↑K : ℝ≥0∞) * ediam s

Tactic:
apply Metric.ediam_le

Premises used: Metric.ediam_le
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
s : Set α
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ edist (f x) (f y) ≤ (↑K : ℝ≥0∞) * ediam s

Tactic:
hf.edist_le_mul_of_le (Metric.edist_le_ediam_of_mem hx hy)

Premises used: Metric.edist_le_ediam_of_mem, LipschitzWith.edist_le_mul_of_le
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
s : Set α
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ edist (f x) (f y) ≤ (↑K : ℝ≥0∞) * ediam s

Tactic:
exact hf.edist_le_mul_of_le (Metric.edist_le_ediam_of_mem hx hy)

Premises used: Metric.edist_le_ediam_of_mem, LipschitzWith.edist_le_mul_of_le
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
x y : α
d : ℝ≥0∞
h : edist x y < d / (↑K : ℝ≥0∞)
⊢ edist (f x) (f y) < d

Tactic:
calc
    edist (f x) (f y) ≤ K * edist x y := hf x y
    _ < d := ENNReal.mul_lt_of_lt_div' h

Premises used: Trans.trans, ENNReal.mul_lt_of_lt_div'
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
⊢ UniformContinuous f

Tactic:
EMetric.uniformContinuous_iff.2 fun ε εpos =>
    ⟨ε / K, ENNReal.div_pos_iff.2 ⟨ne_of_gt εpos, ENNReal.coe_ne_top⟩, hf.edist_lt_of_edist_lt_div⟩

Premises used: Iff.mpr, LipschitzWith.edist_lt_of_edist_lt_div, ENNReal.ofNNReal, ENNReal.div_pos_iff, EMetric.uniformContinuous_iff, ne_of_gt, HDiv.hDiv, And.intro, Exists.intro, ENNReal.coe_ne_top
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    f

Tactic:
hf.uniformContinuous.continuous

Premises used: LipschitzWith.uniformContinuous, UniformContinuous.continuous
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
b : β
x y : α
⊢ edist.{v} (α := β) ((fun (x : α) ↦ b) x) ((fun (x : α) ↦ b) y) ≤ (↑0 : ℝ≥0∞) * edist x y

Tactic:
simp only [edist_self, zero_le]

Premises used: zero_le, PseudoEMetricSpace.edist_self
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
b : β
K : ℝ≥0
x y : α
⊢ edist.{v} (α := β) ((fun (x : α) ↦ b) x) ((fun (x : α) ↦ b) y) ≤ (↑K : ℝ≥0∞) * edist x y

Tactic:
simp only [edist_self, zero_le]

Premises used: zero_le, PseudoEMetricSpace.edist_self
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
β : Type u_1
inst_1 : EMetricSpace β
f : α → β
⊢ LipschitzWith 0 f ↔ ∀ (x y : α), f x = f y

Tactic:
simp [LipschitzWith]

Premises used: LipschitzWith
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
⊢ LipschitzWith.{u, u} (α := α) 1 id

Tactic:
LipschitzWith.of_edist_le fun _ _ => le_rfl

Premises used: le_rfl, LipschitzWith.of_edist_le
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
⊢ LipschitzWith.{u, u} (α := { x : α // x ∈ s }) 1 (Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
LipschitzWith.of_edist_le fun _ _ => le_rfl

Premises used: le_rfl, LipschitzWith.of_edist_le
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
p : β → Prop
hp : ∀ (x : α), p (f x)
⊢ LipschitzWith.{u, v} (β := { y : β // p y }) K fun (x : α) ↦ Subtype.mk (p := fun (y : β) ↦ p y) (f x) ⋯

Tactic:
hf

Premises used: LipschitzWith
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
ι : Type x
α : ι → Type u
inst : (i : ι) → PseudoEMetricSpace (α i)
inst_1 : Fintype ι
i : ι
f g : (x : ι) → α x
⊢ edist (f i) (g i) ≤ edist f g

Tactic:
edist_le_pi_edist f g i

Premises used: edist_le_pi_edist
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
ι : Type x
α : ι → Type u
inst : (i : ι) → PseudoEMetricSpace (α i)
inst_1 : Fintype ι
i : ι
f g : (x : ι) → α x
⊢ edist (eval (β := α) i f) (eval (β := α) i g) ≤ edist f g

Tactic:
convert! edist_le_pi_edist f g i

Premises used: edist_le_pi_edist
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
s : Set α
⊢ LipschitzWith K (s.restrict (π := fun (a : α) ↦ β) f)

Tactic:
fun x y => hf x y

Premises used: LipschitzWith, Set.restrict, Subtype.val
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
Kf Kg : ℝ≥0
f : β → γ
g : α → β
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
x y : α
rw : (↑Kf : ℝ≥0∞) * (↑Kg : ℝ≥0∞) * edist x y = (↑(Kf * Kg) : ℝ≥0∞) * edist x y
rw₁ rw₂ : (↑Kf : ℝ≥0∞) * (↑Kg : ℝ≥0∞) * edist x y = (↑Kf : ℝ≥0∞) * (↑Kg : ℝ≥0∞) * edist x y
⊢ (↑Kf : ℝ≥0∞) * ((↑Kg : ℝ≥0∞) * edist x y) = (↑(Kf * Kg) : ℝ≥0∞) * edist x y

Tactic:
rw [← mul_assoc, ENNReal.coe_mul]

Premises used: mul_assoc, ENNReal.coe_mul
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
Kf Kg : ℝ≥0
f : β → γ
g : α → β
s : Set α
hf : LipschitzWith Kf f
hg : LipschitzOnWith Kg g s
⊢ LipschitzOnWith (Kf * Kg) (f ∘ g) s

Tactic:
lipschitzOnWith_iff_restrict.mpr <| hf.comp hg.to_restrict

Premises used: Iff.mpr, lipschitzOnWith_iff_restrict, LipschitzWith.comp, LipschitzOnWith.to_restrict
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
⊢ LipschitzWith (α := α × β) 1 Prod.fst

Tactic:
LipschitzWith.of_edist_le fun _ _ => le_max_left _ _

Premises used: LipschitzWith.of_edist_le, Prod.fst, EDist.edist, le_max_left, Prod.snd
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
⊢ LipschitzWith (α := α × β) 1 Prod.snd

Tactic:
LipschitzWith.of_edist_le fun _ _ => le_max_right _ _

Premises used: le_max_right, LipschitzWith.of_edist_le, Prod.fst, EDist.edist, Prod.snd
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α → β
Kf : ℝ≥0
hf : LipschitzWith Kf f
g : α → γ
Kg : ℝ≥0
hg : LipschitzWith Kg g
x y : α
rw :
  max (edist.{v} (α := β) ((fun (x : α) ↦ (f x, g x)) x).1 ((fun (x : α) ↦ (f x, g x)) y).1)
      (edist.{w} (α := γ) ((fun (x : α) ↦ (f x, g x)) x).2 ((fun (x : α) ↦ (f x, g x)) y).2) ≤
    max ((↑Kf : ℝ≥0∞) * edist x y) ((↑Kg : ℝ≥0∞) * edist x y)
⊢ edist (α := β × γ) ((fun (x : α) ↦ (f x, g x)) x) ((fun (x : α) ↦ (f x, g x)) y) ≤ (↑(max Kf Kg) : ℝ≥0∞) * edist x y

Tactic:
rw [ENNReal.coe_mono.map_max, Prod.edist_eq, max_mul]

Premises used: Prod.edist_eq, Monotone.map_max, max_mul, ENNReal.coe_mono
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α → β
Kf : ℝ≥0
hf : LipschitzWith Kf f
g : α → γ
Kg : ℝ≥0
hg : LipschitzWith Kg g
x y : α
⊢ max (edist.{v} (α := β) ((fun (x : α) ↦ (f x, g x)) x).1 ((fun (x : α) ↦ (f x, g x)) y).1)
      (edist.{w} (α := γ) ((fun (x : α) ↦ (f x, g x)) x).2 ((fun (x : α) ↦ (f x, g x)) y).2) ≤
    max ((↑Kf : ℝ≥0∞) * edist x y) ((↑Kg : ℝ≥0∞) * edist x y)

Tactic:
max_le_max (hf x y) (hg x y)

Premises used: max_le_max
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α → β
Kf : ℝ≥0
hf : LipschitzWith Kf f
g : α → γ
Kg : ℝ≥0
hg : LipschitzWith Kg g
x y : α
⊢ max (edist.{v} (α := β) ((fun (x : α) ↦ (f x, g x)) x).1 ((fun (x : α) ↦ (f x, g x)) y).1)
      (edist.{w} (α := γ) ((fun (x : α) ↦ (f x, g x)) x).2 ((fun (x : α) ↦ (f x, g x)) y).2) ≤
    max ((↑Kf : ℝ≥0∞) * edist x y) ((↑Kg : ℝ≥0∞) * edist x y)

Tactic:
exact max_le_max (hf x y) (hg x y)

Premises used: max_le_max
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
a : α
⊢ LipschitzWith (α := β) 1 (Prod.mk a)

Tactic:
simpa only [max_eq_right zero_le_one] using (LipschitzWith.const a).prodMk LipschitzWith.id

Premises used: LipschitzWith.id, LipschitzWith.prodMk, zero_le_one, max_eq_right, LipschitzWith.const
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
b : β
⊢ LipschitzWith (β := α × β) 1 fun (a : α) ↦ (a, b)

Tactic:
simpa only [max_eq_left zero_le_one] using LipschitzWith.id.prodMk (LipschitzWith.const b)

Premises used: LipschitzWith.id, LipschitzWith.prodMk, max_eq_left, zero_le_one, LipschitzWith.const
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith.{u, w} (β := γ) Kα fun (a : α) ↦ f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
simp : edist (f a₁ b₁) (f a₂ b₂) ≤ (↑Kα : ℝ≥0∞) * edist (a₁, b₁) (a₂, b₂) + (↑Kβ : ℝ≥0∞) * edist (a₁, b₁) (a₂, b₂)
⊢ edist (uncurry f (a₁, b₁)) (uncurry f (a₂, b₂)) ≤ (↑(Kα + Kβ) : ℝ≥0∞) * edist (a₁, b₁) (a₂, b₂)

Tactic:
simp only [Function.uncurry, ENNReal.coe_add, add_mul]

Premises used: add_mul, ENNReal.coe_add, Function.uncurry
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith.{u, w} (β := γ) Kα fun (a : α) ↦ f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
apply :
  edist (f a₁ b₁) (f a₂ b₁) + edist (f a₂ b₁) (f a₂ b₂) ≤
    (↑Kα : ℝ≥0∞) * edist (a₁, b₁) (a₂, b₂) + (↑Kβ : ℝ≥0∞) * edist (a₁, b₁) (a₂, b₂)
⊢ edist (f a₁ b₁) (f a₂ b₂) ≤ (↑Kα : ℝ≥0∞) * edist (a₁, b₁) (a₂, b₂) + (↑Kβ : ℝ≥0∞) * edist (a₁, b₁) (a₂, b₂)

Tactic:
apply le_trans (edist_triangle _ (f a₂ b₁) _)

Premises used: le_trans, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith.{u, w} (β := γ) Kα fun (a : α) ↦ f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ edist (f a₁ b₁) (f a₂ b₁) + edist (f a₂ b₁) (f a₂ b₂) ≤
    (↑Kα : ℝ≥0∞) * edist (a₁, b₁) (a₂, b₂) + (↑Kβ : ℝ≥0∞) * edist (a₁, b₁) (a₂, b₂)

Tactic:
add_le_add (le_trans (hα _ _ _) <| mul_right_mono <| le_max_left _ _)
      (le_trans (hβ _ _ _) <| mul_right_mono <| le_max_right _ _)

Premises used: le_max_right, add_le_add, mul_right_mono, le_max_left, le_trans
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith.{u, w} (β := γ) Kα fun (a : α) ↦ f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ edist (f a₁ b₁) (f a₂ b₁) + edist (f a₂ b₁) (f a₂ b₂) ≤
    (↑Kα : ℝ≥0∞) * edist (a₁, b₁) (a₂, b₂) + (↑Kβ : ℝ≥0∞) * edist (a₁, b₁) (a₂, b₂)

Tactic:
exact
    add_le_add (le_trans (hα _ _ _) <| mul_right_mono <| le_max_left _ _)
      (le_trans (hβ _ _ _) <| mul_right_mono <| le_max_right _ _)

Premises used: le_max_right, add_le_add, mul_right_mono, le_max_left, le_trans
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
⊢ LipschitzWith (HPow.hPow (β := ℕ) K 0) f^[0]

Tactic:
simpa only [pow_zero] using LipschitzWith.id

Premises used: LipschitzWith.id, pow_zero