awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : Membership.mem (γ := Filter 𝕜) (𝓝 0) (closedBall 0 (ε / R))
r : 𝕜
hr : Membership.mem (γ := Set 𝕜) (closedBall 0 (ε / R)) r
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ -x + x_1) ⁻¹' (r • s)) y
h : ∀ (z : E) (zs : z ∈ s) (hz : r • z = -x + y), y ∈ u
⊢ y ∈ u

Tactic:
obtain ⟨z, zs, hz⟩ : ∃ z : E, z ∈ s ∧ r • z = -x + y := by simpa [mem_smul_set] using hy
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : Membership.mem (γ := Filter 𝕜) (𝓝 0) (closedBall 0 (ε / R))
r : 𝕜
hr : Membership.mem (γ := Set 𝕜) (closedBall 0 (ε / R)) r
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ -x + x_1) ⁻¹' (r • s)) y
z : E
zs : z ∈ s
hz : r • z = -x + y
h₁ : ‖r‖ ≤ ε / R
h₂ : ‖z‖ ≤ R
⊢ ‖r‖ * ‖z‖ ≤ ε / R * R

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : Membership.mem (γ := Filter 𝕜) (𝓝 0) (closedBall 0 (ε / R))
r : 𝕜
hr : Membership.mem (γ := Set 𝕜) (closedBall 0 (ε / R)) r
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ -x + x_1) ⁻¹' (r • s)) y
z : E
zs : z ∈ s
hz : r • z = -x + y
⊢ ‖r‖ ≤ ε / R

Tactic:
mem_closedBall_zero_iff.1 hr

Premises used: Iff.mp, mem_closedBall_zero_iff
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : Membership.mem (γ := Filter 𝕜) (𝓝 0) (closedBall 0 (ε / R))
r : 𝕜
hr : Membership.mem (γ := Set 𝕜) (closedBall 0 (ε / R)) r
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ -x + x_1) ⁻¹' (r • s)) y
z : E
zs : z ∈ s
hz : r • z = -x + y
⊢ ‖z‖ ≤ R

Tactic:
mem_closedBall_zero_iff.1 (hR zs)

Premises used: Iff.mp, mem_closedBall_zero_iff
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : Membership.mem (γ := Filter 𝕜) (𝓝 0) (closedBall 0 (ε / R))
r : 𝕜
hr : Membership.mem (γ := Set 𝕜) (closedBall 0 (ε / R)) r
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ -x + x_1) ⁻¹' (r • s)) y
z : E
zs : z ∈ s
hz : r • z = -x + y
⊢ ‖r‖ ≤ ε / R

Tactic:
exacts [mem_closedBall_zero_iff.1 hr, mem_closedBall_zero_iff.1 (hR zs)]

Premises used: Iff.mp, mem_closedBall_zero_iff
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : Membership.mem (γ := Filter 𝕜) (𝓝 0) (closedBall 0 (ε / R))
r : 𝕜
hr : Membership.mem (γ := Set 𝕜) (closedBall 0 (ε / R)) r
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ -x + x_1) ⁻¹' (r • s)) y
z : E
zs : z ∈ s
hz : r • z = -x + y
⊢ ε / R * R = ε

Tactic:
field
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : Membership.mem (γ := Filter 𝕜) (𝓝 0) (closedBall 0 (ε / R))
r : 𝕜
hr : Membership.mem (γ := Set 𝕜) (closedBall 0 (ε / R)) r
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ -x + x_1) ⁻¹' (r • s)) y
z : E
zs : z ∈ s
hz : r • z = -x + y
⊢ ‖r • z‖ ≤ ε

Tactic:
have I : ‖r • z‖ ≤ ε :=
    calc
      ‖r • z‖ = ‖r‖ * ‖z‖ := norm_smul _ _
      _ ≤ ε / R * R := by
        gcongr
        exacts [mem_closedBall_zero_iff.1 hr, mem_closedBall_zero_iff.1 (hR zs)]
      _ = ε := by field
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : Membership.mem (γ := Filter 𝕜) (𝓝 0) (closedBall 0 (ε / R))
r : 𝕜
hr : Membership.mem (γ := Set 𝕜) (closedBall 0 (ε / R)) r
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ -x + x_1) ⁻¹' (r • s)) y
z : E
zs : z ∈ s
hz : r • z = -x + y
I : ‖r • z‖ ≤ ε
⊢ y = x + r • z

Tactic:
simp only [hz, add_neg_cancel_left]

