awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
⊢ thickenedIndicatorAux δ E x ≤ 1

Tactic:
apply tsub_le_self (α := ℝ≥0∞)

Premises used: tsub_le_self
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
⊢ thickenedIndicatorAux δ E x < ∞

Tactic:
lt_of_le_of_lt (thickenedIndicatorAux_le_one _ _ _) one_lt_top

Premises used: lt_of_le_of_lt, ENNReal.one_lt_top, thickenedIndicatorAux_le_one
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
⊢ thickenedIndicatorAux δ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E) = thickenedIndicatorAux δ E

Tactic:
simp +unfoldPartialApp only [thickenedIndicatorAux, infEDist_closure]

Premises used: thickenedIndicatorAux, Metric.infEDist_closure
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x : α
x_in_E : x ∈ E
⊢ thickenedIndicatorAux δ E x = 1

Tactic:
simp [thickenedIndicatorAux, infEDist_zero_of_mem x_in_E, tsub_zero]

Premises used: tsub_zero, thickenedIndicatorAux, Metric.infEDist_zero_of_mem
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
rw₁ rw₂ : Eq (α := ℝ≥0∞) 1 1
⊢ thickenedIndicatorAux δ E x = 1

Tactic:
rw [← thickenedIndicatorAux_closure_eq, thickenedIndicatorAux_one δ (closure E) x_mem]

Premises used: thickenedIndicatorAux_closure_eq, thickenedIndicatorAux_one, closure
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : x ∉ thickening δ E
⊢ ENNReal.ofReal δ ≤ infEDist x E

Tactic:
rw [thickening, mem_setOf_eq, not_lt] at x_out

Premises used: Set.mem_setOf_eq, Metric.thickening, not_lt
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEDist x E
apply : 1 - infEDist x E / ENNReal.ofReal δ ≤ ⊥
⊢ 1 - infEDist x E / ENNReal.ofReal δ = 0

Tactic:
apply le_antisymm _ bot_le

Premises used: le_antisymm, bot_le
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : ENNReal.ofReal δ ≤ infEDist x E
⊢ 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)
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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 δ ≤ HSub.hSub (α := ℝ≥0∞) 1 1

Tactic:
rw [ENNReal.div_self (ne_of_gt (ENNReal.ofReal_pos.mpr δ_pos)) ofReal_ne_top] at key

Premises used: Iff.mpr, ne_of_gt, ENNReal.ofReal_pos, ENNReal.div_self, ENNReal.ofReal_ne_top
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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 δ ≤ HSub.hSub (α := ℝ≥0∞) 1 1
⊢ 1 - infEDist x E / ENNReal.ofReal δ ≤ ⊥

Tactic:
simpa [tsub_self] using key

Premises used: tsub_self
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
hle : δ₁ ≤ δ₂
E : Set α
⊢ thickenedIndicatorAux δ₁ E ≤ thickenedIndicatorAux δ₂ E

Tactic:
fun _ => tsub_le_tsub (@rfl ℝ≥0∞ 1).le (ENNReal.div_le_div rfl.le (ofReal_le_ofReal hle))

Premises used: tsub_le_tsub, ENNReal.ofReal_le_ofReal, Eq.le, ENNReal.div_le_div, thickenedIndicatorAux, rfl
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
a : α
pos : ∀ (h : a ∈ E), E.indicator (fun (x : α) ↦ 1) a ≤ thickenedIndicatorAux δ E a
neg : ∀ (h : a ∉ E), E.indicator (fun (x : α) ↦ 1) a ≤ thickenedIndicatorAux δ E a
⊢ E.indicator (fun (x : α) ↦ 1) a ≤ thickenedIndicatorAux δ E a

Tactic:
by_cases h : a ∈ E
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
a : α
h : a ∈ E
⊢ E.indicator (fun (x : α) ↦ 1) a ≤ thickenedIndicatorAux δ E a

Tactic:
simp only [h, indicator_of_mem, thickenedIndicatorAux_one δ E h, le_refl]

Premises used: le_refl, thickenedIndicatorAux_one, Set.indicator_of_mem
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
a : α
h : a ∉ E
⊢ E.indicator (fun (x : α) ↦ 1) a ≤ thickenedIndicatorAux δ E a

Tactic:
simp only [h, indicator_of_notMem, not_false_iff, zero_le]

Premises used: zero_le, Set.indicator_of_notMem, not_false_iff
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E₁ E₂ : Set α
subset : E₁ ⊆ E₂
⊢ thickenedIndicatorAux δ E₁ ≤ thickenedIndicatorAux δ E₂

Tactic:
fun _ => tsub_le_tsub (@rfl ℝ≥0∞ 1).le (ENNReal.div_le_div (infEDist_anti subset) rfl.le)

