awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
pos :
  ∀ (h_le : infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ 1),
    1 - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - (1 - infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹) ≤
      (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist x y
neg :
  ∀ (h_le : ¬infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ 1),
    1 - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - (1 - infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹) ≤
      (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist x y
⊢ 1 - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - (1 - infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹) ≤
    (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist x y

Tactic:
by_cases h_le : infEDist y E * (↑δ.toNNReal)⁻¹ ≤ 1

Premises used: Metric.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
h_le : infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ 1
⊢ Ne (α := ℝ≥0∞) 1 ∞

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
h_le : infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ 1
rw rw₁ :
  infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤
    infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹
⊢ 1 - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - (1 - infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹) ≤
    infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹

Tactic:
rw [ENNReal.sub_sub_sub_cancel_left (by finiteness) h_le]

Premises used: ENNReal.sub_sub_sub_cancel_left
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
h_le : infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ 1
⊢ 0 < infEDist x E → 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
h_le : infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ 1
rw : (↑δ.toNNReal : ℝ≥0∞)⁻¹ * (infEDist y E - infEDist x E) ≤ (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist y x
⊢ infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist x y

Tactic:
rw [← ENNReal.sub_mul (by simp [δ_pos]), mul_comm, edist_comm]

Premises used: PseudoEMetricSpace.edist_comm, ENNReal.sub_mul, mul_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
h_le : infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ 1
bc : infEDist y E - infEDist x E ≤ edist y x
⊢ (↑δ.toNNReal : ℝ≥0∞)⁻¹ * (infEDist y E - infEDist x E) ≤ (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist y x

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
h_le : infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ 1
bc : infEDist y E ≤ edist y x + infEDist x E
⊢ infEDist y E - infEDist x E ≤ edist y x

Tactic:
simp only [tsub_le_iff_right]

Premises used: tsub_le_iff_right
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
h_le : infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ 1
⊢ infEDist y E ≤ edist y x + infEDist x E

Tactic:
infEDist_le_edist_add_infEDist

Premises used: Metric.infEDist_le_edist_add_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
h_le : infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ 1
⊢ infEDist y E ≤ edist y x + infEDist x E

Tactic:
exact infEDist_le_edist_add_infEDist

Premises used: Metric.infEDist_le_edist_add_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
h_le : infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ 1
calc :
  1 - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - (1 - infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹) ≤
    infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹
calc₁ :
  infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist x y
⊢ 1 - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - (1 - infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹) ≤
    (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist x y

Tactic:
calc 1 - infEDist x E * (↑δ.toNNReal)⁻¹ - (1 - infEDist y E * (↑δ.toNNReal)⁻¹)
    _ ≤ infEDist y E * (↑δ.toNNReal)⁻¹ - infEDist x E * (↑δ.toNNReal)⁻¹ := by
      rw [ENNReal.sub_sub_sub_cancel_left (by finiteness) h_le]
    _ ≤ (↑δ.toNNReal)⁻¹ * edist x y := by
      rw [← ENNReal.sub_mul (by simp [δ_pos]), mul_comm, edist_comm]
      gcongr
      simp only [tsub_le_iff_right]
      exact infEDist_le_edist_add_infEDist

Premises used: HMul.hMul, HSub.hSub, Metric.infEDist, Inv.inv, EDist.edist, OfNat.ofNat
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
h_le : ¬infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ 1
neg :
  1 ≤
    (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist x y + (1 - infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹) +
      infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹
⊢ 1 - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - (1 - infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹) ≤
    (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist x y

Tactic:
simp only [tsub_le_iff_right]

Premises used: tsub_le_iff_right
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
h_le : ¬infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ 1
neg : 1 ≤ edist x y * (↑δ.toNNReal : ℝ≥0∞)⁻¹ + infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹
⊢ 1 ≤
    (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist x y + (1 - infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹) +
      infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹

Tactic:
rw [tsub_eq_zero_of_le (not_le.mp h_le).le, add_zero, mul_comm]

Premises used: not_le, tsub_eq_zero_of_le, LT.lt.le, Iff.mp, mul_comm, add_zero
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
h_le : ¬infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ 1
⊢ 1 ≤ infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹

Tactic:
(not_le.mp h_le).le

Premises used: not_le, LT.lt.le, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
h_le : ¬infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ 1
rw : infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ (edist y x + infEDist x E) * (↑δ.toNNReal : ℝ≥0∞)⁻¹
⊢ infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ edist x y * (↑δ.toNNReal : ℝ≥0∞)⁻¹ + infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹

Tactic:
rw [← add_mul, edist_comm]

Premises used: PseudoEMetricSpace.edist_comm, add_mul
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
h_le : ¬infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ 1
bc : infEDist y E ≤ edist y x + infEDist x E
⊢ infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ (edist y x + infEDist x E) * (↑δ.toNNReal : ℝ≥0∞)⁻¹

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
h_le : ¬infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ 1
⊢ infEDist y E ≤ edist y x + infEDist x E

Tactic:
infEDist_le_edist_add_infEDist

Premises used: Metric.infEDist_le_edist_add_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
h_le : ¬infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ 1
⊢ infEDist y E ≤ edist y x + infEDist x E

Tactic:
exact infEDist_le_edist_add_infEDist

Premises used: Metric.infEDist_le_edist_add_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
h_le : ¬infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ 1
calc :
  infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ edist x y * (↑δ.toNNReal : ℝ≥0∞)⁻¹ + infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹
⊢ 1 ≤ edist x y * (↑δ.toNNReal : ℝ≥0∞)⁻¹ + infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹

Tactic:
calc 1
    _ ≤ infEDist y E * (↑δ.toNNReal)⁻¹ := (not_le.mp h_le).le
    _ ≤ edist x y * (↑δ.toNNReal)⁻¹ + infEDist x E * (↑δ.toNNReal)⁻¹ := by
      rw [← add_mul, edist_comm]
      gcongr
      exact infEDist_le_edist_add_infEDist

Premises used: not_le, LT.lt.le, Metric.infEDist, Iff.mp, EDist.edist
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
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
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 0,
    (thickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x

Tactic:
by_cases x_mem_closure : x ∈ closure E

Premises used: closure
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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 :
  ∀ (δ : ℝ) (δ_pos : Membership.mem (γ := Set ℝ) (Ioi 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

Tactic:
filter_upwards [self_mem_nhdsWithin] with δ δ_pos

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
δ : ℝ
δ_pos : Membership.mem (γ := Set ℝ) (Ioi 0) δ
⊢ (thickening δ E).mulIndicator f x = (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x

Tactic:
simp only [closure_subset_thickening δ_pos E x_mem_closure, mulIndicator_of_mem, x_mem_closure]

Premises used: Metric.closure_subset_thickening, Set.mulIndicator_of_mem
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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, x ∉ thickening δ E

Tactic:
have obs := eventually_notMem_thickening_of_infEDist_pos x_mem_closure
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
δ : ℝ
x_notin_thE : x ∉ thickening δ E
h :
  Membership.mem (γ := Set ℝ) (Ioi 0) δ →
    (thickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x
⊢ Membership.mem (γ := Set ℝ) (Ioi 0) δ →
    (thickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x

Tactic:
_
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
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
⊢ ∀ᶠ (δ : ℝ) in 𝓝[>] 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 _

Premises used: mem_nhdsWithin_of_mem_nhds, self_mem_nhdsWithin
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
δ : ℝ
x_notin_thE : x ∉ thickening δ E
h : Membership.mem (γ := Set ℝ) (Ioi 0) δ
⊢ (thickening δ E).mulIndicator f x = (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x

Tactic:
simp only [x_notin_thE, not_false_eq_true, mulIndicator_of_notMem, x_mem_closure]

Premises used: Set.mulIndicator_of_notMem, not_false_eq_true
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
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
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0,
    (cthickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x

Tactic:
by_cases x_mem_closure : x ∈ closure E

Premises used: closure
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
⊢ Membership.mem (γ := Set ℝ) univ δ →
    (cthickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x

Tactic:
_
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0,
    (cthickening δ E).mulIndicator f x =
      (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x

Tactic:
filter_upwards [univ_mem] with δ _

Premises used: Filter.univ_mem
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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 δ
⊢ x ∈ cthickening δ E

Tactic:
have obs : x ∈ cthickening δ E := closure_subset_cthickening δ E x_mem_closure
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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
h₁ h₂ : f x = f x
⊢ (cthickening δ E).mulIndicator f x =
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x

Tactic:
rw [mulIndicator_of_mem obs f, mulIndicator_of_mem x_mem_closure f]

Premises used: Set.mulIndicator_of_mem
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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 :
  ∀ (δ : ℝ) (hδ : x ∉ cthickening δ E),
    (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

Tactic:
filter_upwards [eventually_notMem_cthickening_of_infEDist_pos x_mem_closure] with δ hδ

Premises used: Metric.eventually_notMem_cthickening_of_infEDist_pos
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
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δ : x ∉ cthickening δ E
⊢ (cthickening δ E).mulIndicator f x =
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x

Tactic:
simp only [hδ, not_false_eq_true, mulIndicator_of_notMem, x_mem_closure]

Premises used: Set.mulIndicator_of_notMem, not_false_eq_true
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
inst_2 : TopologicalSpace β
f : α → β
E : Set α
rw :
  ∀ (x : α),
    Tendsto (fun (i : ℝ) ↦ (thickening i E).mulIndicator f x) (𝓝[>] 0)
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x))
⊢ Tendsto (fun (δ : ℝ) ↦ (thickening δ E).mulIndicator f) (𝓝[>] 0)
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f))

Tactic:
rw [tendsto_pi_nhds]

Premises used: tendsto_pi_nhds
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
inst_2 : TopologicalSpace β
f : α → β
E : Set α
x : α
rw :
  Tendsto (fun (x_1 : ℝ) ↦ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x) (𝓝[>] 0)
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x))
⊢ Tendsto (fun (i : ℝ) ↦ (thickening i 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)]

Premises used: Filter.tendsto_congr', mulIndicator_thickening_eventually_eq_mulIndicator_closure
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
inst_2 : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun (x_1 : ℝ) ↦ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x) (𝓝[>] 0)
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x))

Tactic:
apply tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
inst_2 : TopologicalSpace β
f : α → β
E : Set α
rw :
  ∀ (x : α),
    Tendsto (fun (i : ℝ) ↦ (cthickening i E).mulIndicator f x) (𝓝 0)
      (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x))
⊢ Tendsto (fun (δ : ℝ) ↦ (cthickening δ E).mulIndicator f) (𝓝 0)
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f))

Tactic:
rw [tendsto_pi_nhds]

Premises used: tendsto_pi_nhds
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
inst_2 : TopologicalSpace β
f : α → β
E : Set α
x : α
rw :
  Tendsto (fun (x_1 : ℝ) ↦ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x) (𝓝 0)
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x))
⊢ Tendsto (fun (i : ℝ) ↦ (cthickening i 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)]

Premises used: Filter.tendsto_congr', mulIndicator_cthickening_eventually_eq_mulIndicator_closure
-- Module: Mathlib.Topology.MetricSpace.ThickenedIndicator
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
β : Type u_2
inst_1 : One β
inst_2 : TopologicalSpace β
f : α → β
E : Set α
x : α
⊢ Tendsto (fun (x_1 : ℝ) ↦ (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x) (𝓝 0)
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).mulIndicator f x))

Tactic:
apply tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
δ : ℝ
s : Set α
x : α
⊢ x ∈ thickening δ s ↔ infEDist x s < ENNReal.ofReal δ

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Metric.thickening
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
obtain : ∀ (ε : ℝ) (ε_pos : 0 < ε) (ε_lt : ENNReal.ofReal ε < infEDist x E), ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ thickening δ E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ thickening δ E

Tactic:
obtain ⟨ε, ⟨ε_pos, ε_lt⟩⟩ := exists_real_pos_lt_infEDist_of_notMem_closure h

Premises used: Metric.exists_real_pos_lt_infEDist_of_notMem_closure
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
h₁ : ∀ (δ : ℝ) (hδ : δ < ε), x ∉ thickening δ E
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, x ∉ thickening δ E

Tactic:
filter_upwards [eventually_lt_nhds ε_pos] with δ hδ

Premises used: eventually_lt_nhds
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
δ : ℝ
hδ : δ < ε
h₁ : ENNReal.ofReal δ ≤ infEDist x E
⊢ x ∉ thickening δ E

Tactic:
simp only [thickening, mem_setOf_eq, not_lt]

Premises used: Set.mem_setOf_eq, Metric.thickening, not_lt
-- Module: Mathlib.Topology.MetricSpace.Thickening
Goal:
α : Type u
inst : PseudoEMetricSpace α
E : Set α
x : α
h : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E
ε : ℝ
ε_pos : 0 < ε
ε_lt : ENNReal.ofReal ε < infEDist x E
δ : ℝ
hδ : δ < ε
⊢ ENNReal.ofReal δ ≤ infEDist x E

Tactic:
(ENNReal.ofReal_le_ofReal hδ.le).trans ε_lt.le

Premises used: ENNReal.ofReal_le_ofReal, LT.lt.le, LE.le.trans