awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this_2 : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
this : Continuous (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g)
refine_1 :
  ∀ (x : E),
    Membership.mem (γ := Set E) (Metric.closedBall 0 1)
      (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g x)
refine_2 :
  Eq (α := C((↑(Metric.closedBall 0 1) : Type w), (↑(Metric.closedBall 0 1) : Type w)))
    (ContinuousMap.comp
      { toFun := codRestrict (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g) (Metric.closedBall 0 1) ⋯,
        continuous_toFun := ⋯ : C(E, (↑(Metric.closedBall 0 1) : Type w)) }
      { toFun := Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (Metric.closedBall 0 1) x),
        continuous_toFun := ⋯ })
    (ContinuousMap.id (↑(Metric.closedBall 0 1) : Type w))
⊢ TietzeExtension.{u, w} (↑(Metric.closedBall 0 1) : Type w)

Tactic:
refine .of_retract ⟨Subtype.val, by fun_prop⟩ ⟨_, this.codRestrict fun x ↦ ?_⟩ ?_
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this_2 : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
this : Continuous (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g)
x : E
pos :
  ∀ (hx : Membership.mem (γ := Set E) (Metric.closedBall 0 1) x),
    Membership.mem (γ := Set E) (Metric.closedBall 0 1)
      (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g x)
neg :
  ∀ (hx : x ∉ Metric.closedBall 0 1),
    Membership.mem (γ := Set E) (Metric.closedBall 0 1)
      (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g x)
⊢ Membership.mem (γ := Set E) (Metric.closedBall 0 1) (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g x)

Tactic:
by_cases hx : x ∈ Metric.closedBall 0 1

Premises used: Metric.closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this_2 : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
this : Continuous (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g)
x : E
hx : Membership.mem (γ := Set E) (Metric.closedBall 0 1) x
⊢ Membership.mem (γ := Set E) (Metric.closedBall 0 1) (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g x)

Tactic:
simpa [piecewise_eq_of_mem (hi := hx)] using hx

Premises used: Set.piecewise_eq_of_mem, Metric.closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this_2 : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
this : Continuous (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g)
x : E
hx : x ∉ Metric.closedBall 0 1
neg : Membership.mem (γ := Set E) (Metric.closedBall 0 1) (HSMul.hSMul.{v, w, w} (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) x)
⊢ Membership.mem (γ := Set E) (Metric.closedBall 0 1) (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g x)

Tactic:
simp only [g, piecewise_eq_of_notMem (hi := hx), RCLike.real_smul_eq_coe_smul (K := 𝕜)]