Premises used: tsub_le_tsub, Eq.le, ENNReal.div_le_div, Metric.infEDist_anti, thickenedIndicatorAux, rfl
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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 δ
inr :
  ∀ (hle : 1 ≤ infEDist x E / ENNReal.ofReal δ),
    1 - infEDist y E / ENNReal.ofReal δ ≤ 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

Premises used: ENNReal.ofReal, HDiv.hDiv, le_total, Metric.infEDist, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
hle : infEDist x E / ENNReal.ofReal δ ≤ 1
⊢ Ne (α := ℝ≥0∞) 1 ∞

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
hle : infEDist x E / ENNReal.ofReal δ ≤ 1
inl : infEDist x E / ENNReal.ofReal δ ≤ infEDist y E / ENNReal.ofReal δ
⊢ 1 - infEDist y E / ENNReal.ofReal δ ≤ 1 - infEDist x E / ENNReal.ofReal δ

Tactic:
rw [ENNReal.sub_le_sub_iff_left hle (by simp)]

Premises used: ENNReal.sub_le_sub_iff_left
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
hle : infEDist x E / ENNReal.ofReal δ ≤ 1
⊢ infEDist x E / ENNReal.ofReal δ ≤ infEDist y E / ENNReal.ofReal δ

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
hle : 1 ≤ infEDist x E / ENNReal.ofReal δ
inr : 1 ≤ infEDist y E / ENNReal.ofReal δ
⊢ 1 - infEDist y E / ENNReal.ofReal δ ≤ 1 - infEDist x E / ENNReal.ofReal δ

Tactic:
rw [tsub_eq_zero_of_le hle, tsub_eq_zero_of_le]

Premises used: tsub_eq_zero_of_le
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
hle : 1 ≤ infEDist x E / ENNReal.ofReal δ
⊢ infEDist x E / ENNReal.ofReal δ ≤ infEDist y E / ENNReal.ofReal δ

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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 δ

Tactic:
exact hle.trans (by gcongr)

Premises used: LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
rw :
  ∀ (x : α),
    Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))
⊢ Tendsto (β := α → ℝ≥0∞) (fun (n : ℕ) ↦ thickenedIndicatorAux (δseq n) E) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator fun (x : α) ↦ 1))

Tactic:
rw [tendsto_pi_nhds]

Premises used: tendsto_pi_nhds
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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))
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))
⊢ 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

Premises used: closure
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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 :
  Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ 1) 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))

Tactic:
simp_rw [thickenedIndicatorAux_one_of_mem_closure _ E x_mem_closure]

Premises used: thickenedIndicatorAux_one_of_mem_closure
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
⊢ Eq (α := ℝ≥0∞) ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x) 1

Tactic:
simp only [x_mem_closure, indicator_of_mem]

Premises used: Set.indicator_of_mem
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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 : Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ 1) atTop (𝓝 1)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ 1) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))

Tactic:
rw [show (indicator (closure E) fun _ => (1 : ℝ≥0∞)) x = 1 by
        simp only [x_mem_closure, indicator_of_mem]]
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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 (𝓝 1)

Tactic:
tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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 (𝓝 1)

Tactic:
exact tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
⊢ Eq (α := ℝ≥0∞) ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x) 0

Tactic:
simp only [x_mem_closure, indicator_of_notMem, not_false_iff]

Premises used: Set.indicator_of_notMem, not_false_iff
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
neg : Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))

Tactic:
rw [show (closure E).indicator (fun _ => (1 : ℝ≥0∞)) x = 0 by
        simp only [x_mem_closure, indicator_of_notMem, not_false_iff]]
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
neg :
  ∀ (ε : ℝ) (ε_pos : 0 < ε) (ε_lt : ENNReal.ofReal ε < infEDist x E),
    Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
⊢ 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⟩⟩

Premises used: Metric.exists_real_pos_lt_infEDist_of_notMem_closure
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
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)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)

Tactic:
rw [Metric.tendsto_nhds] at δseq_lim

Premises used: Metric.tendsto_nhds
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
⊢ ∀ᶠ (x : ℕ) in atTop, dist (δseq x) 0 < ε

Tactic:
specialize δseq_lim ε ε_pos
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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 < ε
⊢ ∃ (a : ℕ), ∀ b ≥ a, |δseq b| < ε

Tactic:
simp only [dist_zero_right, Real.norm_eq_abs, eventually_atTop] at δseq_lim

Premises used: Filter.eventually_atTop, dist_zero_right, Real.norm_eq_abs
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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| < ε
neg :
  ∀ (N : ℕ) (hN : ∀ b ≥ N, |δseq b| < ε),
    Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)

Tactic:
rcases δseq_lim with ⟨N, hN⟩
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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| < ε
neg : ∀ i ≥ N, thickenedIndicatorAux (δseq i) E x = 0
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop (𝓝 0)

Tactic:
apply tendsto_atTop_of_eventually_const (i₀ := N)

Premises used: tendsto_atTop_of_eventually_const
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
⊢ x ∉ thickening ε E

