awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
h : 0 < r
⊢ (↑(OpenPartialHomeomorph.trans' univUnitBall (unitBallBall c r h) ⋯) : E → P) 0 = c

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
h : ¬0 < r
⊢ (↑(Homeomorph.toOpenPartialHomeomorph (IsometryEquiv.toHomeomorph (IsometryEquiv.vaddConst c))) : E → P) 0 = c

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
⊢ 0 ∈ (toPartialEquiv (univBall c r)).source

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
⊢ 0 ∈ (toPartialEquiv (univBall c r)).source

Tactic:
have : 0 ∈ (univBall c r).source := by simp
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
this : 0 ∈ (toPartialEquiv (univBall c r)).source
⊢ (↑(OpenPartialHomeomorph.symm (univBall c r)) : P → E) c = 0

Tactic:
simpa only [univBall_apply_zero] using (univBall c r).left_inv this

Premises used: OpenPartialHomeomorph.univBall, OpenPartialHomeomorph.left_inv, OpenPartialHomeomorph.univBall_apply_zero
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
⊢ Continuous (↑(univBall c r) : E → P)

Tactic:
simpa [continuousOn_univ] using (univBall c r).continuousOn

Premises used: OpenPartialHomeomorph.univBall, OpenPartialHomeomorph.continuousOn, continuousOn_univ
-- Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
P : Type u_2
inst_2 : PseudoMetricSpace P
inst_3 : NormedAddTorsor E P
c : P
r : ℝ
⊢ ContinuousOn (↑(OpenPartialHomeomorph.symm (univBall c r)) : P → E) (ball c r)

Tactic:
(univBall c r).symm.continuousOn.mono <| ball_subset_univBall_target c r

Premises used: OpenPartialHomeomorph.univBall, OpenPartialHomeomorph.continuousOn, ContinuousOn.mono, OpenPartialHomeomorph.ball_subset_univBall_target, OpenPartialHomeomorph.symm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : SeminormedAddCommGroup 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : SMulZeroClass 𝕜 E
inst_3 : IsBoundedSMul 𝕜 E
c : 𝕜
s : Set E
⊢ ediam (c • s) ≤ ‖c‖₊ • ediam s

Tactic:
(lipschitzWith_smul c).ediam_image_le s

Premises used: LipschitzWith.ediam_image_le, lipschitzWith_smul
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
⊢ ediam (c • s) = ‖c‖₊ • ediam s

Tactic:
le_antisymm (ediam_smul_le c s) ?_

Premises used: ediam_smul_le, le_antisymm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
refine : ‖c‖₊ • ediam s ≤ ediam (c • s)
⊢ ediam (c • s) = ‖c‖₊ • ediam s

Tactic:
refine le_antisymm (ediam_smul_le c s) ?_

Premises used: ediam_smul_le, le_antisymm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
inl : nnnorm.{u_1} (E := 𝕜) 0 • ediam s ≤ ediam (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s)
inr : ∀ (hc : c ≠ 0), ‖c‖₊ • ediam s ≤ ediam (c • s)
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)

Tactic:
obtain rfl | hc := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
s : Set E
inl : nnnorm.{u_1} (E := 𝕜) 0 • ediam.{u_2} (X := E) ∅ ≤ ediam (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := Set E) 0 ∅)
inl₁ : ∀ (hs : s.Nonempty), nnnorm.{u_1} (E := 𝕜) 0 • ediam s ≤ ediam (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s)
⊢ nnnorm.{u_1} (E := 𝕜) 0 • ediam s ≤ ediam (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s)

Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
⊢ nnnorm.{u_1} (E := 𝕜) 0 • ediam.{u_2} (X := E) ∅ ≤ ediam (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) (β := Set E) 0 ∅)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
s : Set E
hs : s.Nonempty
⊢ nnnorm.{u_1} (E := 𝕜) 0 • ediam s ≤ ediam (HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 s)