Premises used: Set.piecewise_eq_of_notMem, RCLike.real_smul_eq_coe_smul, Metric.closedBall, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this_2 : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
this : Continuous (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g)
x : E
hx : x ∉ Metric.closedBall 0 1
pos :
  ∀ (hx' : x = 0), Membership.mem (γ := Set E) (Metric.closedBall 0 1) (HSMul.hSMul.{v, w, w} (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) x)
neg :
  ∀ (hx' : ¬x = 0), Membership.mem (γ := Set E) (Metric.closedBall 0 1) (HSMul.hSMul.{v, w, w} (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) x)
⊢ Membership.mem (γ := Set E) (Metric.closedBall 0 1) (HSMul.hSMul.{v, w, w} (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) x)

Tactic:
by_cases hx' : x = 0
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this_2 : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
this : Continuous (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g)
x : E
hx : x ∉ Metric.closedBall 0 1
hx' : x = 0
⊢ Membership.mem (γ := Set E) (Metric.closedBall 0 1) (HSMul.hSMul.{v, w, w} (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) x)

Tactic:
simp [hx']
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this_2 : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
this : Continuous (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g)
x : E
hx : x ∉ Metric.closedBall 0 1
hx' : ¬x = 0
⊢ Membership.mem (γ := Set E) (Metric.closedBall 0 1) (HSMul.hSMul.{v, w, w} (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) x)

Tactic:
simp [hx']
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this_2 : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
this : Continuous (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g)
refine_2 :
  ∀ (x : (↑(Metric.closedBall 0 1) : Type w)),
    Eq.{w + 1} (α := E)
      (↑((ContinuousMap.comp
                {
                  toFun :=
                    codRestrict (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g) (Metric.closedBall 0 1)
                      ⋯,
                  continuous_toFun := ⋯ : C(E, (↑(Metric.closedBall 0 1) : Type w)) }
                { toFun := Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (Metric.closedBall 0 1) x),
                  continuous_toFun := ⋯ } :
              (a : (↑(Metric.closedBall 0 1) : Type w)) → (↑(Metric.closedBall 0 1) : Type w))
            x) :
        E)
      (↑((ContinuousMap.id (↑(Metric.closedBall 0 1) : Type w) :
              (a : (↑(Metric.closedBall 0 1) : Type w)) → (↑(Metric.closedBall 0 1) : Type w))
            x) :
        E)
⊢ Eq (α := C((↑(Metric.closedBall 0 1) : Type w), (↑(Metric.closedBall 0 1) : Type w)))
    (ContinuousMap.comp
      { toFun := codRestrict (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g) (Metric.closedBall 0 1) ⋯,
        continuous_toFun := ⋯ : C(E, (↑(Metric.closedBall 0 1) : Type w)) }
      { toFun := Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (Metric.closedBall 0 1) x),
        continuous_toFun := ⋯ })
    (ContinuousMap.id (↑(Metric.closedBall 0 1) : Type w))

Tactic:
ext x
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this_2 : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
this : Continuous (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g)
x : (↑(Metric.closedBall 0 1) : Type w)
⊢ Eq.{w + 1} (α := E)
    (↑((ContinuousMap.comp
              {
                toFun :=
                  codRestrict (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g) (Metric.closedBall 0 1) ⋯,
                continuous_toFun := ⋯ : C(E, (↑(Metric.closedBall 0 1) : Type w)) }
              { toFun := Subtype.val (p := fun (x : E) ↦ Membership.mem (γ := Set E) (Metric.closedBall 0 1) x),
                continuous_toFun := ⋯ } :
            (a : (↑(Metric.closedBall 0 1) : Type w)) → (↑(Metric.closedBall 0 1) : Type w))
          x) :
      E)
    (↑((ContinuousMap.id (↑(Metric.closedBall 0 1) : Type w) :
            (a : (↑(Metric.closedBall 0 1) : Type w)) → (↑(Metric.closedBall 0 1) : Type w))
          x) :
      E)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
suffices : Continuous (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g)
⊢ TietzeExtension.{u, w} (↑(Metric.closedBall 0 1) : Type w)

Tactic:
suffices this : Continuous (piecewise (Metric.closedBall 0 1) id g) by
    refine .of_retract ⟨Subtype.val, by fun_prop⟩ ⟨_, this.codRestrict fun x ↦ ?_⟩ ?_
    · by_cases hx : x ∈ Metric.closedBall 0 1
      · simpa [piecewise_eq_of_mem (hi := hx)] using hx
      · simp only [g, piecewise_eq_of_notMem (hi := hx), RCLike.real_smul_eq_coe_smul (K := 𝕜)]
        by_cases hx' : x = 0 <;> simp [hx']
    · ext x
      simp
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
⊢ Continuous (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g)

Tactic:
continuous_piecewise (fun x hx ↦ ?_) continuousOn_id ?_

Premises used: continuous_piecewise, continuousOn_id
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
refine_1 : ∀ (x : E) (hx : Membership.mem (γ := Set E) (frontier (Metric.closedBall 0 1)) x), id x = g x
refine_2 : ContinuousOn g (closure (Metric.closedBall 0 1)ᶜ)
⊢ Continuous (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g)

Tactic:
refine continuous_piecewise (fun x hx ↦ ?_) continuousOn_id ?_

Premises used: continuous_piecewise, continuousOn_id
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
x : E
hx : Membership.mem (γ := Set E) (frontier (Metric.closedBall 0 1)) x
⊢ ‖x‖ = 1

Tactic:
simpa [frontier_closedBall (0 : E) one_ne_zero] using hx

Premises used: frontier_closedBall, one_ne_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
x : E
hx : Membership.mem (γ := Set E) (frontier (Metric.closedBall 0 1)) x
⊢ ‖x‖ = 1

Tactic:
replace hx : ‖x‖ = 1 := by simpa [frontier_closedBall (0 : E) one_ne_zero] using hx
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
x : E
hx : ‖x‖ = 1
⊢ id x = g x

Tactic:
simp [g, hx]
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
⊢ ContinuousOn g (closure (Metric.closedBall 0 1)ᶜ)

Tactic:
continuousOn_id.norm.inv₀ ?_ |>.smul continuousOn_id

Premises used: ContinuousOn.smul, ContinuousOn.inv₀, ContinuousOn.norm, continuousOn_id
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
refine_2 : ∀ (x : E), Membership.mem (γ := Set E) (closure (Metric.closedBall 0 1)ᶜ) x → ‖id x‖ ≠ 0
⊢ ContinuousOn g (closure (Metric.closedBall 0 1)ᶜ)

Tactic:
refine continuousOn_id.norm.inv₀ ?_ |>.smul continuousOn_id

Premises used: ContinuousOn.smul, ContinuousOn.inv₀, ContinuousOn.norm, continuousOn_id
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
refine_2 : ∀ (x : E), 1 ≤ ‖x‖ → ¬x = 0
⊢ ∀ (x : E), Membership.mem (γ := Set E) (closure (Metric.closedBall 0 1)ᶜ) x → ‖id x‖ ≠ 0

Tactic:
simp only [closure_compl, interior_closedBall (0 : E) one_ne_zero, mem_compl_iff,
      Metric.mem_ball, dist_zero_right, not_lt, id_eq, ne_eq, norm_eq_zero]

Premises used: norm_eq_zero, interior_closedBall, ne_eq, Metric.mem_ball, not_lt, closure_compl, one_ne_zero, OfNat.ofNat, dist_zero_right, Set.mem_compl_iff, id_eq
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
⊢ ∀ (x : E), 1 ≤ ‖x‖ → ¬x = 0

Tactic:
fun x hx ↦ norm_pos_iff.mp <| one_pos.trans_le hx

Premises used: norm_pos_iff, LT.lt.trans_le, Iff.mp, one_pos
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
⊢ ∀ (x : E), 1 ≤ ‖x‖ → ¬x = 0

Tactic:
exact fun x hx ↦ norm_pos_iff.mp <| one_pos.trans_le hx

Premises used: norm_pos_iff, LT.lt.trans_le, Iff.mp, one_pos
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
this_1 : NormedSpace ℝ E
this : IsScalarTower ℝ 𝕜 E
g : E → E := fun (x : E) ↦ ‖x‖⁻¹ • x
suffices suffices₁ suffices₂ : Continuous (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g)
refine_1 : ∀ (x : E) (hx : Membership.mem (γ := Set E) (frontier (Metric.closedBall 0 1)) x), id x = g x
refine_2 refine_2₁ : ContinuousOn g (closure (Metric.closedBall 0 1)ᶜ)
⊢ TietzeExtension.{u, w} (↑(Metric.closedBall 0 1) : Type w)

Tactic:
classical
  suffices this : Continuous (piecewise (Metric.closedBall 0 1) id g) by
    refine .of_retract ⟨Subtype.val, by fun_prop⟩ ⟨_, this.codRestrict fun x ↦ ?_⟩ ?_
    · by_cases hx : x ∈ Metric.closedBall 0 1
      · simpa [piecewise_eq_of_mem (hi := hx)] using hx
      · simp only [g, piecewise_eq_of_notMem (hi := hx), RCLike.real_smul_eq_coe_smul (K := 𝕜)]
        by_cases hx' : x = 0 <;> simp [hx']
    · ext x
      simp
  refine continuous_piecewise (fun x hx ↦ ?_) continuousOn_id ?_
  · replace hx : ‖x‖ = 1 := by simpa [frontier_closedBall (0 : E) one_ne_zero] using hx
    simp [g, hx]
  · refine continuousOn_id.norm.inv₀ ?_ |>.smul continuousOn_id
    simp only [closure_compl, interior_closedBall (0 : E) one_ne_zero, mem_compl_iff,
      Metric.mem_ball, dist_zero_right, not_lt, id_eq, ne_eq, norm_eq_zero]
    exact fun x hx ↦ norm_pos_iff.mp <| one_pos.trans_le hx

