awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
n : ℕ
rw : LipschitzWith (K ^ n * K) f^[n + 1]
⊢ LipschitzWith (K ^ (n + 1)) f^[n + 1]

Tactic:
rw [pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ n * K) f^[n + 1]

Tactic:
(LipschitzWith.iterate hf n).comp hf

Premises used: Nat.iterate, LipschitzWith.comp
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ n * K) f^[n + 1]

Tactic:
exact (LipschitzWith.iterate hf n).comp hf

Premises used: LipschitzWith.comp
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
rw : edist (f^[n] x) ((f^[n] ∘ f) x) ≤ (↑K : ℝ≥0∞) ^ n * edist x (f x)
⊢ edist (f^[n] x) (f^[n + 1] x) ≤ edist x (f x) * (↑K : ℝ≥0∞) ^ n

Tactic:
rw [iterate_succ, mul_comm]

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

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

Premises used: LipschitzWith.iterate, ENNReal.coe_pow
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f g : Function.End α
Kf Kg : ℝ≥0
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
⊢ LipschitzWith (Kf * Kg) (f * g)

Tactic:
hf.comp hg

Premises used: LipschitzWith.comp
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
ι : Type x
inst : PseudoEMetricSpace α
f : ι → Function.End α
K : ι → ℝ≥0
h : ∀ (i : ι), LipschitzWith (K i) (f i)
⊢ LipschitzWith (List.map K []).prod (List.map f []).prod

Tactic:
simpa using LipschitzWith.id

Premises used: LipschitzWith.id
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
ι : Type x
inst : PseudoEMetricSpace α
f : ι → Function.End α
K : ι → ℝ≥0
h : ∀ (i : ι), LipschitzWith (K i) (f i)
i : ι
l : List ι
simp : LipschitzWith (K i * (List.map K l).prod) (f i * (List.map f l).prod)
⊢ LipschitzWith (List.map K (i :: l)).prod (List.map f (i :: l)).prod

Tactic:
simp only [List.map_cons, List.prod_cons]

Premises used: List.map_cons, List.prod_cons
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
ι : Type x
inst : PseudoEMetricSpace α
f : ι → Function.End α
K : ι → ℝ≥0
h : ∀ (i : ι), LipschitzWith (K i) (f i)
i : ι
l : List ι
⊢ LipschitzWith (K i * (List.map K l).prod) (f i * (List.map f l).prod)

Tactic:
(h i).mul_end (LipschitzWith.list_prod f K h l)

Premises used: LipschitzWith.mul_end
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
ι : Type x
inst : PseudoEMetricSpace α
f : ι → Function.End α
K : ι → ℝ≥0
h : ∀ (i : ι), LipschitzWith (K i) (f i)
i : ι
l : List ι
⊢ LipschitzWith (K i * (List.map K l).prod) (f i * (List.map f l).prod)

Tactic:
exact (h i).mul_end (LipschitzWith.list_prod f K h l)

Premises used: LipschitzWith.mul_end
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : Function.End α
K : ℝ≥0
h : LipschitzWith K f
⊢ LipschitzWith (HPow.hPow (β := ℕ) K 0) (HPow.hPow (β := ℕ) f 0)

Tactic:
simpa only [pow_zero] using LipschitzWith.id

Premises used: LipschitzWith.id, pow_zero
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : Function.End α
K : ℝ≥0
h : LipschitzWith K f
n : ℕ
rw : LipschitzWith (K ^ n * K) (f ^ n * f)
⊢ LipschitzWith (K ^ (n + 1)) (f ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ]

Premises used: pow_succ
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : Function.End α
K : ℝ≥0
h : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ n * K) (f ^ n * f)

Tactic:
(LipschitzWith.pow_end h n).mul_end h

Premises used: LipschitzWith.mul_end
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : Function.End α
K : ℝ≥0
h : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ n * K) (f ^ n * f)

Tactic:
exact (LipschitzWith.pow_end h n).mul_end h

Premises used: LipschitzWith.mul_end
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
β : Type u_1
inst_1 : EMetricSpace β
f : α → β
⊢ LipschitzOnWith 0 f s ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y

Tactic:
simp [LipschitzOnWith]

Premises used: LipschitzOnWith
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
⊢ UniformContinuousOn f s

Tactic:
uniformContinuousOn_iff_restrict.mpr hf.to_restrict.uniformContinuous