Tactic:
simp [zero_smul_set hs, ← Set.singleton_zero]

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 : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
⊢ ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ (↑‖c⁻¹‖₊ : ENNReal) * ediam (c • s)

Tactic:
have := (lipschitzWith_smul c⁻¹).ediam_image_le (c • s)
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
s : Set E
hc : c ≠ 0
this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ (↑‖c⁻¹‖₊ : ENNReal) * ediam (c • s)
inr :
  ∀ (this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ (↑‖c⁻¹‖₊ : ENNReal) • ediam (c • s)),
    ‖c‖₊ • ediam s ≤ ediam (c • s)
inr₁ :
  ∀ (this : ediam (X := E) ((fun (x : E) ↦ c⁻¹ • x) '' (c • s)) ≤ ‖c⁻¹‖₊ • ediam (c • s)),
    ‖c‖₊ • ediam s ≤ ediam (c • s)
inr₂ : ∀ (this : ediam (c⁻¹ • c • s) ≤ ‖c⁻¹‖₊ • ediam (c • s)), ‖c‖₊ • ediam s ≤ ediam (c • s)
inr₃ : ∀ (this : ediam s ≤ ‖c⁻¹‖₊ • ediam (c • s)), ‖c‖₊ • ediam s ≤ ediam (c • s)
inr₄ : ∀ (this : ediam s ≤ ‖c‖₊⁻¹ • ediam (c • s)), ‖c‖₊ • ediam s ≤ ediam (c • s)
inr₅ inr₆ inr₇ inr₈ : ∀ (this : ‖c‖₊ • ediam s ≤ ediam (c • s)), ‖c‖₊ • ediam s ≤ ediam (c • s)
⊢ ‖c‖₊ • ediam s ≤ ediam (c • s)

Tactic:
rwa [← smul_eq_mul, ← ENNReal.smul_def, Set.image_smul, inv_smul_smul₀ hc s, nnnorm_inv,
      le_inv_smul_iff_of_pos (nnnorm_pos.2 hc)] at this

Premises used: nnnorm_inv, Iff.mpr, Set.image_smul, inv_smul_smul₀, ENNReal.smul_def, smul_eq_mul, nnnorm_pos, le_inv_smul_iff_of_pos
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedDivisionRing 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormSMulClass 𝕜 E
c : 𝕜
x : Set E
simp_rw : (ediam (c • x)).toReal = ‖c‖ * (ediam x).toReal
simp_rw₁ : (‖c‖₊ • ediam x).toReal = ‖c‖ * (ediam x).toReal
simp_rw₂ : ‖c‖₊ • (ediam x).toReal = ‖c‖ * (ediam x).toReal
simp_rw₃ : (↑‖c‖₊ : ℝ) • (ediam x).toReal = ‖c‖ * (ediam x).toReal
simp_rw₄ : ‖c‖ • (ediam x).toReal = ‖c‖ * (ediam x).toReal
⊢ diam (c • x) = ‖c‖ * diam x

Tactic:
simp_rw [diam, ediam_smul₀, ENNReal.toReal_smul, NNReal.smul_def, coe_nnnorm, smul_eq_mul]

Premises used: NNReal.smul_def, coe_nnnorm, ediam_smul₀, Metric.diam, smul_eq_mul, ENNReal.toReal_smul
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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
⊢ Function.Surjective (β := E) fun (x : E) ↦ c • x

Tactic:
have : Function.Surjective ((c • ·) : E → E) :=
    Function.RightInverse.surjective (smul_inv_smul₀ hc)
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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
this : Function.Surjective (β := E) fun (x : E) ↦ c • x
trans : Eq (α := ENNReal) (⨅ y ∈ c • s, edist (c • x) y) (⨅ y ∈ s, ‖c‖₊ • edist x y)
trans₁ : ⨅ y ∈ s, ‖c‖₊ • edist x y = HSMul.hSMul (β := ENNReal) ‖c‖₊ (⨅ y ∈ s, edist x y)
⊢ ⨅ y ∈ c • s, edist (c • x) y = HSMul.hSMul (β := ENNReal) ‖c‖₊ (⨅ y ∈ s, edist x y)

