awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : x ∉ thickening δ E
⊢ Eq (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
have rw : (thickenedIndicatorAux δ E x).toNNReal = 0
Tactic: rw [thickenedIndicator_apply, thickenedIndicatorAux_zero δ_pos E x_out, toNNReal_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x : α
x_out : x ∉ thickening δ E
rw : (thickenedIndicatorAux δ E x).toNNReal = 0
⊢ Eq (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
have rw₁ : ENNReal.toNNReal 0 = 0
Tactic: rw [thickenedIndicator_apply, thickenedIndicatorAux_zero δ_pos E x_out, toNNReal_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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
⊢ Eq (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
have rw₂ : Eq (α := ℝ≥0) 0 0
Tactic: rw [thickenedIndicator_apply, thickenedIndicatorAux_zero δ_pos E x_out, toNNReal_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
a : α
⊢ LE.le (α := (fun (x : α) ↦ ℝ≥0) a) (E.indicator (fun (x : α) ↦ 1) a : ℝ≥0)
    (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) a : ℝ≥0)
have 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)
Tactic: by_cases h : a ∈ E
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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)
⊢ LE.le (α := (fun (x : α) ↦ ℝ≥0) a) (E.indicator (fun (x : α) ↦ 1) a : ℝ≥0)
    (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) a : ℝ≥0)
have 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)
Tactic: by_cases h : a ∈ E
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ₁ δ₂ : ℝ
δ₁_pos : 0 < δ₁
δ₂_pos : 0 < δ₂
hle : δ₁ ≤ δ₂
E : Set α
x : α
⊢ LE.le (α := (fun (a : α) ↦ ℝ≥0) x) (((thickenedIndicator δ₁_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0)
    (((thickenedIndicator δ₂_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0)
have apply : thickenedIndicatorAux δ₁ E x ≤ thickenedIndicatorAux δ₂ E x
Tactic: apply (toNNReal_le_toNNReal (by finiteness) (by finiteness)).mpr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ (thickenedIndicatorAux δ E y).toNNReal ≤ (thickenedIndicatorAux δ E x).toNNReal
have hb : thickenedIndicatorAux δ E x ≠ ∞
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
hb : thickenedIndicatorAux δ E x ≠ ∞
⊢ (thickenedIndicatorAux δ E y).toNNReal ≤ (thickenedIndicatorAux δ E x).toNNReal
have h₁ : thickenedIndicatorAux δ E y ≤ thickenedIndicatorAux δ E x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (hypothesis)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δseq : ℕ → ℝ
δseq_pos : ∀ (n : ℕ), 0 < δseq n
δseq_lim : Tendsto δseq atTop (𝓝 0)
E : Set α
⊢ Tendsto (β := (a : α) → ℝ≥0) (fun (n : ℕ) ↦ (⇑(thickenedIndicator ⋯ E) : (a : α) → ℝ≥0)) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator fun (x : α) ↦ 1))
have key : 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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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))
⊢ Tendsto (β := (a : α) → ℝ≥0) (fun (n : ℕ) ↦ (⇑(thickenedIndicator ⋯ E) : (a : α) → ℝ≥0)) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator fun (x : α) ↦ 1))
have 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 sorry E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))
Tactic: rw [tendsto_pi_nhds] at *
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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 (β := ℝ≥0) (fun (i : ℕ) ↦ ((thickenedIndicator ⋯ E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x))
have rw : Tendsto (fun (i : ℕ) ↦ ((thickenedIndicator sorry E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x) atTop
  (𝓝
    (ENNReal.toNNReal
      ((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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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)))
have refine : Ne (α := ℝ≥0∞) ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x) ∞
Tactic: refine Tendsto.comp (tendsto_toNNReal ?_) (key x)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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 : α
⊢ Ne (α := ℝ≥0∞) ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x) ∞
have pos : ∀ (x_mem : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E),
  Ne (α := ℝ≥0∞) ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x) ∞
Tactic: by_cases x_mem : x ∈ closure E
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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) ∞
⊢ Ne (α := ℝ≥0∞) ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x) ∞
have neg : ∀ (x_mem : x ∉ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E),
  Ne (α := ℝ≥0∞) ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] E).indicator (fun (x : α) ↦ 1) x) ∞
