awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
r : ℝ
hr : 0 ≤ r
rw :
  closedBall x r =
    Set.image (α := X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) : (a : X) → Snowflaking X α hα₀ hα₁)
      (closedBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (r ^ α⁻¹) : Set X)
rw₁ :
  closedBall x r =
    closedBall
      ((toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x : X))
      ((r ^ α⁻¹) ^ α)
rw₂ : closedBall x r = closedBall x ((r ^ α⁻¹) ^ α)
⊢ Eq (α := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' closedBall x r : Set X)
    (closedBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (r ^ α⁻¹) : Set X)
have rw₃ : closedBall x r = closedBall x r
Tactic: rw [toSnowflaking.preimage_eq_iff_eq_image, image_toSnowflaking_closedBall _ (by positivity),
    toSnowflaking_ofSnowflaking, Real.rpow_inv_rpow hr hα₀.ne']
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
r : ℝ
hr : 0 ≤ r
⊢ Eq (α := Set X) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) '' closedBall x r : Set X)
    (closedBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (r ^ α⁻¹) : Set X)
have rw : Eq (α := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' closedBall x r : Set X)
  (closedBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (r ^ α⁻¹) : Set X)
Tactic: rw [image_ofSnowflaking_eq_preimage, preimage_toSnowflaking_closedBall _ hr]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Snowflaking (goal)
Goal:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
r : ℝ
hr : 0 ≤ r
rw :
  Eq (α := Set X) ((⇑toSnowflaking : (a : X) → Snowflaking X α hα₀ hα₁) ⁻¹' closedBall x r : Set X)
    (closedBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (r ^ α⁻¹) : Set X)
⊢ Eq (α := Set X) ((⇑ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) '' closedBall x r : Set X)
    (closedBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (r ^ α⁻¹) : Set X)
have rw₁ : Eq (α := Set X) (closedBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (r ^ α⁻¹) : Set X)
  (closedBall ((ofSnowflaking : (a : Snowflaking X α hα₀ hα₁) → X) x) (r ^ α⁻¹) : Set X)
Tactic: rw [image_ofSnowflaking_eq_preimage, preimage_toSnowflaking_closedBall _ hr]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : (x : α) → ℝ≥0 × ℝ≥0∞ := fun (x : α) ↦ (1, infEDist x E / ENNReal.ofReal δ)
sub : (p : ℝ≥0 × ℝ≥0∞) → ℝ≥0∞ := fun (p : ℝ≥0 × ℝ≥0∞) ↦ (↑p.1 : ℝ≥0∞) - p.2
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : α) ↦ 1 - infEDist x E / ENNReal.ofReal δ
have rw : Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] (sub ∘ f)
Tactic: rw [show (fun x : α => (1 : ℝ≥0∞) - infEDist x E / ENNReal.ofReal δ) = sub ∘ f by rfl]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : (x : α) → ℝ≥0 × ℝ≥0∞ := fun (x : α) ↦ (1, infEDist x E / ENNReal.ofReal δ)
sub : (p : ℝ≥0 × ℝ≥0∞) → ℝ≥0∞ := fun (p : ℝ≥0 × ℝ≥0∞) ↦ (↑p.1 : ℝ≥0∞) - p.2
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] (sub ∘ f)
have apply : Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : α) ↦ (f x).2
Tactic: apply (@ENNReal.continuous_nnreal_sub 1).comp
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
f : (x : α) → ℝ≥0 × ℝ≥0∞ := fun (x : α) ↦ (1, infEDist x E / ENNReal.ofReal δ)
sub : (p : ℝ≥0 × ℝ≥0∞) → ℝ≥0∞ := fun (p : ℝ≥0 × ℝ≥0∞) ↦ (↑p.1 : ℝ≥0∞) - p.2
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : α) ↦ (f x).2
have apply : ENNReal.ofReal δ ≠ 0
Tactic: apply (ENNReal.continuous_div_const (ENNReal.ofReal δ) _).comp continuous_infEDist
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_mem : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ thickenedIndicatorAux δ E x = 1
have rw : thickenedIndicatorAux δ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E) x = 1
Tactic: rw [← thickenedIndicatorAux_closure_eq, thickenedIndicatorAux_one δ (closure E) x_mem]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_mem : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
rw : thickenedIndicatorAux δ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E) x = 1
⊢ thickenedIndicatorAux δ E x = 1
have rw₁ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [← thickenedIndicatorAux_closure_eq, thickenedIndicatorAux_one δ (closure E) x_mem]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : x ∉ thickening δ E
⊢ thickenedIndicatorAux δ E x = 0
have x_out₁ : ENNReal.ofReal δ ≤ infEDist x E
Tactic: rw [thickening, mem_setOf_eq, not_lt] at x_out
Cleared hypotheses: x_out
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEDist x E
⊢ 1 - infEDist x E / ENNReal.ofReal δ = 0
have apply : 1 - infEDist x E / ENNReal.ofReal δ ≤ ⊥
Tactic: apply le_antisymm _ bot_le
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEDist x E
⊢ 1 - infEDist x E / ENNReal.ofReal δ ≤ ⊥
have key : 1 - infEDist x E / ENNReal.ofReal δ ≤ 1 - ENNReal.ofReal δ / ENNReal.ofReal δ
Tactic: have key := tsub_le_tsub
    (@rfl _ (1 : ℝ≥0∞)).le (ENNReal.div_le_div x_out (@rfl _ (ENNReal.ofReal δ : ℝ≥0∞)).le)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEDist x E
