awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
s : Set E
x : E
simp_rw : infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEDist x s - ENNReal.ofReal δ ≤ ENNReal.ofReal ε
⊢ x ∈ cthickening (ε + δ) s → x ∈ cthickening ε (thickening δ s)

Tactic:
simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ.le, infEDist_thickening hδ]

Premises used: Metric.mem_cthickening_iff, LT.lt.le, infEDist_thickening, ENNReal.ofReal_add
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
s : Set E
x : E
⊢ infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEDist x s - ENNReal.ofReal δ ≤ ENNReal.ofReal ε

Tactic:
tsub_le_iff_right.2

Premises used: Iff.mpr, tsub_le_iff_right
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
s : Set E
x : E
⊢ infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEDist x s - ENNReal.ofReal δ ≤ ENNReal.ofReal ε

Tactic:
exact tsub_le_iff_right.2

Premises used: Iff.mpr, tsub_le_iff_right
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ : ℝ
hδ : 0 < δ
s : Set E
rw : cthickening 0 (thickening δ s) = cthickening δ s
rw₁ : cthickening (0 + δ) s = cthickening δ s
rw₂ rw₃ : cthickening δ s = cthickening δ s
⊢ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening δ s) = cthickening δ s

Tactic:
rw [← cthickening_zero, cthickening_thickening le_rfl hδ, zero_add]

Premises used: le_rfl, cthickening_thickening, Metric.cthickening_zero, zero_add
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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 δ
inr : ∀ (hδ : 0 < δ), infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ

Tactic:
obtain hδ | hδ := le_or_gt δ 0

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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
inl₃ inl₄ : infEDist x s = infEDist x s
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ

Tactic:
rw [cthickening_of_nonpos hδ, infEDist_closure, ofReal_of_nonpos hδ, tsub_zero]

Premises used: tsub_zero, ENNReal.ofReal_of_nonpos, Metric.infEDist_closure, Metric.cthickening_of_nonpos
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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 δ
inr₂ inr₃ : infEDist x s - ENNReal.ofReal δ = infEDist x s - ENNReal.ofReal δ
⊢ infEDist x (cthickening δ s) = infEDist x s - ENNReal.ofReal δ

Tactic:
rw [← closure_thickening hδ, infEDist_closure, infEDist_thickening hδ]

Premises used: closure_thickening, infEDist_thickening, Metric.infEDist_closure
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 ≤ δ
s : Set E
inl : ∀ (hδ : LE.le (α := ℝ) 0 0), thickening ε (cthickening 0 s) = thickening (ε + 0) s
inr : ∀ (hδ : 0 < δ), thickening ε (cthickening δ s) = thickening (ε + δ) s
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s

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
ε : ℝ
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
inl₂ inl₃ : thickening ε s = thickening ε s
⊢ thickening ε (cthickening 0 s) = thickening (ε + 0) s

Tactic:
rw [cthickening_zero, thickening_closure, add_zero]

Premises used: Metric.cthickening_zero, add_zero, Metric.thickening_closure
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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
inr₂ inr₃ : thickening (ε + δ) s = thickening (ε + δ) s
⊢ thickening ε (cthickening δ s) = thickening (ε + δ) s

Tactic:
rw [← closure_thickening hδ, thickening_closure, thickening_thickening hε hδ]

Premises used: closure_thickening, thickening_thickening, Metric.thickening_closure
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set E
x : E
simp_rw : infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEDist x s - ENNReal.ofReal δ ≤ ENNReal.ofReal ε
⊢ x ∈ cthickening (ε + δ) s → x ∈ cthickening ε (cthickening δ s)

Tactic:
simp_rw [mem_cthickening_iff, ENNReal.ofReal_add hε hδ, infEDist_cthickening]

Premises used: Metric.mem_cthickening_iff, infEDist_cthickening, ENNReal.ofReal_add
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set E
x : E
⊢ infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEDist x s - ENNReal.ofReal δ ≤ ENNReal.ofReal ε

Tactic:
tsub_le_iff_right.2

Premises used: Iff.mpr, tsub_le_iff_right
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 ≤ δ
s : Set E
x : E
⊢ infEDist x s ≤ ENNReal.ofReal ε + ENNReal.ofReal δ → infEDist x s - ENNReal.ofReal δ ≤ ENNReal.ofReal ε

Tactic:
exact tsub_le_iff_right.2

Premises used: Iff.mpr, tsub_le_iff_right
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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 (ε + δ)
rw₂ rw₃ : Metric.ball x (ε + δ) = Metric.ball x (ε + δ)
⊢ thickening ε (Metric.ball x δ) = Metric.ball x (ε + δ)