Premises used: Iff.mpr, uniformContinuousOn_iff_restrict, LipschitzWith.uniformContinuous, LipschitzOnWith.to_restrict
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
⊢ ContinuousOn f s

Tactic:
hf.uniformContinuousOn.continuousOn

Premises used: UniformContinuousOn.continuousOn, LipschitzOnWith.uniformContinuousOn
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
K' : ℝ≥0
h : K ≤ K'
⊢ LipschitzOnWith K' f s

Tactic:
fun _ hx _ hy => (hf hx hy).trans <| mul_left_mono (ENNReal.coe_le_coe.2 h)

Premises used: Iff.mpr, ENNReal.coe_le_coe, mul_left_mono, LipschitzOnWith, LE.le.trans
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
h : LipschitzOnWith K f s
x y : α
hx : x ∈ s
hy : y ∈ s
r : ℝ≥0∞
hr : edist x y ≤ r
⊢ edist (f x) (f y) ≤ (↑K : ℝ≥0∞) * r

Tactic:
(h hx hy).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
s : Set α
f : α → β
hf : LipschitzOnWith K f s
x y : α
hx : x ∈ s
hy : y ∈ s
d : ℝ≥0∞
hd : edist x y < d / (↑K : ℝ≥0∞)
⊢ edist (f x) (f y) < d

Tactic:
hf.to_restrict.edist_lt_of_edist_lt_div <| show edist (⟨x, hx⟩ : s) ⟨y, hy⟩ < d / K from hd

Premises used: LipschitzWith.edist_lt_of_edist_lt_div, LipschitzOnWith.to_restrict, Set.restrict
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
K : ℝ≥0
s : Set α
f : α → β
g : β → γ
t : Set β
Kg : ℝ≥0
hg : LipschitzOnWith Kg g t
hf : LipschitzOnWith K f s
hmaps : MapsTo f s t
⊢ LipschitzOnWith (Kg * K) (g ∘ f) s

Tactic:
lipschitzOnWith_iff_restrict.mpr <| hg.to_restrict.comp (hf.mapsToRestrict hmaps)

Premises used: Iff.mpr, LipschitzOnWith.mapsToRestrict, lipschitzOnWith_iff_restrict, LipschitzWith.comp, LipschitzOnWith.to_restrict
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
s : Set α
f : α → β
g : α → γ
Kf Kg : ℝ≥0
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
x : α
hx : x ∈ s
_ :
  ∀ ⦃y : α⦄,
    y ∈ s →
      edist (α := β × γ) ((fun (x : α) ↦ (f x, g x)) x) ((fun (x : α) ↦ (f x, g x)) y) ≤
        (↑(max Kf Kg) : ℝ≥0∞) * edist x y
⊢ ∀ ⦃y : α⦄,
    y ∈ s →
      edist (α := β × γ) ((fun (x : α) ↦ (f x, g x)) x) ((fun (x : α) ↦ (f x, g x)) y) ≤
        (↑(max Kf Kg) : ℝ≥0∞) * edist x y

Tactic:
_
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
s : Set α
f : α → β
g : α → γ
Kf Kg : ℝ≥0
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
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 γ
s : Set α
f : α → β
g : α → γ
Kf Kg : ℝ≥0
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ 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 hx hy) (hg hx hy)

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 γ
s : Set α
f : α → β
g : α → γ
Kf Kg : ℝ≥0
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ 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 hx hy) (hg hx hy)

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 : α → β → γ
K₁ K₂ : ℝ≥0
s : Set α
t : Set β
hf₁ : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K₁ (fun (x : α) ↦ f x b) s
hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t
simp :
  ∀ x ∈ s,
    ∀ y ∈ t,
      ∀ x_1 ∈ s, ∀ y_1 ∈ t, edist (f x y) (f x_1 y_1) ≤ (↑K₁ : ℝ≥0∞) * Metric.ediam s + (↑K₂ : ℝ≥0∞) * Metric.ediam t
⊢ Metric.ediam (image2 f s t) ≤ (↑K₁ : ℝ≥0∞) * Metric.ediam s + (↑K₂ : ℝ≥0∞) * Metric.ediam t

Tactic:
simp only [Metric.ediam_le_iff, forall_mem_image2]