key : 1 - infEDist x E / ENNReal.ofReal δ ≤ 1 - ENNReal.ofReal δ / ENNReal.ofReal δ
⊢ 1 - infEDist x E / ENNReal.ofReal δ ≤ ⊥
have key₁ : 1 - infEDist x E / ENNReal.ofReal δ ≤ HSub.hSub (α := ℝ≥0∞) 1 1
Tactic: rw [ENNReal.div_self (ne_of_gt (ENNReal.ofReal_pos.mpr δ_pos)) ofReal_ne_top] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
a : α
⊢ E.indicator (fun (x : α) ↦ 1) a ≤ thickenedIndicatorAux δ E a
have pos : ∀ (h : a ∈ E), E.indicator (fun (x : α) ↦ 1) a ≤ thickenedIndicatorAux δ E a
Tactic: by_cases h : a ∈ E
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
a : α
pos : ∀ (h : a ∈ E), E.indicator (fun (x : α) ↦ 1) a ≤ thickenedIndicatorAux δ E a
⊢ E.indicator (fun (x : α) ↦ 1) a ≤ thickenedIndicatorAux δ E a
have neg : ∀ (h : a ∉ E), E.indicator (fun (x : α) ↦ 1) a ≤ thickenedIndicatorAux δ E a
Tactic: by_cases h : a ∈ E
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ 1 - infEDist y E / ENNReal.ofReal δ ≤ 1 - infEDist x E / ENNReal.ofReal δ
have inl : ∀ (hle : infEDist x E / ENNReal.ofReal δ ≤ 1), 1 - infEDist y E / ENNReal.ofReal δ ≤ 1 - infEDist x E / ENNReal.ofReal δ
Tactic: rcases le_total (infEDist x E / ENNReal.ofReal δ) 1 with hle | hle
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
inl :
  ∀ (hle : infEDist x E / ENNReal.ofReal δ ≤ 1),
    1 - infEDist y E / ENNReal.ofReal δ ≤ 1 - infEDist x E / ENNReal.ofReal δ
⊢ 1 - infEDist y E / ENNReal.ofReal δ ≤ 1 - infEDist x E / ENNReal.ofReal δ
have inr : ∀ (hle : 1 ≤ infEDist x E / ENNReal.ofReal δ), 1 - infEDist y E / ENNReal.ofReal δ ≤ 1 - infEDist x E / ENNReal.ofReal δ
Tactic: rcases le_total (infEDist x E / ENNReal.ofReal δ) 1 with hle | hle
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
hle : infEDist x E / ENNReal.ofReal δ ≤ 1
⊢ 1 - infEDist y E / ENNReal.ofReal δ ≤ 1 - infEDist x E / ENNReal.ofReal δ
have inl : infEDist x E / ENNReal.ofReal δ ≤ infEDist y E / ENNReal.ofReal δ
Tactic: rw [ENNReal.sub_le_sub_iff_left hle (by simp)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
hle : 1 ≤ infEDist x E / ENNReal.ofReal δ
⊢ 1 - infEDist y E / ENNReal.ofReal δ ≤ 1 - infEDist x E / ENNReal.ofReal δ
have inr : 1 ≤ infEDist y E / ENNReal.ofReal δ
Tactic: rw [tsub_eq_zero_of_le hle, tsub_eq_zero_of_le]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
⊢ Tendsto (β := α → ℝ≥0∞) (fun (n : ℕ) ↦ thickenedIndicatorAux (δseq n) E) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator fun (x : α) ↦ 1))
have rw : ∀ (x : α),
  Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))
