awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
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
⊢ Metric.ediam (image2 f s t) ≤ (↑K₁ : ℝ≥0∞) * Metric.ediam s + (↑K₂ : ℝ≥0∞) * Metric.ediam t
have 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
Tactic: simp only [Metric.ediam_le_iff, forall_mem_image2]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
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
have 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
Tactic: refine (edist_triangle _ (f a₂ b₁) _).trans ?_
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : LocallyLipschitz f
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    f
have rw : ∀ (x : α), ContinuousAt f x
Tactic: rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : LocallyLipschitz f
x : α
⊢ ContinuousAt f x
have rcases : ∀ (K : ℝ≥0) (t : Set α) (ht : t ∈ 𝓝 x) (hK : LipschitzOnWith K f t), ContinuousAt f x
Tactic: rcases (hf x) with ⟨K, t, ht, hK⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : β → γ
g : α → β
hf : LocallyLipschitz f
hg : LocallyLipschitz g
x : α
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith K (f ∘ g) t
have rcases : ∀ (Kg : ℝ≥0) (t : Set α) (ht : t ∈ 𝓝 x) (hgL : LipschitzOnWith Kg g t),
  ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith K (f ∘ g) t
Tactic: rcases hg x with ⟨Kg, t, ht, hgL⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
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
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith K (f ∘ g) t
have rcases : ∀ (Kf : ℝ≥0) (u : Set β) (hu : u ∈ 𝓝 (g x)) (hfL : LipschitzOnWith Kf f u),
  ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith K (f ∘ g) t
