awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.LinearTopology (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : Module.{u_1, u_3} Rᵐᵒᵖ M
inst_5 : IsCentralScalar R M
⊢ IsLinearTopology.{u_1, u_3} Rᵐᵒᵖ M ↔ IsLinearTopology R M
have mp : IsLinearTopology.{u_1, u_3} Rᵐᵒᵖ M → IsLinearTopology R M
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.LinearTopology (goal)
Goal:
R : Type u_1
M : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : TopologicalSpace M
inst_4 : Module.{u_1, u_3} Rᵐᵒᵖ M
inst_5 : IsCentralScalar R M
mp : IsLinearTopology.{u_1, u_3} Rᵐᵒᵖ M → IsLinearTopology R M
⊢ IsLinearTopology.{u_1, u_3} Rᵐᵒᵖ M ↔ IsLinearTopology R M
have mpr : IsLinearTopology R M → IsLinearTopology.{u_1, u_3} Rᵐᵒᵖ M
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
⊢ CauchySeq (f ∘ u)
have rcases : ∀ (b : ℕ → ℝ) (b_nonneg : ∀ (n : ℕ), 0 ≤ b n) (hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N)
  (blim : Tendsto b atTop (nhds 0)), CauchySeq (f ∘ u)
Tactic: rcases cauchySeq_iff_le_tendsto_0.1 hu with ⟨b, b_nonneg, hb, blim⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ CauchySeq (f ∘ u)
have refine_1 : ∀ (n : ℕ), LE.le (α := ℝ) 0 ((fun (n : ℕ) ↦ (↑K : ℝ) * b n) n)
Tactic: refine cauchySeq_iff_le_tendsto_0.2 ⟨fun n ↦ K * b n, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
refine_1 : ∀ (n : ℕ), LE.le (α := ℝ) 0 ((fun (n : ℕ) ↦ (↑K : ℝ) * b n) n)
⊢ CauchySeq (f ∘ u)
have refine_2 : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun (n : ℕ) ↦ (↑K : ℝ) * b n) N
Tactic: refine cauchySeq_iff_le_tendsto_0.2 ⟨fun n ↦ K * b n, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
refine_1 : ∀ (n : ℕ), LE.le (α := ℝ) 0 ((fun (n : ℕ) ↦ (↑K : ℝ) * b n) n)
refine_2 : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun (n : ℕ) ↦ (↑K : ℝ) * b n) N
⊢ CauchySeq (f ∘ u)
have refine_3 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑K : ℝ) * b n) atTop (nhds 0)
Tactic: refine cauchySeq_iff_le_tendsto_0.2 ⟨fun n ↦ K * b n, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
hf : LipschitzWith K f
u : ℕ → α
hu : CauchySeq u
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑K : ℝ) * b n) atTop (nhds 0)
have refine_3 : Tendsto (fun (n : ℕ) ↦ (↑K : ℝ) * b n) atTop (nhds ((↑K : ℝ) * 0))
Tactic: rw [← mul_zero (K : ℝ)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
⊢ CauchySeq (f ∘ u)
have rcases : ∀ (b : ℕ → ℝ) (b_nonneg : ∀ (n : ℕ), 0 ≤ b n) (hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N)
  (blim : Tendsto b atTop (nhds 0)), CauchySeq (f ∘ u)
Tactic: rcases cauchySeq_iff_le_tendsto_0.1 hu with ⟨b, b_nonneg, hb, blim⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ CauchySeq (f ∘ u)
have refine_1 : ∀ (n : ℕ), LE.le (α := ℝ) 0 ((fun (n : ℕ) ↦ (↑K : ℝ) * b n) n)
Tactic: refine cauchySeq_iff_le_tendsto_0.2 ⟨fun n ↦ K * b n, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
refine_1 : ∀ (n : ℕ), LE.le (α := ℝ) 0 ((fun (n : ℕ) ↦ (↑K : ℝ) * b n) n)
⊢ CauchySeq (f ∘ u)
have refine_2 : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun (n : ℕ) ↦ (↑K : ℝ) * b n) N
Tactic: refine cauchySeq_iff_le_tendsto_0.2 ⟨fun n ↦ K * b n, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
refine_1 : ∀ (n : ℕ), LE.le (α := ℝ) 0 ((fun (n : ℕ) ↦ (↑K : ℝ) * b n) n)
refine_2 : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun (n : ℕ) ↦ (↑K : ℝ) * b n) N
⊢ CauchySeq (f ∘ u)
have refine_3 : Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑K : ℝ) * b n) atTop (nhds 0)
Tactic: refine cauchySeq_iff_le_tendsto_0.2 ⟨fun n ↦ K * b n, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
n m N : ℕ
hn : N ≤ n
hm : N ≤ m
⊢ dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun (n : ℕ) ↦ (↑K : ℝ) * b n) N
have A : ∀ (n : ℕ), u n ∈ s
Tactic: have A n : u n ∈ s := h'u (mem_range_self _)
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
n m N : ℕ
hn : N ≤ n
hm : N ≤ m
A : ∀ (n : ℕ), u n ∈ s
⊢ dist ((f ∘ u) n) ((f ∘ u) m) ≤ (fun (n : ℕ) ↦ (↑K : ℝ) * b n) N
have refine_2 : (↑K : ℝ) * dist (u n) (u m) ≤ (fun (n : ℕ) ↦ (↑K : ℝ) * b n) N
Tactic: apply (hf.dist_le_mul _ (A n) _ (A m)).trans
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
hf : LipschitzOnWith K f s
u : ℕ → α
hu : CauchySeq u
h'u : range u ⊆ s
b : ℕ → ℝ
b_nonneg : ∀ (n : ℕ), 0 ≤ b n
hb : ∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) ≤ b N
blim : Tendsto b atTop (nhds 0)
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ (↑K : ℝ) * b n) atTop (nhds 0)
have refine_3 : Tendsto (fun (n : ℕ) ↦ (↑K : ℝ) * b n) atTop (nhds ((↑K : ℝ) * 0))
Tactic: rw [← mul_zero (K : ℝ)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
x : α
r : ℝ
hr : 0 < r
K : ℝ
h : ∀ (y : α), dist y x < r → dist (f y) (f x) ≤ K * dist y x
⊢ ContinuousAt f x
have refine : Tendsto (β := ℝ) (fun (a : α) ↦ K * dist a x) (nhds x) (nhds 0)
Tactic: refine tendsto_iff_dist_tendsto_zero.2 (squeeze_zero' (Eventually.of_forall fun _ => dist_nonneg)
    (mem_of_superset (ball_mem_nhds _ hr) h) ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf : LocallyLipschitzOn s f
⊢ ∃ (K : ℝ≥0), LipschitzOnWith K f s
have hf' : ContinuousOn f s
Tactic: have hf' := hf.continuousOn
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf : LocallyLipschitzOn s f
hf' : ContinuousOn f s
x : α
hx : x ∈ s
⊢ ∃ ε > 0, ∃ (K : ℝ≥0), LipschitzOnWith K f (ball x ε ∩ s)
have let : ∀ (K : ℝ≥0) (t : Set α) (ht : t ∈ nhdsWithin x s) (hf : LipschitzOnWith K f t),
  ∃ ε > 0, ∃ (K : ℝ≥0), LipschitzOnWith K f (ball x ε ∩ s)
Tactic: let ⟨K, t, ht, hf⟩ := hf hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf_1 : LocallyLipschitzOn s f
hf' : ContinuousOn f s
x : α
hx : x ∈ s
K : ℝ≥0
t : Set α
ht : t ∈ nhdsWithin x s
hf : LipschitzOnWith K f t
⊢ ∃ ε > 0, ∃ (K : ℝ≥0), LipschitzOnWith K f (ball x ε ∩ s)
have let : ∀ (ε : ℝ) (hε : ε > 0) (hε' : ball x ε ∩ s ⊆ t), ∃ ε > 0, ∃ (K : ℝ≥0), LipschitzOnWith K f (ball x ε ∩ s)
Tactic: let ⟨ε, hε, hε'⟩ := Metric.mem_nhdsWithin_iff.1 ht
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf : LocallyLipschitzOn s f
hf' : ContinuousOn f s
⊢ ∃ (K : ℝ≥0), LipschitzOnWith K f s
have hf₁ : ∀ x ∈ s, ∃ ε > 0, ∃ (K : ℝ≥0), LipschitzOnWith K f (ball x ε ∩ s)
Tactic: replace hf : ∀ x ∈ s, ∃ ε > 0, ∃ K, LipschitzOnWith K f (ball x ε ∩ s) := fun x hx ↦ by
    let ⟨K, t, ht, hf⟩ := hf hx
    let ⟨ε, hε, hε'⟩ := Metric.mem_nhdsWithin_iff.1 ht
    exact ⟨ε, hε, K, hf.mono hε'⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
hf : ∀ x ∈ s, ∃ ε > 0, ∃ (K : ℝ≥0), LipschitzOnWith K f (ball x ε ∩ s)
⊢ ∃ (K : ℝ≥0), LipschitzOnWith K f s
have choose : ∀ (ε : (x : α) → x ∈ s → ℝ) (hε : ∀ (x : α) (a : x ∈ s), ε x a > 0) (K : (x : α) → x ∈ s → ℝ≥0)
  (hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)), ∃ (K : ℝ≥0), LipschitzOnWith K f s
Tactic: choose ε hε K hf using hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
⊢ ∃ (K' : ℝ≥0), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑K' : ENNReal) * edist x y
have let : ∀ (K' : ℝ)
  (hK' :
    Membership.mem (γ := Set ℝ) (upperBounds ((fun (y : α) ↦ dist (f x) (f y) / dist x y) '' (s \ ball x (ε x hx))))
      K'),
  ∃ (K' : ℝ≥0), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑K' : ENNReal) * edist x y
Tactic: let ⟨K', hK'⟩ := (hs.diff isOpen_ball).bddAbove_image
      (f := fun y ↦ dist (f x) (f y) / dist x y) <| .div (.mono (by fun_prop) s.diff_subset)
        (by fun_prop) fun y hy ↦ ((hε x hx).trans_le <| not_lt.1 <| dist_comm x y ▸ hy.2).ne'
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
K' : ℝ
hK' :
  Membership.mem (γ := Set ℝ) (upperBounds ((fun (y : α) ↦ dist (f x) (f y) / dist x y) '' (s \ ball x (ε x hx)))) K'
⊢ ∃ (K' : ℝ≥0), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑K' : ENNReal) * edist x y
have refine : ∀ (y : α) (hy : y ∈ s.diff (ball x (ε x hx))), edist (f x) (f y) ≤ (↑(NNReal.mk (max K' 0) sorry) : ENNReal) * edist x y
Tactic: refine ⟨.mk (K' ⊔ 0) le_sup_right, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
K' : ℝ
hK' :
  Membership.mem (γ := Set ℝ) (upperBounds ((fun (y : α) ↦ dist (f x) (f y) / dist x y) '' (s \ ball x (ε x hx)))) K'
y : α
hy : y ∈ s.diff (ball x (ε x hx))
⊢ edist (f x) (f y) ≤ (↑(NNReal.mk (max K' 0) ⋯) : ENNReal) * edist x y
have simp_rw : nndist (f x) (f y) ≤ NNReal.mk (max K' 0) sorry * nndist x y
Tactic: simp_rw [edist_nndist, ← ENNReal.coe_mul, ENNReal.coe_le_coe]
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
K' : ℝ
hK' :
  Membership.mem (γ := Set ℝ) (upperBounds ((fun (y : α) ↦ dist (f x) (f y) / dist x y) '' (s \ ball x (ε x hx)))) K'
y : α
hy : y ∈ s.diff (ball x (ε x hx))
⊢ nndist (f x) (f y) ≤ NNReal.mk (max K' 0) ⋯ * nndist x y
have refine_1 : 0 < nndist x y
Tactic: refine (div_le_iff₀ ?_).1 ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
x : α
hx : x ∈ s
K' : ℝ
hK' :
  Membership.mem (γ := Set ℝ) (upperBounds ((fun (y : α) ↦ dist (f x) (f y) / dist x y) '' (s \ ball x (ε x hx)))) K'
y : α
hy : y ∈ s.diff (ball x (ε x hx))
refine_1 : 0 < nndist x y
⊢ nndist (f x) (f y) ≤ NNReal.mk (max K' 0) ⋯ * nndist x y
have refine_2 : nndist (f x) (f y) / nndist x y ≤ NNReal.mk (max K' 0) sorry
Tactic: refine (div_le_iff₀ ?_).1 ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
⊢ ∃ (K : ℝ≥0), LipschitzOnWith K f s
have this : ∀ (x : α) (hx : x ∈ s), ∃ (K' : ℝ≥0), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑K' : ENNReal) * edist x y
Tactic: have (x) (hx : x ∈ s) : ∃ K' : ℝ≥0, ∀ y ∈ s.diff (ball x (ε x hx)),
      edist (f x) (f y) ≤ K' * edist x y := by
    let ⟨K', hK'⟩ := (hs.diff isOpen_ball).bddAbove_image
      (f := fun y ↦ dist (f x) (f y) / dist x y) <| .div (.mono (by fun_prop) s.diff_subset)
        (by fun_prop) fun y hy ↦ ((hε x hx).trans_le <| not_lt.1 <| dist_comm x y ▸ hy.2).ne'
    refine ⟨.mk (K' ⊔ 0) le_sup_right, fun y hy ↦ ?_⟩
    simp_rw [edist_nndist, ← ENNReal.coe_mul, ENNReal.coe_le_coe]
    refine (div_le_iff₀ ?_).1 ?_
    · exact NNReal.coe_pos.1 <| coe_nndist x y ▸
        ((hε x hx).trans_le <| not_lt.1 <| dist_comm x y ▸ hy.2)
    · simp [← NNReal.coe_le_coe, (mem_upperBounds.1 hK') _ <| mem_image_of_mem _ hy]
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
this :
  ∀ (x : α) (hx : x ∈ s), ∃ (K' : ℝ≥0), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑K' : ENNReal) * edist x y
⊢ ∃ (K : ℝ≥0), LipschitzOnWith K f s
have choose : ∀ (K' : (x : α) → (hx : x ∈ s) → ℝ≥0)
  (hK' :
    ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y),
  ∃ (K : ℝ≥0), LipschitzOnWith K f s
Tactic: choose K' hK' using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
⊢ ∃ (K : ℝ≥0), LipschitzOnWith K f s
have obtain : ∀ (t : Finset (↑s : Type u_1)) (ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) sorry / 2)),
  ∃ (K : ℝ≥0), LipschitzOnWith K f s
Tactic: obtain ⟨t, ht⟩ := hs.elim_nhdsWithin_subcover' (fun x hx ↦ s ∩ ball x (ε x hx / 2))
    (fun x hx ↦ inter_mem_nhdsWithin s <| ball_mem_nhds x <| half_pos <| hε x hx)
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
⊢ ∃ (K : ℝ≥0), LipschitzOnWith K f s
have h : LipschitzOnWith (t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) sorry + 2 * K' (↑i : α) sorry) f s
Tactic: use t.sup fun i ↦ K _ i.2 + 2 * K' _ i.2
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ edist (f x) (f y) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal) * edist x y
have h : ∀ (z : (↑s : Type u_1)) (hz : z ∈ t) (hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) sorry / 2)),
  edist (f x) (f y) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) sorry + 2 * K' (↑i : α) sorry) : ENNReal) * edist x y
Tactic: let ⟨z, hz, hx'⟩ := mem_iUnion₂.1 <| ht hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
⊢ edist (f x) (f y) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal) * edist x y
have pos : ∀ (hy' : y ∈ ball (↑z : α) (ε (↑z : α) sorry)),
  edist (f x) (f y) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) sorry + 2 * K' (↑i : α) sorry) : ENNReal) * edist x y
Tactic: by_cases hy' : y ∈ ball z.1 (ε _ z.2)
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
pos :
  ∀ (hy' : y ∈ ball (↑z : α) (ε (↑z : α) ⋯)),
    edist (f x) (f y) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal) * edist x y
⊢ edist (f x) (f y) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal) * edist x y
have neg : ∀ (hy' : y ∉ ball (↑z : α) (ε (↑z : α) sorry)),
  edist (f x) (f y) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) sorry + 2 * K' (↑i : α) sorry) : ENNReal) * edist x y
Tactic: by_cases hy' : y ∈ ball z.1 (ε _ z.2)
-- Lean 4 proof step from Mathlib.Topology.Algebra.MetricSpace.Lipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
s : Set α
hs : IsCompact s
hf' : ContinuousOn f s
ε : (x : α) → x ∈ s → ℝ
hε : ∀ (x : α) (a : x ∈ s), ε x a > 0
K : (x : α) → x ∈ s → ℝ≥0
hf : ∀ (x : α) (a : x ∈ s), LipschitzOnWith (K x a) f (ball x (ε x a) ∩ s)
K' : (x : α) → (hx : x ∈ s) → ℝ≥0
hK' : ∀ (x : α) (hx : x ∈ s), ∀ y ∈ s.diff (ball x (ε x hx)), edist (f x) (f y) ≤ (↑(K' x hx) : ENNReal) * edist x y
t : Finset (↑s : Type u_1)
ht : s ⊆ ⋃ x ∈ t, s ∩ ball (↑x : α) (ε (↑x : α) ⋯ / 2)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : (↑s : Type u_1)
hz : z ∈ t
hx' : x ∈ s ∩ ball (↑z : α) (ε (↑z : α) ⋯ / 2)
hy' : y ∈ ball (↑z : α) (ε (↑z : α) ⋯)
⊢ edist (f x) (f y) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) ⋯ + 2 * K' (↑i : α) ⋯) : ENNReal) * edist x y
have pos : (↑(K (↑z : α) sorry) : ENNReal) ≤ (↑(t.sup fun (i : (↑s : Type u_1)) ↦ K (↑i : α) sorry + 2 * K' (↑i : α) sorry) : ENNReal)
Tactic: refine (hf _ z.2 ⟨hx'.2.trans <| half_lt_self <| hε _ z.2, hx⟩ ⟨hy', hy⟩).trans <|
      mul_le_mul_of_nonneg_right ?_ zero_le