awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] f
have refine : ∀ (x : α) (ε : ℝ≥0∞) (ε0 : ε > 0), ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)
Tactic: refine continuous_iff_continuousAt.2 fun x => ENNReal.tendsto_nhds_of_Icc fun ε ε0 => ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
⊢ ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)
have rcases : ∀ (δ : ℝ≥0) (δ0 : δ > 0) (hδ : (↑δ : ℝ≥0∞) * C < ε), ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)
Tactic: rcases ENNReal.exists_nnreal_pos_mul_lt hC ε0.ne' with ⟨δ, δ0, hδ⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : (↑δ : ℝ≥0∞) * C < ε
⊢ ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)
have hδ₁ : C * (↑δ : ℝ≥0∞) < ε
Tactic: rw [mul_comm] at hδ
Cleared hypotheses: hδ
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * (↑δ : ℝ≥0∞) < ε
⊢ ∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)
have h₁ : ∀ (y : α) (hy : y ∈ closedEBall x (↑δ : ℝ≥0∞)), f y ∈ Icc (f x - ε) (f x + ε)
Tactic: filter_upwards [Metric.closedEBall_mem_nhds x (ENNReal.coe_pos.2 δ0)] with y hy
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * (↑δ : ℝ≥0∞) < ε
y : α
hy : y ∈ closedEBall x (↑δ : ℝ≥0∞)
⊢ f y ∈ Icc (f x - ε) (f x + ε)
have h₁ : f y + C * edist x y ≤ f y + ε
Tactic: refine ⟨tsub_le_iff_right.2 <| (h x y).trans ?_, (h y x).trans ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * (↑δ : ℝ≥0∞) < ε
y : α
hy : y ∈ closedEBall x (↑δ : ℝ≥0∞)
h₁ : f y + C * edist x y ≤ f y + ε
⊢ f y ∈ Icc (f x - ε) (f x + ε)
have h₂ : f x + C * edist y x ≤ f x + ε
Tactic: refine ⟨tsub_le_iff_right.2 <| (h x y).trans ?_, (h y x).trans ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * (↑δ : ℝ≥0∞) < ε
y : α
hy : y ∈ closedEBall x (↑δ : ℝ≥0∞)
⊢ f y + C * edist x y ≤ f y + ε
have h₁ : f y + C * edist x y ≤ f y + C * (↑δ : ℝ≥0∞)
Tactic: grw [← hδ.le]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * (↑δ : ℝ≥0∞) < ε
y : α
hy : y ∈ closedEBall x (↑δ : ℝ≥0∞)
⊢ f x + C * edist y x ≤ f x + ε
have h₁ : f x + C * edist y x ≤ f x + C * (↑δ : ℝ≥0∞)
Tactic: grw [← hδ.le]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * (↑δ : ℝ≥0∞) < ε
y : α
hy : y ∈ closedEBall x (↑δ : ℝ≥0∞)
⊢ f y + C * edist x y ≤ f y + C * (↑δ : ℝ≥0∞)
have h₁ : edist x y ≤ (↑δ : ℝ≥0∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α → ℝ≥0∞
C : ℝ≥0∞
hC : C ≠ ∞
h : ∀ (x y : α), f x ≤ f y + C * edist x y
x : α
ε : ℝ≥0∞
ε0 : ε > 0
δ : ℝ≥0
δ0 : δ > 0
hδ : C * (↑δ : ℝ≥0∞) < ε
y : α
hy : y ∈ closedEBall x (↑δ : ℝ≥0∞)
⊢ f x + C * edist y x ≤ f x + C * (↑δ : ℝ≥0∞)
have h₁ : edist y x ≤ (↑δ : ℝ≥0∞)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
⊢ Continuous[instTopologicalSpaceProd, _] fun (p : α × α) ↦ edist p.1 p.2
have apply : ∀ (x y : α × α), edist x.1 x.2 ≤ edist y.1 y.2 + 2 * edist x y
Tactic: apply continuous_of_le_add_edist 2 (by decide)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x x' + edist x' y' + edist y' y = edist x' y' + (edist x x' + edist y y')
have rw : edist x x' + edist x' y' + edist y' y = edist x' y' + (edist x x' + edist y' y)
Tactic: rw [edist_comm y y']
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x' y' + (edist x x' + edist y y') ≤ edist x' y' + (edist (x, y) (x', y') + edist (x, y) (x', y'))
have bc : edist x x' ≤ edist (x, y) (x', y')
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y x' y' : α
bc : edist x x' ≤ edist (x, y) (x', y')
⊢ edist x' y' + (edist x x' + edist y y') ≤ edist x' y' + (edist (x, y) (x', y') + edist (x, y) (x', y'))
have bc₁ : edist y y' ≤ edist (x, y) (x', y')
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y x' y' : α
⊢ edist x' y' + (edist (x, y) (x', y') + edist (x, y) (x', y')) = edist x' y' + 2 * edist (x, y) (x', y')
have rw : edist x' y' + edist (x, y) (x', y') * 2 = edist x' y' + 2 * edist (x, y) (x', y')
Tactic: rw [← mul_two, mul_comm]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y x' y' : α
rw : edist x' y' + edist (x, y) (x', y') * 2 = edist x' y' + 2 * edist (x, y) (x', y')
⊢ edist x' y' + (edist (x, y) (x', y') + edist (x, y) (x', y')) = edist x' y' + 2 * edist (x, y) (x', y')
have rw₁ : edist x' y' + 2 * edist (x, y) (x', y') = edist x' y' + 2 * edist (x, y) (x', y')
Tactic: rw [← mul_two, mul_comm]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y x' y' : α
⊢ edist (x, y).1 (x, y).2 ≤ edist (x', y').1 (x', y').2 + 2 * edist (x, y) (x', y')
have edist : edist x x' + edist x' y' + edist y' y = edist x' y' + (edist x x' + edist y y')
Tactic: calc
    edist x y ≤ edist x x' + edist x' y' + edist y' y := edist_triangle4 _ _ _ _
    _ = edist x' y' + (edist x x' + edist y y') := by rw [edist_comm y y']; abel
    _ ≤ edist x' y' + (edist (x, y) (x', y') + edist (x, y) (x', y')) := by
      gcongr <;> apply_rules [le_max_left, le_max_right]
    _ = edist x' y' + 2 * edist (x, y) (x', y') := by rw [← mul_two, mul_comm]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y x' y' : α
edist :
  EDist.edist x x' + EDist.edist x' y' + EDist.edist y' y = EDist.edist x' y' + (EDist.edist x x' + EDist.edist y y')
⊢ EDist.edist (x, y).1 (x, y).2 ≤ EDist.edist (x', y').1 (x', y').2 + 2 * EDist.edist (x, y) (x', y')
have edist₁ : EDist.edist x' y' + (EDist.edist x x' + EDist.edist y y') ≤
  EDist.edist x' y' + (EDist.edist (x, y) (x', y') + EDist.edist (x, y) (x', y'))
Tactic: calc
    edist x y ≤ edist x x' + edist x' y' + edist y' y := edist_triangle4 _ _ _ _
    _ = edist x' y' + (edist x x' + edist y y') := by rw [edist_comm y y']; abel
    _ ≤ edist x' y' + (edist (x, y) (x', y') + edist (x, y) (x', y')) := by
      gcongr <;> apply_rules [le_max_left, le_max_right]
    _ = edist x' y' + 2 * edist (x, y) (x', y') := by rw [← mul_two, mul_comm]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y x' y' : α
edist :
  EDist.edist x x' + EDist.edist x' y' + EDist.edist y' y = EDist.edist x' y' + (EDist.edist x x' + EDist.edist y y')
edist₁ :
  EDist.edist x' y' + (EDist.edist x x' + EDist.edist y y') ≤
    EDist.edist x' y' + (EDist.edist (x, y) (x', y') + EDist.edist (x, y) (x', y'))
⊢ EDist.edist (x, y).1 (x, y).2 ≤ EDist.edist (x', y').1 (x', y').2 + 2 * EDist.edist (x, y) (x', y')
have edist₂ : EDist.edist x' y' + (EDist.edist (x, y) (x', y') + EDist.edist (x, y) (x', y')) =
  EDist.edist x' y' + 2 * EDist.edist (x, y) (x', y')
Tactic: calc
    edist x y ≤ edist x x' + edist x' y' + edist y' y := edist_triangle4 _ _ _ _
    _ = edist x' y' + (edist x x' + edist y y') := by rw [edist_comm y y']; abel
    _ ≤ edist x' y' + (edist (x, y) (x', y') + edist (x, y) (x', y')) := by
      gcongr <;> apply_rules [le_max_left, le_max_right]
    _ = edist x' y' + 2 * edist (x, y) (x', y') := by rw [← mul_two, mul_comm]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s : Set α
⊢ ediam (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = ediam s
have refine : ∀ (x : α) (hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) (y : α)
  (hy : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s), edist x y ≤ ediam s
Tactic: refine le_antisymm (ediam_le fun x hx y hy => ?_) (ediam_mono subset_closure)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s : Set α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
y : α
hy : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ edist x y ≤ ediam s
have this : edist x y ∈ closure (Iic (ediam s))
Tactic: have : edist x y ∈ closure (Iic (ediam s)) :=
    map_mem_closure₂ continuous_edist hx hy fun x hx y hy => edist_le_ediam_of_mem hx hy
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
s : Set α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
y : α
hy : y ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
this : edist x y ∈ closure (Iic (ediam s))
⊢ edist x y ≤ ediam s
have rwa : ∀ (this : edist x y ∈ Iic (ediam s)), edist x y ≤ ediam s
Tactic: rwa [closure_Iic] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
⊢ IsClosed[Pi.topologicalSpace] {f : α → β | LipschitzOnWith K f s}
have simp : IsClosed[Pi.topologicalSpace] (⋂ i ∈ s, ⋂ i_1 ∈ s, {x : α → β | edist (x i) (x i_1) ≤ (↑K : ℝ≥0∞) * edist i i_1})
Tactic: simp only [LipschitzOnWith, setOf_forall]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
⊢ IsClosed[Pi.topologicalSpace] (⋂ i ∈ s, ⋂ i_1 ∈ s, {x : α → β | edist (x i) (x i_1) ≤ (↑K : ℝ≥0∞) * edist i i_1})
have refine_1 : ∀ x ∈ s, ∀ y ∈ s, Continuous[Pi.topologicalSpace, _] fun (x_3 : α → β) ↦ edist (x_3 x) (x_3 y)
Tactic: refine isClosed_biInter fun x _ => isClosed_biInter fun y _ => isClosed_le ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_4
β : Type u_5
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
s : Set α
refine_1 : ∀ x ∈ s, ∀ y ∈ s, Continuous[Pi.topologicalSpace, _] fun (x_3 : α → β) ↦ edist (x_3 x) (x_3 y)
⊢ IsClosed[Pi.topologicalSpace] (⋂ i ∈ s, ⋂ i_1 ∈ s, {x : α → β | edist (x i) (x i_1) ≤ (↑K : ℝ≥0∞) * edist i i_1})
have refine_2 : ∀ x ∈ s, ∀ y ∈ s, Continuous[Pi.topologicalSpace, _] fun (x_3 : α → β) ↦ (↑K : ℝ≥0∞) * edist x y
Tactic: refine isClosed_biInter fun x _ => isClosed_biInter fun y _ => isClosed_le ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
⊢ LipschitzOnWith K f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
have this : Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ (↑K : ℝ≥0∞) * x
Tactic: have := ENNReal.continuous_const_mul (ENNReal.coe_ne_top (r := K))
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
this : Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ (↑K : ℝ≥0∞) * x
⊢ LipschitzOnWith K f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
have refine_1 : ∀ (x : α) (hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) (y : α) (hy : y ∈ s),
  ContinuousOn (Y := ℝ≥0∞) (fun (x : α) ↦ edist (f x) (f y))
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
Tactic: refine fun x hx ↦ le_on_closure (fun y hy ↦ le_on_closure (fun x hx ↦ hf hx hy) ?_ ?_ hx) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
this : Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ (↑K : ℝ≥0∞) * x
refine_1 :
  ∀ (x : α) (hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) (y : α) (hy : y ∈ s),
    ContinuousOn (Y := ℝ≥0∞) (fun (x : α) ↦ edist (f x) (f y))
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
⊢ LipschitzOnWith K f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
have refine_2 : ∀ (x : α) (hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) (y : α) (hy : y ∈ s),
  ContinuousOn (Y := ℝ≥0∞) (fun (x : α) ↦ (↑K : ℝ≥0∞) * edist x y)
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
Tactic: refine fun x hx ↦ le_on_closure (fun y hy ↦ le_on_closure (fun x hx ↦ hf hx hy) ?_ ?_ hx) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
this : Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ (↑K : ℝ≥0∞) * x
refine_1 :
  ∀ (x : α) (hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) (y : α) (hy : y ∈ s),
    ContinuousOn (Y := ℝ≥0∞) (fun (x : α) ↦ edist (f x) (f y))
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
refine_2 :
  ∀ (x : α) (hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) (y : α) (hy : y ∈ s),
    ContinuousOn (Y := ℝ≥0∞) (fun (x : α) ↦ (↑K : ℝ≥0∞) * edist x y)
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
⊢ LipschitzOnWith K f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
have refine_3 : ∀ (x : α) (hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s),
  ContinuousOn (Y := ℝ≥0∞) (fun (y : α) ↦ edist (f x) (f y))
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
Tactic: refine fun x hx ↦ le_on_closure (fun y hy ↦ le_on_closure (fun x hx ↦ hf hx hy) ?_ ?_ hx) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
this : Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ (↑K : ℝ≥0∞) * x
refine_1 :
  ∀ (x : α) (hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) (y : α) (hy : y ∈ s),
    ContinuousOn (Y := ℝ≥0∞) (fun (x : α) ↦ edist (f x) (f y))
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
refine_2 :
  ∀ (x : α) (hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) (y : α) (hy : y ∈ s),
    ContinuousOn (Y := ℝ≥0∞) (fun (x : α) ↦ (↑K : ℝ≥0∞) * edist x y)
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
refine_3 :
  ∀ (x : α) (hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s),
    ContinuousOn (Y := ℝ≥0∞) (fun (y : α) ↦ edist (f x) (f y))
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
⊢ LipschitzOnWith K f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
have refine_4 : ∀ (x : α) (hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s),
  ContinuousOn (Y := ℝ≥0∞) (fun (y : α) ↦ (↑K : ℝ≥0∞) * edist x y)
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
Tactic: refine fun x hx ↦ le_on_closure (fun y hy ↦ le_on_closure (fun x hx ↦ hf hx hy) ?_ ?_ hx) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
this : Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ (↑K : ℝ≥0∞) * x
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
y : α
hy : y ∈ s
⊢ ContinuousOn (Y := ℝ≥0∞) (fun (x : α) ↦ (↑K : ℝ≥0∞) * edist x y)
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
have funProp : (↑K : ℝ≥0∞) ≠ ∞
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
s : Set α
K : ℝ≥0
hcont : ContinuousOn f (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
hf : LipschitzOnWith K f s
this : Continuous (Y := ℝ≥0∞) fun (x : ℝ≥0∞) ↦ (↑K : ℝ≥0∞) * x
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ ContinuousOn (Y := ℝ≥0∞) (fun (y : α) ↦ (↑K : ℝ≥0∞) * edist x y)
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s)
have funProp : (↑K : ℝ≥0∞) ≠ ∞
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
s : Set ℝ
h : Bornology.IsBounded s
⊢ ediam s = ENNReal.ofReal (sSup s - sInf s)
have inl : ∀ (h : Bornology.IsBounded (α := ℝ) ∅), ediam (X := ℝ) ∅ = ENNReal.ofReal (HSub.hSub (α := ℝ) (sSup ∅) (sInf ∅))
Tactic: rcases eq_empty_or_nonempty s with (rfl | hne)
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
s : Set ℝ
h : Bornology.IsBounded s
inl : ∀ (h : Bornology.IsBounded (α := ℝ) ∅), ediam (X := ℝ) ∅ = ENNReal.ofReal (HSub.hSub (α := ℝ) (sSup ∅) (sInf ∅))
⊢ ediam s = ENNReal.ofReal (sSup s - sInf s)
have inr : ∀ (hne : s.Nonempty), ediam s = ENNReal.ofReal (sSup s - sInf s)
Tactic: rcases eq_empty_or_nonempty s with (rfl | hne)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ ediam s = ENNReal.ofReal (sSup s - sInf s)
have inr : ∀ (x : ℝ) (hx : x ∈ s) (y : ℝ) (hy : y ∈ s), dist x y ≤ sSup s - sInf s
Tactic: refine le_antisymm (Metric.ediam_le_of_forall_dist_le fun x hx y hy => ?_) ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
inr : ∀ (x : ℝ) (hx : x ∈ s) (y : ℝ) (hy : y ∈ s), dist x y ≤ sSup s - sInf s
⊢ ediam s = ENNReal.ofReal (sSup s - sInf s)
have inr₁ : ENNReal.ofReal (sSup s - sInf s) ≤ ediam s
Tactic: refine le_antisymm (Metric.ediam_le_of_forall_dist_le fun x hx y hy => ?_) ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ ENNReal.ofReal (sSup s - sInf s) ≤ ediam s
have inr : sSup s - sInf s ≤ (ediam s).toReal
Tactic: apply ENNReal.ofReal_le_of_le_toReal
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
s : Set ℝ
h : Bornology.IsBounded s
hne : s.Nonempty
⊢ sSup s - sInf s ≤ (ediam s).toReal
have inr : sSup s - sInf s ≤ Metric.diam (closure s)
Tactic: rw [← Metric.diam, ← Metric.diam_closure]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
s : Set ℝ
h : Bornology.IsBounded s
⊢ Metric.diam s = sSup s - sInf s
have rw : 0 ≤ sSup s - sInf s
Tactic: rw [Metric.diam, Real.ediam_eq h, ENNReal.toReal_ofReal]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a b : ℝ
⊢ ediam (Ioo a b) = ENNReal.ofReal (b - a)
have inl : ∀ (h : b ≤ a), ediam (Ioo a b) = ENNReal.ofReal (b - a)
Tactic: rcases le_or_gt b a with (h | h)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a b : ℝ
inl : ∀ (h : b ≤ a), ediam (Ioo a b) = ENNReal.ofReal (b - a)
⊢ ediam (Ioo a b) = ENNReal.ofReal (b - a)
have inr : ∀ (h : a < b), ediam (Ioo a b) = ENNReal.ofReal (b - a)
Tactic: rcases le_or_gt b a with (h | h)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a b : ℝ
h : a < b
⊢ ediam (Ioo a b) = ENNReal.ofReal (b - a)
have inr : ENNReal.ofReal (sSup (Ioo a b) - sInf (Ioo a b)) = ENNReal.ofReal (b - a)
Tactic: rw [Real.ediam_eq (isBounded_Ioo _ _), csSup_Ioo h, csInf_Ioo h]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a b : ℝ
h : a < b
inr : ENNReal.ofReal (sSup (Ioo a b) - sInf (Ioo a b)) = ENNReal.ofReal (b - a)
⊢ ediam (Ioo a b) = ENNReal.ofReal (b - a)
have inr₁ : ENNReal.ofReal (b - sInf (Ioo a b)) = ENNReal.ofReal (b - a)
Tactic: rw [Real.ediam_eq (isBounded_Ioo _ _), csSup_Ioo h, csInf_Ioo h]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a b : ℝ
h : a < b
inr : ENNReal.ofReal (sSup (Ioo a b) - sInf (Ioo a b)) = ENNReal.ofReal (b - a)
inr₁ : ENNReal.ofReal (b - sInf (Ioo a b)) = ENNReal.ofReal (b - a)
⊢ ediam (Ioo a b) = ENNReal.ofReal (b - a)
have inr₂ : ENNReal.ofReal (b - a) = ENNReal.ofReal (b - a)
Tactic: rw [Real.ediam_eq (isBounded_Ioo _ _), csSup_Ioo h, csInf_Ioo h]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a b : ℝ
⊢ ediam (Icc a b) = ENNReal.ofReal (b - a)
have inl : ∀ (h : a ≤ b), ediam (Icc a b) = ENNReal.ofReal (b - a)
Tactic: rcases le_or_gt a b with (h | h)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a b : ℝ
inl : ∀ (h : a ≤ b), ediam (Icc a b) = ENNReal.ofReal (b - a)
⊢ ediam (Icc a b) = ENNReal.ofReal (b - a)
have inr : ∀ (h : b < a), ediam (Icc a b) = ENNReal.ofReal (b - a)
Tactic: rcases le_or_gt a b with (h | h)
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a b : ℝ
h : a ≤ b
⊢ ediam (Icc a b) = ENNReal.ofReal (b - a)
have inl : ENNReal.ofReal (sSup (Icc a b) - sInf (Icc a b)) = ENNReal.ofReal (b - a)
Tactic: rw [Real.ediam_eq (isBounded_Icc _ _), csSup_Icc h, csInf_Icc h]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a b : ℝ
h : a ≤ b
inl : ENNReal.ofReal (sSup (Icc a b) - sInf (Icc a b)) = ENNReal.ofReal (b - a)
⊢ ediam (Icc a b) = ENNReal.ofReal (b - a)
have inl₁ : ENNReal.ofReal (b - sInf (Icc a b)) = ENNReal.ofReal (b - a)
Tactic: rw [Real.ediam_eq (isBounded_Icc _ _), csSup_Icc h, csInf_Icc h]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a b : ℝ
h : a ≤ b
inl : ENNReal.ofReal (sSup (Icc a b) - sInf (Icc a b)) = ENNReal.ofReal (b - a)
inl₁ : ENNReal.ofReal (b - sInf (Icc a b)) = ENNReal.ofReal (b - a)
⊢ ediam (Icc a b) = ENNReal.ofReal (b - a)
have inl₂ : ENNReal.ofReal (b - a) = ENNReal.ofReal (b - a)
Tactic: rw [Real.ediam_eq (isBounded_Icc _ _), csSup_Icc h, csInf_Icc h]