Premises used: norm_eq_zero, norm_pos_iff, interior_closedBall, ne_eq, Metric.mem_ball, not_lt, LT.lt.trans_le, ContinuousOn.smul, closure_compl, Iff.mp, continuous_piecewise, ContinuousOn.inv₀, ContinuousOn.norm, continuousOn_id, one_ne_zero, OfNat.ofNat, dist_zero_right, one_pos, Set.mem_compl_iff, id_eq
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
r : ℝ
hr : 0 < r
⊢ TietzeExtension.{u, w} (↑(ball 0 r) : Type w)

Tactic:
have : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
  .of_homeo <| show (Metric.ball (0 : E) r) ≃ₜ (Metric.ball (0 : E) 1) from
    OpenPartialHomeomorph.unitBallBall (0 : E) r hr |>.toHomeomorphSourceTarget.symm

Premises used: Real, OpenPartialHomeomorph.unitBallBall, OpenPartialHomeomorph.toHomeomorphSourceTarget, Homeomorph.symm, OfNat.ofNat, NormedSpace.restrictScalars, TietzeExtension.of_homeo
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
symm : (↑(closedBall 0 1) : Type w) ≃ₜ (↑(closedBall y r) : Type w)
⊢ (↑(closedBall y r) : Type w) ≃ₜ (↑(closedBall 0 1) : Type w)

