awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
f : α → β
E : Set α
x : α
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    (thickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
have pos : ∀ (x_mem_closure : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E),
  ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    (thickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
Tactic: by_cases x_mem_closure : x ∈ closure E
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
f : α → β
E : Set α
x : α
pos :
  ∀ (x_mem_closure : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E),
    ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
      (thickening δ E).mulIndicator f x =
        (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    (thickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
have neg : ∀ (x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E),
  ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    (thickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
Tactic: by_cases x_mem_closure : x ∈ closure E
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    (thickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
have h : ∀ (δ : ℝ) (δ_pos : Membership.mem (γ := Set ℝ) (Ioi 0) δ),
  (thickening δ E).mulIndicator f x = (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
Tactic: filter_upwards [self_mem_nhdsWithin] with δ δ_pos
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    (thickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
have obs : ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ thickening δ E
Tactic: have obs := eventually_notMem_thickening_of_infEDist_pos x_mem_closure
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
obs : ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ thickening δ E
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    (thickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
have h : ∀ (δ : ℝ) (x_notin_thE : x ∉ thickening δ E),
  Membership.mem (γ := Set ℝ) (Ioi 0) δ →
    (thickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
Tactic: filter_upwards [mem_nhdsWithin_of_mem_nhds obs, self_mem_nhdsWithin]
      with δ x_notin_thE _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
f : α → β
E : Set α
x : α
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0,
    (cthickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
have pos : ∀ (x_mem_closure : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E),
  ∀ᶠ (δ : ℝ) in 𝓝 0,
    (cthickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
Tactic: by_cases x_mem_closure : x ∈ closure E
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
f : α → β
E : Set α
x : α
pos :
  ∀ (x_mem_closure : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E),
    ∀ᶠ (δ : ℝ) in 𝓝 0,
      (cthickening δ E).mulIndicator f x =
        (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0,
    (cthickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
have neg : ∀ (x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E),
  ∀ᶠ (δ : ℝ) in 𝓝 0,
    (cthickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
Tactic: by_cases x_mem_closure : x ∈ closure E
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0,
    (cthickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
have h : ∀ (δ : ℝ),
  Membership.mem (γ := Set ℝ) univ δ →
    (cthickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
Tactic: filter_upwards [univ_mem] with δ _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
δ : ℝ
h : Membership.mem (γ := Set ℝ) univ δ
⊢ (cthickening δ E).mulIndicator f x =
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
have obs : x ∈ cthickening δ E
Tactic: have obs : x ∈ cthickening δ E := closure_subset_cthickening δ E x_mem_closure
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
δ : ℝ
h : Membership.mem (γ := Set ℝ) univ δ
obs : x ∈ cthickening δ E
⊢ (cthickening δ E).mulIndicator f x =
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
have h : f x = (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
Tactic: rw [mulIndicator_of_mem obs f, mulIndicator_of_mem x_mem_closure f]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
δ : ℝ
h_1 : Membership.mem (γ := Set ℝ) univ δ
obs : x ∈ cthickening δ E
h : f x = (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
⊢ (cthickening δ E).mulIndicator f x =
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
have h₁ : f x = f x
Tactic: rw [mulIndicator_of_mem obs f, mulIndicator_of_mem x_mem_closure f]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
f : α → β
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0,
    (cthickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
have h : ∀ (δ : ℝ) (hδ : x ∉ cthickening δ E),
  (cthickening δ E).mulIndicator f x =
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
Tactic: filter_upwards [eventually_notMem_cthickening_of_infEDist_pos x_mem_closure] with δ hδ
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
inst_2 : TopologicalSpace β
f : α → β
E : Set α
⊢ Tendsto (fun (δ : ℝ) ↦ (thickening δ E).mulIndicator f) (𝓝[>] 0)
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f))
have rw : ∀ (x : α),
  Tendsto (fun (i : ℝ) ↦ (thickening i E).mulIndicator f x) (𝓝[>] 0)
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x))
Tactic: rw [tendsto_pi_nhds]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
inst_2 : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun (i : ℝ) ↦ (thickening i E).mulIndicator f x) (𝓝[>] 0)
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x))
have rw : Tendsto (fun (x_1 : ℝ) ↦ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x) (𝓝[>] 0)
  (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x))
Tactic: rw [tendsto_congr' (mulIndicator_thickening_eventually_eq_mulIndicator_closure f E x)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
inst_2 : TopologicalSpace β
f : α → β
E : Set α
⊢ Tendsto (fun (δ : ℝ) ↦ (cthickening δ E).mulIndicator f) (𝓝 0)
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f))
have rw : ∀ (x : α),
  Tendsto (fun (i : ℝ) ↦ (cthickening i E).mulIndicator f x) (𝓝 0)
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x))
Tactic: rw [tendsto_pi_nhds]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
inst_2 : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun (i : ℝ) ↦ (cthickening i E).mulIndicator f x) (𝓝 0)
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x))
have rw : Tendsto (fun (x_1 : ℝ) ↦ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x) (𝓝 0)
  (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x))
Tactic: rw [tendsto_congr' (mulIndicator_cthickening_eventually_eq_mulIndicator_closure f E x)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ thickening δ E
have obtain : ∀ (ε : ℝ) (ε_pos : 0 < ε) (ε_lt : ENNReal.ofReal ε < infEDist x E), ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ thickening δ E
Tactic: obtain ⟨ε, ⟨ε_pos, ε_lt⟩⟩ := exists_real_pos_lt_infEDist_of_notMem_closure h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ thickening δ E
have h₁ : ∀ (δ : ℝ) (hδ : δ < ε), x ∉ thickening δ E
Tactic: filter_upwards [eventually_lt_nhds ε_pos] with δ hδ
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
δ : ℝ
hδ : δ < ε
⊢ x ∉ thickening δ E
have h₁ : ENNReal.ofReal δ ≤ infEDist x E
Tactic: simp only [thickening, mem_setOf_eq, not_lt]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
A : Set α
⊢ Pairwise (α := ℝ) (Function.onFun.{1, u + 1, 1} (β := Set α) Disjoint fun (r : ℝ) ↦ frontier (thickening r A))
have refine : ∀ (r₁ r₂ : ℝ) (hr : r₁ < r₂), Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))
Tactic: refine (pairwise_disjoint_on _).2 fun r₁ r₂ hr => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))
have inl : ∀ (h₁ : r₁ ≤ 0), Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))
Tactic: rcases le_total r₁ 0 with h₁ | h₁
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
inl : ∀ (h₁ : r₁ ≤ 0), Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))
have inr : ∀ (h₁ : 0 ≤ r₁), Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))
Tactic: rcases le_total r₁ 0 with h₁ | h₁
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
⊢ Disjoint (frontier (thickening r₁ A)) (frontier (thickening r₂ A))
have inr : ∀ (h : ENNReal.ofReal r₁ = ENNReal.ofReal r₂), r₁ = r₂
Tactic: refine ((disjoint_singleton.2 fun h => hr.ne ?_).preimage _).mono (frontier_thickening_subset _)
    (frontier_thickening_subset _)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
