awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : α → α
hf : LocallyLipschitz f
⊢ LocallyLipschitz f^[0]

Tactic:
simpa only [pow_zero] using LocallyLipschitz.id

Premises used: LocallyLipschitz.id, pow_zero
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : α → α
hf : LocallyLipschitz f
n : ℕ
rw : LocallyLipschitz (f^[n] ∘ f)
⊢ LocallyLipschitz f^[n + 1]

Tactic:
rw [iterate_add, iterate_one]

Premises used: Function.iterate_add, Function.iterate_one
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : α → α
hf : LocallyLipschitz f
n : ℕ
⊢ LocallyLipschitz (f^[n] ∘ f)

Tactic:
(hf.iterate n).comp hf

Premises used: LocallyLipschitz.comp
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : α → α
hf : LocallyLipschitz f
n : ℕ
⊢ LocallyLipschitz (f^[n] ∘ f)

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

Premises used: LocallyLipschitz.comp
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
inst : PseudoEMetricSpace α
f g : Function.End α
hf : LocallyLipschitz f
hg : LocallyLipschitz g
⊢ LocallyLipschitz (f * g)

Tactic:
hf.comp hg

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

Tactic:
simpa only [pow_zero] using LocallyLipschitz.id

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

Tactic:
rw [pow_succ]

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

Tactic:
(h.pow_end n).mul_end h

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

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

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

Tactic:
continuousOn_iff_continuous_restrict.2 hf.restrict.continuous

Premises used: Iff.mpr, LocallyLipschitzOn.restrict, LocallyLipschitz.continuous, continuousOn_iff_continuous_restrict
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
⊢ ContinuousWithinAt f (s ×ˢ t) (x, y)

Tactic:
Metric.nhds_basis_closedEBall.tendsto_right_iff.2 fun ε (ε0 : 0 < ε) => ?_

Premises used: Iff.mpr, ContinuousWithinAt, Metric.nhds_basis_closedEBall, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
refine : ∀ (ε : ℝ≥0∞) (ε0 : 0 < ε), ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ Metric.closedEBall (f (x, y)) ε
⊢ ContinuousWithinAt f (s ×ˢ t) (x, y)

Tactic:
refine Metric.nhds_basis_closedEBall.tendsto_right_iff.2 fun ε (ε0 : 0 < ε) => ?_

Premises used: Iff.mpr, Metric.nhds_basis_closedEBall, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε
⊢ 0 < ε / 2

