-- Mathlib/Topology/TietzeExtension.lean
theorem tietze_extension_step (f : X →ᵇ ℝ) (e : C(X, Y)) (he : IsClosedEmbedding e) :
    ∃ g : Y →ᵇ ℝ, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖

Proof state:
case inr.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hd : Disjoint (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3))) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖

Tactic:
refine ⟨g, ?_, ?_⟩

Result:
case inr.intro.intro.intro.refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hd : Disjoint (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3))) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
⊢ ‖g‖ ≤ ‖f‖ / 3

case inr.intro.intro.intro.refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hd : Disjoint (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3))) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
⊢ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖

Proof state:
case inr.intro.intro.intro.refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hd : Disjoint (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3))) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
⊢ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖

Tactic:
refine (dist_le <| mul_nonneg h23.le hf.le).mpr fun x => ?_

Result:
case inr.intro.intro.intro.refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hd : Disjoint (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3))) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
x : X
⊢ dist ((g.compContinuous e) x) (f x) ≤ 2 / 3 * ‖f‖

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hd : Disjoint (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3))) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
x : X
⊢ -‖f‖ ≤ f x ∧ f x ≤ ‖f‖

Tactic:
simpa only [Real.norm_eq_abs, abs_le] using f.norm_coe_le_norm x

Result:
no goals

Proof state:
case inr.intro.intro.intro.refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hd : Disjoint (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3))) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
y : Y
⊢ ‖g y‖ ≤ ‖f‖ / 3

Tactic:
simpa [abs_le, neg_div] using hgf y

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖

Tactic:
rcases eq_or_ne f 0 with (rfl | hf)

Result:
case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
⊢ ∃ g, ‖g‖ ≤ ‖0‖ / 3 ∧ dist (g.compContinuous e) 0 ≤ 2 / 3 * ‖0‖

case inr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : f ≠ 0
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖

Proof state:
case inr.intro.intro.intro.refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hd : Disjoint (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3))) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
x : X
⊢ dist ((g.compContinuous e) x) (f x) ≤ 2 / 3 * ‖f‖

Tactic:
have hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖ := by
  simpa only [Real.norm_eq_abs, abs_le] using f.norm_coe_le_norm x

Result:
case inr.intro.intro.intro.refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hd : Disjoint (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3))) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
x : X
hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖
⊢ dist ((g.compContinuous e) x) (f x) ≤ 2 / 3 * ‖f‖