awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
key : ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1
⊢ (thickenedIndicatorAux δ E x).toNNReal ≤ 1

Tactic:
(toNNReal_le_toNNReal (lt_of_le_of_lt (key _) one_lt_top).ne one_ne_top).mpr (key _)

Premises used: Iff.mpr, lt_of_le_of_lt, ENNReal.toNNReal_le_toNNReal, ENNReal.one_lt_top, ENNReal.toNNReal, WithTop.untopD, WithTop.recTopCoe, LT.lt.ne, ENNReal.one_ne_top
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
key : ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1
⊢ (thickenedIndicatorAux δ E x).toNNReal ≤ 1

Tactic:
exact (toNNReal_le_toNNReal (lt_of_le_of_lt (key _) one_lt_top).ne one_ne_top).mpr (key _)

Premises used: Iff.mpr, lt_of_le_of_lt, ENNReal.toNNReal_le_toNNReal, ENNReal.one_lt_top, LT.lt.ne, ENNReal.one_ne_top
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
key : ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1
⊢ (thickenedIndicatorAux δ E y).toNNReal ≤ 1

Tactic:
(toNNReal_le_toNNReal (lt_of_le_of_lt (key _) one_lt_top).ne one_ne_top).mpr (key _)

Premises used: Iff.mpr, lt_of_le_of_lt, ENNReal.toNNReal_le_toNNReal, ENNReal.one_lt_top, ENNReal.toNNReal, WithTop.untopD, WithTop.recTopCoe, LT.lt.ne, ENNReal.one_ne_top
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
key : ∀ (x : α), thickenedIndicatorAux δ E x ≤ 1
⊢ (thickenedIndicatorAux δ E y).toNNReal ≤ 1

Tactic:
exact (toNNReal_le_toNNReal (lt_of_le_of_lt (key _) one_lt_top).ne one_ne_top).mpr (key _)

Premises used: Iff.mpr, lt_of_le_of_lt, ENNReal.toNNReal_le_toNNReal, ENNReal.one_lt_top, LT.lt.ne, ENNReal.one_ne_top
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
⊢ (⇑(thickenedIndicator δ_pos E) : (a : α) → ℝ≥0) = ENNReal.toNNReal ∘ thickenedIndicatorAux δ E

Tactic:
rfl

Premises used: ENNReal.toNNReal, WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
⊢ thickenedIndicatorAux δ E x ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
⊢ (ENNReal.toNNReal ∘ thickenedIndicatorAux δ E) x ≤ 1

Tactic:
simpa using (toNNReal_le_toNNReal (by finiteness) one_ne_top).mpr
    (thickenedIndicatorAux_le_one δ E x)

Premises used: Iff.mpr, ENNReal.toNNReal_le_toNNReal, ENNReal.one_ne_top, thickenedIndicatorAux_le_one
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
rw₂ rw₃ : Eq (α := ℝ≥0) 1 1
⊢ Eq (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)

Tactic:
rw [thickenedIndicator_apply, thickenedIndicatorAux_one_of_mem_closure δ E x_mem, toNNReal_one]

