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
δ : ℝ
hδ : 0 < δ
s : Set E
rw : cthickening 0 (thickening δ s) = cthickening δ s
rw₁ : cthickening (0 + δ) s = cthickening δ s
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening δ s) = cthickening δ s
have rw₂ : cthickening δ 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
δ : ℝ
s : Set E
x : E
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ
have inl : ∀ (hδ : δ ≤ 0), infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ
Tactic: obtain hδ | hδ := le_or_gt δ 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
inl : ∀ (hδ : δ ≤ 0), infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ
have inr : ∀ (hδ : 0 < δ), infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ
Tactic: obtain hδ | hδ := le_or_gt δ 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : δ ≤ 0
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ
have inl : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = infEDist x s - ENNReal.ofReal δ
Tactic: rw [cthickening_of_nonpos hδ, infEDist_closure, ofReal_of_nonpos hδ, tsub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : δ ≤ 0
inl : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = infEDist x s - ENNReal.ofReal δ
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ
have inl₁ : infEDist x s = infEDist x s - ENNReal.ofReal δ
Tactic: rw [cthickening_of_nonpos hδ, infEDist_closure, ofReal_of_nonpos hδ, tsub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : δ ≤ 0
inl : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = infEDist x s - ENNReal.ofReal δ
inl₁ : infEDist x s = infEDist x s - ENNReal.ofReal δ
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ
have inl₂ : infEDist x s = infEDist x s - 0
Tactic: rw [cthickening_of_nonpos hδ, infEDist_closure, ofReal_of_nonpos hδ, tsub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : δ ≤ 0
inl : infEDist x (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = infEDist x s - ENNReal.ofReal δ
inl₁ : infEDist x s = infEDist x s - ENNReal.ofReal δ
inl₂ : infEDist x s = infEDist x s - 0
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ
have inl₃ : infEDist x s = infEDist x s
Tactic: rw [cthickening_of_nonpos hδ, infEDist_closure, ofReal_of_nonpos hδ, tsub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Ball.Pointwise (goal)
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
s : Set E
x : E
hδ : 0 < δ
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ
have inr : infEDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening δ s)) =
  infEDist x s - ENNReal.ofReal δ
Tactic: rw [← closure_thickening hδ, infEDist_closure, 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
δ : ℝ
s : Set E
x : E
hδ : 0 < δ
inr :
  infEDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening δ s)) =
    infEDist x s - ENNReal.ofReal δ
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ
have inr₁ : infEDist x (thickening δ s) = infEDist x s - ENNReal.ofReal δ
Tactic: rw [← closure_thickening hδ, infEDist_closure, 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
δ : ℝ
s : Set E
x : E
hδ : 0 < δ
inr :
  infEDist x (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening δ s)) =
    infEDist x s - ENNReal.ofReal δ
inr₁ : infEDist x (thickening δ s) = infEDist x s - ENNReal.ofReal δ
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ
have inr₂ : infEDist x s - ENNReal.ofReal δ = infEDist x s - ENNReal.ofReal δ
Tactic: rw [← closure_thickening hδ, infEDist_closure, 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 < ε
hδ : 0 ≤ δ
s : Set E
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s
have inl : ∀ (hδ : LE.le (α := ℝ) 0 0), thickening ε (cthickening 0 s) = thickening (ε + 0) s
Tactic: obtain rfl | hδ := hδ.eq_or_lt
Cleared hypotheses: δ, 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
inl : ∀ (hδ : LE.le (α := ℝ) 0 0), thickening ε (cthickening 0 s) = thickening (ε + 0) s
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s
have inr : ∀ (hδ : 0 < δ), thickening ε (cthickening δ s) = thickening (ε + δ) s
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
ε : ℝ
hε : 0 < ε
s : Set E
hδ : LE.le (α := ℝ) 0 0
⊢ thickening ε (cthickening 0 s) = thickening (ε + 0) s
have inl : thickening ε (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = thickening (ε + 0) s
Tactic: rw [cthickening_zero, thickening_closure, add_zero]
-- 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
hδ : LE.le (α := ℝ) 0 0
inl : thickening ε (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = thickening (ε + 0) s
⊢ thickening ε (cthickening 0 s) = thickening (ε + 0) s
have inl₁ : thickening ε s = thickening (ε + 0) s
Tactic: rw [cthickening_zero, thickening_closure, add_zero]
-- 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
hδ : LE.le (α := ℝ) 0 0
inl : thickening ε (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s) = thickening (ε + 0) s
inl₁ : thickening ε s = thickening (ε + 0) s
⊢ thickening ε (cthickening 0 s) = thickening (ε + 0) s
have inl₂ : thickening ε s = thickening ε s
Tactic: rw [cthickening_zero, thickening_closure, add_zero]
-- 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δ_1 : 0 ≤ δ
s : Set E
hδ : 0 < δ
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s
have inr : thickening ε (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening δ s)) = thickening (ε + δ) s
Tactic: rw [← closure_thickening hδ, thickening_closure, thickening_thickening 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 < ε
hδ_1 : 0 ≤ δ
s : Set E
hδ : 0 < δ
inr :
  thickening ε (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening δ s)) = thickening (ε + δ) s
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s
have inr₁ : thickening ε (thickening δ s) = thickening (ε + δ) s
Tactic: rw [← closure_thickening hδ, thickening_closure, thickening_thickening 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 < ε
hδ_1 : 0 ≤ δ
s : Set E
hδ : 0 < δ
inr :
  thickening ε (closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening δ s)) = thickening (ε + δ) s
inr₁ : thickening ε (thickening δ s) = thickening (ε + δ) s
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s
have inr₂ : thickening (ε + δ) s = thickening (ε + δ) s
Tactic: rw [← closure_thickening hδ, thickening_closure, thickening_thickening 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 ≤ ε
hδ : 0 ≤ δ
s : Set E
x : E
⊢ x ∈ cthickening (ε + δ) s → x ∈ cthickening ε (cthickening δ 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δ, infEDist_cthickening]
-- 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 < δ
x : E
⊢ thickening ε (Metric.ball x δ) = Metric.ball x (ε + δ)
have rw : thickening ε (thickening δ {x}) = Metric.ball x (ε + δ)
Tactic: rw [← thickening_singleton, thickening_thickening hε hδ, thickening_singleton]
-- 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 < δ
x : E
rw : thickening ε (thickening δ {x}) = Metric.ball x (ε + δ)
⊢ thickening ε (Metric.ball x δ) = Metric.ball x (ε + δ)
have rw₁ : thickening (ε + δ) {x} = Metric.ball x (ε + δ)
Tactic: rw [← thickening_singleton, thickening_thickening hε hδ, thickening_singleton]
-- 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 < δ
x : E
rw : thickening ε (thickening δ {x}) = Metric.ball x (ε + δ)
rw₁ : thickening (ε + δ) {x} = Metric.ball x (ε + δ)
⊢ thickening ε (Metric.ball x δ) = Metric.ball x (ε + δ)
have rw₂ : Metric.ball x (ε + δ) = Metric.ball x (ε + δ)
Tactic: rw [← thickening_singleton, thickening_thickening hε hδ, thickening_singleton]
-- 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 ≤ δ
x : E
⊢ thickening ε (Metric.closedBall x δ) = Metric.ball x (ε + δ)
have rw : thickening ε (cthickening δ {x}) = Metric.ball x (ε + δ)
Tactic: rw [← cthickening_singleton _ hδ, thickening_cthickening hε hδ, thickening_singleton]
-- 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 ≤ δ
x : E
rw : thickening ε (cthickening δ {x}) = Metric.ball x (ε + δ)
⊢ thickening ε (Metric.closedBall x δ) = Metric.ball x (ε + δ)
have rw₁ : thickening (ε + δ) {x} = Metric.ball x (ε + δ)
Tactic: rw [← cthickening_singleton _ hδ, thickening_cthickening hε hδ, thickening_singleton]
-- 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 ≤ δ
x : E
rw : thickening ε (cthickening δ {x}) = Metric.ball x (ε + δ)
rw₁ : thickening (ε + δ) {x} = Metric.ball x (ε + δ)
⊢ thickening ε (Metric.closedBall x δ) = Metric.ball x (ε + δ)
have rw₂ : Metric.ball x (ε + δ) = Metric.ball x (ε + δ)
Tactic: rw [← cthickening_singleton _ hδ, thickening_cthickening hε hδ, thickening_singleton]
-- 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 < δ
x : E
⊢ cthickening ε (Metric.ball x δ) = Metric.closedBall x (ε + δ)
have rw : cthickening ε (thickening δ {x}) = Metric.closedBall x (ε + δ)
Tactic: rw [← thickening_singleton, cthickening_thickening hε hδ,
      cthickening_singleton _ (add_nonneg hε hδ.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 ≤ ε
hδ : 0 < δ
x : E
rw : cthickening ε (thickening δ {x}) = Metric.closedBall x (ε + δ)
⊢ cthickening ε (Metric.ball x δ) = Metric.closedBall x (ε + δ)
have rw₁ : cthickening (ε + δ) {x} = Metric.closedBall x (ε + δ)
Tactic: rw [← thickening_singleton, cthickening_thickening hε hδ,
      cthickening_singleton _ (add_nonneg hε hδ.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 ≤ ε
hδ : 0 < δ
x : E
rw : cthickening ε (thickening δ {x}) = Metric.closedBall x (ε + δ)
rw₁ : cthickening (ε + δ) {x} = Metric.closedBall x (ε + δ)
⊢ cthickening ε (Metric.ball x δ) = Metric.closedBall x (ε + δ)
have rw₂ : Metric.closedBall x (ε + δ) = Metric.closedBall x (ε + δ)
Tactic: rw [← thickening_singleton, cthickening_thickening hε hδ,
      cthickening_singleton _ (add_nonneg hε hδ.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 ≤ ε
hδ : 0 ≤ δ
x : E
⊢ cthickening ε (Metric.closedBall x δ) = Metric.closedBall x (ε + δ)
have rw : cthickening ε (cthickening δ {x}) = Metric.closedBall x (ε + δ)
Tactic: rw [← cthickening_singleton _ hδ, cthickening_cthickening hε hδ,
      cthickening_singleton _ (add_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
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
x : E
rw : cthickening ε (cthickening δ {x}) = Metric.closedBall x (ε + δ)
⊢ cthickening ε (Metric.closedBall x δ) = Metric.closedBall x (ε + δ)
have rw₁ : cthickening (ε + δ) {x} = Metric.closedBall x (ε + δ)
Tactic: rw [← cthickening_singleton _ hδ, cthickening_cthickening hε hδ,
      cthickening_singleton _ (add_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
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
x : E
rw : cthickening ε (cthickening δ {x}) = Metric.closedBall x (ε + δ)
rw₁ : cthickening (ε + δ) {x} = Metric.closedBall x (ε + δ)
⊢ cthickening ε (Metric.closedBall x δ) = Metric.closedBall x (ε + δ)
have rw₂ : Metric.closedBall x (ε + δ) = Metric.closedBall x (ε + δ)
Tactic: rw [← cthickening_singleton _ hδ, cthickening_cthickening hε hδ,
      cthickening_singleton _ (add_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
δ ε : ℝ
hε : 0 < ε
hδ : 0 < δ
a b : E
⊢ Metric.ball a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)
have rw : a +ᵥ thickening ε (Metric.ball b δ) = Metric.ball (a + b) (ε + δ)
Tactic: rw [ball_add, thickening_ball hε hδ b, Metric.vadd_ball, vadd_eq_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 < ε
hδ : 0 < δ
a b : E
rw : a +ᵥ thickening ε (Metric.ball b δ) = Metric.ball (a + b) (ε + δ)
⊢ Metric.ball a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)
have rw₁ : a +ᵥ Metric.ball b (ε + δ) = Metric.ball (a + b) (ε + δ)
Tactic: rw [ball_add, thickening_ball hε hδ b, Metric.vadd_ball, vadd_eq_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 < ε
hδ : 0 < δ
a b : E
rw : a +ᵥ thickening ε (Metric.ball b δ) = Metric.ball (a + b) (ε + δ)
rw₁ : a +ᵥ Metric.ball b (ε + δ) = Metric.ball (a + b) (ε + δ)
⊢ Metric.ball a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)
have rw₂ : Metric.ball (a +ᵥ b) (ε + δ) = Metric.ball (a + b) (ε + δ)
Tactic: rw [ball_add, thickening_ball hε hδ b, Metric.vadd_ball, vadd_eq_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 < ε
hδ : 0 < δ
a b : E
rw : a +ᵥ thickening ε (Metric.ball b δ) = Metric.ball (a + b) (ε + δ)
rw₁ : a +ᵥ Metric.ball b (ε + δ) = Metric.ball (a + b) (ε + δ)
rw₂ : Metric.ball (a +ᵥ b) (ε + δ) = Metric.ball (a + b) (ε + δ)
⊢ Metric.ball a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)
have rw₃ : Metric.ball (a + b) (ε + δ) = Metric.ball (a + b) (ε + δ)
Tactic: rw [ball_add, thickening_ball hε hδ b, Metric.vadd_ball, vadd_eq_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 < ε
hδ : 0 < δ
a b : E
⊢ Metric.ball a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)
have simp_rw : Metric.ball a ε + -Metric.ball b δ = Metric.ball (a + -b) (ε + δ)
Tactic: simp_rw [sub_eq_add_neg, neg_ball, ball_add_ball 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 < ε
hδ : 0 < δ
a b : E
simp_rw : Metric.ball a ε + -Metric.ball b δ = Metric.ball (a + -b) (ε + δ)
⊢ Metric.ball a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)
have simp_rw₁ : Metric.ball a ε + Metric.ball (-b) δ = Metric.ball (a + -b) (ε + δ)
Tactic: simp_rw [sub_eq_add_neg, neg_ball, ball_add_ball 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 < ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.ball a ε + Metric.closedBall b δ = Metric.ball (a + b) (ε + δ)
have rw : a +ᵥ thickening ε (Metric.closedBall b δ) = Metric.ball (a + b) (ε + δ)
Tactic: rw [ball_add, thickening_closedBall hε hδ b, Metric.vadd_ball, vadd_eq_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 < ε
hδ : 0 ≤ δ
a b : E
rw : a +ᵥ thickening ε (Metric.closedBall b δ) = Metric.ball (a + b) (ε + δ)
⊢ Metric.ball a ε + Metric.closedBall b δ = Metric.ball (a + b) (ε + δ)
have rw₁ : a +ᵥ Metric.ball b (ε + δ) = Metric.ball (a + b) (ε + δ)
Tactic: rw [ball_add, thickening_closedBall hε hδ b, Metric.vadd_ball, vadd_eq_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 < ε
hδ : 0 ≤ δ
a b : E
rw : a +ᵥ thickening ε (Metric.closedBall b δ) = Metric.ball (a + b) (ε + δ)
rw₁ : a +ᵥ Metric.ball b (ε + δ) = Metric.ball (a + b) (ε + δ)
⊢ Metric.ball a ε + Metric.closedBall b δ = Metric.ball (a + b) (ε + δ)
have rw₂ : Metric.ball (a +ᵥ b) (ε + δ) = Metric.ball (a + b) (ε + δ)
Tactic: rw [ball_add, thickening_closedBall hε hδ b, Metric.vadd_ball, vadd_eq_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 < ε
hδ : 0 ≤ δ
a b : E
rw : a +ᵥ thickening ε (Metric.closedBall b δ) = Metric.ball (a + b) (ε + δ)
rw₁ : a +ᵥ Metric.ball b (ε + δ) = Metric.ball (a + b) (ε + δ)
rw₂ : Metric.ball (a +ᵥ b) (ε + δ) = Metric.ball (a + b) (ε + δ)
⊢ Metric.ball a ε + Metric.closedBall b δ = Metric.ball (a + b) (ε + δ)
have rw₃ : Metric.ball (a + b) (ε + δ) = Metric.ball (a + b) (ε + δ)
Tactic: rw [ball_add, thickening_closedBall hε hδ b, Metric.vadd_ball, vadd_eq_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 < ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.ball a ε - Metric.closedBall b δ = Metric.ball (a - b) (ε + δ)
have simp_rw : Metric.ball a ε + -Metric.closedBall b δ = Metric.ball (a + -b) (ε + δ)
Tactic: simp_rw [sub_eq_add_neg, neg_closedBall, ball_add_closedBall 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 < ε
hδ : 0 ≤ δ
a b : E
simp_rw : Metric.ball a ε + -Metric.closedBall b δ = Metric.ball (a + -b) (ε + δ)
⊢ Metric.ball a ε - Metric.closedBall b δ = Metric.ball (a - b) (ε + δ)
have simp_rw₁ : Metric.ball a ε + Metric.closedBall (-b) δ = Metric.ball (a + -b) (ε + δ)
Tactic: simp_rw [sub_eq_add_neg, neg_closedBall, ball_add_closedBall 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 ≤ ε
hδ : 0 < δ
a b : E
⊢ Metric.closedBall a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)
have rw : Metric.ball b δ + Metric.closedBall a ε = Metric.ball (a + b) (ε + δ)
Tactic: rw [add_comm, ball_add_closedBall hδ hε b, add_comm, add_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
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
a b : E
rw : Metric.ball b δ + Metric.closedBall a ε = Metric.ball (a + b) (ε + δ)
⊢ Metric.closedBall a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)
have rw₁ : Metric.ball (b + a) (δ + ε) = Metric.ball (a + b) (ε + δ)
Tactic: rw [add_comm, ball_add_closedBall hδ hε b, add_comm, add_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
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
a b : E
rw : Metric.ball b δ + Metric.closedBall a ε = Metric.ball (a + b) (ε + δ)
rw₁ : Metric.ball (b + a) (δ + ε) = Metric.ball (a + b) (ε + δ)
⊢ Metric.closedBall a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)
have rw₂ : Metric.ball (a + b) (δ + ε) = Metric.ball (a + b) (ε + δ)
Tactic: rw [add_comm, ball_add_closedBall hδ hε b, add_comm, add_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
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
a b : E
rw : Metric.ball b δ + Metric.closedBall a ε = Metric.ball (a + b) (ε + δ)
rw₁ : Metric.ball (b + a) (δ + ε) = Metric.ball (a + b) (ε + δ)
rw₂ : Metric.ball (a + b) (δ + ε) = Metric.ball (a + b) (ε + δ)
⊢ Metric.closedBall a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)
have rw₃ : Metric.ball (a + b) (ε + δ) = Metric.ball (a + b) (ε + δ)
Tactic: rw [add_comm, ball_add_closedBall hδ hε b, add_comm, add_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
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
a b : E
⊢ Metric.closedBall a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)
have simp_rw : Metric.closedBall a ε + -Metric.ball b δ = Metric.ball (a + -b) (ε + δ)
Tactic: simp_rw [sub_eq_add_neg, neg_ball, closedBall_add_ball 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 ≤ ε
hδ : 0 < δ
a b : E
simp_rw : Metric.closedBall a ε + -Metric.ball b δ = Metric.ball (a + -b) (ε + δ)
⊢ Metric.closedBall a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)
have simp_rw₁ : Metric.closedBall a ε + Metric.ball (-b) δ = Metric.ball (a + -b) (ε + δ)
Tactic: simp_rw [sub_eq_add_neg, neg_ball, closedBall_add_ball hε hδ]