Tactic:
rw [← thickening_singleton, thickening_thickening hε hδ, thickening_singleton]

Premises used: Metric.thickening_singleton, thickening_thickening
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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 (ε + δ)
rw₂ rw₃ : Metric.ball x (ε + δ) = Metric.ball x (ε + δ)
⊢ thickening ε (Metric.closedBall x δ) = Metric.ball x (ε + δ)

Tactic:
rw [← cthickening_singleton _ hδ, thickening_cthickening hε hδ, thickening_singleton]

Premises used: Metric.cthickening_singleton, Metric.thickening_singleton, thickening_cthickening
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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 (ε + δ)
rw₂ rw₃ : Metric.closedBall x (ε + δ) = Metric.closedBall x (ε + δ)
⊢ cthickening ε (Metric.ball x δ) = Metric.closedBall x (ε + δ)

Tactic:
rw [← thickening_singleton, cthickening_thickening hε hδ,
      cthickening_singleton _ (add_nonneg hε hδ.le)]

Premises used: cthickening_thickening, LT.lt.le, add_nonneg, Metric.cthickening_singleton, Metric.thickening_singleton
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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 (ε + δ)
rw₂ rw₃ : Metric.closedBall x (ε + δ) = Metric.closedBall x (ε + δ)
⊢ cthickening ε (Metric.closedBall x δ) = Metric.closedBall x (ε + δ)

Tactic:
rw [← cthickening_singleton _ hδ, cthickening_cthickening hε hδ,
      cthickening_singleton _ (add_nonneg hε hδ)]

Premises used: add_nonneg, Metric.cthickening_singleton, cthickening_cthickening
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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) (ε + δ)
rw₃ rw₄ : Metric.ball (a + b) (ε + δ) = Metric.ball (a + b) (ε + δ)
⊢ Metric.ball a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)

Tactic:
rw [ball_add, thickening_ball hε hδ b, Metric.vadd_ball, vadd_eq_add]

Premises used: Metric.vadd_ball, ball_add, vadd_eq_add, thickening_ball
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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) (ε + δ)
simp_rw₁ : Metric.ball a ε + Metric.ball (-b) δ = Metric.ball (a + -b) (ε + δ)
⊢ Metric.ball a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)

Tactic:
simp_rw [sub_eq_add_neg, neg_ball, ball_add_ball hε hδ]

Premises used: neg_ball, sub_eq_add_neg, ball_add_ball
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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) (ε + δ)
rw₃ rw₄ : Metric.ball (a + b) (ε + δ) = Metric.ball (a + b) (ε + δ)
⊢ Metric.ball a ε + Metric.closedBall b δ = Metric.ball (a + b) (ε + δ)

Tactic:
rw [ball_add, thickening_closedBall hε hδ b, Metric.vadd_ball, vadd_eq_add]

Premises used: Metric.vadd_ball, thickening_closedBall, ball_add, vadd_eq_add
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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) (ε + δ)
simp_rw₁ : Metric.ball a ε + Metric.closedBall (-b) δ = Metric.ball (a + -b) (ε + δ)
⊢ Metric.ball a ε - Metric.closedBall b δ = Metric.ball (a - b) (ε + δ)

Tactic:
simp_rw [sub_eq_add_neg, neg_closedBall, ball_add_closedBall hε hδ]

Premises used: sub_eq_add_neg, ball_add_closedBall, neg_closedBall
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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) (ε + δ)
rw₃ rw₄ : Metric.ball (a + b) (ε + δ) = Metric.ball (a + b) (ε + δ)
⊢ Metric.closedBall a ε + Metric.ball b δ = Metric.ball (a + b) (ε + δ)

Tactic:
rw [add_comm, ball_add_closedBall hδ hε b, add_comm, add_comm δ]

Premises used: ball_add_closedBall, add_comm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
a b : E
simp_rw : Metric.closedBall a ε + -Metric.ball b δ = Metric.ball (a + -b) (ε + δ)
simp_rw₁ : Metric.closedBall a ε + Metric.ball (-b) δ = Metric.ball (a + -b) (ε + δ)
⊢ Metric.closedBall a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)

Tactic:
simp_rw [sub_eq_add_neg, neg_ball, closedBall_add_ball hε hδ]