Premises used: ENNReal.toNNReal_one, thickenedIndicator_apply, thickenedIndicatorAux_one_of_mem_closure
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
X : Type u_2
inst : PseudoEMetricSpace X
δ : ℝ
δ_pos : 0 < δ
F : Set X
x : X
hxF : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
rw rw₁ : LE.le (α := ℝ≥0) 1 1
⊢ LE.le (α := ℝ≥0) (1 : ℝ≥0) (((thickenedIndicator δ_pos F : X →ᵇ ℝ≥0) : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
rw [thickenedIndicator_one_of_mem_closure δ_pos F hxF]

Premises used: thickenedIndicator_one_of_mem_closure
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
X : Type u_2
inst : PseudoEMetricSpace X
δ : ℝ
δ_pos : 0 < δ
F : Set X
x : X
hxF : x ∈ F
⊢ LE.le (α := ℝ≥0) (1 : ℝ≥0) (((thickenedIndicator δ_pos F : X →ᵇ ℝ≥0) : (a : X) → ℝ≥0) x : ℝ≥0)

Tactic:
one_le_thickenedIndicator_apply' δ_pos (subset_closure hxF)

Premises used: subset_closure, one_le_thickenedIndicator_apply'
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_in_E : x ∈ E
⊢ Eq (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)

Tactic:
thickenedIndicator_one_of_mem_closure _ _ (subset_closure x_in_E)

Premises used: thickenedIndicator_one_of_mem_closure, subset_closure
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : x ∉ thickening δ E
rw : (thickenedIndicatorAux δ E x).toNNReal = 0
rw₁ : ENNReal.toNNReal 0 = 0
rw₂ rw₃ : Eq (α := ℝ≥0) 0 0
⊢ Eq (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)

Tactic:
rw [thickenedIndicator_apply, thickenedIndicatorAux_zero δ_pos E x_out, toNNReal_zero]

Premises used: thickenedIndicatorAux_zero, thickenedIndicator_apply, ENNReal.toNNReal_zero
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
pos :
  ∀ (h : a ∈ E),
    LE.le (α := (fun (x : α) ↦ ℝ≥0) a) (E.indicator (fun (x : α) ↦ 1) a : ℝ≥0)
      (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) a : ℝ≥0)
neg :
  ∀ (h : a ∉ E),
    LE.le (α := (fun (x : α) ↦ ℝ≥0) a) (E.indicator (fun (x : α) ↦ 1) a : ℝ≥0)
      (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) a : ℝ≥0)
⊢ LE.le (α := (fun (x : α) ↦ ℝ≥0) a) (E.indicator (fun (x : α) ↦ 1) a : ℝ≥0)
    (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) a : ℝ≥0)

Tactic:
by_cases h : a ∈ E
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
h : a ∈ E
⊢ LE.le (α := (fun (x : α) ↦ ℝ≥0) a) (E.indicator (fun (x : α) ↦ 1) a : ℝ≥0)
    (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) a : ℝ≥0)

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

Premises used: le_refl, Set.indicator_of_mem, thickenedIndicator_one
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
h : a ∉ E
⊢ LE.le (α := (fun (x : α) ↦ ℝ≥0) a) (E.indicator (fun (x : α) ↦ 1) a : ℝ≥0)
    (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) a : ℝ≥0)

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 α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
x : α
⊢ thickenedIndicatorAux δ₁ E x ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
x : α
⊢ thickenedIndicatorAux δ₂ E x ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
x : α
apply : thickenedIndicatorAux δ₁ E x ≤ thickenedIndicatorAux δ₂ E x
⊢ LE.le (α := (fun (a : α) ↦ ℝ≥0) x) (((thickenedIndicator δ₁_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0)
    (((thickenedIndicator δ₂_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0)

Tactic:
apply (toNNReal_le_toNNReal (by finiteness) (by finiteness)).mpr

Premises used: Iff.mpr, ENNReal.toNNReal_le_toNNReal
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
x : α
⊢ thickenedIndicatorAux δ₁ E x ≤ thickenedIndicatorAux δ₂ E x

Tactic:
apply thickenedIndicatorAux_mono hle

Premises used: thickenedIndicatorAux_mono
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E₁ E₂ : Set α
subset : E₁ ⊆ E₂
x : α
⊢ thickenedIndicatorAux δ E₁ x ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E₁ E₂ : Set α
subset : E₁ ⊆ E₂
x : α
⊢ thickenedIndicatorAux δ E₂ x ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
hb : thickenedIndicatorAux δ E x ≠ ∞
h₁ : thickenedIndicatorAux δ E y ≤ thickenedIndicatorAux δ E x
⊢ (thickenedIndicatorAux δ E y).toNNReal ≤ (thickenedIndicatorAux δ E x).toNNReal

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ thickenedIndicatorAux δ E x ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ thickenedIndicatorAux δ E y ≤ thickenedIndicatorAux δ E x

Tactic:
thickenedIndicatorAux_mono_infEDist δ h

Premises used: thickenedIndicatorAux_mono_infEDist
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ thickenedIndicatorAux δ E y ≤ thickenedIndicatorAux δ E x

Tactic:
exact thickenedIndicatorAux_mono_infEDist δ h

Premises used: thickenedIndicatorAux_mono_infEDist
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δ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))

Tactic:
have key := thickenedIndicatorAux_tendsto_indicator_closure δseq_lim E
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key :
  Tendsto (β := α → ℝ≥0∞) (fun (n : ℕ) ↦ thickenedIndicatorAux (δseq n) E) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator fun (x : α) ↦ 1))
