awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
i : ι
⊢ (fun (i : ι) ↦ ‖swap (φ := fun (a : ι) (a_1 : α) ↦ ℝ) g a₀ i‖) i ≤ ‖f a₀‖
have h : ‖(↑(f a₀) : (i : ι) → ℝ) i‖ ≤ ‖f a₀‖
Tactic: simp_rw [← hgeq i ha₀_in_s]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
⊢ ∃ (g : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)), LipschitzWith K g ∧ EqOn f g s
have hf_extb : ∀ (a : α), Memℓp (E := fun (i : ι) ↦ ℝ) (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g a) ∞
Tactic: have hf_extb : ∀ a : α, Memℓp (swap g a) ∞ := by
      apply LipschitzWith.uniformly_bounded (swap g) hgl a₀
      use ‖f a₀‖
      rintro - ⟨i, rfl⟩
      simp_rw [← hgeq i ha₀_in_s]
      exact lp.norm_apply_le_norm top_ne_zero (f a₀) i
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (E := fun (i : ι) ↦ ℝ) (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g a) ∞
f_ext' : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞) :=
  fun (i : α) ↦
    Subtype.mk (p := fun (x : PreLp fun (x : ι) ↦ ℝ) ↦
      Membership.mem (γ := AddSubgroup (PreLp fun (x : ι) ↦ ℝ)) (lp (fun (x : ι) ↦ ℝ) ∞) x)
      (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g i) ⋯
⊢ ∃ (g : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)), LipschitzWith K g ∧ EqOn f g s
have inr : LipschitzWith K f_ext'
Tactic: refine ⟨f_ext', ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (E := fun (i : ι) ↦ ℝ) (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g a) ∞
f_ext' : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞) :=
  fun (i : α) ↦
    Subtype.mk (p := fun (x : PreLp fun (x : ι) ↦ ℝ) ↦
      Membership.mem (γ := AddSubgroup (PreLp fun (x : ι) ↦ ℝ)) (lp (fun (x : ι) ↦ ℝ) ∞) x)
      (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g i) ⋯
inr : LipschitzWith K f_ext'
⊢ ∃ (g : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)), LipschitzWith K g ∧ EqOn f g s
have inr₁ : EqOn f f_ext' s
Tactic: refine ⟨f_ext', ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (E := fun (i : ι) ↦ ℝ) (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g a) ∞
f_ext' : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞) :=
  fun (i : α) ↦
    Subtype.mk (p := fun (x : PreLp fun (x : ι) ↦ ℝ) ↦
      Membership.mem (γ := AddSubgroup (PreLp fun (x : ι) ↦ ℝ)) (lp (fun (x : ι) ↦ ℝ) ∞) x)
      (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g i) ⋯