Premises used: neg_ball, sub_eq_add_neg, closedBall_add_ball
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
inst_2 : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
rw : b +ᵥ cthickening δ (Metric.closedBall a ε) = Metric.closedBall (a + b) (ε + δ)
rw₁ : b +ᵥ Metric.closedBall a (δ + ε) = Metric.closedBall (a + b) (ε + δ)
rw₂ : Metric.closedBall (b +ᵥ a) (δ + ε) = Metric.closedBall (a + b) (ε + δ)
rw₃ : Metric.closedBall (b + a) (δ + ε) = Metric.closedBall (a + b) (ε + δ)
rw₄ : Metric.closedBall (a + b) (δ + ε) = Metric.closedBall (a + b) (ε + δ)
rw₅ rw₆ : Metric.closedBall (a + b) (ε + δ) = Metric.closedBall (a + b) (ε + δ)
⊢ Metric.closedBall a ε + Metric.closedBall b δ = Metric.closedBall (a + b) (ε + δ)

Tactic:
rw [(isCompact_closedBall _ _).add_closedBall hδ b, cthickening_closedBall hδ hε a,
    Metric.vadd_closedBall, vadd_eq_add, add_comm, add_comm δ]

Premises used: Metric.vadd_closedBall, add_comm, cthickening_closedBall, vadd_eq_add, ProperSpace.isCompact_closedBall, IsCompact.add_closedBall
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
δ ε : ℝ
inst_2 : ProperSpace E
hε : 0 ≤ ε
hδ : 0 ≤ δ
a b : E
rw : Metric.closedBall a ε + -Metric.closedBall b δ = Metric.closedBall (a - b) (ε + δ)
rw₁ : Metric.closedBall a ε + Metric.closedBall (-b) δ = Metric.closedBall (a - b) (ε + δ)
rw₂ : Metric.closedBall (a + -b) (ε + δ) = Metric.closedBall (a - b) (ε + δ)
rw₃ rw₄ : Metric.closedBall (a + -b) (ε + δ) = Metric.closedBall (a + -b) (ε + δ)
⊢ Metric.closedBall a ε - Metric.closedBall b δ = Metric.closedBall (a - b) (ε + δ)

Tactic:
rw [sub_eq_add_neg, neg_closedBall, closedBall_add_closedBall hε hδ, sub_eq_add_neg]

Premises used: closedBall_add_closedBall, sub_eq_add_neg, neg_closedBall
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
inl :
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 (closedBall x r) =
    closedBall (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x) (norm.{u_1} (E := 𝕜) 0 * r)
inr : ∀ (hc : c ≠ 0), c • closedBall x r = closedBall (c • x) (‖c‖ * r)
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)

Tactic:
rcases eq_or_ne c 0 with (rfl | hc)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
x : E
r : ℝ
hr : 0 ≤ r
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 (closedBall x r) =
    closedBall (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x) (norm.{u_1} (E := 𝕜) 0 * r)

Tactic:
simp [hr, zero_smul_set, Set.singleton_zero, nonempty_closedBall]

Premises used: Set.zero_smul_set, Metric.nonempty_closedBall, Set.singleton_zero
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
hc : c ≠ 0
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)

Tactic:
smul_closedBall' hc x r

Premises used: smul_closedBall'
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
hc : c ≠ 0
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)

Tactic:
exact smul_closedBall' hc x r

Premises used: smul_closedBall'
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
c : 𝕜
rw : closedBall (HSMul.hSMul (β := E) c 0) (‖c‖ * 1) = closedBall 0 ‖c‖
rw₁ : Eq.{u_2 + 1} (α := Set E) (closedBall 0 (‖c‖ * 1)) (closedBall 0 ‖c‖)
rw₂ rw₃ : Eq.{u_2 + 1} (α := Set E) (closedBall 0 ‖c‖) (closedBall 0 ‖c‖)
⊢ HSMul.hSMul (β := Set E) c (closedBall 0 1) = closedBall 0 ‖c‖

Tactic:
rw [_root_.smul_closedBall _ _ zero_le_one, smul_zero, mul_one]

Premises used: smul_zero, zero_le_one, mul_one, smul_closedBall
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
rw : Eq.{u_2 + 1} (α := Set E) (closedBall 0 ‖r‖) (closedBall 0 r)
rw₁ rw₂ : Eq.{u_2 + 1} (α := Set E) (closedBall 0 r) (closedBall 0 r)
⊢ HSMul.hSMul (β := Set E) r (closedBall 0 1) = closedBall 0 r

Tactic:
rw [smul_unitClosedBall, Real.norm_of_nonneg hr]

Premises used: smul_unitClosedBall, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedSpace ℝ E
inst_4 : Nontrivial E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
inl :
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 (sphere x r) =
    sphere (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x) (norm.{u_1} (E := 𝕜) 0 * r)
inr : ∀ (hc : c ≠ 0), c • sphere x r = sphere (c • x) (‖c‖ * r)
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)

Tactic:
rcases eq_or_ne c 0 with (rfl | hc)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedSpace ℝ E
inst_4 : Nontrivial E
x : E
r : ℝ
hr : 0 ≤ r
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 (sphere x r) =
    sphere (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x) (norm.{u_1} (E := 𝕜) 0 * r)