rw :
  ∀
    (key :
      ∀ (x : α),
        Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop
          (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x)))
    (x : α),
    Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ((thickenedIndicator ⋯ E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))
⊢ Tendsto (β := (a : α) → ℝ≥0) (fun (n : ℕ) ↦ (⇑(thickenedIndicator ⋯ E) : (a : α) → ℝ≥0)) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator fun (x : α) ↦ 1))

Tactic:
rw [tendsto_pi_nhds] at *

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

Tactic:
(congr_fun (comp_indicator_const 1 ENNReal.toNNReal toNNReal_zero) x).symm

Premises used: ENNReal.toNNReal, WithTop.untopD, congr_fun, OfNat.ofNat, Eq.symm, WithTop.recTopCoe, Set.comp_indicator_const, ENNReal.toNNReal_zero
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key :
  ∀ (x : α),
    Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))
x : α
⊢ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x =
    ENNReal.toNNReal ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x)

Tactic:
refine (congr_fun (comp_indicator_const 1 ENNReal.toNNReal toNNReal_zero) x).symm

Premises used: ENNReal.toNNReal, congr_fun, OfNat.ofNat, Eq.symm, Set.comp_indicator_const, ENNReal.toNNReal_zero
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key :
  ∀ (x : α),
    Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))
x : α
rw :
  Tendsto (fun (i : ℕ) ↦ ((thickenedIndicator ⋯ E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x) atTop
    (𝓝
      (ENNReal.toNNReal
        ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x)))
⊢ Tendsto (β := ℝ≥0) (fun (i : ℕ) ↦ ((thickenedIndicator ⋯ E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))

Tactic:
rw [show indicator (closure E) (fun _ => (1 : ℝ≥0)) x =
        (indicator (closure E) (fun _ => (1 : ℝ≥0∞)) x).toNNReal
      by refine (congr_fun (comp_indicator_const 1 ENNReal.toNNReal toNNReal_zero) x).symm]
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key :
  ∀ (x : α),
    Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))
x : α
⊢ Tendsto (fun (i : ℕ) ↦ ((thickenedIndicator ⋯ E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x) atTop
    (𝓝
      (ENNReal.toNNReal
        ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x)))

Tactic:
Tendsto.comp (tendsto_toNNReal ?_) (key x)

Premises used: ENNReal.tendsto_toNNReal, ENNReal.toNNReal, WithTop.untopD, Filter.Tendsto.comp, WithTop.recTopCoe
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key :
  ∀ (x : α),
    Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))
x : α
refine :
  Ne (α := ℝ≥0∞) ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x) ∞
⊢ Tendsto (fun (i : ℕ) ↦ ((thickenedIndicator ⋯ E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x) atTop
    (𝓝
      (ENNReal.toNNReal
        ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x)))

Tactic:
refine Tendsto.comp (tendsto_toNNReal ?_) (key x)

Premises used: ENNReal.tendsto_toNNReal, Filter.Tendsto.comp
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key :
  ∀ (x : α),
    Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))
x : α
pos :
  ∀ (x_mem : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E),
    Ne (α := ℝ≥0∞) ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x) ∞
neg :
  ∀ (x_mem : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E),
    Ne (α := ℝ≥0∞) ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x) ∞
⊢ Ne (α := ℝ≥0∞) ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x) ∞

Tactic:
by_cases x_mem : x ∈ closure E

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

Tactic:
simp [x_mem]
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
key :
  ∀ (x : α),
    Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ thickenedIndicatorAux (δseq i) E x) atTop
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))
x : α
x_mem : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
⊢ Ne (α := ℝ≥0∞) ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x) ∞