Premises used: add_neg_cancel_left
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this : Membership.mem (γ := Filter 𝕜) (𝓝 0) (closedBall 0 (ε / R))
r : 𝕜
hr : Membership.mem (γ := Set 𝕜) (closedBall 0 (ε / R)) r
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ -x + x_1) ⁻¹' (r • s)) y
z : E
zs : z ∈ s
hz : r • z = -x + y
I : ‖r • z‖ ≤ ε
⊢ y = x + r • z

Tactic:
have : y = x + r • z := by simp only [hz, add_neg_cancel_left]
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this_1 : Membership.mem (γ := Filter 𝕜) (𝓝 0) (closedBall 0 (ε / R))
r : 𝕜
hr : Membership.mem (γ := Set 𝕜) (closedBall 0 (ε / R)) r
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ -x + x_1) ⁻¹' (r • s)) y
z : E
zs : z ∈ s
hz : r • z = -x + y
I : ‖r • z‖ ≤ ε
this : y = x + r • z
h : y ∈ closedBall x ε
⊢ y ∈ u

Tactic:
apply hε
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
s : Set E
hs : Bornology.IsBounded s
u : Set E
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
R : ℝ
Rpos : 0 < R
hR : s ⊆ closedBall 0 R
this_1 : Membership.mem (γ := Filter 𝕜) (𝓝 0) (closedBall 0 (ε / R))
r : 𝕜
hr : Membership.mem (γ := Set 𝕜) (closedBall 0 (ε / R)) r
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ -x + x_1) ⁻¹' (r • s)) y
z : E
zs : z ∈ s
hz : r • z = -x + y
I : ‖r • z‖ ≤ ε
this : y = x + r • z
⊢ y ∈ closedBall x ε

Tactic:
simpa only [this, dist_eq_norm, add_sub_cancel_left, mem_closedBall] using I

Premises used: dist_eq_norm, add_sub_cancel_left, Metric.mem_closedBall
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
rw : Eq.{u_2 + 1} (α := Set E) (ball 0 ‖r‖) (ball 0 r)
rw₁ rw₂ : Eq.{u_2 + 1} (α := Set E) (ball 0 r) (ball 0 r)
⊢ HSMul.hSMul (β := Set E) r (ball 0 1) = ball 0 r

Tactic:
rw [smul_unitBall hr.ne', Real.norm_of_nonneg hr.le]

Premises used: LT.lt.le, LT.lt.ne', smul_unitBall, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
⊢ EqOn (fun (x : ℝ) ↦ ‖x‖) id (Ioo a b)

Tactic:
have : EqOn (‖·‖) id (Ioo a b) := fun x hx ↦ abs_of_pos (ha.trans_lt hx.1)
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun (x : ℝ) ↦ ‖x‖) id (Ioo a b)
⊢ 0 ∉ Ioo a b

Tactic:
simp [ha.not_gt]

Premises used: LE.le.not_gt
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun (x : ℝ) ↦ ‖x‖) id (Ioo a b)
rw : Eq.{u_2 + 1} (α := Set E) ((fun (x : E) ↦ ‖x‖) ⁻¹' Ioo (a * r) (b * r)) (ball 0 (b * r) \ closedBall 0 (a * r))
⊢ HSMul.hSMul (β := Set E) (Ioo a b) (sphere 0 r) = ball 0 (b * r) \ closedBall 0 (a * r)

Tactic:
rw [set_smul_sphere_zero (by simp [ha.not_gt]), ← image_image (· * r), this.image_eq, image_id,
    image_mul_right_Ioo _ _ hr]

Premises used: Set.image_image, HMul.hMul, set_smul_sphere_zero, Set.image_mul_right_Ioo, Set.EqOn.image_eq, Set.image_id
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun (x : ℝ) ↦ ‖x‖) id (Ioo a b)
h :
  ∀ (x : E),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ ‖x‖) ⁻¹' Ioo (a * r) (b * r)) x ↔
      Membership.mem (γ := Set E) (ball 0 (b * r) \ closedBall 0 (a * r)) x
⊢ Eq.{u_2 + 1} (α := Set E) ((fun (x : E) ↦ ‖x‖) ⁻¹' Ioo (a * r) (b * r)) (ball 0 (b * r) \ closedBall 0 (a * r))

Tactic:
ext x
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
this : EqOn (fun (x : ℝ) ↦ ‖x‖) id (Ioo a b)
x : E
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ ‖x‖) ⁻¹' Ioo (a * r) (b * r)) x ↔
    Membership.mem (γ := Set E) (ball 0 (b * r) \ closedBall 0 (a * r)) x

Tactic:
simp [and_comm]