Tactic:
symm
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
⊢ Ne.{v + 1} (α := 𝕜) (↑r : 𝕜) 0

Tactic:
exact_mod_cast hr.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
apply :
  Eq (α := Set E) (closedBall 0 1)
    ((⇑(DilationEquiv.toHomeomorph (DilationEquiv.smulTorsor.{v, w, w} (𝕜 := 𝕜) y (k := (↑r : 𝕜)) ⋯)) : (a : E) → E) ⁻¹'
      closedBall y r)
⊢ (↑(closedBall 0 1) : Type w) ≃ₜ (↑(closedBall y r) : Type w)

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

Premises used: DilationEquiv.toHomeomorph, Homeomorph.sets, DilationEquiv.smulTorsor
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
h :
  ∀ (x : E),
    Membership.mem (γ := Set E) (closedBall 0 1) x ↔
      Membership.mem (γ := Set E)
        ((⇑(DilationEquiv.toHomeomorph (DilationEquiv.smulTorsor.{v, w, w} (𝕜 := 𝕜) y (k := (↑r : 𝕜)) ⋯)) :
            (a : E) → E) ⁻¹'
          closedBall y r)
        x
⊢ Eq (α := Set E) (closedBall 0 1)
    ((⇑(DilationEquiv.toHomeomorph (DilationEquiv.smulTorsor.{v, w, w} (𝕜 := 𝕜) y (k := (↑r : 𝕜)) ⋯)) : (a : E) → E) ⁻¹'
      closedBall y r)

Tactic:
ext x
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
x : E
h : ‖x‖ ≤ 1 ↔ r * ‖x‖ ≤ r
⊢ Membership.mem (γ := Set E) (closedBall 0 1) x ↔
    Membership.mem (γ := Set E)
      ((⇑(DilationEquiv.toHomeomorph (DilationEquiv.smulTorsor.{v, w, w} (𝕜 := 𝕜) y (k := (↑r : 𝕜)) ⋯)) :
          (a : E) → E) ⁻¹'
        closedBall y r)
      x

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]

Premises used: DilationEquiv.coe_toHomeomorph, norm_smul, RCLike.norm_ofReal, LT.lt.le, dist_add_self_left, DilationEquiv.smulTorsor_apply, vadd_eq_add, abs_of_nonneg, Metric.mem_closedBall, dist_zero_right, Set.mem_preimage
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
y : E
r : ℝ
hr : 0 < r
x : E
⊢ ‖x‖ ≤ 1 ↔ r * ‖x‖ ≤ r

Tactic:
(mul_le_iff_le_one_right hr).symm

