awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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
⊢ Membership.mem (γ := Set E) (Metric.closedBall 0 1) (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g x)
have 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)
Tactic: by_cases hx : x ∈ Metric.closedBall 0 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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)
⊢ Membership.mem (γ := Set E) (Metric.closedBall 0 1) (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g x)
have 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)
Tactic: by_cases hx : x ∈ Metric.closedBall 0 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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
⊢ Membership.mem (γ := Set E) (Metric.closedBall 0 1) (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g x)
have neg : Membership.mem (γ := Set E) (Metric.closedBall 0 1) (HSMul.hSMul.{v, w, w} (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) x)
Tactic: simp only [g, piecewise_eq_of_notMem (hi := hx), RCLike.real_smul_eq_coe_smul (K := 𝕜)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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
⊢ Membership.mem (γ := Set E) (Metric.closedBall 0 1) (HSMul.hSMul.{v, w, w} (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) x)
have pos : ∀ (hx' : x = 0), Membership.mem (γ := Set E) (Metric.closedBall 0 1) (HSMul.hSMul.{v, w, w} (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) x)
Tactic: by_cases hx' : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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)
⊢ Membership.mem (γ := Set E) (Metric.closedBall 0 1) (HSMul.hSMul.{v, w, w} (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) x)
have neg : ∀ (hx' : ¬x = 0), Membership.mem (γ := Set E) (Metric.closedBall 0 1) (HSMul.hSMul.{v, w, w} (α := 𝕜) (↑‖x‖⁻¹ : 𝕜) x)
Tactic: by_cases hx' : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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)
⊢ 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))
have 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) sorry,
                continuous_toFun := sorry : 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 := sorry } :
            (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: ext x
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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
⊢ TietzeExtension.{u, w} (↑(Metric.closedBall 0 1) : Type w)
have suffices : Continuous (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g)
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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)
have refine_1 : ∀ (x : E) (hx : Membership.mem (γ := Set E) (frontier (Metric.closedBall 0 1)) x), id x = g x
Tactic: refine continuous_piecewise (fun x hx ↦ ?_) continuousOn_id ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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
⊢ Continuous (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g)
have refine_2 : ContinuousOn g (closure (Metric.closedBall 0 1)ᶜ)
Tactic: refine continuous_piecewise (fun x hx ↦ ?_) continuousOn_id ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (hypothesis)
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
⊢ id x = g x
have hx₁ : ‖x‖ = 1
Tactic: replace hx : ‖x‖ = 1 := by simpa [frontier_closedBall (0 : E) one_ne_zero] using hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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)ᶜ)
have refine_2 : ∀ (x : E), Membership.mem (γ := Set E) (closure (Metric.closedBall 0 1)ᶜ) x → ‖id x‖ ≠ 0
Tactic: refine continuousOn_id.norm.inv₀ ?_ |>.smul continuousOn_id
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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), Membership.mem (γ := Set E) (closure (Metric.closedBall 0 1)ᶜ) x → ‖id x‖ ≠ 0
have refine_2 : ∀ (x : E), 1 ≤ ‖x‖ → ¬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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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
⊢ TietzeExtension.{u, w} (↑(Metric.closedBall 0 1) : Type w)
have suffices : Continuous (piecewise (β := fun (a : E) ↦ E) (Metric.closedBall 0 1) id g)
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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)
⊢ TietzeExtension.{u, w} (↑(Metric.closedBall 0 1) : Type w)
have refine_1 : ∀ (x : E) (hx : Membership.mem (γ := Set E) (frontier (Metric.closedBall 0 1)) x), id x = g x
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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
⊢ TietzeExtension.{u, w} (↑(Metric.closedBall 0 1) : Type w)
have refine_2 : ContinuousOn g (closure (Metric.closedBall 0 1)ᶜ)
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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
⊢ (↑(closedBall y r) : Type w) ≃ₜ (↑(closedBall 0 1) : Type w)
have symm : (↑(closedBall 0 1) : Type w) ≃ₜ (↑(closedBall y r) : Type w)
Tactic: symm
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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
⊢ (↑(closedBall 0 1) : Type w) ≃ₜ (↑(closedBall y r) : Type w)
have apply : Eq (α := Set E) (closedBall 0 1)
  ((⇑(DilationEquiv.toHomeomorph (DilationEquiv.smulTorsor.{v, w, w} (𝕜 := 𝕜) y (k := (↑r : 𝕜)) sorry)) : (a : E) → E) ⁻¹'
    closedBall y r)
