awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
refine : ∀ (h : Disjoint (ball x δ) (ball y ε)) (hxy : dist x y < δ + ε), False
⊢ Disjoint (ball x δ) (ball y ε) ↔ δ + ε ≤ dist x y

Tactic:
refine ⟨fun h => le_of_not_gt fun hxy => ?_, ball_disjoint_ball⟩
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < δ + ε
⊢ dist x y < ε + δ

Tactic:
rw [add_comm] at hxy

Premises used: add_comm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < ε + δ
obtain : ∀ (z : E) (hxz : dist x z < δ) (hzy : dist z y < ε), False
⊢ False

Tactic:
obtain ⟨z, hxz, hzy⟩ := exists_dist_lt_lt hδ hε hxy

Premises used: exists_dist_lt_lt
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist x z < δ
hzy : dist z y < ε
⊢ dist z x < δ

Tactic:
rw [dist_comm] at hxz

Premises used: dist_comm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist x z < δ
hzy : dist z y < ε
hxz₁ : dist z x < δ
⊢ dist z y < ε

Tactic:
rw [dist_comm] at hxz

Premises used: dist_comm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist z x < δ
hzy : dist z y < ε
⊢ False

Tactic:
h.le_bot ⟨hxz, hzy⟩

Premises used: Disjoint.le_bot, Set.Mem, And.intro
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : Disjoint (ball x δ) (ball y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist z x < δ
hzy : dist z y < ε
⊢ False

Tactic:
exact h.le_bot ⟨hxz, hzy⟩

Premises used: Disjoint.le_bot, And.intro
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
⊢ Disjoint (ball x δ) (closedBall y ε) ↔ δ + ε ≤ dist x y

Tactic:
⟨fun h => le_of_not_gt fun hxy => ?_, ball_disjoint_closedBall⟩

Premises used: le_of_not_gt, Metric.ball_disjoint_closedBall, Iff.intro
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
refine : ∀ (h : Disjoint (ball x δ) (closedBall y ε)) (hxy : dist x y < δ + ε), False
⊢ Disjoint (ball x δ) (closedBall y ε) ↔ δ + ε ≤ dist x y

Tactic:
refine ⟨fun h => le_of_not_gt fun hxy => ?_, ball_disjoint_closedBall⟩
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < δ + ε
⊢ dist x y < ε + δ

Tactic:
rw [add_comm] at hxy

Premises used: add_comm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < ε + δ
obtain : ∀ (z : E) (hxz : dist x z < δ) (hzy : dist z y ≤ ε), False
⊢ False

Tactic:
obtain ⟨z, hxz, hzy⟩ := exists_dist_lt_le hδ hε hxy

Premises used: exists_dist_lt_le
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist x z < δ
hzy : dist z y ≤ ε
⊢ dist z x < δ

Tactic:
rw [dist_comm] at hxz

Premises used: dist_comm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist x z < δ
hzy : dist z y ≤ ε
hxz₁ : dist z x < δ
⊢ dist z y ≤ ε

Tactic:
rw [dist_comm] at hxz

Premises used: dist_comm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist z x < δ
hzy : dist z y ≤ ε
⊢ False

Tactic:
h.le_bot ⟨hxz, hzy⟩

Premises used: Disjoint.le_bot, Set.Mem, And.intro
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : Disjoint (ball x δ) (closedBall y ε)
hxy : dist x y < ε + δ
z : E
hxz : dist z x < δ
hzy : dist z y ≤ ε
⊢ False

Tactic:
exact h.le_bot ⟨hxz, hzy⟩

Premises used: Disjoint.le_bot, And.intro
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
rw : Disjoint (ball y ε) (closedBall x δ) ↔ δ + ε ≤ dist x y
rw₁ : ε + δ ≤ dist y x ↔ δ + ε ≤ dist x y
rw₂ : δ + ε ≤ dist y x ↔ δ + ε ≤ dist x y
rw₃ rw₄ : δ + ε ≤ dist x y ↔ δ + ε ≤ dist x y
⊢ Disjoint (closedBall x δ) (ball y ε) ↔ δ + ε ≤ dist x y

Tactic:
rw [disjoint_comm, disjoint_ball_closedBall_iff hε hδ, add_comm, dist_comm]

Premises used: disjoint_comm, dist_comm, add_comm, disjoint_ball_closedBall_iff
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
⊢ Disjoint (closedBall x δ) (closedBall y ε) ↔ δ + ε < dist x y

Tactic:
⟨fun h => lt_of_not_ge fun hxy => ?_, closedBall_disjoint_closedBall⟩

Premises used: lt_of_not_ge, Iff.intro, Metric.closedBall_disjoint_closedBall
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
refine : ∀ (h : Disjoint (closedBall x δ) (closedBall y ε)) (hxy : dist x y ≤ δ + ε), False
⊢ Disjoint (closedBall x δ) (closedBall y ε) ↔ δ + ε < dist x y

Tactic:
refine ⟨fun h => lt_of_not_ge fun hxy => ?_, closedBall_disjoint_closedBall⟩
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : dist x y ≤ δ + ε
⊢ dist x y ≤ ε + δ

Tactic:
rw [add_comm] at hxy

Premises used: add_comm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : dist x y ≤ ε + δ
obtain : ∀ (z : E) (hxz : dist x z ≤ δ) (hzy : dist z y ≤ ε), False
⊢ False

Tactic:
obtain ⟨z, hxz, hzy⟩ := exists_dist_le_le hδ hε hxy

Premises used: exists_dist_le_le
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : dist x y ≤ ε + δ
z : E
hxz : dist x z ≤ δ
hzy : dist z y ≤ ε
⊢ dist z x ≤ δ

Tactic:
rw [dist_comm] at hxz

Premises used: dist_comm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : dist x y ≤ ε + δ
z : E
hxz : dist x z ≤ δ
hzy : dist z y ≤ ε
hxz₁ : dist z x ≤ δ
⊢ dist z y ≤ ε

Tactic:
rw [dist_comm] at hxz

Premises used: dist_comm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : dist x y ≤ ε + δ
z : E
hxz : dist z x ≤ δ
hzy : dist z y ≤ ε
⊢ False

Tactic:
h.le_bot ⟨hxz, hzy⟩

Premises used: Disjoint.le_bot, Set.Mem, And.intro
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : Disjoint (closedBall x δ) (closedBall y ε)
hxy : dist x y ≤ ε + δ
z : E
hxz : dist z x ≤ δ
hzy : dist z y ≤ ε
⊢ False

Tactic:
exact h.le_bot ⟨hxz, hzy⟩

Premises used: Disjoint.le_bot, And.intro
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
inl : ∀ (hs : infEDist x s < ENNReal.ofReal δ), infEDist x (thickening δ s) = infEDist x s - ENNReal.ofReal δ
inr : ∀ (hs : ENNReal.ofReal δ ≤ infEDist x s), infEDist x (thickening δ s) = infEDist x s - ENNReal.ofReal δ
⊢ infEDist x (thickening δ s) = infEDist x s - ENNReal.ofReal δ

Tactic:
obtain hs | hs := lt_or_ge (infEDist x s) (ENNReal.ofReal δ)

Premises used: ENNReal.ofReal, Metric.infEDist, lt_or_ge
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : infEDist x s < ENNReal.ofReal δ
inl : x ∈ thickening δ s
⊢ infEDist x (thickening δ s) = infEDist x s - ENNReal.ofReal δ

Tactic:
rw [infEDist_zero_of_mem, tsub_eq_zero_of_le hs.le]

Premises used: tsub_eq_zero_of_le, LT.lt.le, Metric.infEDist_zero_of_mem
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : infEDist x s < ENNReal.ofReal δ
⊢ x ∈ thickening δ s

Tactic:
hs

Premises used: Set.Mem, setOf, Metric.thickening
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : infEDist x s < ENNReal.ofReal δ
⊢ x ∈ thickening δ s

Tactic:
exact hs
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
⊢ infEDist x (thickening δ s) = infEDist x s - ENNReal.ofReal δ

Tactic:
(tsub_le_iff_right.2 infEDist_le_infEDist_thickening_add).antisymm' ?_

Premises used: Iff.mpr, LE.le.antisymm', tsub_le_iff_right, Metric.infEDist_le_infEDist_thickening_add
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
inr : infEDist x (thickening δ s) ≤ infEDist x s - ENNReal.ofReal δ
⊢ infEDist x (thickening δ s) = infEDist x s - ENNReal.ofReal δ

Tactic:
refine (tsub_le_iff_right.2 infEDist_le_infEDist_thickening_add).antisymm' ?_

Premises used: Iff.mpr, LE.le.antisymm', tsub_le_iff_right, Metric.infEDist_le_infEDist_thickening_add
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
⊢ infEDist x (thickening δ s) ≤ infEDist x s - ENNReal.ofReal δ

Tactic:
le_sub_of_add_le_right ofReal_ne_top ?_

Premises used: ENNReal.le_sub_of_add_le_right, ENNReal.ofReal_ne_top
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
inr : infEDist x (thickening δ s) + ENNReal.ofReal δ ≤ infEDist x s
⊢ infEDist x (thickening δ s) ≤ infEDist x s - ENNReal.ofReal δ

Tactic:
refine le_sub_of_add_le_right ofReal_ne_top ?_

Premises used: ENNReal.le_sub_of_add_le_right, ENNReal.ofReal_ne_top
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ ≤ infEDist x s

Tactic:
le_infEDist.2 fun z hz => le_of_forall_gt fun r h => ?_

Premises used: Iff.mpr, Metric.le_infEDist, le_of_forall_gt
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
inr : ∀ (z : E) (hz : z ∈ s) (r : ℝ≥0∞) (h : edist x z < r), infEDist x (thickening δ s) + ENNReal.ofReal δ < r
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ ≤ infEDist x s

Tactic:
refine le_infEDist.2 fun z hz => le_of_forall_gt fun r h => ?_

Premises used: Iff.mpr, Metric.le_infEDist, le_of_forall_gt
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
h : edist x z < ∞
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ < ∞

Tactic:
add_lt_top.2 ⟨lt_top_iff_ne_top.2 <| infEDist_ne_top ⟨z, self_subset_thickening hδ _ hz⟩,
      ofReal_lt_top⟩

Premises used: Iff.mpr, ENNReal.ofReal_lt_top, Metric.infEDist_ne_top, lt_top_iff_ne_top, And.intro, Metric.self_subset_thickening, Exists.intro, ENNReal.add_lt_top
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
h : edist x z < ∞
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ < ∞

Tactic:
exact add_lt_top.2 ⟨lt_top_iff_ne_top.2 <| infEDist_ne_top ⟨z, self_subset_thickening hδ _ hz⟩,
      ofReal_lt_top⟩

Premises used: Iff.mpr, ENNReal.ofReal_lt_top, Metric.infEDist_ne_top, lt_top_iff_ne_top, And.intro, Metric.self_subset_thickening, Exists.intro, ENNReal.add_lt_top
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < (↑r : ℝ≥0∞)
⊢ 0 < (↑r : ℝ) - δ

Tactic:
sub_pos_of_lt ?_

Premises used: sub_pos_of_lt
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < (↑r : ℝ≥0∞)
refine : δ < (↑r : ℝ)
⊢ 0 < (↑r : ℝ) - δ

Tactic:
refine sub_pos_of_lt ?_

Premises used: sub_pos_of_lt
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < (↑r : ℝ≥0∞)
⊢ ENNReal.ofReal δ < (↑r : ℝ≥0∞)

Tactic:
have := hs.trans_lt ((infEDist_le_edist_of_mem hz).trans_lt h)
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < (↑r : ℝ≥0∞)
this : ENNReal.ofReal δ < (↑r : ℝ≥0∞)
⊢ (↑(NNReal.mk δ ⋯) : ℝ≥0∞) < (↑r : ℝ≥0∞)

Tactic:
rw [ofReal_eq_coe_nnreal hδ.le] at this

Premises used: LT.lt.le, ENNReal.ofReal_eq_coe_nnreal
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < (↑r : ℝ≥0∞)
this : (↑(NNReal.mk δ ⋯) : ℝ≥0∞) < (↑r : ℝ≥0∞)
⊢ δ < (↑r : ℝ)

Tactic:
mod_cast this

Premises used: cast, ENNReal.coe_lt_coe._simp_1, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < (↑r : ℝ≥0∞)
this : (↑(NNReal.mk δ ⋯) : ℝ≥0∞) < (↑r : ℝ≥0∞)
⊢ δ < (↑r : ℝ)

Tactic:
exact mod_cast this
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < (↑r : ℝ≥0∞)
⊢ 0 < (↑r : ℝ) - δ

Tactic:
have hr : 0 < ↑r - δ := by
      refine sub_pos_of_lt ?_
      have := hs.trans_lt ((infEDist_le_edist_of_mem hz).trans_lt h)
      rw [ofReal_eq_coe_nnreal hδ.le] at this
      exact mod_cast this
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < (↑r : ℝ≥0∞)
hr : 0 < (↑r : ℝ) - δ
⊢ dist x z < δ + ((↑r : ℝ) - δ)

Tactic:
rw [edist_lt_coe, ← dist_lt_coe, ← add_sub_cancel δ ↑r] at h

Premises used: edist_lt_coe, dist_lt_coe, add_sub_cancel, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : edist x z < (↑r : ℝ≥0∞)
hr : 0 < (↑r : ℝ) - δ
h₁ : dist x z < δ + ((↑r : ℝ) - δ)
⊢ 0 < (↑r : ℝ) - δ

Tactic:
rw [edist_lt_coe, ← dist_lt_coe, ← add_sub_cancel δ ↑r] at h

Premises used: edist_lt_coe, dist_lt_coe, add_sub_cancel, NNReal.toReal
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : dist x z < δ + ((↑r : ℝ) - δ)
hr : 0 < (↑r : ℝ) - δ
inr :
  ∀ (y : E) (hxy : dist x y < (↑r : ℝ) - δ) (hyz : dist y z < δ),
    infEDist x (thickening δ s) + ENNReal.ofReal δ < (↑r : ℝ≥0∞)
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ < (↑r : ℝ≥0∞)

Tactic:
obtain ⟨y, hxy, hyz⟩ := exists_dist_lt_lt hr hδ h

Premises used: exists_dist_lt_lt
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : dist x z < δ + ((↑r : ℝ) - δ)
hr : 0 < (↑r : ℝ) - δ
y : E
hxy : dist x y < (↑r : ℝ) - δ
hyz : dist y z < δ
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ < (↑r : ℝ≥0∞)

Tactic:
(ENNReal.add_lt_add_right ofReal_ne_top <|
      infEDist_lt_iff.2 ⟨_, mem_thickening_iff.2 ⟨_, hz, hyz⟩, edist_lt_ofReal.2 hxy⟩).trans_le ?_

Premises used: Iff.mpr, Metric.mem_thickening_iff, edist_lt_ofReal, LT.lt.trans_le, And.intro, Exists.intro, ENNReal.ofReal_ne_top, Metric.infEDist_lt_iff, ENNReal.add_lt_add_right
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : dist x z < δ + ((↑r : ℝ) - δ)
hr : 0 < (↑r : ℝ) - δ
y : E
hxy : dist x y < (↑r : ℝ) - δ
hyz : dist y z < δ
inr : ENNReal.ofReal ((↑r : ℝ) - δ) + ENNReal.ofReal δ ≤ (↑r : ℝ≥0∞)
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ < (↑r : ℝ≥0∞)

Tactic:
refine (ENNReal.add_lt_add_right ofReal_ne_top <|
      infEDist_lt_iff.2 ⟨_, mem_thickening_iff.2 ⟨_, hz, hyz⟩, edist_lt_ofReal.2 hxy⟩).trans_le ?_

Premises used: Iff.mpr, Metric.mem_thickening_iff, edist_lt_ofReal, LT.lt.trans_le, And.intro, Exists.intro, ENNReal.ofReal_ne_top, Metric.infEDist_lt_iff, ENNReal.add_lt_add_right
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : NNReal
h : dist x z < δ + ((↑r : ℝ) - δ)
hr : 0 < (↑r : ℝ) - δ
y : E
hxy : dist x y < (↑r : ℝ) - δ
hyz : dist y z < δ
inr : ENNReal.ofReal ((↑r : ℝ) - δ + δ) ≤ (↑r : ℝ≥0∞)
inr₁ : ENNReal.ofReal (↑r : ℝ) ≤ (↑r : ℝ≥0∞)
inr₂ inr₃ : (↑r : ℝ≥0∞) ≤ (↑r : ℝ≥0∞)
⊢ ENNReal.ofReal ((↑r : ℝ) - δ) + ENNReal.ofReal δ ≤ (↑r : ℝ≥0∞)

Tactic:
rw [← ofReal_add hr.le hδ.le, sub_add_cancel, ofReal_coe_nnreal]

Premises used: LT.lt.le, ENNReal.ofReal_coe_nnreal, ENNReal.ofReal_add, sub_add_cancel
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
hs : ENNReal.ofReal δ ≤ infEDist x s
z : E
hz : z ∈ s
r : ℝ≥0∞
h : edist x z < r
inr : ∀ (h : edist x z < ∞), infEDist x (thickening δ s) + ENNReal.ofReal δ < ∞
inr₁ : ∀ (r : NNReal) (h : edist x z < (↑r : ℝ≥0∞)), infEDist x (thickening δ s) + ENNReal.ofReal δ < (↑r : ℝ≥0∞)
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ < r

Tactic:
cases r with
  | top =>
    exact add_lt_top.2 ⟨lt_top_iff_ne_top.2 <| infEDist_ne_top ⟨z, self_subset_thickening hδ _ hz⟩,
      ofReal_lt_top⟩
  | coe r =>
    have hr : 0 < ↑r - δ := by
      refine sub_pos_of_lt ?_
      have := hs.trans_lt ((infEDist_le_edist_of_mem hz).trans_lt h)
      rw [ofReal_eq_coe_nnreal hδ.le] at this
      exact mod_cast this
    rw [edist_lt_coe, ← dist_lt_coe, ← add_sub_cancel δ ↑r] at h
    obtain ⟨y, hxy, hyz⟩ := exists_dist_lt_lt hr hδ h
    refine (ENNReal.add_lt_add_right ofReal_ne_top <|
      infEDist_lt_iff.2 ⟨_, mem_thickening_iff.2 ⟨_, hz, hyz⟩, edist_lt_ofReal.2 hxy⟩).trans_le ?_
    rw [← ofReal_add hr.le hδ.le, sub_add_cancel, ofReal_coe_nnreal]

Premises used: Iff.mpr, ENNReal.ofReal_lt_top, Metric.infEDist_ne_top, lt_top_iff_ne_top, edist_lt_coe, dist_lt_coe, And.intro, Metric.self_subset_thickening, ENNReal.ofReal_coe_nnreal, Exists.intro, ENNReal.add_lt_top, sub_add_cancel
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x : E
simp_rw : (∃ z ∈ s, dist x z < ε + δ) → ∃ (z : E), (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε
⊢ x ∈ thickening (ε + δ) s → x ∈ thickening ε (thickening δ s)

Tactic:
simp_rw [mem_thickening_iff]

Premises used: Metric.mem_thickening_iff
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x z : E
hz : z ∈ s
hxz : dist x z < ε + δ
⊢ dist x z < δ + ε

Tactic:
rw [add_comm] at hxz

Premises used: add_comm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x z : E
hz : z ∈ s
hxz : dist x z < δ + ε
obtain : ∀ (y : E) (hxy : dist x y < ε) (hyz : dist y z < δ), ∃ (z : E), (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε
⊢ ∃ (z : E), (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε

Tactic:
obtain ⟨y, hxy, hyz⟩ := exists_dist_lt_lt hε hδ hxz

Premises used: exists_dist_lt_lt
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x z : E
hz : z ∈ s
hxz : dist x z < δ + ε
y : E
hxy : dist x y < ε
hyz : dist y z < δ
⊢ ∃ (z : E), (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε

Tactic:
⟨y, ⟨_, hz, hyz⟩, hxy⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x z : E
hz : z ∈ s
hxz : dist x z < δ + ε
y : E
hxy : dist x y < ε
hyz : dist y z < δ
⊢ ∃ (z : E), (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε

Tactic:
exact ⟨y, ⟨_, hz, hyz⟩, hxy⟩