Premises used: and_comm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : dist x (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) z = a * dist x z
⊢ ∃ (y : E), dist x y = b * dist x z ∧ dist y z = a * dist x z

Tactic:
use a • x + b • z
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : dist (HSMul.hSMul (α := ℝ) 1 x) (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) z = a * dist x z
⊢ dist x (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) z = a * dist x z

Tactic:
nth_rw 1 [← one_smul ℝ x]

Premises used: Real, one_smul
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h :
  dist (HSMul.hSMul (α := ℝ) 1 x) (a • x + b • z) = b * dist x z ∧
    dist (a • x + b • z) (HSMul.hSMul (α := ℝ) 1 z) = a * dist x z
⊢ dist (HSMul.hSMul (α := ℝ) 1 x) (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) z = a * dist x z

Tactic:
nth_rw 4 [← one_smul ℝ z]

Premises used: Real, one_smul
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ dist (HSMul.hSMul (α := ℝ) 1 x) (a • x + b • z) = b * dist x z ∧
    dist (a • x + b • z) (HSMul.hSMul (α := ℝ) 1 z) = a * dist x z

Tactic:
simp [dist_eq_norm, ← hab, add_smul, ← smul_sub, norm_smul_of_nonneg, ha, hb]

Premises used: dist_eq_norm, norm_smul_of_nonneg, smul_sub, add_smul
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
inl : ∀ (hε : LE.le (α := ℝ) 0 0) (h : dist x z ≤ 0 + δ), ∃ (y : E), dist x y ≤ δ ∧ dist y z ≤ 0
inr : ∀ (hε' : 0 < ε), ∃ (y : E), dist x y ≤ δ ∧ dist y z ≤ ε
⊢ ∃ (y : E), dist x y ≤ δ ∧ dist y z ≤ ε

Tactic:
obtain rfl | hε' := hε.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ : ℝ
hδ : 0 ≤ δ
hε : LE.le (α := ℝ) 0 0
h : dist x z ≤ 0 + δ
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : dist x z ≤ δ), dist x z ≤ δ
⊢ dist x z ≤ δ

Tactic:
rwa [zero_add] at h

Premises used: zero_add
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ : ℝ
hδ : 0 ≤ δ
hε : LE.le (α := ℝ) 0 0
h : dist x z ≤ 0 + δ
⊢ ∃ (y : E), dist x y ≤ δ ∧ dist y z ≤ 0

Tactic:
exact ⟨z, by rwa [zero_add] at h, (dist_self _).le⟩
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
⊢ 0 < ε + δ

Tactic:
have hεδ := add_pos_of_pos_of_nonneg hε' hδ
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
hεδ : 0 < ε + δ
rw : (ε + δ) / (ε + δ) = 1
rw₁ rw₂ : Eq (α := ℝ) 1 1
⊢ ε / (ε + δ) + δ / (ε + δ) = 1