Tactic:
trans ⨅ (y) (_ : y ∈ s), ‖c‖₊ • edist x y
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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
this : Function.Surjective (β := E) fun (x : E) ↦ c • x
⊢ Eq (α := ENNReal) (⨅ y ∈ c • s, edist (c • x) y) (⨅ y ∈ s, ‖c‖₊ • edist x y)

Tactic:
(this.iInf_congr _ fun y => ?_).symm

Premises used: Function.Surjective.iInf_congr, Eq.symm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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
this : Function.Surjective (β := E) fun (x : E) ↦ c • x
refine : ∀ (y : E), Eq (α := ENNReal) (⨅ (_ : c • y ∈ c • s), edist (c • x) (c • y)) (⨅ (_ : y ∈ s), ‖c‖₊ • edist x y)
⊢ Eq (α := ENNReal) (⨅ y ∈ c • s, edist (c • x) y) (⨅ y ∈ s, ‖c‖₊ • edist x y)

Tactic:
refine (this.iInf_congr _ fun y => ?_).symm

Premises used: Function.Surjective.iInf_congr, Eq.symm
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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
this : Function.Surjective (β := E) fun (x : E) ↦ c • x
y : E
simp_rw : Eq (α := ENNReal) (⨅ (_ : y ∈ s), edist (c • x) (c • y)) (⨅ (_ : y ∈ s), ‖c‖₊ • edist x y)
⊢ Eq (α := ENNReal) (⨅ (_ : c • y ∈ c • s), edist (c • x) (c • y)) (⨅ (_ : y ∈ s), ‖c‖₊ • edist x y)

Tactic:
simp_rw [smul_mem_smul_set_iff₀ hc, edist_smul₀]

Premises used: Set.smul_mem_smul_set_iff₀, edist_smul₀
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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
this : Function.Surjective (β := E) fun (x : E) ↦ c • x
⊢ (↑‖c‖₊ : ENNReal) ≠ 0

Tactic:
simp [hc]
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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
this : Function.Surjective (β := E) fun (x : E) ↦ c • x
⊢ (↑‖c‖₊ : ENNReal) ≠ 0

Tactic:
have : (‖c‖₊ : ENNReal) ≠ 0 := by simp [hc]
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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
this_1 : Function.Surjective (β := E) fun (x : E) ↦ c • x
this : (↑‖c‖₊ : ENNReal) ≠ 0
simp_rw : ⨅ y ∈ s, (↑‖c‖₊ : ENNReal) • edist x y = HSMul.hSMul (β := ENNReal) (↑‖c‖₊ : ENNReal) (⨅ y ∈ s, edist x y)
simp_rw₁ : ⨅ y ∈ s, (↑‖c‖₊ : ENNReal) * edist x y = (↑‖c‖₊ : ENNReal) * ⨅ y ∈ s, edist x y
⊢ ⨅ y ∈ s, ‖c‖₊ • edist x y = HSMul.hSMul (β := ENNReal) ‖c‖₊ (⨅ y ∈ s, edist x y)

Tactic:
simp_rw [ENNReal.smul_def, smul_eq_mul, ENNReal.mul_iInf_of_ne this ENNReal.coe_ne_top]

Premises used: ENNReal.smul_def, ENNReal.mul_iInf_of_ne, smul_eq_mul, ENNReal.coe_ne_top
-- Module: Mathlib.Analysis.Normed.Module.Ball.Pointwise
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
simp_rw₄ : ‖c‖ • (infEDist x s).toReal = ‖c‖ * (infEDist x s).toReal
⊢ infDist (c • x) (c • s) = ‖c‖ * infDist x s

Tactic:
simp_rw [Metric.infDist, infEDist_smul₀ hc s, ENNReal.toReal_smul, NNReal.smul_def, coe_nnnorm,
    smul_eq_mul]