Tactic: apply (DilationEquiv.smulTorsor y (k := (r : 𝕜)) <| by exact_mod_cast hr.ne').toHomeomorph.sets
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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
⊢ Eq (α := Set E) (closedBall 0 1)
    ((⇑(DilationEquiv.toHomeomorph (DilationEquiv.smulTorsor.{v, w, w} (𝕜 := 𝕜) y (k := (↑r : 𝕜)) ⋯)) : (a : E) → E) ⁻¹'
      closedBall y r)
have 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 : 𝕜)) sorry)) :
          (a : E) → E) ⁻¹'
        closedBall y r)
      x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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
⊢ 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
have h : ‖x‖ ≤ 1 ↔ r * ‖x‖ ≤ 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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
Goal:
⊢ TietzeExtension (↑I : Type)
have rw : TietzeExtension (↑(Metric.closedBall 2⁻¹ 2⁻¹) : Type)
Tactic: rw [unitInterval.eq_closedBall]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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
⊢ ∃ (g : X →ᵇ E), ‖g‖ = ‖f‖ ∧ g.restrict s = f
have pos : ∀ (hf : ‖f‖ = 0), ∃ (g : X →ᵇ E), ‖g‖ = ‖f‖ ∧ g.restrict s = f
Tactic: by_cases hf : ‖f‖ = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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
⊢ ∃ (g : X →ᵇ E), ‖g‖ = ‖f‖ ∧ g.restrict s = f
have neg : ∀ (hf : ¬‖f‖ = 0), ∃ (g : X →ᵇ E), ‖g‖ = ‖f‖ ∧ g.restrict s = f
Tactic: by_cases hf : ‖f‖ = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (hypothesis)
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
have this : TietzeExtension.{u, w} (↑(Metric.closedBall 0 ‖f‖) : Type w)
Tactic: have := Metric.instTietzeExtensionClosedBall.{u, v} 𝕜 (0 : E) (by simp_all : 0 < ‖f‖)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (hypothesis)
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)
⊢ ∃ (g : X →ᵇ E), ‖g‖ = ‖f‖ ∧ g.restrict s = f
have hf' : ∀ (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
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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)
hf' :
  ∀ (x : (↑s : Type u)),
    Membership.mem.{w, w} (α := E) (γ := Set E) (Metric.closedBall 0 ‖f‖) ((f : (a : (↑s : Type u)) → E) x : E)
⊢ ∃ (g : X →ᵇ E), ‖g‖ = ‖f‖ ∧ g.restrict s = f
have neg : ∀ (g : C(X, E))
  (hg_mem : ∀ (x : X), Membership.mem.{w, w} (α := E) (γ := Set E) (Metric.closedBall 0 ‖f‖) ((g : (a : X) → E) x : E))
  (hg : ContinuousMap.restrict s g = (↑f : C((↑s : Type u), E))), ∃ (g : X →ᵇ E), ‖g‖ = ‖f‖ ∧ g.restrict s = f
Tactic: obtain ⟨g, hg_mem, hg⟩ := (f : C(s, E)).exists_forall_mem_restrict_eq hs hf'
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (hypothesis)
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)
hf' :
  ∀ (x : (↑s : Type u)),
    Membership.mem.{w, w} (α := E) (γ := Set E) (Metric.closedBall 0 ‖f‖) ((f : (a : (↑s : Type u)) → E) x : E)