Tactic: rw [tendsto_pi_nhds]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))
have pos : ∀ (x_mem_closure : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E),
  Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) 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 α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
pos :
  ∀ (x_mem_closure : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E),
    Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))
have neg : ∀ (x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E),
  Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) 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 α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))
have pos : Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ 1) atTop
  (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))
Tactic: simp_rw [thickenedIndicatorAux_one_of_mem_closure _ E x_mem_closure]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ 1) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))
have pos : Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ 1) atTop (𝓝 1)
Tactic: rw [show (indicator (closure E) fun _ => (1 : ℝ≥0∞)) x = 1 by
        simp only [x_mem_closure, indicator_of_mem]]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))
have neg : Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
Tactic: rw [show (closure E).indicator (fun _ => (1 : ℝ≥0∞)) x = 0 by
        simp only [x_mem_closure, indicator_of_notMem, not_false_iff]]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
have neg : ∀ (ε : ℝ) (ε_pos : 0 < ε) (ε_lt : ENNReal.ofReal ε < infEDist x E),
  Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
Tactic: rcases exists_real_pos_lt_infEDist_of_notMem_closure x_mem_closure with ⟨ε, ⟨ε_pos, ε_lt⟩⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
have neg : ∀ (δseq_lim : ∀ ε > 0, ∀ᶠ (x : ℕ) in atTop, dist (δseq x) 0 < ε) (E : Set α) (x : α)
  (x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E) (ε : ℝ) (ε_pos : 0 < ε)
  (ε_lt : ENNReal.ofReal ε < infEDist x E),
  Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
Tactic: rw [Metric.tendsto_nhds] at δseq_lim
Cleared hypotheses: δseq_lim, E, x, x_mem_closure, ε, ε_pos, ε_lt
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : ∀ ε > 0, ∀ᶠ (x : ℕ) in atTop, dist (δseq x) 0 < ε
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
have δseq_lim₁ : ∀ᶠ (x : ℕ) in atTop, dist (δseq x) 0 < ε
Tactic: specialize δseq_lim ε ε_pos
Cleared hypotheses: δseq_lim
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
δseq_lim : ∀ᶠ (x : ℕ) in atTop, dist (δseq x) 0 < ε
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
have δseq_lim₁ : ∃ (a : ℕ), ∀ b ≥ a, |δseq b| < ε
Tactic: simp only [dist_zero_right, Real.norm_eq_abs, eventually_atTop] at δseq_lim
Cleared hypotheses: δseq_lim
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
δseq_lim : ∃ (a : ℕ), ∀ b ≥ a, |δseq b| < ε
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
have neg : ∀ (N : ℕ) (hN : ∀ b ≥ N, |δseq b| < ε),
  Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
Tactic: rcases δseq_lim with ⟨N, hN⟩
Cleared hypotheses: δseq_lim
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
N : ℕ
hN : ∀ b ≥ N, |δseq b| < ε
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
have neg : ∀ i ≥ N, thickenedIndicatorAux (δseq i) E x = 0
Tactic: apply tendsto_atTop_of_eventually_const (i₀ := N)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
N : ℕ
hN : ∀ b ≥ N, |δseq b| < ε
n : ℕ
n_large : n ≥ N
⊢ thickenedIndicatorAux (δseq n) E x = 0
have key : x ∉ thickening ε E
Tactic: have key : x ∉ thickening ε E := by simpa only [thickening, mem_setOf_eq, not_lt] using ε_lt.le
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
N : ℕ
hN : ∀ b ≥ N, |δseq b| < ε
n : ℕ
n_large : n ≥ N
key : x ∉ thickening ε E
⊢ thickenedIndicatorAux (δseq n) E x = 0
have neg : thickenedIndicatorAux (δseq n) E x ≤ 0
Tactic: refine le_antisymm ?_ bot_le
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
E : Set α
x : α
x_mem_closure : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
N : ℕ
hN : ∀ b ≥ N, |δseq b| < ε
n : ℕ
n_large : n ≥ N
key : x ∉ thickening ε E
⊢ thickenedIndicatorAux (δseq n) E x ≤ 0
have neg : thickenedIndicatorAux ε E x ≤ 0
Tactic: apply (thickenedIndicatorAux_mono (lt_of_abs_lt (hN n n_large)).le E x).trans
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : α) ↦
    (thickenedIndicatorAux δ E x).toNNReal