Premises used: infEDist_smul₀, Metric.infDist, NNReal.smul_def, coe_nnnorm, smul_eq_mul, ENNReal.toReal_smul
-- 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
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
h : ∀ (y : E), y ∈ c • ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)
⊢ c • ball x r = ball (c • x) (‖c‖ * r)

Tactic:
ext y
-- 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
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
h : c⁻¹ • y ∈ ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)
⊢ y ∈ c • ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ hc]

Premises used: Set.mem_smul_set_iff_inv_smul_mem₀
-- 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
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
rw : c⁻¹ • y ∈ ball (c⁻¹ • c • x) r
| c⁻¹ • y ∈ ball x r

Tactic:
rw [← inv_smul_smul₀ hc x]

Premises used: inv_smul_smul₀
-- 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
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
h : c⁻¹ • y ∈ ball (c⁻¹ • c • x) r ↔ y ∈ ball (c • x) (‖c‖ * r)
⊢ c⁻¹ • y ∈ ball x r ↔ y ∈ ball (c • x) (‖c‖ * r)

Tactic:
conv_lhs => rw [← inv_smul_smul₀ hc x]

Premises used: inv_smul_smul₀
-- 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
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ ball (c⁻¹ • c • x) r ↔ y ∈ ball (c • x) (‖c‖ * r)

Tactic:
simp [← div_eq_inv_mul, div_lt_iff₀ (norm_pos_iff.2 hc), mul_comm _ r, dist_smul₀]

Premises used: Iff.mpr, norm_pos_iff, div_lt_iff₀, mul_comm, dist_smul₀, div_eq_inv_mul
-- 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
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‖)
rw₂ rw₃ : Eq.{u_2 + 1} (α := Set E) (ball 0 ‖c‖) (ball 0 ‖c‖)
⊢ HSMul.hSMul (β := Set E) c (ball 0 1) = ball 0 ‖c‖

Tactic:
rw [_root_.smul_ball hc, smul_zero, mul_one]

Premises used: smul_zero, smul_ball, mul_one
-- 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
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
h : ∀ (y : E), y ∈ c • sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)
⊢ c • sphere x r = sphere (c • x) (‖c‖ * r)

Tactic:
ext y
-- 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
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
h : c⁻¹ • y ∈ sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)
⊢ y ∈ c • sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ hc]

Premises used: Set.mem_smul_set_iff_inv_smul_mem₀
-- 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
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
rw : c⁻¹ • y ∈ sphere (c⁻¹ • c • x) r
| c⁻¹ • y ∈ sphere x r

Tactic:
rw [← inv_smul_smul₀ hc x]

Premises used: inv_smul_smul₀
-- 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
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
h : c⁻¹ • y ∈ sphere (c⁻¹ • c • x) r ↔ y ∈ sphere (c • x) (‖c‖ * r)
⊢ c⁻¹ • y ∈ sphere x r ↔ y ∈ sphere (c • x) (‖c‖ * r)

Tactic:
conv_lhs => rw [← inv_smul_smul₀ hc x]

Premises used: inv_smul_smul₀
-- 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
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
y : E
⊢ c⁻¹ • y ∈ sphere (c⁻¹ • c • x) r ↔ y ∈ sphere (c • x) (‖c‖ * r)

Tactic:
simp only [mem_sphere, dist_smul₀, norm_inv, ← div_eq_inv_mul, div_eq_iff (norm_pos_iff.2 hc).ne',
    mul_comm r]

Premises used: Iff.mpr, norm_pos_iff, norm_inv, Metric.mem_sphere, LT.lt.ne', div_eq_iff, mul_comm, dist_smul₀, div_eq_inv_mul
-- 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
c : 𝕜
hc : c ≠ 0
x : E
r : ℝ
⊢ c • closedBall x r = closedBall (c • x) (‖c‖ * r)