Tactic: rcases hf (g x) with ⟨Kf, u, hu, hfL⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
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
have refine : LipschitzOnWith (Kf * Kg) (f ∘ g) (t ∩ g ⁻¹' u)
Tactic: refine ⟨Kf * Kg, t ∩ g⁻¹' u, inter_mem ht (hg.continuous.continuousAt hu), ?_⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
f : α → β
hf : LocallyLipschitz f
g : α → γ
hg : LocallyLipschitz g
x : α
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith (β := β × γ) K (fun (x : α) ↦ (f x, g x)) t
have 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
Tactic: rcases hf x with ⟨Kf, t₁, h₁t, hfL⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
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₁
⊢ ∃ (K : ℝ≥0), ∃ t ∈ 𝓝 x, LipschitzOnWith (β := β × γ) K (fun (x : α) ↦ (f x, g x)) t
have 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
Tactic: rcases hg x with ⟨Kg, t₂, h₂t, hgL⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
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
have refine : LipschitzOnWith (β := β × γ) (max Kf Kg) (fun (x : α) ↦ (f x, g x)) (t₁ ∩ t₂)
Tactic: refine ⟨max Kf Kg, t₁ ∩ t₂, Filter.inter_mem h₁t h₂t, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : α → α
hf : LocallyLipschitz f
n : ℕ
⊢ LocallyLipschitz f^[n + 1]
have rw : LocallyLipschitz (f^[n] ∘ f)
Tactic: rw [iterate_add, iterate_one]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
f : Function.End α
h : LocallyLipschitz f
n : ℕ
⊢ LocallyLipschitz (f ^ (n + 1))
have rw : LocallyLipschitz (f ^ n * f)
Tactic: rw [pow_succ]
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
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)
have refine : ∀ (ε : ℝ≥0∞) (ε0 : 0 < ε), ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ Metric.closedEBall (f (x, y)) ε
Tactic: refine Metric.nhds_basis_closedEBall.tendsto_right_iff.2 fun ε (ε0 : 0 < ε) => ?_
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (hypothesis)
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 < ε
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ Metric.closedEBall (f (x, y)) ε
have ε0₁ : 0 < ε / 2
Tactic: replace ε0 : 0 < ε / 2 := ENNReal.half_pos ε0.ne'
Cleared hypotheses: ε0
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
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
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ Metric.closedEBall (f (x, y)) ε
have 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)) ε
Tactic: obtain ⟨δ, δpos, hδ⟩ : ∃ δ : ℝ≥0, 0 < δ ∧ (δ : ℝ≥0∞) * ↑(3 * K) < ε / 2 :=
    ENNReal.exists_nnreal_pos_mul_lt ENNReal.coe_ne_top ε0.ne'
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (hypothesis)
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
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ Metric.closedEBall (f (x, y)) ε
have δpos₁ : 0 < (↑δ : ℝ≥0∞)
Tactic: rw [← ENNReal.coe_pos] at δpos
Cleared hypotheses: δpos, hδ
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
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_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ Metric.closedEBall (f (x, y)) ε
have 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)) ε
Tactic: rcases EMetric.mem_closure_iff.1 (hss' hx) δ δpos with ⟨x', hx', hxx'⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (hypothesis)
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∞)
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ Metric.closedEBall (f (x, y)) ε
have A : s ∩ Metric.eball x (↑δ : ℝ≥0∞) ∈ 𝓝[s] x
Tactic: have A : s ∩ Metric.eball x δ ∈ 𝓝[s] x :=
    inter_mem_nhdsWithin _ (Metric.eball_mem_nhds _ δpos)
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (hypothesis)
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
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ Metric.closedEBall (f (x, y)) ε
have B : 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))
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
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 : β
⊢ (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)) ε
have 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)) ε
Tactic: ⟨⟨has, hax⟩, ⟨hbt, hby⟩⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
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
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ Metric.closedEBall (f (x, y)) ε
have 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)) ε
Tactic: filter_upwards [nhdsWithin_prod A B] with ⟨a, b⟩ ⟨⟨has, hax⟩, ⟨hbt, hby⟩⟩
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
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)) + edist (f (x', b)) (f (x', y)) + edist (f (x', y)) (f (x, y)) ≤
    (↑K : ℝ≥0∞) * ((↑δ : ℝ≥0∞) + (↑δ : ℝ≥0∞)) + ε / 2 + (↑K : ℝ≥0∞) * (↑δ : ℝ≥0∞)
have h₁ : edist (f (a, b)) (f (x', b)) ≤ (↑K : ℝ≥0∞) * ((↑δ : ℝ≥0∞) + (↑δ : ℝ≥0∞))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
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∞))
⊢ 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∞)
have h₂ : edist (f (x', b)) (f (x', y)) ≤ ε / 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
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
⊢ 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∞)
have h₃ : edist (f (x', y)) (f (x, y)) ≤ (↑K : ℝ≥0∞) * (↑δ : ℝ≥0∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
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∞))
have h₁ : edist (a, b).1 x' ≤ (↑δ : ℝ≥0∞) + (↑δ : ℝ≥0∞)
Tactic: refine (hb b hbt).edist_le_mul_of_le has (hs' hx') ?_
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
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
⊢ f (a, b) ∈ Metric.closedEBall (f (x, y)) ε
have edist : 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: calc
    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)) := edist_triangle4 _ _ _ _
    _ ≤ K * (δ + δ) + ε / 2 + K * δ := by
      gcongr
      · refine (hb b hbt).edist_le_mul_of_le has (hs' hx') ?_
        exact (edist_triangle _ _ _).trans (add_le_add (le_of_lt hax) hxx'.le)
      · exact hby
      · exact (hb y hy).edist_le_mul_of_le (hs' hx') hx ((edist_comm _ _).trans_le hxx'.le)
    _ = δ * ↑(3 * K) + ε / 2 := by push_cast; ring
    _ ≤ ε / 2 + ε / 2 := by gcongr
    _ = ε := ENNReal.add_halves _
-- Lean 4 proof step from Mathlib.Topology.EMetricSpace.Lipschitz (goal)
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.edist x x' < (↑δ : ℝ≥0∞)
A : s ∩ Metric.eball x (↑δ : ℝ≥0∞) ∈ 𝓝[s] x
B : t ∩ {b : β | EDist.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.edist (f (x', b)) (f (x', y)) ≤ ε / 2} (a, b).2
edist :
  EDist.edist (f (a, b)) (f (x', b)) + EDist.edist (f (x', b)) (f (x', y)) + EDist.edist (f (x', y)) (f (x, y)) ≤
    (↑K : ℝ≥0∞) * ((↑δ : ℝ≥0∞) + (↑δ : ℝ≥0∞)) + ε / 2 + (↑K : ℝ≥0∞) * (↑δ : ℝ≥0∞)
⊢ f (a, b) ∈ Metric.closedEBall (f (x, y)) ε
have edist₁ : (↑K : ℝ≥0∞) * ((↑δ : ℝ≥0∞) + (↑δ : ℝ≥0∞)) + ε / 2 + (↑K : ℝ≥0∞) * (↑δ : ℝ≥0∞) = (↑δ : ℝ≥0∞) * (↑(3 * K) : ℝ≥0∞) + ε / 2
Tactic: calc
    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)) := edist_triangle4 _ _ _ _
    _ ≤ K * (δ + δ) + ε / 2 + K * δ := by
      gcongr
      · refine (hb b hbt).edist_le_mul_of_le has (hs' hx') ?_
        exact (edist_triangle _ _ _).trans (add_le_add (le_of_lt hax) hxx'.le)
      · exact hby
      · exact (hb y hy).edist_le_mul_of_le (hs' hx') hx ((edist_comm _ _).trans_le hxx'.le)
    _ = δ * ↑(3 * K) + ε / 2 := by push_cast; ring
    _ ≤ ε / 2 + ε / 2 := by gcongr
    _ = ε := ENNReal.add_halves _