Premises used: Set.forall_mem_image2, Metric.ediam_le_iff
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α → β → γ
K₁ K₂ : ℝ≥0
s : Set α
t : Set β
hf₁ : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K₁ (fun (x : α) ↦ f x b) s
hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t
a₁ : α
ha₁ : a₁ ∈ s
b₁ : β
hb₁ : b₁ ∈ t
a₂ : α
ha₂ : a₂ ∈ s
b₂ : β
hb₂ : b₂ ∈ t
⊢ edist (f a₁ b₁) (f a₂ b₂) ≤ (↑K₁ : ℝ≥0∞) * Metric.ediam s + (↑K₂ : ℝ≥0∞) * Metric.ediam t

Tactic:
(edist_triangle _ (f a₂ b₁) _).trans ?_

Premises used: LE.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
s : Set α
t : Set β
hf₁ : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K₁ (fun (x : α) ↦ f x b) s
hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t
a₁ : α
ha₁ : a₁ ∈ s
b₁ : β
hb₁ : b₁ ∈ t
a₂ : α
ha₂ : a₂ ∈ s
b₂ : β
hb₂ : b₂ ∈ t
refine :
  edist (f a₁ b₁) (f a₂ b₁) + edist (f a₂ b₁) (f a₂ b₂) ≤ (↑K₁ : ℝ≥0∞) * Metric.ediam s + (↑K₂ : ℝ≥0∞) * Metric.ediam t
⊢ edist (f a₁ b₁) (f a₂ b₂) ≤ (↑K₁ : ℝ≥0∞) * Metric.ediam s + (↑K₂ : ℝ≥0∞) * Metric.ediam t

Tactic:
refine (edist_triangle _ (f a₂ b₁) _).trans ?_

Premises used: LE.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
s : Set α
t : Set β
hf₁ : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K₁ (fun (x : α) ↦ f x b) s
hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t
a₁ : α
ha₁ : a₁ ∈ s
b₁ : β
hb₁ : b₁ ∈ t
a₂ : α
ha₂ : a₂ ∈ s
b₂ : β
hb₂ : b₂ ∈ t
⊢ edist (f a₁ b₁) (f a₂ b₁) + edist (f a₂ b₁) (f a₂ b₂) ≤ (↑K₁ : ℝ≥0∞) * Metric.ediam s + (↑K₂ : ℝ≥0∞) * Metric.ediam t

Tactic:
add_le_add
      ((hf₁ b₁ hb₁ ha₁ ha₂).trans <| mul_right_mono <| Metric.edist_le_ediam_of_mem ha₁ ha₂)
      ((hf₂ a₂ ha₂ hb₁ hb₂).trans <| mul_right_mono <| Metric.edist_le_ediam_of_mem hb₁ hb₂)

Premises used: add_le_add, mul_right_mono, Metric.edist_le_ediam_of_mem, LE.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
s : Set α
t : Set β
hf₁ : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K₁ (fun (x : α) ↦ f x b) s
hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t
a₁ : α
ha₁ : a₁ ∈ s
b₁ : β
hb₁ : b₁ ∈ t
a₂ : α
ha₂ : a₂ ∈ s
b₂ : β
hb₂ : b₂ ∈ t
⊢ edist (f a₁ b₁) (f a₂ b₁) + edist (f a₂ b₁) (f a₂ b₂) ≤ (↑K₁ : ℝ≥0∞) * Metric.ediam s + (↑K₂ : ℝ≥0∞) * Metric.ediam t

Tactic:
exact
    add_le_add
      ((hf₁ b₁ hb₁ ha₁ ha₂).trans <| mul_right_mono <| Metric.edist_le_ediam_of_mem ha₁ ha₂)
      ((hf₂ a₂ ha₂ hb₁ hb₂).trans <| mul_right_mono <| Metric.edist_le_ediam_of_mem hb₁ hb₂)

Premises used: add_le_add, mul_right_mono, Metric.edist_le_ediam_of_mem, LE.le.trans
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
K : ℝ≥0
hf : LipschitzWith K f
⊢ LocallyLipschitz f

Tactic:
fun _ ↦ ⟨K, univ, Filter.univ_mem, lipschitzOnWith_univ.mpr hf⟩

Premises used: Iff.mpr, Set.univ, LocallyLipschitz, And.intro, lipschitzOnWith_univ, Exists.intro, Filter.univ_mem
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
⊢ LocallyLipschitz.{u, u} (α := α) id