⊢ LipschitzWith K f_ext'
have inr : ∀ (i : ι), LipschitzWith (β := (fun (x : ι) ↦ ℝ) i) K fun (a : α) ↦ (↑(f_ext' a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i
Tactic: rw [LipschitzWith.coordinate]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Kuratowski (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞)
K : ℝ≥0
hfl :
  ∀ (i : ι), LipschitzOnWith (β := (fun (x : ι) ↦ ℝ) i) K (fun (a : α) ↦ (↑(f a) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) s
g : (i : ι) → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun (x : α) ↦ (↑(f x) : (i : ι) → (fun (x : ι) ↦ ℝ) i) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (E := fun (i : ι) ↦ ℝ) (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g a) ∞
f_ext' : α → ↥(lp (fun (x : ι) ↦ ℝ) ∞) :=
  fun (i : α) ↦
    Subtype.mk (p := fun (x : PreLp fun (x : ι) ↦ ℝ) ↦
      Membership.mem (γ := AddSubgroup (PreLp fun (x : ι) ↦ ℝ)) (lp (fun (x : ι) ↦ ℝ) ∞) x)
      (swap (φ := fun (x : ι) (y : α) ↦ ℝ) g i) ⋯
a : α
hyp : a ∈ s
⊢ f a = f_ext' a
have inr : ∀ (i : ι), (↑(f a) : (i : ι) → ℝ) i = (↑(f_ext' a) : (i : ι) → ℝ) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ LipschitzWith K f ↔ ∀ (x y : α), dist (f x) (f y) ≤ (↑K : ℝ) * dist x y
have simp : (∀ (x y : α), (↑(nndist (f x) (f y)) : ℝ≥0∞) ≤ (↑K : ℝ≥0∞) * (↑(nndist x y) : ℝ≥0∞)) ↔
  ∀ (x y : α), (↑(nndist (f x) (f y)) : ℝ) ≤ (↑K : ℝ) * (↑(nndist x y) : ℝ)
Tactic: simp only [LipschitzWith, edist_nndist, dist_nndist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ (∀ (x y : α), (↑(nndist (f x) (f y)) : ℝ≥0∞) ≤ (↑K : ℝ≥0∞) * (↑(nndist x y) : ℝ≥0∞)) ↔
    ∀ (x y : α), (↑(nndist (f x) (f y)) : ℝ) ≤ (↑K : ℝ) * (↑(nndist x y) : ℝ)
have norm_cast : (∀ (x y : α), nndist (f x) (f y) ≤ K * nndist x y) ↔ ∀ (x y : α), nndist (f x) (f y) ≤ K * nndist x y
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
⊢ LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ (↑K : ℝ) * dist x y
have simp : (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → (↑(nndist (f x) (f y)) : ℝ≥0∞) ≤ (↑K : ℝ≥0∞) * (↑(nndist x y) : ℝ≥0∞)) ↔
  ∀ x ∈ s, ∀ y ∈ s, (↑(nndist (f x) (f y)) : ℝ) ≤ (↑K : ℝ) * (↑(nndist x y) : ℝ)
Tactic: simp only [LipschitzOnWith, edist_nndist, dist_nndist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → (↑(nndist (f x) (f y)) : ℝ≥0∞) ≤ (↑K : ℝ≥0∞) * (↑(nndist x y) : ℝ≥0∞)) ↔
    ∀ x ∈ s, ∀ y ∈ s, (↑(nndist (f x) (f y)) : ℝ) ≤ (↑K : ℝ) * (↑(nndist x y) : ℝ)
have norm_cast : (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → nndist (f x) (f y) ≤ K * nndist x y) ↔
  ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → nndist (f x) (f y) ≤ K * nndist x y
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
K : ℝ
h : ∀ (x y : α), dist (f x) (f y) ≤ K * dist x y
x y : α
⊢ K * dist x y ≤ (↑K.toNNReal : ℝ) * dist x y
have hbc : K ≤ (↑K.toNNReal : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ
hf : LipschitzWith K f
hr : dist x y ≤ r
⊢ (↑K : ℝ) * dist x y ≤ (↑K : ℝ) * r
have ha : 0 ≤ (↑K : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
x y : α
r : ℝ
hf : LipschitzWith K f
hK : K ≠ 0
hr : dist x y < r
⊢ (↑K : ℝ) * dist x y < (↑K : ℝ) * r
have ha : 0 < (↑K : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ LipschitzWith.{u, 0} (α := α × α) 2 (uncurry dist)
have rw : LipschitzWith.{u, 0} (α := α × α) (HAdd.hAdd (α := ℝ≥0) 1 1) (uncurry dist)
Tactic: rw [← one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
K : ℝ≥0
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * (↑K : ℝ) ^ n
have rw : dist (f^[n] x) ((f^[n] ∘ f) x) ≤ (↑K : ℝ) ^ n * dist x (f x)
Tactic: rw [iterate_succ, mul_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
⊢ LipschitzWith 1 Real.toNNReal
have refine : ∀ (x y : ℝ), dist x.toNNReal y.toNNReal ≤ (↑1 : ℝ) * dist x y
Tactic: refine lipschitzWith_iff_dist_le_mul.mpr (fun x y ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
s : Set α
f : α → β
K : ℝ
h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ K * dist x y ≤ (↑K.toNNReal : ℝ) * dist x y
have hbc : K ≤ (↑K.toNNReal : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
⊢ ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn f g s
have inl : ∀ (hf : LipschitzOnWith K f ∅), ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn f g ∅
Tactic: rcases eq_empty_or_nonempty s with (rfl | hs)
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
inl : ∀ (hf : LipschitzOnWith K f ∅), ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn f g ∅
⊢ ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn f g s
have inr : ∀ (hs : s.Nonempty), ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn f g s
Tactic: rcases eq_empty_or_nonempty s with (rfl | hs)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
⊢ ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn f g s
have this : Nonempty.{u + 1} (↑s : Type u)
Tactic: have : Nonempty s := by simp only [hs, nonempty_coe_sort]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
y : α
⊢ BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
have rcases : ∀ (z : α) (hz : z ∈ s), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
Tactic: rcases hs with ⟨z, hz⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
y z : α
hz : z ∈ s
⊢ BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
have refine : Membership.mem (γ := Set ℝ) (lowerBounds (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)))
  (f z - (↑K : ℝ) * dist y z)
Tactic: refine ⟨f z - K * dist y z, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
y z : α
hz : z ∈ s
t : (↑s : Type u)
⊢ f z - (↑K : ℝ) * dist y z ≤ f (↑t : α) + (↑K : ℝ) * dist y (↑t : α)
have rw : f z ≤ f (↑t : α) + (↑K : ℝ) * (dist y z + dist y (↑t : α))
Tactic: rw [sub_le_iff_le_add, add_assoc, ← mul_add, add_comm (dist y t)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
y z : α
hz : z ∈ s
t : (↑s : Type u)
⊢ f (↑t : α) + (↑K : ℝ) * dist z (↑t : α) ≤ f (↑t : α) + (↑K : ℝ) * (dist y z + dist y (↑t : α))
have bc : dist z (↑t : α) ≤ dist y z + dist y (↑t : α)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
y z : α
hz : z ∈ s
t : (↑s : Type u)
⊢ f z ≤ f (↑t : α) + (↑K : ℝ) * (dist y z + dist y (↑t : α))
have f₁ : f (↑t : α) + (↑K : ℝ) * dist z (↑t : α) ≤ f (↑t : α) + (↑K : ℝ) * (dist y z + dist y (↑t : α))
Tactic: calc
      f z ≤ f t + K * dist z t := hf.le_add_mul hz t.2
      _ ≤ f t + K * (dist y z + dist y t) := by gcongr; apply dist_triangle_left
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
⊢ ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn f g s
have B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
Tactic: have B : ∀ y : α, BddBelow (range fun x : s => f x + K * dist y x) := fun y => by
    rcases hs with ⟨z, hz⟩
    refine ⟨f z - K * dist y z, ?_⟩
    rintro w ⟨t, rfl⟩
    dsimp
    rw [sub_le_iff_le_add, add_assoc, ← mul_add, add_comm (dist y t)]
    calc
      f z ≤ f t + K * dist z t := hf.le_add_mul hz t.2
      _ ≤ f t + K * (dist y z + dist y t) := by gcongr; apply dist_triangle_left
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
x : α
hx : x ∈ s
⊢ f x = g x
have refine : g x ≤ f x
Tactic: refine le_antisymm (le_ciInf fun y => hf.le_add_mul hx y.2) ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (hypothesis)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
⊢ ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn f g s
have E : EqOn f g s
Tactic: have E : EqOn f g s := fun x hx => by
    refine le_antisymm (le_ciInf fun y => hf.le_add_mul hx y.2) ?_
    simpa only [add_zero, Subtype.coe_mk, mul_zero, dist_self] using ciInf_le (B x) ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
E : EqOn f g s
⊢ ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn f g s
have inr : ∀ (x y : α), g x ≤ g y + (↑K : ℝ) * dist x y
Tactic: refine ⟨g, LipschitzWith.of_le_add_mul K fun x y => ?_, E⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
E : EqOn f g s
x y : α
⊢ g x ≤ g y + (↑K : ℝ) * dist x y
have inr : g x - (↑K : ℝ) * dist x y ≤ g y
Tactic: rw [← sub_le_iff_le_add]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
E : EqOn f g s
x y : α
⊢ g x - (↑K : ℝ) * dist x y ≤ g y
have inr : ∀ (z : (↑s : Type u)), g x - (↑K : ℝ) * dist x y ≤ f (↑z : α) + (↑K : ℝ) * dist y (↑z : α)
Tactic: refine le_ciInf fun z => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
E : EqOn f g s
x y : α
z : (↑s : Type u)
⊢ g x - (↑K : ℝ) * dist x y ≤ f (↑z : α) + (↑K : ℝ) * dist y (↑z : α)
have inr : g x ≤ f (↑z : α) + (↑K : ℝ) * dist y (↑z : α) + (↑K : ℝ) * dist x y
Tactic: rw [sub_le_iff_le_add]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
E : EqOn f g s
x y : α
z : (↑s : Type u)
⊢ f (↑z : α) + (↑K : ℝ) * dist x (↑z : α) ≤ f (↑z : α) + (↑K : ℝ) * dist y (↑z : α) + (↑K : ℝ) * dist x y
have rw : f (↑z : α) + (↑K : ℝ) * dist x (↑z : α) ≤ f (↑z : α) + (↑K : ℝ) * (dist x y + dist y (↑z : α))
Tactic: rw [add_assoc, ← mul_add, add_comm (dist y z)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
E : EqOn f g s
x y : α
z : (↑s : Type u)
⊢ f (↑z : α) + (↑K : ℝ) * dist x (↑z : α) ≤ f (↑z : α) + (↑K : ℝ) * (dist x y + dist y (↑z : α))
have bc : dist x (↑z : α) ≤ dist x y + dist y (↑z : α)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : s.Nonempty
this : Nonempty.{u + 1} (↑s : Type u)
g : (y : α) → ℝ := fun (y : α) ↦ ⨅ (x : (↑s : Type u)), f (↑x : α) + (↑K : ℝ) * dist y (↑x : α)
B : ∀ (y : α), BddBelow (α := ℝ) (range fun (x : (↑s : Type u)) ↦ f (↑x : α) + (↑K : ℝ) * dist y (↑x : α))
E : EqOn f g s
x y : α
z : (↑s : Type u)
⊢ g x ≤ f (↑z : α) + (↑K : ℝ) * dist y (↑z : α) + (↑K : ℝ) * dist x y
have g₁ : f (↑z : α) + (↑K : ℝ) * dist x (↑z : α) ≤ f (↑z : α) + (↑K : ℝ) * dist y (↑z : α) + (↑K : ℝ) * dist x y
Tactic: calc
    g x ≤ f z + K * dist x z := ciInf_le (B x) _
    _ ≤ f z + K * dist y z + K * dist x y := by
      rw [add_assoc, ← mul_add, add_comm (dist y z)]
      gcongr
      apply dist_triangle
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (hypothesis)
Goal:
α : Type u
ι : Type x
inst : PseudoMetricSpace α
inst_1 : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
i : ι
⊢ ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn (fun (x : α) ↦ f x i) g s
have this : LipschitzOnWith (β := ℝ) K (fun (x : α) ↦ f x i) s
Tactic: have : LipschitzOnWith K (fun x : α => f x i) s :=
      LipschitzOnWith.of_dist_le_mul fun x hx y hy =>
        (dist_le_pi_dist _ _ i).trans (hf.dist_le_mul x hx y hy)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (hypothesis)
Goal:
α : Type u
ι : Type x
inst : PseudoMetricSpace α
inst_1 : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
⊢ ∃ (g : α → ι → ℝ), LipschitzWith K g ∧ EqOn f g s
have this : ∀ (i : ι), ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn (fun (x : α) ↦ f x i) g s
Tactic: have : ∀ i, ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s := fun i => by
    have : LipschitzOnWith K (fun x : α => f x i) s :=
      LipschitzOnWith.of_dist_le_mul fun x hx y hy =>
        (dist_le_pi_dist _ _ i).trans (hf.dist_le_mul x hx y hy)
    exact this.extend_real
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
ι : Type x
inst : PseudoMetricSpace α
inst_1 : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : ∀ (i : ι), ∃ (g : α → ℝ), LipschitzWith K g ∧ EqOn (fun (x : α) ↦ f x i) g s
⊢ ∃ (g : α → ι → ℝ), LipschitzWith K g ∧ EqOn f g s
have choose : ∀ (g : (i : ι) → α → ℝ) (hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun (x : α) ↦ f x i) (g i) s),
  ∃ (g : α → ι → ℝ), LipschitzWith K g ∧ EqOn f g s
Tactic: choose g hg using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
ι : Type x
inst : PseudoMetricSpace α
inst_1 : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : (i : ι) → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun (x : α) ↦ f x i) (g i) s
⊢ ∃ (g : α → ι → ℝ), LipschitzWith K g ∧ EqOn f g s
have refine_1 : ∀ (x y : α), (dist.{x} (α := ι → ℝ) (fun (i : ι) ↦ g i x) fun (i : ι) ↦ g i y) ≤ (↑K : ℝ) * dist x y
Tactic: refine ⟨fun x i => g i x, LipschitzWith.of_dist_le_mul fun x y => ?_, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
ι : Type x
inst : PseudoMetricSpace α
inst_1 : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : (i : ι) → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun (x : α) ↦ f x i) (g i) s
refine_1 : ∀ (x y : α), (dist.{x} (α := ι → ℝ) (fun (i : ι) ↦ g i x) fun (i : ι) ↦ g i y) ≤ (↑K : ℝ) * dist x y
⊢ ∃ (g : α → ι → ℝ), LipschitzWith K g ∧ EqOn f g s
have refine_2 : ∀ (x : α) (hx : x ∈ s), f x = (fun (x : α) (i : ι) ↦ g i x) x
Tactic: refine ⟨fun x i => g i x, LipschitzWith.of_dist_le_mul fun x y => ?_, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Lipschitz (goal)
Goal:
α : Type u
ι : Type x
inst : PseudoMetricSpace α
inst_1 : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : (i : ι) → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun (x : α) ↦ f x i) (g i) s
x : α
hx : x ∈ s
⊢ f x = (fun (x : α) (i : ι) ↦ g i x) x
have refine_2 : ∀ (i : ι), f x i = (fun (x : α) (i : ι) ↦ g i x) x i
Tactic: ext1 i