awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
hx : x ∈ thickening δ E
⊢ x ∈ cthickening δ E
have hx₁ : infEDist x E < ENNReal.ofReal δ
Tactic: rw [thickening, mem_setOf_eq] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bornology.IsBounded E
⊢ Bornology.IsBounded (Metric.cthickening δ E)
have this : Bornology.IsBounded (thickening (max (δ + 1) 1) E)
Tactic: have : IsBounded (thickening (max (δ + 1) 1) E) := h.thickening
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
δ : ℝ
E : Set α
h : Bornology.IsBounded E
this : Bornology.IsBounded (thickening (max (δ + 1) 1) E)
⊢ Bornology.IsBounded (Metric.cthickening δ E)
have apply : Metric.cthickening δ E ⊆ thickening (max (δ + 1) 1) E
Tactic: apply this.subset
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E ⊆ cthickening δ E
have rw : cthickening (min δ 0) E ⊆ cthickening δ E
Tactic: rw [← cthickening_of_nonpos (min_le_right δ 0)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E ⊆ thickening δ E
have rw : cthickening 0 E ⊆ thickening δ E
Tactic: rw [← cthickening_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s t : Set α
⊢ thickening δ (s ∪ t) = thickening δ s ∪ thickening δ t
have simp_rw : Eq.{u + 1} (α := Set α) {x : α | infEDist x (s ∪ t) < ENNReal.ofReal δ}
  ({x : α | infEDist x s < ENNReal.ofReal δ} ∪ {x : α | infEDist x t < ENNReal.ofReal δ})
Tactic: simp_rw [thickening, infEDist_union, min_lt_iff, setOf_or]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s t : Set α
simp_rw :
  Eq.{u + 1} (α := Set α) {x : α | infEDist x (s ∪ t) < ENNReal.ofReal δ}
    ({x : α | infEDist x s < ENNReal.ofReal δ} ∪ {x : α | infEDist x t < ENNReal.ofReal δ})
⊢ thickening δ (s ∪ t) = thickening δ s ∪ thickening δ t
have simp_rw₁ : Eq.{u + 1} (α := Set α) {x : α | min (infEDist x s) (infEDist x t) < ENNReal.ofReal δ}
  ({x : α | infEDist x s < ENNReal.ofReal δ} ∪ {x : α | infEDist x t < ENNReal.ofReal δ})
Tactic: simp_rw [thickening, infEDist_union, min_lt_iff, setOf_or]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s t : Set α
simp_rw :
  Eq.{u + 1} (α := Set α) {x : α | infEDist x (s ∪ t) < ENNReal.ofReal δ}
    ({x : α | infEDist x s < ENNReal.ofReal δ} ∪ {x : α | infEDist x t < ENNReal.ofReal δ})
simp_rw₁ :
  Eq.{u + 1} (α := Set α) {x : α | min (infEDist x s) (infEDist x t) < ENNReal.ofReal δ}
    ({x : α | infEDist x s < ENNReal.ofReal δ} ∪ {x : α | infEDist x t < ENNReal.ofReal δ})
⊢ thickening δ (s ∪ t) = thickening δ s ∪ thickening δ t
have simp_rw₂ : Eq.{u + 1} (α := Set α) {x : α | infEDist x s < ENNReal.ofReal δ ∨ infEDist x t < ENNReal.ofReal δ}
  ({x : α | infEDist x s < ENNReal.ofReal δ} ∪ {x : α | infEDist x t < ENNReal.ofReal δ})
Tactic: simp_rw [thickening, infEDist_union, min_lt_iff, setOf_or]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s t : Set α
⊢ cthickening δ (s ∪ t) = cthickening δ s ∪ cthickening δ t
have simp_rw : Eq.{u + 1} (α := Set α) {x : α | infEDist x (s ∪ t) ≤ ENNReal.ofReal δ}
  ({x : α | infEDist x s ≤ ENNReal.ofReal δ} ∪ {x : α | infEDist x t ≤ ENNReal.ofReal δ})
Tactic: simp_rw [cthickening, infEDist_union, min_le_iff, setOf_or]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s t : Set α
simp_rw :
  Eq.{u + 1} (α := Set α) {x : α | infEDist x (s ∪ t) ≤ ENNReal.ofReal δ}
    ({x : α | infEDist x s ≤ ENNReal.ofReal δ} ∪ {x : α | infEDist x t ≤ ENNReal.ofReal δ})
⊢ cthickening δ (s ∪ t) = cthickening δ s ∪ cthickening δ t
have simp_rw₁ : Eq.{u + 1} (α := Set α) {x : α | min (infEDist x s) (infEDist x t) ≤ ENNReal.ofReal δ}
  ({x : α | infEDist x s ≤ ENNReal.ofReal δ} ∪ {x : α | infEDist x t ≤ ENNReal.ofReal δ})
Tactic: simp_rw [cthickening, infEDist_union, min_le_iff, setOf_or]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s t : Set α
simp_rw :
  Eq.{u + 1} (α := Set α) {x : α | infEDist x (s ∪ t) ≤ ENNReal.ofReal δ}
    ({x : α | infEDist x s ≤ ENNReal.ofReal δ} ∪ {x : α | infEDist x t ≤ ENNReal.ofReal δ})
simp_rw₁ :
  Eq.{u + 1} (α := Set α) {x : α | min (infEDist x s) (infEDist x t) ≤ ENNReal.ofReal δ}
    ({x : α | infEDist x s ≤ ENNReal.ofReal δ} ∪ {x : α | infEDist x t ≤ ENNReal.ofReal δ})
⊢ cthickening δ (s ∪ t) = cthickening δ s ∪ cthickening δ t
have simp_rw₂ : Eq.{u + 1} (α := Set α) {x : α | infEDist x s ≤ ENNReal.ofReal δ ∨ infEDist x t ≤ ENNReal.ofReal δ}
  ({x : α | infEDist x s ≤ ENNReal.ofReal δ} ∪ {x : α | infEDist x t ≤ ENNReal.ofReal δ})
Tactic: simp_rw [cthickening, infEDist_union, min_le_iff, setOf_or]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
ι : Sort u_1
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
f : ι → Set α
⊢ Eq.{u + 1} (α := Set α) (thickening δ (⋃ (i : ι), f i)) (⋃ (i : ι), thickening δ (f i))
have simp_rw : Eq.{u + 1} (α := Set α) {x : α | infEDist x (⋃ (i : ι), f i) < ENNReal.ofReal δ}
  (⋃ (i : ι), {x : α | infEDist x (f i) < ENNReal.ofReal δ})
Tactic: simp_rw [thickening, infEDist_iUnion, iInf_lt_iff, setOf_exists]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
ι : Sort u_1
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
f : ι → Set α
simp_rw :
  Eq.{u + 1} (α := Set α) {x : α | infEDist x (⋃ (i : ι), f i) < ENNReal.ofReal δ}
    (⋃ (i : ι), {x : α | infEDist x (f i) < ENNReal.ofReal δ})
⊢ Eq.{u + 1} (α := Set α) (thickening δ (⋃ (i : ι), f i)) (⋃ (i : ι), thickening δ (f i))
have simp_rw₁ : Eq.{u + 1} (α := Set α) {x : α | ⨅ (i : ι), infEDist x (f i) < ENNReal.ofReal δ}
  (⋃ (i : ι), {x : α | infEDist x (f i) < ENNReal.ofReal δ})
Tactic: simp_rw [thickening, infEDist_iUnion, iInf_lt_iff, setOf_exists]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
ι : Sort u_1
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
f : ι → Set α
simp_rw :
  Eq.{u + 1} (α := Set α) {x : α | infEDist x (⋃ (i : ι), f i) < ENNReal.ofReal δ}
    (⋃ (i : ι), {x : α | infEDist x (f i) < ENNReal.ofReal δ})
simp_rw₁ :
  Eq.{u + 1} (α := Set α) {x : α | ⨅ (i : ι), infEDist x (f i) < ENNReal.ofReal δ}
    (⋃ (i : ι), {x : α | infEDist x (f i) < ENNReal.ofReal δ})
⊢ Eq.{u + 1} (α := Set α) (thickening δ (⋃ (i : ι), f i)) (⋃ (i : ι), thickening δ (f i))
have simp_rw₂ : Eq.{u + 1} (α := Set α) {x : α | ∃ (i : ι), infEDist x (f i) < ENNReal.ofReal δ}
  (⋃ (i : ι), {x : α | infEDist x (f i) < ENNReal.ofReal δ})
Tactic: simp_rw [thickening, infEDist_iUnion, iInf_lt_iff, setOf_exists]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
⊢ ediam (cthickening (↑ε : ℝ) s) ≤ ediam s + 2 * (↑ε : ℝ≥0∞)
have refine : ∀ (x : α) (hx : x ∈ cthickening (↑ε : ℝ) s) (y : α) (hy : y ∈ cthickening (↑ε : ℝ) s) (δ : ℝ≥0) (hδ : 0 < δ),
  ediam s + 2 * (↑ε : ℝ≥0∞) < ∞ → edist x y ≤ ediam s + 2 * (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
Tactic: refine ediam_le fun x hx y hy => ENNReal.le_of_forall_pos_le_add fun δ hδ _ => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x : α
hx : x ∈ cthickening (↑ε : ℝ) s
y : α
hy : y ∈ cthickening (↑ε : ℝ) s
δ : ℝ≥0
hδ : 0 < δ
h : ediam s + 2 * (↑ε : ℝ≥0∞) < ∞
⊢ edist x y ≤ ediam s + 2 * (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
have rw : ∀ (hx : infEDist x s ≤ (↑ε : ℝ≥0∞)) (y : α) (hy : infEDist y s ≤ (↑ε : ℝ≥0∞)) (δ : ℝ≥0) (hδ : 0 < δ),
  ediam s + 2 * (↑ε : ℝ≥0∞) < ∞ → edist x y ≤ ediam s + 2 * (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
Tactic: rw [mem_cthickening_iff, ENNReal.ofReal_coe_nnreal] at hx hy
Cleared hypotheses: hx, y, hy, δ, hδ, h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x : α
hx : infEDist x s ≤ (↑ε : ℝ≥0∞)
y : α
hy : infEDist y s ≤ (↑ε : ℝ≥0∞)
δ : ℝ≥0
hδ : 0 < δ
h : ediam s + 2 * (↑ε : ℝ≥0∞) < ∞
⊢ edist x y ≤ ediam s + 2 * (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
have hε : (↑ε : ℝ≥0∞) < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
Tactic: have hε : (ε : ℝ≥0∞) < ε + δ := ENNReal.coe_lt_coe.2 (lt_add_of_pos_right _ hδ)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x : α
hx : infEDist x s ≤ (↑ε : ℝ≥0∞)
y : α
hy : infEDist y s ≤ (↑ε : ℝ≥0∞)
δ : ℝ≥0
hδ : 0 < δ
h : ediam s + 2 * (↑ε : ℝ≥0∞) < ∞
hε : (↑ε : ℝ≥0∞) < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
⊢ edist x y ≤ ediam s + 2 * (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
have hx₁ : infEDist x s < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
Tactic: replace hx := hx.trans_lt hε
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x y : α
hy : infEDist y s ≤ (↑ε : ℝ≥0∞)
δ : ℝ≥0
hδ : 0 < δ
h : ediam s + 2 * (↑ε : ℝ≥0∞) < ∞
hε : (↑ε : ℝ≥0∞) < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
hx : infEDist x s < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
⊢ edist x y ≤ ediam s + 2 * (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
have obtain : ∀ (x' : α) (hx' : x' ∈ s) (hxx' : edist x x' < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)),
  edist x y ≤ ediam s + 2 * (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
Tactic: obtain ⟨x', hx', hxx'⟩ := infEDist_lt_iff.mp hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x y : α
hy : infEDist y s ≤ (↑ε : ℝ≥0∞)
δ : ℝ≥0
hδ : 0 < δ
h : ediam s + 2 * (↑ε : ℝ≥0∞) < ∞
hε : (↑ε : ℝ≥0∞) < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
hx : infEDist x s < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
x' : α
hx' : x' ∈ s
hxx' : edist x x' < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
⊢ (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + (infEDist y s + ediam s) ≤ (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + ((↑ε : ℝ≥0∞) + ediam s)
have grw : (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + ((↑ε : ℝ≥0∞) + ediam s) ≤ (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + ((↑ε : ℝ≥0∞) + ediam s)
Tactic: grw [hy]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x y : α
hy : infEDist y s ≤ (↑ε : ℝ≥0∞)
δ : ℝ≥0
hδ : 0 < δ
h : ediam s + 2 * (↑ε : ℝ≥0∞) < ∞
hε : (↑ε : ℝ≥0∞) < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
hx : infEDist x s < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
x' : α
hx' : x' ∈ s
hxx' : edist x x' < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
⊢ (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + ((↑ε : ℝ≥0∞) + ediam s) = ediam s + 2 * (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
have rw : (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + ((↑ε : ℝ≥0∞) + ediam s) = ediam s + ((↑ε : ℝ≥0∞) + (↑ε : ℝ≥0∞)) + (↑δ : ℝ≥0∞)
Tactic: rw [two_mul]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x y : α
hy : infEDist y s ≤ (↑ε : ℝ≥0∞)
δ : ℝ≥0
hδ : 0 < δ
h : ediam s + 2 * (↑ε : ℝ≥0∞) < ∞
hε : (↑ε : ℝ≥0∞) < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
hx : infEDist x s < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
x' : α
hx' : x' ∈ s
hxx' : edist x x' < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
⊢ edist x y ≤ ediam s + 2 * (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
have edist : (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + (infEDist y s + ediam s) ≤ (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + ((↑ε : ℝ≥0∞) + ediam s)
Tactic: calc
    edist x y ≤ edist x x' + edist y x' := edist_triangle_right _ _ _
    _ ≤ ε + δ + (infEDist y s + ediam s) :=
      add_le_add hxx'.le (edist_le_infEDist_add_ediam hx')
    _ ≤ ε + δ + (ε + ediam s) := by grw [hy]
    _ = _ := by rw [two_mul]; ac_rfl
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
ε : ℝ≥0
x y : α
hy : infEDist y s ≤ (↑ε : ℝ≥0∞)
δ : ℝ≥0
hδ : 0 < δ
h : ediam s + 2 * (↑ε : ℝ≥0∞) < ∞
hε : (↑ε : ℝ≥0∞) < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
hx : infEDist x s < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
x' : α
hx' : x' ∈ s
hxx' : EDist.edist x x' < (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
edist : (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + (infEDist y s + ediam s) ≤ (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + ((↑ε : ℝ≥0∞) + ediam s)
⊢ EDist.edist x y ≤ ediam s + 2 * (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
have edist₁ : (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞) + ((↑ε : ℝ≥0∞) + ediam s) = ediam s + 2 * (↑ε : ℝ≥0∞) + (↑δ : ℝ≥0∞)
Tactic: calc
    edist x y ≤ edist x x' + edist y x' := edist_triangle_right _ _ _
    _ ≤ ε + δ + (infEDist y s + ediam s) :=
      add_le_add hxx'.le (edist_le_infEDist_add_ediam hx')
    _ ≤ ε + δ + (ε + ediam s) := by grw [hy]
    _ = _ := by rw [two_mul]; ac_rfl
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
ε : ℝ
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
⊢ diam (cthickening ε s) ≤ diam s + 2 * ε
have lift : ∀ (ε : ℝ≥0), diam (cthickening (↑ε : ℝ) s) ≤ diam s + 2 * (↑ε : ℝ)
Tactic: lift ε to ℝ≥0 using hε
Cleared hypotheses: ε, hε
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
⊢ diam (cthickening (↑ε : ℝ) s) ≤ diam s + 2 * (↑ε : ℝ)
have refine_1 : ediam s = ∞ → ediam (cthickening (↑ε : ℝ) s) = ∞
Tactic: refine (toReal_le_add' (ediam_cthickening_le _) ?_ ?_).trans_eq ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
refine_1 : ediam s = ∞ → ediam (cthickening (↑ε : ℝ) s) = ∞
⊢ diam (cthickening (↑ε : ℝ) s) ≤ diam s + 2 * (↑ε : ℝ)
have refine_2 : 2 * (↑ε : ℝ≥0∞) = ∞ → ediam (cthickening (↑ε : ℝ) s) = ∞
Tactic: refine (toReal_le_add' (ediam_cthickening_le _) ?_ ?_).trans_eq ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
ε : ℝ≥0
refine_1 : ediam s = ∞ → ediam (cthickening (↑ε : ℝ) s) = ∞
refine_2 : 2 * (↑ε : ℝ≥0∞) = ∞ → ediam (cthickening (↑ε : ℝ) s) = ∞
⊢ diam (cthickening (↑ε : ℝ) s) ≤ diam s + 2 * (↑ε : ℝ)
have refine_3 : (ediam s).toReal + (2 * (↑ε : ℝ≥0∞)).toReal = diam s + 2 * (↑ε : ℝ)
Tactic: refine (toReal_le_add' (ediam_cthickening_le _) ?_ ?_).trans_eq ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
ε : ℝ
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
⊢ diam (thickening ε s) ≤ diam s + 2 * ε
have pos : ∀ (hs : Bornology.IsBounded s), diam (thickening ε s) ≤ diam s + 2 * ε
Tactic: by_cases hs : IsBounded s
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
ε : ℝ
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
pos : ∀ (hs : Bornology.IsBounded s), diam (thickening ε s) ≤ diam s + 2 * ε
⊢ diam (thickening ε s) ≤ diam s + 2 * ε
have neg : ∀ (hs : ¬Bornology.IsBounded s), diam (thickening ε s) ≤ diam s + 2 * ε
Tactic: by_cases hs : IsBounded s
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
ε : ℝ
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
hs : ¬Bornology.IsBounded s
⊢ diam (thickening ε s) ≤ diam s + 2 * ε
have neg : ∀ (hε : LE.le (α := ℝ) 0 0), diam (thickening 0 s) ≤ diam s + HMul.hMul (α := ℝ) 2 0
Tactic: obtain rfl | hε := hε.eq_or_lt
Cleared hypotheses: ε, hε
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
ε : ℝ
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
hε : 0 ≤ ε
hs : ¬Bornology.IsBounded s
neg : ∀ (hε : LE.le (α := ℝ) 0 0), diam (thickening 0 s) ≤ diam s + HMul.hMul (α := ℝ) 2 0
⊢ diam (thickening ε s) ≤ diam s + 2 * ε
have neg₁ : ∀ (hε : 0 < ε), diam (thickening ε s) ≤ diam s + 2 * ε
Tactic: obtain rfl | hε := hε.eq_or_lt
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
ε : ℝ
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
hε_1 : 0 ≤ ε
hs : ¬Bornology.IsBounded s
hε : 0 < ε
⊢ diam (thickening ε s) ≤ diam s + 2 * ε
have neg : 0 ≤ diam s + 2 * ε
Tactic: rw [diam_eq_zero_of_unbounded (mt (IsBounded.subset · <| self_subset_thickening hε _) hs)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε : ℝ
s : Set α
⊢ thickening ε s = ∅ ↔ ε ≤ 0 ∨ s = ∅
have inl : ∀ (hε : 0 < ε), thickening ε s = ∅ ↔ ε ≤ 0 ∨ s = ∅
Tactic: obtain hε | hε := lt_or_ge 0 ε
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
ε : ℝ
s : Set α
inl : ∀ (hε : 0 < ε), thickening ε s = ∅ ↔ ε ≤ 0 ∨ s = ∅
⊢ thickening ε s = ∅ ↔ ε ≤ 0 ∨ s = ∅
have inr : ∀ (hε : ε ≤ 0), thickening ε s = ∅ ↔ ε ≤ 0 ∨ s = ∅
Tactic: obtain hε | hε := lt_or_ge 0 ε
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
⊢ ∃ (δ : ℝ), 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t)
have obtain : ∀ (r : ℝ≥0) (hr : 0 < r) (h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y),
  ∃ (δ : ℝ), 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t)
Tactic: obtain ⟨r, hr, h⟩ := exists_pos_forall_lt_edist hs ht hst
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
⊢ ∃ (δ : ℝ), 0 < δ ∧ Disjoint (thickening δ s) (thickening δ t)
have refine : Disjoint (thickening ((↑r : ℝ) / 2) s) (thickening ((↑r : ℝ) / 2) t)
Tactic: refine ⟨r / 2, half_pos (NNReal.coe_pos.2 hr), ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
⊢ Disjoint (thickening ((↑r : ℝ) / 2) s) (thickening ((↑r : ℝ) / 2) t)
have rw : thickening ((↑r : ℝ) / 2) s ⊓ thickening ((↑r : ℝ) / 2) t ≤ ⊥
Tactic: rw [disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z : α
hzs : z ∈ thickening ((↑r : ℝ) / 2) s
hzt : z ∈ thickening ((↑r : ℝ) / 2) t
⊢ Membership.mem (γ := Set α) ⊥ z
have hzs₁ : ∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal ((↑r : ℝ) / 2)
Tactic: rw [mem_thickening_iff_exists_edist_lt] at hzs hzt
Cleared hypotheses: hzs, hzt
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z : α
hzs : z ∈ thickening ((↑r : ℝ) / 2) s
hzt : z ∈ thickening ((↑r : ℝ) / 2) t
hzs₁ : ∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal ((↑r : ℝ) / 2)
⊢ Membership.mem (γ := Set α) ⊥ z
have hzt₁ : ∃ z_1 ∈ t, edist z z_1 < ENNReal.ofReal ((↑r : ℝ) / 2)
Tactic: rw [mem_thickening_iff_exists_edist_lt] at hzs hzt
Cleared hypotheses: hzs, hzt
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z : α
hzs : ∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal ((↑r : ℝ) / 2)
hzt : ∃ z_1 ∈ t, edist z z_1 < ENNReal.ofReal ((↑r : ℝ) / 2)
⊢ Membership.mem (γ := Set α) ⊥ z
have hzs₁ : ∃ z_1 ∈ s, edist z z_1 < (↑(r / 2) : ℝ≥0∞)
Tactic: rw [← NNReal.coe_two, ← NNReal.coe_div, ENNReal.ofReal_coe_nnreal] at hzs hzt
Cleared hypotheses: hzs, hzt
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z : α
hzs : ∃ z_1 ∈ s, edist z z_1 < ENNReal.ofReal ((↑r : ℝ) / 2)
hzt : ∃ z_1 ∈ t, edist z z_1 < ENNReal.ofReal ((↑r : ℝ) / 2)
hzs₁ : ∃ z_1 ∈ s, edist z z_1 < (↑(r / 2) : ℝ≥0∞)
⊢ Membership.mem (γ := Set α) ⊥ z
have hzt₁ : ∃ z_1 ∈ t, edist z z_1 < (↑(r / 2) : ℝ≥0∞)
Tactic: rw [← NNReal.coe_two, ← NNReal.coe_div, ENNReal.ofReal_coe_nnreal] at hzs hzt
Cleared hypotheses: hzs, hzt
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z : α
hzs : ∃ z_1 ∈ s, edist z z_1 < (↑(r / 2) : ℝ≥0∞)
hzt : ∃ z_1 ∈ t, edist z z_1 < (↑(r / 2) : ℝ≥0∞)
⊢ Membership.mem (γ := Set α) ⊥ z
have obtain : ∀ (x : α) (hx : x ∈ s) (hzx : edist z x < (↑(r / 2) : ℝ≥0∞)), Membership.mem (γ := Set α) ⊥ z
Tactic: obtain ⟨x, hx, hzx⟩ := hzs
Cleared hypotheses: hzs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z : α
hzt : ∃ z_1 ∈ t, edist z z_1 < (↑(r / 2) : ℝ≥0∞)
x : α
hx : x ∈ s
hzx : edist z x < (↑(r / 2) : ℝ≥0∞)
⊢ Membership.mem (γ := Set α) ⊥ z
have obtain : ∀ (y : α) (hy : y ∈ t) (hzy : edist z y < (↑(r / 2) : ℝ≥0∞)), Membership.mem (γ := Set α) ⊥ z
Tactic: obtain ⟨y, hy, hzy⟩ := hzt
Cleared hypotheses: hzt
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < (↑(r / 2) : ℝ≥0∞)
y : α
hy : y ∈ t
hzy : edist z y < (↑(r / 2) : ℝ≥0∞)
⊢ Membership.mem (γ := Set α) ⊥ z
have refine : edist x y ≤ (↑r : ℝ≥0∞)
Tactic: refine (h x hx y hy).not_ge ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < (↑(r / 2) : ℝ≥0∞)
y : α
hy : y ∈ t
hzy : edist z y < (↑(r / 2) : ℝ≥0∞)
⊢ (↑(r / 2) : ℝ≥0∞) + (↑(r / 2) : ℝ≥0∞) = (↑r : ℝ≥0∞)
have rw : (↑(r / 2 + r / 2) : ℝ≥0∞) = (↑r : ℝ≥0∞)
Tactic: rw [← ENNReal.coe_add, add_halves]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
s t : Set α
hst : Disjoint s t
hs : IsCompact s
ht : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] t
r : ℝ≥0
hr : 0 < r
h : ∀ x ∈ s, ∀ y ∈ t, (↑r : ℝ≥0∞) < edist x y
z x : α
hx : x ∈ s
hzx : edist z x < (↑(r / 2) : ℝ≥0∞)
y : α
hy : y ∈ t
hzy : edist z y < (↑(r / 2) : ℝ≥0∞)
rw : (↑(r / 2 + r / 2) : ℝ≥0∞) = (↑r : ℝ≥0∞)
⊢ (↑(r / 2) : ℝ≥0∞) + (↑(r / 2) : ℝ≥0∞) = (↑r : ℝ≥0∞)
have rw₁ : (↑r : ℝ≥0∞) = (↑r : ℝ≥0∞)
Tactic: rw [← ENNReal.coe_add, add_halves]