-- Mathlib/Analysis/Complex/Tietze.lean
theorem Metric.instTietzeExtensionClosedBall (𝕜 : Type v) [RCLike 𝕜] {E : Type w}
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] [FiniteDimensional 𝕜 E] (y : E) {r : ℝ} (hr : 0 < r) :
    TietzeExtension.{u, w} (Metric.closedBall y r) :=
  .of_homeo <| by
    show (Metric.closedBall y r) ≃ₜ (Metric.closedBall (0 : E) 1)
    symm
    apply (DilationEquiv.smulTorsor y (k := (r : 𝕜)) <| by exact_mod_cast hr.ne').toHomeomorph.sets
    ext x
    simp only [mem_closedBall, dist_zero_right, DilationEquiv.coe_toHomeomorph, Set.mem_preimage,
      DilationEquiv.smulTorsor_apply, vadd_eq_add, dist_add_self_left, norm_smul,
      RCLike.norm_ofReal, abs_of_nonneg hr.le]
    exact (mul_le_iff_le_one_right hr).symm

Proof state:
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
⊢ ↑(closedBall y r) ≃ₜ ↑(closedBall 0 1)

Tactic:
symm

Result:
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
⊢ ↑(closedBall 0 1) ≃ₜ ↑(closedBall y r)

Proof state:
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
⊢ ↑(closedBall y r) ≃ₜ ?m.56929

Tactic:
show (Metric.closedBall y r) ≃ₜ (Metric.closedBall (0 : E) 1)

Result:
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
⊢ ↑(closedBall y r) ≃ₜ ↑(closedBall 0 1)

Proof state:
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
⊢ ↑r ≠ 0

Tactic:
exact_mod_cast hr.ne'

Result:
no goals

Proof state:
case h
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
x : E
⊢ x ∈ closedBall 0 1 ↔ x ∈ ⇑(DilationEquiv.smulTorsor y ⋯).toHomeomorph ⁻¹' closedBall y r

Tactic:
simp only [mem_closedBall, dist_zero_right, DilationEquiv.coe_toHomeomorph, Set.mem_preimage,
  DilationEquiv.smulTorsor_apply, vadd_eq_add, dist_add_self_left, norm_smul,
  RCLike.norm_ofReal, abs_of_nonneg hr.le]

Result:
case h
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
x : E
⊢ ‖x‖ ≤ 1 ↔ r * ‖x‖ ≤ r

Proof state:
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
⊢ closedBall 0 1 = ⇑(DilationEquiv.smulTorsor y ⋯).toHomeomorph ⁻¹' closedBall y r

Tactic:
ext x

Result:
case h
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
x : E
⊢ x ∈ closedBall 0 1 ↔ x ∈ ⇑(DilationEquiv.smulTorsor y ⋯).toHomeomorph ⁻¹' closedBall y r

Proof state:
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
⊢ ↑(closedBall 0 1) ≃ₜ ↑(closedBall y r)

Tactic:
apply (DilationEquiv.smulTorsor y (k := (r : 𝕜)) <| by exact_mod_cast hr.ne').toHomeomorph.sets

Result:
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
⊢ closedBall 0 1 = ⇑(DilationEquiv.smulTorsor y ⋯).toHomeomorph ⁻¹' closedBall y r

Proof state:
case h
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
x : E
⊢ ‖x‖ ≤ 1 ↔ r * ‖x‖ ≤ r

Tactic:
exact (mul_le_iff_le_one_right hr).symm

Result:
no goals