Tactic:
simpa only [thickening, mem_setOf_eq, not_lt] using ε_lt.le

Premises used: LT.lt.le, Set.mem_setOf_eq, Metric.thickening, not_lt
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
⊢ x ∉ thickening ε E

Tactic:
have key : x ∉ thickening ε E := by simpa only [thickening, mem_setOf_eq, not_lt] using ε_lt.le
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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

Tactic:
le_antisymm ?_ bot_le

Premises used: le_antisymm, bot_le
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
neg : thickenedIndicatorAux (δseq n) E x ≤ 0
⊢ thickenedIndicatorAux (δseq n) E x = 0

Tactic:
refine le_antisymm ?_ bot_le

Premises used: le_antisymm, bot_le
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
neg : thickenedIndicatorAux ε E x ≤ 0
⊢ thickenedIndicatorAux (δseq n) E x ≤ 0

Tactic:
apply (thickenedIndicatorAux_mono (lt_of_abs_lt (hN n n_large)).le E x).trans

Premises used: thickenedIndicatorAux_mono, LT.lt.le, lt_of_abs_lt, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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 ε E x ≤ 0

Tactic:
(thickenedIndicatorAux_zero ε_pos E key).le

Premises used: thickenedIndicatorAux_zero, Eq.le
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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 ε E x ≤ 0

Tactic:
exact (thickenedIndicatorAux_zero ε_pos E key).le

Premises used: thickenedIndicatorAux_zero, Eq.le
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
apply : ∀ (x : α), Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | a ≠ ∞} (thickenedIndicatorAux δ E x)
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, _] fun (x : α) ↦
    (thickenedIndicatorAux δ E x).toNNReal

Tactic:
apply ContinuousOn.comp_continuous continuousOn_toNNReal
      (continuous_thickenedIndicatorAux δ_pos E)

Premises used: ContinuousOn.comp_continuous, ENNReal.continuousOn_toNNReal, continuous_thickenedIndicatorAux
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
⊢ Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | a ≠ ∞} (thickenedIndicatorAux δ E x)

Tactic:
(lt_of_le_of_lt (@thickenedIndicatorAux_le_one _ _ δ E x) one_lt_top).ne

Premises used: lt_of_le_of_lt, Set.Mem, setOf, ENNReal.one_lt_top, Not, LT.lt.ne, thickenedIndicatorAux_le_one
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
⊢ Membership.mem (γ := Set ℝ≥0∞) {a : ℝ≥0∞ | a ≠ ∞} (thickenedIndicatorAux δ E x)

Tactic:
exact (lt_of_le_of_lt (@thickenedIndicatorAux_le_one _ _ δ E x) one_lt_top).ne

Premises used: lt_of_le_of_lt, ENNReal.one_lt_top, LT.lt.ne, thickenedIndicatorAux_le_one
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
h : ∀ (x y : α), dist (thickenedIndicatorAux δ E x).toNNReal (thickenedIndicatorAux δ E y).toNNReal ≤ 2
⊢ ∃ (C : ℝ), ∀ (x y : α), dist (thickenedIndicatorAux δ E x).toNNReal (thickenedIndicatorAux δ E y).toNNReal ≤ C

Tactic:
use 2
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : |(↑(thickenedIndicatorAux δ E x).toNNReal : ℝ)| + |(↑(thickenedIndicatorAux δ E y).toNNReal : ℝ)| ≤ 2
⊢ |(↑(thickenedIndicatorAux δ E x).toNNReal : ℝ) - (↑(thickenedIndicatorAux δ E y).toNNReal : ℝ)| ≤ 2

Tactic:
apply (abs_sub _ _).trans

Premises used: abs_sub, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h :
  (↑(thickenedIndicatorAux δ E x).toNNReal : ℝ) + (↑(thickenedIndicatorAux δ E y).toNNReal : ℝ) ≤ HAdd.hAdd (α := ℝ) 1 1
⊢ |(↑(thickenedIndicatorAux δ E x).toNNReal : ℝ)| + |(↑(thickenedIndicatorAux δ E y).toNNReal : ℝ)| ≤ 2

Tactic:
rw [NNReal.abs_eq, NNReal.abs_eq, ← one_add_one_eq_two]

Premises used: one_add_one_eq_two, NNReal.abs_eq
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
⊢ ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1

Tactic:
have key := @thickenedIndicatorAux_le_one _ _ δ E
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
key : ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1
h : (↑(thickenedIndicatorAux δ E x).toNNReal : ℝ) ≤ 1
h₁ : (↑(thickenedIndicatorAux δ E y).toNNReal : ℝ) ≤ 1
⊢ (↑(thickenedIndicatorAux δ E x).toNNReal : ℝ) + (↑(thickenedIndicatorAux δ E y).toNNReal : ℝ) ≤ HAdd.hAdd (α := ℝ) 1 1

Tactic:
apply add_le_add

Premises used: add_le_add