Tactic:
simp [x_mem]
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
inr :
  ∀
    (this :
      ∀ (x y : α) (h : infEDist x E ≤ infEDist y E),
        edist (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0)
            (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) y : ℝ≥0) ≤
          (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y)
    (h : ¬infEDist x E ≤ infEDist y E),
    edist (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0)
        (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) y : ℝ≥0) ≤
      (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y
wlog :
  ∀ (x y : α) (h : infEDist x E ≤ infEDist y E),
    edist (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0)
        (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) y : ℝ≥0) ≤
      (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y
⊢ edist (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0)
      (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) y : ℝ≥0) ≤
    (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y

Tactic:
wlog h : infEDist x E ≤ infEDist y E generalizing x y

Premises used: Metric.infEDist
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
this :
  ∀ (x y : α) (h : infEDist x E ≤ infEDist y E),
    edist (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0)
        (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) y : ℝ≥0) ≤
      (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y
h : ¬infEDist x E ≤ infEDist y E
⊢ edist (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) y : ℝ≥0)
      (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0) ≤
    (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist y x

Tactic:
specialize this y x (le_of_not_ge h)

Premises used: le_of_not_ge
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : ¬infEDist x E ≤ infEDist y E
this :
  edist (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) y : ℝ≥0)
      (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0) ≤
    (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist y x
inr :
  edist (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) y : ℝ≥0)
      (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0) ≤
    (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y
inr₁ inr₂ inr₃ inr₄ :
  edist (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) y : ℝ≥0)
      (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0) ≤
    (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist y x
⊢ edist (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0)
      (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) y : ℝ≥0) ≤
    (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y

Tactic:
rwa [edist_comm, edist_comm x]

Premises used: PseudoEMetricSpace.edist_comm
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
simp_rw :
  ENNReal.ofReal |(thickenedIndicatorAux δ E x).toReal - (thickenedIndicatorAux δ E y).toReal| ≤
    (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y
⊢ edist (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0)
      (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) y : ℝ≥0) ≤
    (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y

Tactic:
simp_rw [edist_dist, NNReal.dist_eq, thickenedIndicator_apply, coe_toNNReal_eq_toReal]

Premises used: ENNReal.coe_toNNReal_eq_toReal, edist_dist, thickenedIndicator_apply, NNReal.dist_eq
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
rw :
  ENNReal.ofReal |(thickenedIndicatorAux δ E x - thickenedIndicatorAux δ E y).toReal| ≤
    (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y
⊢ ENNReal.ofReal |(thickenedIndicatorAux δ E x).toReal - (thickenedIndicatorAux δ E y).toReal| ≤
    (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y

Tactic:
rw [← ENNReal.toReal_sub_of_le (thickenedIndicatorAux_mono_infEDist _ h) (by finiteness)]

Premises used: thickenedIndicatorAux_mono_infEDist, ENNReal.toReal_sub_of_le
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
simp : 1 - infEDist x E / ENNReal.ofReal δ - (1 - infEDist y E / ENNReal.ofReal δ) ≤ (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y
⊢ ENNReal.ofReal |(thickenedIndicatorAux δ E x - thickenedIndicatorAux δ E y).toReal| ≤
    (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y

Tactic:
simp only [thickenedIndicatorAux, abs_toReal, ne_eq, sub_eq_top_iff, one_ne_top, false_and,
    not_false_eq_true, and_true, ofReal_toReal]

Premises used: and_true, false_and, ENNReal.ofReal_toReal, ENNReal.sub_eq_top_iff, ne_eq, thickenedIndicatorAux, ENNReal.abs_toReal, not_false_eq_true, ENNReal.one_ne_top
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ δ.toNNReal ≠ 0

Tactic:
simp [δ_pos]
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
rw :
  1 - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - (1 - infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹) ≤
    (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist x y
⊢ 1 - infEDist x E / ENNReal.ofReal δ - (1 - infEDist y E / ENNReal.ofReal δ) ≤ (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y

Tactic:
rw [ENNReal.coe_inv (by simp [δ_pos]), ENNReal.ofReal, div_eq_mul_inv, div_eq_mul_inv]

Premises used: ENNReal.coe_inv, ENNReal.ofReal, div_eq_mul_inv