Tactic:
simp [zero_smul_set, Set.singleton_zero, hr]

Premises used: Set.zero_smul_set, Set.singleton_zero
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedSpace ℝ E
inst_4 : Nontrivial E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
hc : c ≠ 0
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)

Tactic:
smul_sphere' hc x r

Premises used: smul_sphere'
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedSpace ℝ E
inst_4 : Nontrivial E
c : 𝕜
x : E
r : ℝ
hr : 0 ≤ r
hc : c ≠ 0
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)

Tactic:
exact smul_sphere' hc x r

Premises used: smul_sphere'
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
rw : HVAdd.hVAdd (β := Set E) x (ball 0 r) = ball x r
rw₁ rw₂ : ball x r = ball x r
⊢ x +ᵥ HSMul.hSMul (β := Set E) r (ball 0 1) = ball x r

Tactic:
rw [smul_unitBall_of_pos hr, vadd_ball_zero]

Premises used: vadd_ball_zero, smul_unitBall_of_pos
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
r : ℝ
hr : 0 ≤ r
x : E
rw : HVAdd.hVAdd (β := Set E) x (closedBall 0 ‖r‖) = closedBall x r
rw₁ : HVAdd.hVAdd (β := Set E) x (closedBall 0 r) = closedBall x r
rw₂ rw₃ : closedBall x r = closedBall x r
⊢ x +ᵥ HSMul.hSMul (β := Set E) r (closedBall 0 1) = closedBall x r

Tactic:
rw [smul_unitClosedBall, Real.norm_of_nonneg hr, vadd_closedBall_zero]

Premises used: smul_unitClosedBall, vadd_closedBall_zero, Real.norm_of_nonneg
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : (↑{0}ᶜ : Type u_2)
⊢ 0 < ‖(↑x : E)‖

Tactic:
simpa [-Subtype.coe_prop] using x.2

Premises used: Subtype.coe_prop, Subtype.property
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : (↑{0}ᶜ : Type u_2)
this : 0 < ‖(↑x : E)‖
⊢ Membership.mem (γ := Set E) (sphere 0 r) (r • ‖(↑x : E)‖⁻¹ • (↑x : E))

Tactic:
simp [norm_smul, abs_of_pos hr, this.ne']

Premises used: norm_smul, LT.lt.ne', abs_of_pos
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : (↑{0}ᶜ : Type u_2)
this : 0 < ‖(↑x : E)‖
⊢ 0 < ‖(↑x : E)‖ / r

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx : Membership.mem (γ := Set E) {0}ᶜ x
⊢ 0 < ‖x‖

Tactic:
simpa using hx
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx : Membership.mem (γ := Set E) {0}ᶜ x
⊢ 0 < ‖x‖

Tactic:
have : 0 < ‖x‖ := by simpa using hx
-- Module: Mathlib.Analysis.Normed.Module.Ball.RadialEquiv
Goal:
E_1 : Type u_1
inst : NormedAddCommGroup E_1
inst_1 : NormedSpace ℝ E_1
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
r : ℝ
hr : 0 < r
x : E
hx : Membership.mem (γ := Set E) {0}ᶜ x
this : 0 < ‖x‖
a :
  (↑((fun (x : (↑(sphere 0 r) : Type u_2) × (↑(Ioi 0) : Type)) ↦
            (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) ((↑x.2 : ℝ) • (↑x.1 : E)) ⋯ :
              { x : E // Membership.mem (γ := Set E) {0}ᶜ x }))
          ((fun (x : (↑{0}ᶜ : Type u_2)) ↦
              have this := ⋯;
              (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) (r • ‖(↑x : E)‖⁻¹ • (↑x : E))
                  ⋯,
                Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) (‖(↑x : E)‖ / r) ⋯))
            (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) x hx))) :
      E) =
    (↑(Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) x hx) : E)
⊢ (fun (x : (↑(sphere 0 r) : Type u_2) × (↑(Ioi 0) : Type)) ↦
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) ((↑x.2 : ℝ) • (↑x.1 : E)) ⋯ :
          { x : E // Membership.mem (γ := Set E) {0}ᶜ x }))
      ((fun (x : (↑{0}ᶜ : Type u_2)) ↦
          have this := ⋯;
          (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) (sphere 0 r) x) (r • ‖(↑x : E)‖⁻¹ • (↑x : E)) ⋯,
            Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioi 0) x) (‖(↑x : E)‖ / r) ⋯))
        (Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) x hx)) =
    Subtype.mk (p := fun (x : E) ↦ Membership.mem (γ := Set E) {0}ᶜ x) x hx

Tactic:
ext