Tactic: by_cases x_mem : x ∈ closure E
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
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
have 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
Tactic: wlog h : infEDist x E ≤ infEDist y E generalizing x y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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
⊢ edist (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0)
      (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) y : ℝ≥0) ≤
    (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y
have 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
Tactic: wlog h : infEDist x E ≤ infEDist y E generalizing x y
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (hypothesis)
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) x : ℝ≥0)
      (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) y : ℝ≥0) ≤
    (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y
have this₁ : 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)
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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
⊢ edist (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0)
      (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) y : ℝ≥0) ≤
    (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y
have inr : edist (α := ℝ≥0) (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) y : ℝ≥0)
    (((thickenedIndicator δ_pos E : α →ᵇ ℝ≥0) : (a : α) → ℝ≥0) x : ℝ≥0) ≤
  (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y
Tactic: rwa [edist_comm, edist_comm x]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
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
have simp_rw : ENNReal.ofReal |(thickenedIndicatorAux δ E x).toReal - (thickenedIndicatorAux δ E y).toReal| ≤
  (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y
Tactic: simp_rw [edist_dist, NNReal.dist_eq, thickenedIndicator_apply, coe_toNNReal_eq_toReal]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ ENNReal.ofReal |(thickenedIndicatorAux δ E x).toReal - (thickenedIndicatorAux δ E y).toReal| ≤
    (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y
have rw : ENNReal.ofReal |(thickenedIndicatorAux δ E x - thickenedIndicatorAux δ E y).toReal| ≤ (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y
Tactic: rw [← ENNReal.toReal_sub_of_le (thickenedIndicatorAux_mono_infEDist _ h) (by finiteness)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ ENNReal.ofReal |(thickenedIndicatorAux δ E x - thickenedIndicatorAux δ E y).toReal| ≤
    (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y
have simp : 1 - infEDist x E / ENNReal.ofReal δ - (1 - infEDist y E / ENNReal.ofReal δ) ≤ (↑δ.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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ 1 - infEDist x E / ENNReal.ofReal δ - (1 - infEDist y E / ENNReal.ofReal δ) ≤ (↑δ.toNNReal⁻¹ : ℝ≥0∞) * edist x y
have rw : 1 - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - (1 - infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹) ≤
  (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist x y
Tactic: rw [ENNReal.coe_inv (by simp [δ_pos]), ENNReal.ofReal, div_eq_mul_inv, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
δ : ℝ
δ_pos : 0 < δ
E : Set α
x y : α
h : infEDist x E ≤ infEDist y E
⊢ 1 - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - (1 - infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹) ≤
    (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist x y
have 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
Tactic: by_cases h_le : infEDist y E * (↑δ.toNNReal)⁻¹ ≤ 1
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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
⊢ 1 - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - (1 - infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹) ≤
    (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist x y
have 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
Tactic: by_cases h_le : infEDist y E * (↑δ.toNNReal)⁻¹ ≤ 1
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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 x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - (1 - infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹) ≤
    infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹
have rw : infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - infEDist x 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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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 * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist x y
have rw : (↑δ.toNNReal : ℝ≥0∞)⁻¹ * (infEDist y E - infEDist x E) ≤ (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist y x
Tactic: rw [← ENNReal.sub_mul (by simp [δ_pos]), mul_comm, edist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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
⊢ (↑δ.toNNReal : ℝ≥0∞)⁻¹ * (infEDist y E - infEDist x E) ≤ (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist y x
have bc : infEDist y E - infEDist x E ≤ edist y x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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 - infEDist x E ≤ edist y x
have bc : infEDist y E ≤ edist y x + infEDist x E
Tactic: simp only [tsub_le_iff_right]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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 x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - (1 - infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹) ≤
    (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist x y
have calc : 1 - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - (1 - infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹) ≤
  infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹
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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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∞)⁻¹
⊢ 1 - infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - (1 - infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹) ≤
    (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist x y
have calc₁ : infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - infEDist x 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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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 x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ - (1 - infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹) ≤
    (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist x y
have neg : 1 ≤
  (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist x y + (1 - infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹) +
    infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹
Tactic: simp only [tsub_le_iff_right]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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 ≤
    (↑δ.toNNReal : ℝ≥0∞)⁻¹ * edist x y + (1 - infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹) +
      infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹
have neg : 1 ≤ edist x y * (↑δ.toNNReal : ℝ≥0∞)⁻¹ + infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹
Tactic: rw [tsub_eq_zero_of_le (not_le.mp h_le).le, add_zero, mul_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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 * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ edist x y * (↑δ.toNNReal : ℝ≥0∞)⁻¹ + infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹
have rw : infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ (edist y x + infEDist x E) * (↑δ.toNNReal : ℝ≥0∞)⁻¹
Tactic: rw [← add_mul, edist_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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 * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ (edist y x + infEDist x E) * (↑δ.toNNReal : ℝ≥0∞)⁻¹
have bc : infEDist y E ≤ edist y x + infEDist x E
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.ThickenedIndicator (goal)
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 ≤ edist x y * (↑δ.toNNReal : ℝ≥0∞)⁻¹ + infEDist x E * (↑δ.toNNReal : ℝ≥0∞)⁻¹
have calc : infEDist y E * (↑δ.toNNReal : ℝ≥0∞)⁻¹ ≤ 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