have apply : ∀ (x : α), Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | a ≠ ∞} (thickenedIndicatorAux δ E x)
Tactic: apply ContinuousOn.comp_continuous continuousOn_toNNReal
      (continuous_thickenedIndicatorAux δ_pos E)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ ∃ (C : ℝ), ∀ (x y : α), dist (thickenedIndicatorAux δ E x).toNNReal (thickenedIndicatorAux δ E y).toNNReal ≤ C
have h : ∀ (x y : α), dist (thickenedIndicatorAux δ E x).toNNReal (thickenedIndicatorAux δ E y).toNNReal ≤ 2
Tactic: use 2
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
⊢ |(↑(thickenedIndicatorAux δ E x).toNNReal : ℝ) - (↑(thickenedIndicatorAux δ E y).toNNReal : ℝ)| ≤ 2
have h : |(↑(thickenedIndicatorAux δ E x).toNNReal : ℝ)| + |(↑(thickenedIndicatorAux δ E y).toNNReal : ℝ)| ≤ 2
Tactic: apply (abs_sub _ _).trans
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
⊢ |(↑(thickenedIndicatorAux δ E x).toNNReal : ℝ)| + |(↑(thickenedIndicatorAux δ E y).toNNReal : ℝ)| ≤ 2
have h : (↑(thickenedIndicatorAux δ E x).toNNReal : ℝ) + (↑(thickenedIndicatorAux δ E y).toNNReal : ℝ) ≤ HAdd.hAdd (α := ℝ) 1 1
Tactic: rw [NNReal.abs_eq, NNReal.abs_eq, ← one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
⊢ (↑(thickenedIndicatorAux δ E x).toNNReal : ℝ) + (↑(thickenedIndicatorAux δ E y).toNNReal : ℝ) ≤ HAdd.hAdd (α := ℝ) 1 1
have key : ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1
Tactic: have key := @thickenedIndicatorAux_le_one _ _ δ E
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
key : ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1
⊢ (↑(thickenedIndicatorAux δ E x).toNNReal : ℝ) + (↑(thickenedIndicatorAux δ E y).toNNReal : ℝ) ≤ HAdd.hAdd (α := ℝ) 1 1
have h : (↑(thickenedIndicatorAux δ E x).toNNReal : ℝ) ≤ 1
Tactic: apply add_le_add
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
key : ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1
h : (↑(thickenedIndicatorAux δ E x).toNNReal : ℝ) ≤ 1
⊢ (↑(thickenedIndicatorAux δ E x).toNNReal : ℝ) + (↑(thickenedIndicatorAux δ E y).toNNReal : ℝ) ≤ HAdd.hAdd (α := ℝ) 1 1
have h₁ : (↑(thickenedIndicatorAux δ E y).toNNReal : ℝ) ≤ 1
Tactic: apply add_le_add
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_mem : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ Eq (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
have rw : (thickenedIndicatorAux δ E x).toNNReal = 1
Tactic: rw [thickenedIndicator_apply, thickenedIndicatorAux_one_of_mem_closure δ E x_mem, toNNReal_one]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_mem : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
rw : (thickenedIndicatorAux δ E x).toNNReal = 1
⊢ Eq (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
have rw₁ : ENNReal.toNNReal 1 = 1
Tactic: rw [thickenedIndicator_apply, thickenedIndicatorAux_one_of_mem_closure δ E x_mem, toNNReal_one]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_mem : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
rw : (thickenedIndicatorAux δ E x).toNNReal = 1
rw₁ : ENNReal.toNNReal 1 = 1
⊢ Eq (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)
have rw₂ : Eq (α := ℝ≥0) 1 1
Tactic: rw [thickenedIndicator_apply, thickenedIndicatorAux_one_of_mem_closure δ E x_mem, toNNReal_one]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
X : Type u_2
inst : PseudoEMetricSpace X
δ : ℝ
δ_pos : 0 < δ
F : Set X
x : X
hxF : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
⊢ LE.le (α := ℝ≥0) (1 : ℝ≥0) (((thickenedIndicator δ_pos F : X →ᵇ ℝ≥0) : (a : X) → ℝ≥0) x : ℝ≥0)
have rw : LE.le (α := ℝ≥0) 1 1
Tactic: rw [thickenedIndicator_one_of_mem_closure δ_pos F hxF]