Premises used: Iff.symm, mul_le_iff_le_one_right
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
𝕜 : Type v
inst : RCLike 𝕜
E : Type w
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : 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

Premises used: Iff.symm, mul_le_iff_le_one_right
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
rw : TietzeExtension (↑(Metric.closedBall 2⁻¹ 2⁻¹) : Type)
⊢ TietzeExtension (↑I : Type)

Tactic:
rw [unitInterval.eq_closedBall]

Premises used: unitInterval.eq_closedBall
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
⊢ LT.lt (α := ℝ) 0 2⁻¹

Tactic:
norm_num
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
⊢ TietzeExtension (↑(Metric.closedBall 2⁻¹ 2⁻¹) : Type)

Tactic:
exact Metric.instTietzeExtensionClosedBall ℝ _ (by norm_num)

Premises used: Real, Metric.instTietzeExtensionClosedBall
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst_2 : RCLike 𝕜
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
f : BoundedContinuousFunction.{u, w} (↑s : Type u) E
pos : ∀ (hf : ‖f‖ = 0), ∃ (g : X →ᵇ E), ‖g‖ = ‖f‖ ∧ g.restrict s = f
neg : ∀ (hf : ¬‖f‖ = 0), ∃ (g : X →ᵇ E), ‖g‖ = ‖f‖ ∧ g.restrict s = f
⊢ ∃ (g : X →ᵇ E), ‖g‖ = ‖f‖ ∧ g.restrict s = f

Tactic:
by_cases hf : ‖f‖ = 0
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst_2 : RCLike 𝕜
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
f : BoundedContinuousFunction.{u, w} (↑s : Type u) E
hf : ‖f‖ = 0
⊢ norm (E := X →ᵇ E) 0 = ‖f‖ ∧ restrict 0 s = f

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst_2 : RCLike 𝕜
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
f : BoundedContinuousFunction.{u, w} (↑s : Type u) E
hf : ‖f‖ = 0
⊢ ∃ (g : X →ᵇ E), ‖g‖ = ‖f‖ ∧ g.restrict s = f

Tactic:
exact ⟨0, by aesop⟩
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst_2 : RCLike 𝕜
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
f : BoundedContinuousFunction.{u, w} (↑s : Type u) E
hf : ¬‖f‖ = 0
⊢ 0 < ‖f‖

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst_2 : RCLike 𝕜
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
f : BoundedContinuousFunction.{u, w} (↑s : Type u) E
hf : ¬‖f‖ = 0
⊢ TietzeExtension.{u, w} (↑(Metric.closedBall 0 ‖f‖) : Type w)

Tactic:
have := Metric.instTietzeExtensionClosedBall.{u, v} 𝕜 (0 : E) (by simp_all : 0 < ‖f‖)
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst_2 : RCLike 𝕜
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
f : BoundedContinuousFunction.{u, w} (↑s : Type u) E
hf : ¬‖f‖ = 0
this : TietzeExtension.{u, w} (↑(Metric.closedBall 0 ‖f‖) : Type w)
x : (↑s : Type u)
⊢ Membership.mem.{w, w} (α := E) (γ := Set E) (Metric.closedBall 0 ‖f‖) ((f : (a : (↑s : Type u)) → E) x : E)

Tactic:
simpa using f.norm_coe_le_norm x

Premises used: BoundedContinuousFunction.norm_coe_le_norm
-- Module: Mathlib.Analysis.Complex.Tietze
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst_2 : RCLike 𝕜
E : Type w
inst_3 : NormedAddCommGroup E
inst_4 : NormedSpace 𝕜 E
inst_5 : FiniteDimensional 𝕜 E
f : BoundedContinuousFunction.{u, w} (↑s : Type u) E
hf : ¬‖f‖ = 0
this : TietzeExtension.{u, w} (↑(Metric.closedBall 0 ‖f‖) : Type w)
⊢ ∀ (x : (↑s : Type u)),
    Membership.mem.{w, w} (α := E) (γ := Set E) (Metric.closedBall 0 ‖f‖) ((f : (a : (↑s : Type u)) → E) x : E)

Tactic:
have hf' x : f x ∈ Metric.closedBall 0 ‖f‖ := by simpa using f.norm_coe_le_norm x