Tactic:
replace ε0 : 0 < ε / 2 := ENNReal.half_pos ε0.ne'
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
⊢ ∃ (δ : ℝ≥0), 0 < δ ∧ (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2

Tactic:
ENNReal.exists_nnreal_pos_mul_lt ENNReal.coe_ne_top ε0.ne'

Premises used: ENNReal.exists_nnreal_pos_mul_lt, LT.lt.ne', ENNReal.coe_ne_top
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
obtain :
  ∀ (δ : ℝ≥0) (δpos : 0 < δ) (hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2),
    ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ Metric.closedEBall (f (x, y)) ε
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ Metric.closedEBall (f (x, y)) ε

Tactic:
obtain ⟨δ, δpos, hδ⟩ : ∃ δ : ℝ≥0, 0 < δ ∧ (δ : ℝ≥0∞) * ↑(3 * K) < ε / 2 :=
    ENNReal.exists_nnreal_pos_mul_lt ENNReal.coe_ne_top ε0.ne'

Premises used: ENNReal.exists_nnreal_pos_mul_lt, HMul.hMul, LT.lt.ne', OfNat.ofNat, ENNReal.coe_ne_top
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < δ
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
⊢ 0 < (↑δ : ℝ≥0∞)

Tactic:
rw [← ENNReal.coe_pos] at δpos

Premises used: ENNReal.coe_pos
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < δ
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
δpos₁ : 0 < (↑δ : ℝ≥0∞)
⊢ (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2

Tactic:
rw [← ENNReal.coe_pos] at δpos

Premises used: ENNReal.coe_pos
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < (↑δ : ℝ≥0∞)
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
rcases :
  ∀ (x' : α) (hx' : x' ∈ s') (hxx' : edist x x' < (↑δ : ℝ≥0∞)),
    ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ Metric.closedEBall (f (x, y)) ε
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ Metric.closedEBall (f (x, y)) ε

Tactic:
rcases EMetric.mem_closure_iff.1 (hss' hx) δ δpos with ⟨x', hx', hxx'⟩

Premises used: ENNReal.ofNNReal, Iff.mp, EMetric.mem_closure_iff
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < (↑δ : ℝ≥0∞)
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < (↑δ : ℝ≥0∞)
⊢ s ∩ Metric.eball x (↑δ : ℝ≥0∞) ∈ 𝓝[s] x

Tactic:
have A : s ∩ Metric.eball x δ ∈ 𝓝[s] x :=
    inter_mem_nhdsWithin _ (Metric.eball_mem_nhds _ δpos)
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < (↑δ : ℝ≥0∞)
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < (↑δ : ℝ≥0∞)
A : s ∩ Metric.eball x (↑δ : ℝ≥0∞) ∈ 𝓝[s] x
⊢ t ∩ {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y

Tactic:
have B : t ∩ { b | edist (f (x', b)) (f (x', y)) ≤ ε / 2 } ∈ 𝓝[t] y :=
    inter_mem self_mem_nhdsWithin (ha x' hx' y hy (Metric.closedEBall_mem_nhds (f (x', y)) ε0))
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < (↑δ : ℝ≥0∞)
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < (↑δ : ℝ≥0∞)
A : s ∩ Metric.eball x (↑δ : ℝ≥0∞) ∈ 𝓝[s] x
B : t ∩ {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
h :
  ∀ (has : (a, b).1 ∈ s) (hax : (a, b).1 ∈ Metric.eball x (↑δ : ℝ≥0∞)) (hbt : (a, b).2 ∈ t)
    (hby : Membership.mem (γ := Set β) {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} (a, b).2),
    f (a, b) ∈ Metric.closedEBall (f (x, y)) ε
⊢ (a, b) ∈ (s ∩ Metric.eball x (↑δ : ℝ≥0∞)) ×ˢ (t ∩ {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2}) →
    f (a, b) ∈ Metric.closedEBall (f (x, y)) ε

Tactic:
⟨⟨has, hax⟩, ⟨hbt, hby⟩⟩
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < (↑δ : ℝ≥0∞)
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < (↑δ : ℝ≥0∞)
A : s ∩ Metric.eball x (↑δ : ℝ≥0∞) ∈ 𝓝[s] x
B : t ∩ {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
h :
  ∀ (a : α) (b : β) (has : (a, b).1 ∈ s) (hax : (a, b).1 ∈ Metric.eball x (↑δ : ℝ≥0∞)) (hbt : (a, b).2 ∈ t)
    (hby : Membership.mem (γ := Set β) {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} (a, b).2),
    f (a, b) ∈ Metric.closedEBall (f (x, y)) ε
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ Metric.closedEBall (f (x, y)) ε

Tactic:
filter_upwards [nhdsWithin_prod A B] with ⟨a, b⟩ ⟨⟨has, hax⟩, ⟨hbt, hby⟩⟩

Premises used: nhdsWithin_prod
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < (↑δ : ℝ≥0∞)
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < (↑δ : ℝ≥0∞)
A : s ∩ Metric.eball x (↑δ : ℝ≥0∞) ∈ 𝓝[s] x
B : t ∩ {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x (↑δ : ℝ≥0∞)
hbt : (a, b).2 ∈ t
hby : Membership.mem (γ := Set β) {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} (a, b).2
⊢ edist (f (a, b)) (f (x, y)) ≤
    edist (f (a, b)) (f (x', b)) + edist (f (x', b)) (f (x', y)) + edist (f (x', y)) (f (x, y))

Tactic:
edist_triangle4 _ _ _ _

Premises used: edist_triangle4
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < (↑δ : ℝ≥0∞)
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < (↑δ : ℝ≥0∞)
A : s ∩ Metric.eball x (↑δ : ℝ≥0∞) ∈ 𝓝[s] x
B : t ∩ {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x (↑δ : ℝ≥0∞)
hbt : (a, b).2 ∈ t
hby : Membership.mem (γ := Set β) {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} (a, b).2
h₁ : edist (f (a, b)) (f (x', b)) ≤ (↑K : ℝ≥0∞) * ((↑δ : ℝ≥0∞) + (↑δ : ℝ≥0∞))
h₂ : edist (f (x', b)) (f (x', y)) ≤ ε / 2
h₃ : edist (f (x', y)) (f (x, y)) ≤ (↑K : ℝ≥0∞) * (↑δ : ℝ≥0∞)
⊢ edist (f (a, b)) (f (x', b)) + edist (f (x', b)) (f (x', y)) + edist (f (x', y)) (f (x, y)) ≤
    (↑K : ℝ≥0∞) * ((↑δ : ℝ≥0∞) + (↑δ : ℝ≥0∞)) + ε / 2 + (↑K : ℝ≥0∞) * (↑δ : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < (↑δ : ℝ≥0∞)
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < (↑δ : ℝ≥0∞)
A : s ∩ Metric.eball x (↑δ : ℝ≥0∞) ∈ 𝓝[s] x
B : t ∩ {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x (↑δ : ℝ≥0∞)
hbt : (a, b).2 ∈ t
hby : Membership.mem (γ := Set β) {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} (a, b).2
⊢ edist (f (a, b)) (f (x', b)) ≤ (↑K : ℝ≥0∞) * ((↑δ : ℝ≥0∞) + (↑δ : ℝ≥0∞))

Tactic:
(hb b hbt).edist_le_mul_of_le has (hs' hx') ?_

Premises used: LipschitzOnWith.edist_le_mul_of_le
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < (↑δ : ℝ≥0∞)
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < (↑δ : ℝ≥0∞)
A : s ∩ Metric.eball x (↑δ : ℝ≥0∞) ∈ 𝓝[s] x
B : t ∩ {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x (↑δ : ℝ≥0∞)
hbt : (a, b).2 ∈ t
hby : Membership.mem (γ := Set β) {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} (a, b).2
h₁ : edist (a, b).1 x' ≤ (↑δ : ℝ≥0∞) + (↑δ : ℝ≥0∞)
⊢ edist (f (a, b)) (f (x', b)) ≤ (↑K : ℝ≥0∞) * ((↑δ : ℝ≥0∞) + (↑δ : ℝ≥0∞))

Tactic:
refine (hb b hbt).edist_le_mul_of_le has (hs' hx') ?_

Premises used: LipschitzOnWith.edist_le_mul_of_le
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < (↑δ : ℝ≥0∞)
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < (↑δ : ℝ≥0∞)
A : s ∩ Metric.eball x (↑δ : ℝ≥0∞) ∈ 𝓝[s] x
B : t ∩ {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x (↑δ : ℝ≥0∞)
hbt : (a, b).2 ∈ t
hby : Membership.mem (γ := Set β) {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} (a, b).2
⊢ edist (a, b).1 x' ≤ (↑δ : ℝ≥0∞) + (↑δ : ℝ≥0∞)

Tactic:
(edist_triangle _ _ _).trans (add_le_add (le_of_lt hax) hxx'.le)

Premises used: add_le_add, le_of_lt, LT.lt.le, LE.le.trans, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < (↑δ : ℝ≥0∞)
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < (↑δ : ℝ≥0∞)
A : s ∩ Metric.eball x (↑δ : ℝ≥0∞) ∈ 𝓝[s] x
B : t ∩ {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x (↑δ : ℝ≥0∞)
hbt : (a, b).2 ∈ t
hby : Membership.mem (γ := Set β) {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} (a, b).2
⊢ edist (a, b).1 x' ≤ (↑δ : ℝ≥0∞) + (↑δ : ℝ≥0∞)

Tactic:
exact (edist_triangle _ _ _).trans (add_le_add (le_of_lt hax) hxx'.le)

Premises used: add_le_add, le_of_lt, LT.lt.le, LE.le.trans, PseudoEMetricSpace.edist_triangle
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < (↑δ : ℝ≥0∞)
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < (↑δ : ℝ≥0∞)
A : s ∩ Metric.eball x (↑δ : ℝ≥0∞) ∈ 𝓝[s] x
B : t ∩ {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x (↑δ : ℝ≥0∞)
hbt : (a, b).2 ∈ t
hby : Membership.mem (γ := Set β) {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} (a, b).2
⊢ edist (f (x', b)) (f (x', y)) ≤ ε / 2

Tactic:
hby

Premises used: Set.Mem, setOf
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < (↑δ : ℝ≥0∞)
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < (↑δ : ℝ≥0∞)
A : s ∩ Metric.eball x (↑δ : ℝ≥0∞) ∈ 𝓝[s] x
B : t ∩ {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x (↑δ : ℝ≥0∞)
hbt : (a, b).2 ∈ t
hby : Membership.mem (γ := Set β) {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} (a, b).2
⊢ edist (f (x', b)) (f (x', y)) ≤ ε / 2

Tactic:
exact hby
-- Module: Mathlib.Topology.EMetricSpace.Lipschitz
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s'
K : ℝ≥0
ha : ∀ a ∈ s', ContinuousOn.{v, w} (Y := γ) (fun (y : β) ↦ f (a, y)) t
hb : ∀ b ∈ t, LipschitzOnWith.{u, w} (β := γ) K (fun (x : α) ↦ f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < (↑δ : ℝ≥0∞)
hδ : (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < (↑δ : ℝ≥0∞)
A : s ∩ Metric.eball x (↑δ : ℝ≥0∞) ∈ 𝓝[s] x
B : t ∩ {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).1 ∈ s
hax : (a, b).1 ∈ Metric.eball x (↑δ : ℝ≥0∞)
hbt : (a, b).2 ∈ t
hby : Membership.mem (γ := Set β) {b : β | edist (f (x', b)) (f (x', y)) ≤ ε / 2} (a, b).2
⊢ edist (f (x', y)) (f (x, y)) ≤ (↑K : ℝ≥0∞) * (↑δ : ℝ≥0∞)

Tactic:
(hb y hy).edist_le_mul_of_le (hs' hx') hx ((edist_comm _ _).trans_le hxx'.le)

Premises used: PseudoEMetricSpace.edist_comm, LT.lt.le, LipschitzOnWith.edist_le_mul_of_le, Eq.trans_le