awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
⊢ infDist (c • x) (c • s) = ‖c‖ * infDist x s
have simp_rw : (infEDist (c • x) (c • s)).toReal = ‖c‖ * (infEDist x s).toReal
Tactic: simp_rw [Metric.infDist, infEDist_smul₀ hc s, ENNReal.toReal_smul, NNReal.smul_def, coe_nnnorm,
    smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
simp_rw : (infEDist (c • x) (c • s)).toReal = ‖c‖ * (infEDist x s).toReal
⊢ infDist (c • x) (c • s) = ‖c‖ * infDist x s
have simp_rw₁ : (‖c‖₊ • infEDist x s).toReal = ‖c‖ * (infEDist x s).toReal
Tactic: simp_rw [Metric.infDist, infEDist_smul₀ hc s, ENNReal.toReal_smul, NNReal.smul_def, coe_nnnorm,
    smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
simp_rw : (infEDist (c • x) (c • s)).toReal = ‖c‖ * (infEDist x s).toReal
simp_rw₁ : (‖c‖₊ • infEDist x s).toReal = ‖c‖ * (infEDist x s).toReal
⊢ infDist (c • x) (c • s) = ‖c‖ * infDist x s
have simp_rw₂ : ‖c‖₊ • (infEDist x s).toReal = ‖c‖ * (infEDist x s).toReal
Tactic: simp_rw [Metric.infDist, infEDist_smul₀ hc s, ENNReal.toReal_smul, NNReal.smul_def, coe_nnnorm,
    smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
simp_rw : (infEDist (c • x) (c • s)).toReal = ‖c‖ * (infEDist x s).toReal
simp_rw₁ : (‖c‖₊ • infEDist x s).toReal = ‖c‖ * (infEDist x s).toReal
simp_rw₂ : ‖c‖₊ • (infEDist x s).toReal = ‖c‖ * (infEDist x s).toReal
⊢ infDist (c • x) (c • s) = ‖c‖ * infDist x s
have simp_rw₃ : (↑‖c‖₊ : ℝ) • (infEDist x s).toReal = ‖c‖ * (infEDist x s).toReal
Tactic: simp_rw [Metric.infDist, infEDist_smul₀ hc s, ENNReal.toReal_smul, NNReal.smul_def, coe_nnnorm,
    smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
hc : c ≠ 0
s : Set E
x : E
simp_rw : (infEDist (c • x) (c • s)).toReal = ‖c‖ * (infEDist x s).toReal
simp_rw₁ : (‖c‖₊ • infEDist x s).toReal = ‖c‖ * (infEDist x s).toReal
simp_rw₂ : ‖c‖₊ • (infEDist x s).toReal = ‖c‖ * (infEDist x s).toReal
simp_rw₃ : (↑‖c‖₊ : ℝ) • (infEDist x s).toReal = ‖c‖ * (infEDist x s).toReal
⊢ infDist (c • x) (c • s) = ‖c‖ * infDist x s
have simp_rw₄ : ‖c‖ • (infEDist x s).toReal = ‖c‖ * (infEDist x s).toReal
Tactic: simp_rw [Metric.infDist, infEDist_smul₀ hc s, ENNReal.toReal_smul, NNReal.smul_def, coe_nnnorm,
    smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
⊢ c • ball x r = ball (c • x) (‖c‖ * r)
have h : ∀ (y : E), y ∈ c • ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ y ∈ c • ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)
have h : c⁻¹ • y ∈ ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)
Tactic: rw [mem_smul_set_iff_inv_smul_mem₀ hc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
| c⁻¹ • y ∈ ball x r
have rw : c⁻¹ • y ∈ ball (c⁻¹ • c • x) r
Tactic: rw [← inv_smul_smul₀ hc x]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)
have h : c⁻¹ • y ∈ ball (c⁻¹ • c • x) r ↔ y ∈ ball (c • x) (‖c‖ * r)
Tactic: conv_lhs => rw [← inv_smul_smul₀ hc x]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
⊢ HSMul.hSMul (β := Set E) c (ball 0 1) = ball 0 ‖c‖
have rw : ball (HSMul.hSMul (β := E) c 0) (‖c‖ * 1) = ball 0 ‖c‖
Tactic: rw [_root_.smul_ball hc, smul_zero, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
rw : ball (HSMul.hSMul (β := E) c 0) (‖c‖ * 1) = ball 0 ‖c‖
⊢ HSMul.hSMul (β := Set E) c (ball 0 1) = ball 0 ‖c‖
have rw₁ : Eq.{u_2 + 1} (α := Set E) (ball 0 (‖c‖ * 1)) (ball 0 ‖c‖)
Tactic: rw [_root_.smul_ball hc, smul_zero, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
rw : ball (HSMul.hSMul (β := E) c 0) (‖c‖ * 1) = ball 0 ‖c‖
rw₁ : Eq.{u_2 + 1} (α := Set E) (ball 0 (‖c‖ * 1)) (ball 0 ‖c‖)
⊢ HSMul.hSMul (β := Set E) c (ball 0 1) = ball 0 ‖c‖
have rw₂ : Eq.{u_2 + 1} (α := Set E) (ball 0 ‖c‖) (ball 0 ‖c‖)
Tactic: rw [_root_.smul_ball hc, smul_zero, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)
have h : ∀ (y : E), y ∈ c • sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ y ∈ c • sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)
have h : c⁻¹ • y ∈ sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)
Tactic: rw [mem_smul_set_iff_inv_smul_mem₀ hc]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
| c⁻¹ • y ∈ sphere x r
have rw : c⁻¹ • y ∈ sphere (c⁻¹ • c • x) r
Tactic: rw [← inv_smul_smul₀ hc x]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)
have h : c⁻¹ • y ∈ sphere (c⁻¹ • c • x) r ↔ y ∈ sphere (c • x) (‖c‖ * r)
Tactic: conv_lhs => rw [← inv_smul_smul₀ hc x]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
c : 𝕜
hc : c ∈ s
⊢ HSMul.hSMul (β := Set E) c (sphere 0 r) = sphere 0 (‖c‖ * r)
have rw : sphere (HSMul.hSMul (β := E) c 0) (‖c‖ * r) = sphere 0 (‖c‖ * r)
Tactic: rw [smul_sphere' (ne_of_mem_of_not_mem hc hs), smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
c : 𝕜
hc : c ∈ s
rw : sphere (HSMul.hSMul (β := E) c 0) (‖c‖ * r) = sphere 0 (‖c‖ * r)
⊢ HSMul.hSMul (β := Set E) c (sphere 0 r) = sphere 0 (‖c‖ * r)
have rw₁ : Eq.{u_2 + 1} (α := Set E) (sphere 0 (‖c‖ * r)) (sphere 0 (‖c‖ * r))
Tactic: rw [smul_sphere' (ne_of_mem_of_not_mem hc hs), smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
⊢ Eq.{u_2 + 1} (α := Set E) (⋃ c ∈ s, sphere 0 (‖c‖ * r))
    (preimage (β := ℝ) (fun (x : E) ↦ ‖x‖) ((fun (x : 𝕜) ↦ ‖x‖ * r) '' s))
have h : ∀ (x : E),
  Membership.mem (γ := Set E) (⋃ c ∈ s, sphere 0 (‖c‖ * r)) x ↔
    Membership.mem (γ := Set E) (preimage (β := ℝ) (fun (x : E) ↦ ‖x‖) ((fun (x : 𝕜) ↦ ‖x‖ * r) '' s)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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
⊢ ∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u
have obtain : ∀ (ε : ℝ) (εpos : 0 < ε) (hε : closedBall x ε ⊆ u), ∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u
Tactic: obtain ⟨ε, εpos, hε⟩ : ∃ ε : ℝ, 0 < ε ∧ closedBall x ε ⊆ u := nhds_basis_closedBall.mem_iff.1 hu
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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 : 𝕜) in 𝓝 0, {x} + r • s ⊆ u
have obtain : ∀ (R : ℝ) (Rpos : 0 < R) (hR : s ⊆ closedBall 0 R), ∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u
Tactic: obtain ⟨R, Rpos, hR⟩ : ∃ R : ℝ, 0 < R ∧ s ⊆ closedBall 0 R := hs.subset_closedBall_lt 0 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (hypothesis)
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
⊢ ∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u
have this : Membership.mem (γ := Filter 𝕜) (𝓝 0) (closedBall 0 (ε / R))
Tactic: have : Metric.closedBall (0 : 𝕜) (ε / R) ∈ 𝓝 (0 : 𝕜) := closedBall_mem_nhds _ (div_pos εpos Rpos)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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 : 𝕜) in 𝓝 0, {x} + r • s ⊆ u
have h : ∀ (r : 𝕜) (hr : Membership.mem (γ := Set 𝕜) (closedBall 0 (ε / R)) r), {x} + r • s ⊆ u
Tactic: filter_upwards [this] with r hr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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
⊢ {x} + r • s ⊆ u
have h : (fun (x_1 : E) ↦ -x + x_1) ⁻¹' (r • s) ⊆ u
Tactic: simp only [image_add_left, singleton_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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
⊢ y ∈ u
have h : ∀ (z : E) (zs : z ∈ s) (hz : r • z = -x + y), y ∈ u
Tactic: obtain ⟨z, zs, hz⟩ : ∃ z : E, z ∈ s ∧ r • z = -x + y := by simpa [mem_smul_set] using hy
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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‖ ≤ ε / R * R
have h₁ : ‖r‖ ≤ ε / R
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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
⊢ ‖r‖ * ‖z‖ ≤ ε / R * R
have h₂ : ‖z‖ ≤ R
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (hypothesis)
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
⊢ y ∈ u
have I : ‖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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (hypothesis)
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 ∈ u
have this₁ : y = x + r • z
Tactic: have : y = x + r • z := by simp only [hz, add_neg_cancel_left]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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 ∈ u
have h : y ∈ closedBall x ε
Tactic: apply 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
r : ℝ
hr : 0 < r
⊢ HSMul.hSMul (β := Set E) r (ball 0 1) = ball 0 r
have rw : Eq.{u_2 + 1} (α := Set E) (ball 0 ‖r‖) (ball 0 r)
Tactic: rw [smul_unitBall hr.ne', Real.norm_of_nonneg hr.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
r : ℝ
hr : 0 < r
rw : Eq.{u_2 + 1} (α := Set E) (ball 0 ‖r‖) (ball 0 r)
⊢ HSMul.hSMul (β := Set E) r (ball 0 1) = ball 0 r
have rw₁ : Eq.{u_2 + 1} (α := Set E) (ball 0 r) (ball 0 r)
Tactic: rw [smul_unitBall hr.ne', Real.norm_of_nonneg hr.le]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (hypothesis)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b r : ℝ
ha : 0 ≤ a
hr : 0 < r
⊢ HSMul.hSMul (β := Set E) (Ioo a b) (sphere 0 r) = ball 0 (b * r) \ closedBall 0 (a * r)
have this : 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)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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)
⊢ HSMul.hSMul (β := Set E) (Ioo a b) (sphere 0 r) = ball 0 (b * r) \ closedBall 0 (a * r)
have rw : Eq.{u_2 + 1} (α := Set E) ((fun (x : E) ↦ ‖x‖) ⁻¹' Ioo (a * r) (b * 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
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)
⊢ Eq.{u_2 + 1} (α := Set E) ((fun (x : E) ↦ ‖x‖) ⁻¹' Ioo (a * r) (b * r)) (ball 0 (b * r) \ closedBall 0 (a * r))
have 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
Tactic: ext x
-- 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
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ (y : E), dist x y = b * dist x z ∧ dist y z = a * dist x z
have h : dist x (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) z = a * dist x z
Tactic: use a • x + b • z
-- 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
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ dist x (a • x + b • z) = b * dist x z ∧ dist (a • x + b • z) z = a * dist x z
have h : 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 1 [← one_smul ℝ x]
-- 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
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) z = a * dist x z
have 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
Tactic: nth_rw 4 [← one_smul ℝ z]
-- 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 inl : ∀ (hε : LE.le (α := ℝ) 0 0) (h : dist x z ≤ 0 + δ), ∃ (y : E), dist x y ≤ δ ∧ dist y z ≤ 0
Tactic: obtain rfl | hε' := hε.eq_or_lt
Cleared hypotheses: ε, 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
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
⊢ ∃ (y : E), dist x y ≤ δ ∧ dist y z ≤ ε
have inr : ∀ (hε' : 0 < ε), ∃ (y : E), dist x y ≤ δ ∧ dist y z ≤ ε
Tactic: obtain rfl | hε' := hε.eq_or_lt
-- 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ε : LE.le (α := ℝ) 0 0
h : dist x z ≤ 0 + δ
⊢ dist x z ≤ δ
have rwa : ∀ (h : dist x z ≤ δ), dist x z ≤ δ
Tactic: rwa [zero_add] at h
Cleared hypotheses: 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
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
⊢ ∃ (y : E), dist x y ≤ δ ∧ dist y z ≤ ε
have hεδ : 0 < ε + δ
Tactic: have hεδ := add_pos_of_pos_of_nonneg 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
x z : E
δ ε : ℝ
hδ : 0 ≤ δ
hε : 0 ≤ ε
h : dist x z ≤ ε + δ
hε' : 0 < ε
hεδ : 0 < ε + δ
⊢ ε / (ε + δ) + δ / (ε + δ) = 1
have rw : (ε + δ) / (ε + δ) = 1
Tactic: rw [← add_div, div_self 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 ≤ ε + δ
hε' : 0 < ε
hεδ : 0 < ε + δ
rw : (ε + δ) / (ε + δ) = 1
⊢ ε / (ε + δ) + δ / (ε + δ) = 1
have rw₁ : Eq (α := ℝ) 1 1
Tactic: rw [← add_div, div_self 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 ≤ ε + δ
hε' : 0 < ε
hεδ : 0 < ε + δ
⊢ ∃ (y : E), dist x y ≤ δ ∧ dist y z ≤ ε
have inr : ∀ (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ε <| add_nonneg hε hδ)
    (div_nonneg hδ <| add_nonneg hε hδ) <| by
      rw [← add_div, div_self 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 ≤ ε + δ
hε' : 0 < ε
hεδ : 0 < ε + δ
y : E
hy : dist x y = δ / (ε + δ) * dist x z ∧ dist y z = ε / (ε + δ) * dist x z
⊢ dist x y ≤ δ ∧ dist y z ≤ ε
have inr : 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 ≤ ε + δ
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 / (ε + δ) * ε ≤ ε
have 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 / (ε + δ) * ε ≤ ε
Tactic: rw [← div_le_one hεδ] at h
Cleared hypotheses: h, hε', 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 < ε + δ
⊢ ε / (ε + δ) + δ / (ε + δ) = 1
have rw : (ε + δ) / (ε + δ) = 1
Tactic: rw [← add_div, div_self (add_pos_of_pos_of_nonneg 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_of_pos_of_nonneg hε hδ).ne']