awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z < ε + δ
⊢ ∃ (y : E), dist x y ≤ δ ∧ dist y z < ε
have refine : ∀ (y : E) (hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z), dist x y ≤ δ ∧ dist y z < ε
Tactic: refine (exists_dist_eq x z (div_nonneg hε.le <| add_nonneg hε.le hδ)
    (div_nonneg hδ <| add_nonneg hε.le hδ) <| by
      rw [← add_div, div_self (add_pos_of_pos_of_nonneg hε hδ).ne']).imp
    fun y hy => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x y ≤ δ ∧ dist y z < ε
have rw : dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε < ε
Tactic: rw [hy.1, hy.2, div_mul_comm, div_mul_comm ε]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε < ε
have rw : ∀ (h : dist x z / (ε + δ) < 1) (y : E) (hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z),
  dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε < ε
Tactic: rw [← div_lt_one (add_pos_of_pos_of_nonneg hε hδ)] at h
Cleared hypotheses: h, y, hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : dist x z < ε + δ
⊢ ∃ (y : E), dist x y < δ ∧ dist y z ≤ ε
have obtain : ∀ (y : E) (yz : dist z y ≤ ε) (xy : dist y x < δ), ∃ (y : E), dist x y < δ ∧ dist y z ≤ ε
Tactic: obtain ⟨y, yz, xy⟩ :=
    exists_dist_le_lt hε hδ (show dist z x < δ + ε by simpa only [dist_comm, add_comm] using h)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
⊢ ε / (ε + δ) + δ / (ε + δ) = 1
have rw : (ε + δ) / (ε + δ) = 1
Tactic: rw [← add_div, div_self (add_pos hε hδ).ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
rw : (ε + δ) / (ε + δ) = 1
⊢ ε / (ε + δ) + δ / (ε + δ) = 1
have rw₁ : Eq (α := ℝ) 1 1
Tactic: rw [← add_div, div_self (add_pos hε hδ).ne']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
⊢ ∃ (y : E), dist x y < δ ∧ dist y z < ε
have refine : ∀ (y : E) (hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z), dist x y < δ ∧ dist y z < ε
Tactic: refine (exists_dist_eq x z (div_nonneg hε.le <| add_nonneg hε.le hδ.le)
    (div_nonneg hδ.le <| add_nonneg hε.le hδ.le) <| by
      rw [← add_div, div_self (add_pos hε hδ).ne']).imp
    fun y hy => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x y < δ ∧ dist y z < ε
have rw : dist x z / (ε + δ) * δ < δ ∧ dist x z / (ε + δ) * ε < ε
Tactic: rw [hy.1, hy.2, div_mul_comm, div_mul_comm ε]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ < δ ∧ dist x z / (ε + δ) * ε < ε
have rw : ∀ (h : dist x z / (ε + δ) < 1) (y : E) (hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z),
  dist x z / (ε + δ) * δ < δ ∧ dist x z / (ε + δ) * ε < ε
Tactic: rw [← div_lt_one (add_pos hε hδ)] at h
Cleared hypotheses: h, y, hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
⊢ Disjoint (ball x δ) (ball y ε) ↔ δ + ε ≤ dist x y
have refine : ∀ (h : Disjoint (ball x δ) (ball y ε)) (hxy : dist x y < δ + ε), False
Tactic: refine ⟨fun h => le_of_not_gt fun hxy => ?_, ball_disjoint_ball⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (hypothesis)
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 < δ + ε
⊢ False
have hxy₁ : dist x y < ε + δ
Tactic: rw [add_comm] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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 < ε + δ
⊢ False
have obtain : ∀ (z : E) (hxz : dist x z < δ) (hzy : dist z y < ε), False
Tactic: obtain ⟨z, hxz, hzy⟩ := exists_dist_lt_lt hδ hε hxy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (hypothesis)
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 < ε
⊢ False
have hxz₁ : dist z x < δ
Tactic: rw [dist_comm] at hxz
Cleared hypotheses: hxz, hzy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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
have refine : ∀ (h : Disjoint (ball x δ) (closedBall y ε)) (hxy : dist x y < δ + ε), False
Tactic: refine ⟨fun h => le_of_not_gt fun hxy => ?_, ball_disjoint_closedBall⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (hypothesis)
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 < δ + ε
⊢ False
have hxy₁ : dist x y < ε + δ
Tactic: rw [add_comm] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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 < ε + δ
⊢ False
have obtain : ∀ (z : E) (hxz : dist x z < δ) (hzy : dist z y ≤ ε), False
Tactic: obtain ⟨z, hxz, hzy⟩ := exists_dist_lt_le hδ hε hxy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (hypothesis)
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 ≤ ε
⊢ False
have hxz₁ : dist z x < δ
Tactic: rw [dist_comm] at hxz
Cleared hypotheses: hxz, hzy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x y : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
⊢ Disjoint (closedBall x δ) (ball y ε) ↔ δ + ε ≤ dist x y
have rw : Disjoint (ball y ε) (closedBall x δ) ↔ δ + ε ≤ dist x y
Tactic: rw [disjoint_comm, disjoint_ball_closedBall_iff hε hδ, add_comm, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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
⊢ Disjoint (closedBall x δ) (ball y ε) ↔ δ + ε ≤ dist x y
have rw₁ : ε + δ ≤ dist y x ↔ δ + ε ≤ dist x y
Tactic: rw [disjoint_comm, disjoint_ball_closedBall_iff hε hδ, add_comm, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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
⊢ Disjoint (closedBall x δ) (ball y ε) ↔ δ + ε ≤ dist x y
have rw₂ : δ + ε ≤ dist y x ↔ δ + ε ≤ dist x y
Tactic: rw [disjoint_comm, disjoint_ball_closedBall_iff hε hδ, add_comm, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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
⊢ Disjoint (closedBall x δ) (ball y ε) ↔ δ + ε ≤ dist x y
have rw₃ : δ + ε ≤ dist x y ↔ δ + ε ≤ dist x y
Tactic: rw [disjoint_comm, disjoint_ball_closedBall_iff hε hδ, add_comm, dist_comm]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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
have refine : ∀ (h : Disjoint (closedBall x δ) (closedBall y ε)) (hxy : dist x y ≤ δ + ε), False
Tactic: refine ⟨fun h => lt_of_not_ge fun hxy => ?_, closedBall_disjoint_closedBall⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (hypothesis)
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 ≤ δ + ε
⊢ False
have hxy₁ : dist x y ≤ ε + δ
Tactic: rw [add_comm] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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 ≤ ε + δ
⊢ False
have obtain : ∀ (z : E) (hxz : dist x z ≤ δ) (hzy : dist z y ≤ ε), False
Tactic: obtain ⟨z, hxz, hzy⟩ := exists_dist_le_le hδ hε hxy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (hypothesis)
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 ≤ ε
⊢ False
have hxz₁ : dist z x ≤ δ
Tactic: rw [dist_comm] at hxz
Cleared hypotheses: hxz, hzy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
x : E
⊢ infEDist x (thickening δ s) = infEDist x s - ENNReal.ofReal δ
have inl : ∀ (hs : 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 δ)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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 δ
⊢ infEDist x (thickening δ s) = infEDist x s - ENNReal.ofReal δ
have inr : ∀ (hs : ENNReal.ofReal δ ≤ infEDist x s), infEDist x (thickening δ s) = infEDist x s - ENNReal.ofReal δ
Tactic: obtain hs | hs := lt_or_ge (infEDist x s) (ENNReal.ofReal δ)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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 δ
⊢ infEDist x (thickening δ s) = infEDist x s - ENNReal.ofReal δ
have inl : x ∈ thickening δ s
Tactic: rw [infEDist_zero_of_mem, tsub_eq_zero_of_le hs.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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 δ
have inr : infEDist x (thickening δ s) ≤ infEDist x s - ENNReal.ofReal δ
Tactic: refine (tsub_le_iff_right.2 infEDist_le_infEDist_thickening_add).antisymm' ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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 δ
have inr : infEDist x (thickening δ s) + ENNReal.ofReal δ ≤ infEDist x s
Tactic: refine le_sub_of_add_le_right ofReal_ne_top ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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
have inr : ∀ (z : E) (hz : z ∈ s) (r : ℝ≥0∞) (h : edist x z < r), infEDist x (thickening δ s) + ENNReal.ofReal δ < r
Tactic: refine le_infEDist.2 fun z hz => le_of_forall_gt fun r h => ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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 : ℝ) - δ
have refine : δ < (↑r : ℝ)
Tactic: refine sub_pos_of_lt ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (hypothesis)
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∞)
⊢ δ < (↑r : ℝ)
have this : ENNReal.ofReal δ < (↑r : ℝ≥0∞)
Tactic: have := hs.trans_lt ((infEDist_le_edist_of_mem hz).trans_lt h)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (hypothesis)
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∞)
⊢ δ < (↑r : ℝ)
have this₁ : (↑(NNReal.mk δ sorry) : ℝ≥0∞) < (↑r : ℝ≥0∞)
Tactic: rw [ofReal_eq_coe_nnreal hδ.le] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (hypothesis)
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∞)
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ < (↑r : ℝ≥0∞)
have hr : 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (hypothesis)
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 : ℝ) - δ
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ < (↑r : ℝ≥0∞)
have h₁ : dist x z < δ + ((↑r : ℝ) - δ)
Tactic: rw [edist_lt_coe, ← dist_lt_coe, ← add_sub_cancel δ ↑r] at h
Cleared hypotheses: h, hr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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 : ℝ) - δ
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ < (↑r : ℝ≥0∞)
have inr : ∀ (y : E) (hxy : dist x y < (↑r : ℝ) - δ) (hyz : dist y z < δ),
  infEDist x (thickening δ s) + ENNReal.ofReal δ < (↑r : ℝ≥0∞)
Tactic: obtain ⟨y, hxy, hyz⟩ := exists_dist_lt_lt hr hδ h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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∞)
have inr : ENNReal.ofReal ((↑r : ℝ) - δ) + 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 ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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 < δ
⊢ ENNReal.ofReal ((↑r : ℝ) - δ) + ENNReal.ofReal δ ≤ (↑r : ℝ≥0∞)
have inr : ENNReal.ofReal ((↑r : ℝ) - δ + δ) ≤ (↑r : ℝ≥0∞)
Tactic: rw [← ofReal_add hr.le hδ.le, sub_add_cancel, ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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∞)
⊢ ENNReal.ofReal ((↑r : ℝ) - δ) + ENNReal.ofReal δ ≤ (↑r : ℝ≥0∞)
have inr₁ : ENNReal.ofReal (↑r : ℝ) ≤ (↑r : ℝ≥0∞)
Tactic: rw [← ofReal_add hr.le hδ.le, sub_add_cancel, ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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∞)
⊢ ENNReal.ofReal ((↑r : ℝ) - δ) + ENNReal.ofReal δ ≤ (↑r : ℝ≥0∞)
have inr₂ : (↑r : ℝ≥0∞) ≤ (↑r : ℝ≥0∞)
Tactic: rw [← ofReal_add hr.le hδ.le, sub_add_cancel, ofReal_coe_nnreal]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ < r
have inr : ∀ (h : edist x z < ∞), infEDist x (thickening δ s) + ENNReal.ofReal δ < ∞
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]
Cleared hypotheses: r, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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 δ < ∞
⊢ infEDist x (thickening δ s) + ENNReal.ofReal δ < r
have inr₁ : ∀ (r : NNReal) (h : edist x z < (↑r : ℝ≥0∞)), infEDist x (thickening δ s) + ENNReal.ofReal δ < (↑r : ℝ≥0∞)
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]
Cleared hypotheses: r, h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
s : Set E
x : E
⊢ x ∈ thickening (ε + δ) s → x ∈ thickening ε (thickening δ s)
have simp_rw : (∃ z ∈ s, dist x z < ε + δ) → ∃ (z : E), (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε
Tactic: simp_rw [mem_thickening_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (hypothesis)
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 < ε + δ
⊢ ∃ (z : E), (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε
have hxz₁ : dist x z < δ + ε
Tactic: rw [add_comm] at hxz
Cleared hypotheses: hxz
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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 < δ + ε
⊢ ∃ (z : E), (∃ z_1 ∈ s, dist z z_1 < δ) ∧ dist x z < ε
have obtain : ∀ (y : E) (hxy : dist x y < ε) (hyz : dist y 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
s : Set E
x : E
⊢ x ∈ cthickening (ε + δ) s → x ∈ cthickening ε (thickening δ s)
have simp_rw : infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEDist x s - ENNReal.ofReal δ ≤ ENNReal.ofReal ε
Tactic: simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ.le, infEDist_thickening hδ]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening δ s) = cthickening δ s
have rw : cthickening 0 (thickening δ s) = cthickening δ s
Tactic: rw [← cthickening_zero, cthickening_thickening le_rfl hδ, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
rw : cthickening 0 (thickening δ s) = cthickening δ s
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening δ s) = cthickening δ s
have rw₁ : cthickening (0 + δ) s = cthickening δ s
Tactic: rw [← cthickening_zero, cthickening_thickening le_rfl hδ, zero_add]