h : ENNReal.ofReal r₁ = ENNReal.ofReal r₂
⊢ r₁ = r₂
have h₂ : (ENNReal.ofReal r₁).toReal = (ENNReal.ofReal r₂).toReal
Tactic: apply_fun ENNReal.toReal at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
h : (ENNReal.ofReal r₁).toReal = (ENNReal.ofReal r₂).toReal
⊢ r₁ = r₂
have inr : ∀ (h : r₁ = (ENNReal.ofReal r₂).toReal), r₁ = r₂
Tactic: rwa [ENNReal.toReal_ofReal h₁, ENNReal.toReal_ofReal (h₁.trans hr.le)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
A : Set α
r₁ r₂ : ℝ
hr : r₁ < r₂
h₁ : 0 ≤ r₁
h : (ENNReal.ofReal r₁).toReal = (ENNReal.ofReal r₂).toReal
inr : ∀ (h : r₁ = (ENNReal.ofReal r₂).toReal), r₁ = r₂
⊢ r₁ = r₂
have inr₁ : ∀ (h : r₁ = r₂), r₁ = r₂
Tactic: rwa [ENNReal.toReal_ofReal h₁, ENNReal.toReal_ofReal (h₁.trans hr.le)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
⊢ x ∈ (thickening δ (thickening δ E)ᶜ)ᶜ
have simp : ENNReal.ofReal δ ≤ infEDist x {x : α | infEDist x E < ENNReal.ofReal δ}ᶜ
Tactic: simp only [thickening, mem_compl_iff, mem_setOf_eq, not_lt]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
⊢ ENNReal.ofReal δ ≤ infEDist x {x : α | infEDist x E < ENNReal.ofReal δ}ᶜ
have apply : ∀ (y : α) (hy : Membership.mem (γ := Set α) {x : α | infEDist x E < ENNReal.ofReal δ}ᶜ y), ENNReal.ofReal δ ≤ edist x y
Tactic: apply le_infEDist.mpr fun y hy ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
y : α
hy : Membership.mem (γ := Set α) {x : α | infEDist x E < ENNReal.ofReal δ}ᶜ y
⊢ ENNReal.ofReal δ ≤ edist x y
have hy₁ : ENNReal.ofReal δ ≤ infEDist y E
Tactic: simp only [mem_compl_iff, mem_setOf_eq, not_lt] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ thickening δ (thickening δ E)ᶜ ⊆ Eᶜ
have apply : Eᶜᶜ ⊆ (thickening δ (thickening δ E)ᶜ)ᶜ
Tactic: apply compl_subset_compl.mp
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
δ : ℝ
X : Type u
inst : PseudoMetricSpace X
E : Set X
x z : X
⊢ edist x z < ENNReal.ofReal δ ↔ dist x z < δ
have rw : edist x z < ENNReal.ofReal δ ↔ (edist x z).toReal < δ
Tactic: rw [dist_edist, lt_ofReal_iff_toReal_lt (edist_ne_top _ _)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
δ : ℝ
X : Type u
inst : PseudoMetricSpace X
E : Set X
x z : X
rw : edist x z < ENNReal.ofReal δ ↔ (edist x z).toReal < δ
⊢ edist x z < ENNReal.ofReal δ ↔ dist x z < δ
have rw₁ : (edist x z).toReal < δ ↔ (edist x z).toReal < δ
Tactic: rw [dist_edist, lt_ofReal_iff_toReal_lt (edist_ne_top _ _)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (hypothesis)
Goal:
δ : ℝ
X : Type u
inst : PseudoMetricSpace X
E : Set X
x : X
⊢ x ∈ thickening δ E ↔ ∃ z ∈ E, dist x z < δ
have key_iff : ∀ (z : X), edist x z < ENNReal.ofReal δ ↔ dist x z < δ
Tactic: have key_iff : ∀ z : X, edist x z < ENNReal.ofReal δ ↔ dist x z < δ := fun z ↦ by
    rw [dist_edist, lt_ofReal_iff_toReal_lt (edist_ne_top _ _)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
δ : ℝ
X : Type u
inst : PseudoMetricSpace X
E : Set X
x : X
key_iff : ∀ (z : X), edist x z < ENNReal.ofReal δ ↔ dist x z < δ
⊢ x ∈ thickening δ E ↔ ∃ z ∈ E, dist x z < δ
have simp_rw : (∃ z ∈ E, edist x z < ENNReal.ofReal δ) ↔ ∃ z ∈ E, dist x z < δ
Tactic: simp_rw [mem_thickening_iff_exists_edist_lt, key_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
x : X
⊢ thickening δ {x} = ball x δ
have h : ∀ (x_1 : X), Membership.mem (γ := Set X) (thickening δ {x}) x_1 ↔ x_1 ∈ ball x δ
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
E : Set X
⊢ thickening δ E = ⋃ x ∈ E, ball x δ
have h : ∀ (x : X), x ∈ thickening δ E ↔ Membership.mem (γ := Set X) (⋃ x ∈ E, ball x δ) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
E : Set X
x : X
⊢ x ∈ thickening δ E ↔ Membership.mem (γ := Set X) (⋃ x ∈ E, ball x δ) x
have h : x ∈ thickening δ E ↔ ∃ i ∈ E, x ∈ ball i δ
Tactic: simp only [mem_iUnion₂, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bornology.IsBounded E
⊢ Bornology.IsBounded (thickening δ E)
have inl : ∀ (h : Bornology.IsBounded.{u} (α := X) ∅), Bornology.IsBounded.{u} (α := X) (thickening δ ∅)
Tactic: rcases E.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
Cleared hypotheses: E, h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bornology.IsBounded E
inl : ∀ (h : Bornology.IsBounded.{u} (α := X) ∅), Bornology.IsBounded.{u} (α := X) (thickening δ ∅)
⊢ Bornology.IsBounded (thickening δ E)
have inr : ∀ (x : X) (hx : x ∈ E), Bornology.IsBounded (thickening δ E)
Tactic: rcases E.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bornology.IsBounded E
x : X
hx : x ∈ E
⊢ Bornology.IsBounded (thickening δ E)
have inr : ∀ (y : X) (hy : y ∈ thickening δ E), y ∈ closedBall x (δ + diam E)
Tactic: refine (isBounded_iff_subset_closedBall x).2 ⟨δ + diam E, fun y hy ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bornology.IsBounded E
x : X
hx : x ∈ E
y : X
hy : y ∈ thickening δ E
⊢ infDist y E + diam E ≤ δ + diam E
have grw : δ + diam E ≤ δ + diam E
Tactic: grw [(mem_thickening_iff_infDist_lt ⟨x, hx⟩).1 hy]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
X : Type u
inst : PseudoMetricSpace X
δ : ℝ
E : Set X
h : Bornology.IsBounded E
x : X
hx : x ∈ E
y : X
hy : y ∈ thickening δ E
⊢ y ∈ closedBall x (δ + diam E)
have dist : infDist y E + diam E ≤ δ + diam E
Tactic: calc
      dist y x ≤ infDist y E + diam E := dist_le_infDist_add_diam (x := y) h hx
      _ ≤ δ + diam E := by grw [(mem_thickening_iff_infDist_lt ⟨x, hx⟩).1 hy]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ cthickening δ E
have obtain : ∀ (ε : ℝ) (ε_pos : 0 < ε) (ε_lt : ENNReal.ofReal ε < infEDist x E), ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ cthickening δ E
Tactic: obtain ⟨ε, ⟨ε_pos, ε_lt⟩⟩ := exists_real_pos_lt_infEDist_of_notMem_closure h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ cthickening δ E
have h₁ : ∀ (δ : ℝ) (hδ : δ < ε), x ∉ cthickening δ E
Tactic: filter_upwards [eventually_lt_nhds ε_pos] with δ hδ
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
δ : ℝ
hδ : δ < ε
⊢ x ∉ cthickening δ E
have h₁ : ENNReal.ofReal δ < infEDist x E
Tactic: simp only [cthickening, mem_setOf_eq, not_le]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x y : α
δ : ℝ
E : Set α
h : y ∈ E
h' : dist x y ≤ δ
⊢ x ∈ cthickening δ E
have apply : edist x y ≤ ENNReal.ofReal δ
Tactic: apply mem_cthickening_of_edist_le x y δ E h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x y : α
δ : ℝ
E : Set α
h : y ∈ E
h' : dist x y ≤ δ
⊢ edist x y ≤ ENNReal.ofReal δ
have rw : ENNReal.ofReal (dist x y) ≤ ENNReal.ofReal δ
Tactic: rw [edist_dist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
hδ : δ ≤ 0
E : Set α
⊢ cthickening δ E = closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
have h : ∀ (x : α), x ∈ cthickening δ E ↔ x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ cthickening (max 0 δ) E = cthickening δ E
have inl : δ ≤ 0 → cthickening (max 0 δ) E = cthickening δ E
Tactic: cases le_total δ 0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
inl : δ ≤ 0 → cthickening (max 0 δ) E = cthickening δ E
⊢ cthickening (max 0 δ) E = cthickening δ E
have inr : 0 ≤ δ → cthickening (max 0 δ) E = cthickening δ E
Tactic: cases le_total δ 0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
δ : ℝ
hδ : 0 ≤ δ
⊢ cthickening δ {x} = closedBall x δ
have h : ∀ (y : α), Membership.mem (γ := Set α) (cthickening δ {x}) y ↔ y ∈ closedBall x δ
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
δ : ℝ
⊢ closedBall x δ ⊆ cthickening δ {x}
have inl : ∀ (hδ : δ < 0), closedBall x δ ⊆ cthickening δ {x}
Tactic: rcases lt_or_ge δ 0 with (hδ | hδ)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Thickening (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
δ : ℝ
inl : ∀ (hδ : δ < 0), closedBall x δ ⊆ cthickening δ {x}
⊢ closedBall x δ ⊆ cthickening δ {x}
have inr : ∀ (hδ : 0 ≤ δ), closedBall x δ ⊆ cthickening δ {x}
Tactic: rcases lt_or_ge δ 0 with (hδ | hδ)