Tactic:
LipschitzWith.id.locallyLipschitz

Premises used: LipschitzWith.id, LipschitzWith.locallyLipschitz
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
b : β
⊢ LocallyLipschitz.{u, v} (β := β) fun (x : α) ↦ b

Tactic:
(LipschitzWith.const b).locallyLipschitz

Premises used: LipschitzWith.locallyLipschitz, LipschitzWith.const
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : LocallyLipschitz f
rw : ∀ (x : α), ContinuousAt f x
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    f

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : LocallyLipschitz f
x : α
rcases : ∀ (K : ℝ≥0) (t : Set α) (ht : t ∈ 𝓝 x) (hK : LipschitzOnWith K f t), ContinuousAt f x
⊢ ContinuousAt f x

Tactic:
rcases (hf x) with ⟨K, t, ht, hK⟩
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : LocallyLipschitz f
x : α
K : ℝ≥0
t : Set α
ht : t ∈ 𝓝 x
hK : LipschitzOnWith K f t
⊢ ContinuousAt f x

Tactic:
(hK.continuousOn).continuousAt ht

Premises used: LipschitzOnWith.continuousOn, ContinuousOn.continuousAt
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : LocallyLipschitz f
x : α
K : ℝ≥0
t : Set α
ht : t ∈ 𝓝 x
hK : LipschitzOnWith K f t
⊢ ContinuousAt f x

Tactic:
exact (hK.continuousOn).continuousAt ht

Premises used: LipschitzOnWith.continuousOn, ContinuousOn.continuousAt
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : β → γ
g : α → β
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : α
rcases :
  ∀ (Kg : ℝ≥0) (t : Set α) (ht : t ∈ 𝓝 x) (hgL : LipschitzOnWith Kg g t),
    ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith K (f ∘ g) t
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith K (f ∘ g) t

Tactic:
rcases hg x with ⟨Kg, t, ht, hgL⟩
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : β → γ
g : α → β
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : α
Kg : ℝ≥0
t : Set α
ht : t ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t
rcases :
  ∀ (Kf : ℝ≥0) (u : Set β) (hu : u ∈ 𝓝 (g x)) (hfL : LipschitzOnWith Kf f u),
    ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith K (f ∘ g) t
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith K (f ∘ g) t

Tactic:
rcases hf (g x) with ⟨Kf, u, hu, hfL⟩
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : β → γ
g : α → β
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : α
Kg : ℝ≥0
t : Set α
ht : t ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t
Kf : ℝ≥0
u : Set β
hu : u ∈ 𝓝 (g x)
hfL : LipschitzOnWith Kf f u
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith K (f ∘ g) t

Tactic:
⟨Kf * Kg, t ∩ g⁻¹' u, inter_mem ht (hg.continuous.continuousAt hu), ?_⟩