Tactic:
rw [← add_div, div_self hεδ.ne']

Premises used: LT.lt.ne', div_self, add_div
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
hεδ : 0 < ε + δ
inr :
  ∀ (y : E) (hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z), dist x y ≤ δ ∧ dist y z ≤ ε
⊢ ∃ (y : E), dist x y ≤ δ ∧ dist y z ≤ ε

Tactic:
refine (exists_dist_eq x z (div_nonneg hε <| add_nonneg hε hδ)
    (div_nonneg hδ <| add_nonneg hε hδ) <| by
      rw [← add_div, div_self hεδ.ne']).imp
    fun y hy => ?_

Premises used: exists_dist_eq, add_nonneg, Exists.imp, div_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
hεδ : 0 < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
inr : dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε ≤ ε
⊢ dist x y ≤ δ ∧ dist y z ≤ ε

Tactic:
rw [hy.1, hy.2, div_mul_comm, div_mul_comm ε]

Premises used: And.right, And.left, div_mul_comm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
hεδ : 0 < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
inr :
  ∀ (h : dist x z / (ε + δ) ≤ 1) (hε' : 0 < ε) (hεδ : 0 < ε + δ) (y : E)
    (hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z),
    dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε ≤ ε
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε ≤ ε

Tactic:
rw [← div_le_one hεδ] at h

Premises used: div_le_one
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z / (ε + δ) ≤ 1
hε' : 0 < ε
hεδ : 0 < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε ≤ ε

Tactic:
⟨mul_le_of_le_one_left hδ h, mul_le_of_le_one_left hε h⟩

Premises used: mul_le_of_le_one_left, And.intro
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z / (ε + δ) ≤ 1
hε' : 0 < ε
hεδ : 0 < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε ≤ ε

Tactic:
exact ⟨mul_le_of_le_one_left hδ h, mul_le_of_le_one_left hε h⟩
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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
rw₁ rw₂ : Eq (α := ℝ) 1 1
⊢ ε / (ε + δ) + δ / (ε + δ) = 1

Tactic:
rw [← add_div, div_self (add_pos_of_pos_of_nonneg hε hδ).ne']

Premises used: LT.lt.ne', div_self, add_pos_of_pos_of_nonneg, add_div
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
h : dist x z < ε + δ
refine :
  ∀ (y : E) (hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z), dist x y ≤ δ ∧ dist y z < ε
⊢ ∃ (y : E), 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 => ?_

Premises used: exists_dist_eq, LT.lt.le, add_nonneg, Exists.imp, div_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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
rw : dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε < ε
⊢ dist x y ≤ δ ∧ dist y z < ε

Tactic:
rw [hy.1, hy.2, div_mul_comm, div_mul_comm ε]

Premises used: And.right, And.left, div_mul_comm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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
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 / (ε + δ) * ε < ε
⊢ dist x z / (ε + δ) * δ ≤ δ ∧ dist x z / (ε + δ) * ε < ε

Tactic:
rw [← div_lt_one (add_pos_of_pos_of_nonneg hε hδ)] at h

Premises used: div_lt_one, add_pos_of_pos_of_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
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:
⟨mul_le_of_le_one_left hδ h.le, mul_lt_of_lt_one_left hε h⟩

Premises used: LT.lt.le, mul_le_of_le_one_left, And.intro, mul_lt_of_lt_one_left
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 < ε
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:
exact ⟨mul_le_of_le_one_left hδ h.le, mul_lt_of_lt_one_left hε h⟩
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : dist x z < ε + δ
⊢ dist z x < δ + ε

Tactic:
simpa only [dist_comm, add_comm] using h

Premises used: dist_comm, add_comm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 ≤ ε
h : dist x z < ε + δ
obtain : ∀ (y : E) (yz : dist z y ≤ ε) (xy : dist y x < δ), ∃ (y : E), dist x y < δ ∧ dist y z ≤ ε
⊢ ∃ (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)

Premises used: exists_dist_le_lt
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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
yz : dist z y ≤ ε
xy : dist y x < δ
⊢ dist x y < δ ∧ dist y z ≤ ε

Tactic:
simp [dist_comm x y, dist_comm y z, *]

Premises used: dist_comm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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
yz : dist z y ≤ ε
xy : dist y x < δ
⊢ ∃ (y : E), dist x y < δ ∧ dist y z ≤ ε

Tactic:
exact ⟨y, by simp [dist_comm x y, dist_comm y z, *]⟩
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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
rw₁ rw₂ : Eq (α := ℝ) 1 1
⊢ ε / (ε + δ) + δ / (ε + δ) = 1

Tactic:
rw [← add_div, div_self (add_pos hε hδ).ne']

Premises used: add_pos, LT.lt.ne', div_self, add_div
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
h : dist x z < ε + δ
refine :
  ∀ (y : E) (hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z), dist x y < δ ∧ dist y z < ε
⊢ ∃ (y : E), 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 => ?_

Premises used: exists_dist_eq, LT.lt.le, add_nonneg, Exists.imp, div_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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
rw : dist x z / (ε + δ) * δ < δ ∧ dist x z / (ε + δ) * ε < ε
⊢ dist x y < δ ∧ dist y z < ε

Tactic:
rw [hy.1, hy.2, div_mul_comm, div_mul_comm ε]

Premises used: And.right, And.left, div_mul_comm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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
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 / (ε + δ) * ε < ε
⊢ dist x z / (ε + δ) * δ < δ ∧ dist x z / (ε + δ) * ε < ε

Tactic:
rw [← div_lt_one (add_pos hε hδ)] at h

Premises used: add_pos, div_lt_one
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
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:
⟨mul_lt_of_lt_one_left hδ h, mul_lt_of_lt_one_left hε h⟩

Premises used: And.intro, mul_lt_of_lt_one_left
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
x z : E
δ ε : ℝ
hδ : 0 < δ
hε : 0 < ε
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:
exact ⟨mul_lt_of_lt_one_left hδ h, mul_lt_of_lt_one_left hε h⟩
-- 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 δ) (ball y ε) ↔ δ + ε ≤ dist x y

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

Premises used: Metric.ball_disjoint_ball, le_of_not_gt, Iff.intro