g : C(X, E)
hg_mem : ∀ (x : X), Membership.mem.{w, w} (α := E) (γ := Set E) (Metric.closedBall 0 ‖f‖) ((g : (a : X) → E) x : E)
hg : ContinuousMap.restrict s g = (↑f : C((↑s : Type u), E))
⊢ ∃ (g : X →ᵇ E), ‖g‖ = ‖f‖ ∧ g.restrict s = f
have hg_mem₁ : ∀ (x : X), norm.{w} (E := E) ((g : (a : X) → E) x : E) ≤ ‖f‖
Tactic: simp only [Metric.mem_closedBall, dist_zero_right] at hg_mem
Cleared hypotheses: hg_mem
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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)
hf' :
  ∀ (x : (↑s : Type u)),
    Membership.mem.{w, w} (α := E) (γ := Set E) (Metric.closedBall 0 ‖f‖) ((f : (a : (↑s : Type u)) → E) x : E)
g : C(X, E)
hg : ContinuousMap.restrict s g = (↑f : C((↑s : Type u), E))
hg_mem : ∀ (x : X), norm.{w} (E := E) ((g : (a : X) → E) x : E) ≤ ‖f‖
g' : X →ᵇ E := ofNormedAddCommGroup (⇑g : (a : X) → E) ⋯ ‖f‖ hg_mem
⊢ g'.restrict s = f
have h : ∀ (x : (↑s : Type u)),
  Eq.{w + 1} (α := E) ((g'.restrict s : (a : (↑s : Type u)) → E) x : E) ((f : (a : (↑s : Type u)) → E) x : E)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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)
hf' :
  ∀ (x : (↑s : Type u)),
    Membership.mem.{w, w} (α := E) (γ := Set E) (Metric.closedBall 0 ‖f‖) ((f : (a : (↑s : Type u)) → E) x : E)
g : C(X, E)
hg : ContinuousMap.restrict s g = (↑f : C((↑s : Type u), E))
hg_mem : ∀ (x : X), norm.{w} (E := E) ((g : (a : X) → E) x : E) ≤ ‖f‖
g' : X →ᵇ E := ofNormedAddCommGroup (⇑g : (a : X) → E) ⋯ ‖f‖ hg_mem
⊢ ∃ (g : X →ᵇ E), ‖g‖ = ‖f‖ ∧ g.restrict s = f
have neg : ‖g'‖ = ‖f‖
Tactic: refine ⟨g', ?_, by ext x; congrm($(hg) x)⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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)
hf' :
  ∀ (x : (↑s : Type u)),
    Membership.mem.{w, w} (α := E) (γ := Set E) (Metric.closedBall 0 ‖f‖) ((f : (a : (↑s : Type u)) → E) x : E)
g : C(X, E)
hg : ContinuousMap.restrict s g = (↑f : C((↑s : Type u), E))
hg_mem : ∀ (x : X), norm.{w} (E := E) ((g : (a : X) → E) x : E) ≤ ‖f‖
g' : X →ᵇ E := ofNormedAddCommGroup (⇑g : (a : X) → E) ⋯ ‖f‖ hg_mem
⊢ ‖g'‖ = ‖f‖
have neg : ‖f‖ ≤ ‖g'‖
Tactic: apply le_antisymm ((g'.norm_le <| by positivity).mpr hg_mem)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Tietze (goal)
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)
hf' :
  ∀ (x : (↑s : Type u)),
    Membership.mem.{w, w} (α := E) (γ := Set E) (Metric.closedBall 0 ‖f‖) ((f : (a : (↑s : Type u)) → E) x : E)
g : C(X, E)
hg : ContinuousMap.restrict s g = (↑f : C((↑s : Type u), E))
hg_mem : ∀ (x : X), norm.{w} (E := E) ((g : (a : X) → E) x : E) ≤ ‖f‖
g' : X →ᵇ E := ofNormedAddCommGroup (⇑g : (a : X) → E) ⋯ ‖f‖ hg_mem
⊢ ‖f‖ ≤ ‖g'‖
have neg : ∀ (x : (↑s : Type u)), norm.{w} (E := E) ((f : (a : (↑s : Type u)) → E) x : E) ≤ ‖g'‖
Tactic: refine (f.norm_le <| by positivity).mpr fun x ↦ ?_