Tactic:
simp only [← ball_union_sphere, Set.smul_set_union, _root_.smul_ball hc, smul_sphere' hc]

Premises used: smul_sphere', Metric.ball_union_sphere, Set.smul_set_union, smul_ball
-- 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
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
c : 𝕜
hc : c ∈ s
rw : sphere (HSMul.hSMul (β := E) c 0) (‖c‖ * r) = sphere 0 (‖c‖ * r)
rw₁ rw₂ : Eq.{u_2 + 1} (α := Set E) (sphere 0 (‖c‖ * r)) (sphere 0 (‖c‖ * r))
⊢ HSMul.hSMul (β := Set E) c (sphere 0 r) = sphere 0 (‖c‖ * r)

Tactic:
rw [smul_sphere' (ne_of_mem_of_not_mem hc hs), smul_zero]

Premises used: smul_sphere', smul_zero, ne_of_mem_of_not_mem
-- 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
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
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
⊢ Eq.{u_2 + 1} (α := Set E) (⋃ c ∈ s, sphere 0 (‖c‖ * r))
    (preimage (β := ℝ) (fun (x : E) ↦ ‖x‖) ((fun (x : 𝕜) ↦ ‖x‖ * r) '' s))

Tactic:
ext
-- 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
s : Set 𝕜
hs : 0 ∉ s
r : ℝ
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:
simp [eq_comm]

Premises used: eq_comm
-- 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
s : Set E
hs : IsBounded s
c : 𝕜
⊢ IsBounded (c • s)

Tactic:
(lipschitzWith_smul c).isBounded_image hs

Premises used: LipschitzWith.isBounded_image, lipschitzWith_smul
-- 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
⊢ ∃ (ε : ℝ), 0 < ε ∧ closedBall x ε ⊆ u

Tactic:
nhds_basis_closedBall.mem_iff.1 hu

Premises used: Filter.HasBasis.mem_iff, Iff.mp, Metric.nhds_basis_closedBall
-- 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
obtain : ∀ (ε : ℝ) (εpos : 0 < ε) (hε : closedBall x ε ⊆ u), ∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u
⊢ ∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u

Tactic:
obtain ⟨ε, εpos, hε⟩ : ∃ ε : ℝ, 0 < ε ∧ closedBall x ε ⊆ u := nhds_basis_closedBall.mem_iff.1 hu

Premises used: Filter.HasBasis.mem_iff, Iff.mp, Metric.nhds_basis_closedBall
-- 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 : ℝ), 0 < R ∧ s ⊆ closedBall 0 R

Tactic:
hs.subset_closedBall_lt 0 0

Premises used: Bornology.IsBounded.subset_closedBall_lt, OfNat.ofNat
-- 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
obtain : ∀ (R : ℝ) (Rpos : 0 < R) (hR : s ⊆ closedBall 0 R), ∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u
⊢ ∀ᶠ (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

Premises used: Bornology.IsBounded.subset_closedBall_lt, OfNat.ofNat
-- 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
⊢ Membership.mem (γ := Filter 𝕜) (𝓝 0) (closedBall 0 (ε / R))

Tactic:
have : Metric.closedBall (0 : 𝕜) (ε / R) ∈ 𝓝 (0 : 𝕜) := closedBall_mem_nhds _ (div_pos εpos Rpos)
-- 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))
h : ∀ (r : 𝕜) (hr : Membership.mem (γ := Set 𝕜) (closedBall 0 (ε / R)) r), {x} + r • s ⊆ u
⊢ ∀ᶠ (r : 𝕜) in 𝓝 0, {x} + r • s ⊆ u

Tactic:
filter_upwards [this] with r hr
-- 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
h : (fun (x_1 : E) ↦ -x + x_1) ⁻¹' (r • s) ⊆ u
⊢ {x} + r • s ⊆ u

Tactic:
simp only [image_add_left, singleton_add]

Premises used: Set.image_add_left, Set.singleton_add
-- 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 ∈ s, r • z = -x + y

Tactic:
simpa [mem_smul_set] using hy

Premises used: Set.mem_smul_set