Premises used: HMul.hMul, Filter.inter_mem, Inter.inter, Continuous.continuousAt, LocallyLipschitz.continuous, Set.preimage, And.intro, Exists.intro
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : β → γ
g : α → β
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : α
Kg : ℝ≥0
t : Set α
ht : t ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t
Kf : ℝ≥0
u : Set β
hu : u ∈ 𝓝 (g x)
hfL : LipschitzOnWith Kf f u
refine : LipschitzOnWith (Kf * Kg) (f ∘ g) (t ∩ g ⁻¹' u)
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith K (f ∘ g) t

Tactic:
refine ⟨Kf * Kg, t ∩ g⁻¹' u, inter_mem ht (hg.continuous.continuousAt hu), ?_⟩
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : β → γ
g : α → β
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : α
Kg : ℝ≥0
t : Set α
ht : t ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t
Kf : ℝ≥0
u : Set β
hu : u ∈ 𝓝 (g x)
hfL : LipschitzOnWith Kf f u
⊢ LipschitzOnWith (Kf * Kg) (f ∘ g) (t ∩ g ⁻¹' u)

Tactic:
hfL.comp (hgL.mono inter_subset_left)
    ((mapsTo_preimage g u).mono_left inter_subset_right)

Premises used: LipschitzOnWith.mono, Set.inter_subset_left, Set.mapsTo_preimage, Set.MapsTo.mono_left, LipschitzOnWith.comp, Set.inter_subset_right
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : β → γ
g : α → β
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : α
Kg : ℝ≥0
t : Set α
ht : t ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t
Kf : ℝ≥0
u : Set β
hu : u ∈ 𝓝 (g x)
hfL : LipschitzOnWith Kf f u
⊢ LipschitzOnWith (Kf * Kg) (f ∘ g) (t ∩ g ⁻¹' u)

Tactic:
exact hfL.comp (hgL.mono inter_subset_left)
    ((mapsTo_preimage g u).mono_left inter_subset_right)

Premises used: LipschitzOnWith.mono, Set.inter_subset_left, Set.mapsTo_preimage, Set.MapsTo.mono_left, LipschitzOnWith.comp, Set.inter_subset_right
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
x : α
rcases :
  ∀ (Kf : ℝ≥0) (t₁ : Set α) (h₁t : t₁ ∈ 𝓝 x) (hfL : LipschitzOnWith Kf f t₁),
    ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith (β := β × γ) K (fun (x : α) ↦ (f x, g x)) t
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith (β := β × γ) K (fun (x : α) ↦ (f x, g x)) t

Tactic:
rcases hf x with ⟨Kf, t₁, h₁t, hfL⟩
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
x : α
Kf : ℝ≥0
t₁ : Set α
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
rcases :
  ∀ (Kg : ℝ≥0) (t₂ : Set α) (h₂t : t₂ ∈ 𝓝 x) (hgL : LipschitzOnWith Kg g t₂),
    ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith (β := β × γ) K (fun (x : α) ↦ (f x, g x)) t
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith (β := β × γ) K (fun (x : α) ↦ (f x, g x)) t

Tactic:
rcases hg x with ⟨Kg, t₂, h₂t, hgL⟩
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
x : α
Kf : ℝ≥0
t₁ : Set α
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set α
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith (β := β × γ) K (fun (x : α) ↦ (f x, g x)) t

Tactic:
⟨max Kf Kg, t₁ ∩ t₂, Filter.inter_mem h₁t h₂t, ?_⟩

Premises used: Filter.inter_mem, Inter.inter, Max.max, And.intro, Exists.intro
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
x : α
Kf : ℝ≥0
t₁ : Set α
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set α
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
refine : LipschitzOnWith (β := β × γ) (max Kf Kg) (fun (x : α) ↦ (f x, g x)) (t₁ ∩ t₂)
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith (β := β × γ) K (fun (x : α) ↦ (f x, g x)) t

Tactic:
refine ⟨max Kf Kg, t₁ ∩ t₂, Filter.inter_mem h₁t h₂t, ?_⟩
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
x : α
Kf : ℝ≥0
t₁ : Set α
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set α
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
⊢ LipschitzOnWith (β := β × γ) (max Kf Kg) (fun (x : α) ↦ (f x, g x)) (t₁ ∩ t₂)

Tactic:
(hfL.mono inter_subset_left).prodMk (hgL.mono inter_subset_right)

Premises used: LipschitzOnWith.mono, LipschitzOnWith.prodMk, Set.inter_subset_left, Set.inter_subset_right
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
x : α
Kf : ℝ≥0
t₁ : Set α
h₁t : t₁ ∈ 𝓝 x
hfL : LipschitzOnWith Kf f t₁
Kg : ℝ≥0
t₂ : Set α
h₂t : t₂ ∈ 𝓝 x
hgL : LipschitzOnWith Kg g t₂
⊢ LipschitzOnWith (β := β × γ) (max Kf Kg) (fun (x : α) ↦ (f x, g x)) (t₁ ∩ t₂)

Tactic:
exact (hfL.mono inter_subset_left).prodMk (hgL.mono inter_subset_right)

Premises used: LipschitzOnWith.mono, LipschitzOnWith.prodMk, Set.inter_subset_left, Set.inter_subset_right
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
a : α
⊢ LocallyLipschitz (α := β) (Prod.mk a)

Tactic:
(LipschitzWith.prodMk_left a).locallyLipschitz

Premises used: LipschitzWith.locallyLipschitz, LipschitzWith.prodMk_left
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
b : β
⊢ LocallyLipschitz (β := α × β) fun (a : α) ↦ (a, b)

Tactic:
(LipschitzWith.prodMk_right b).locallyLipschitz

Premises used: LipschitzWith.prodMk_right, LipschitzWith.locallyLipschitz