X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
h3 : 0 < 3
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (compContinuous g e) f ≤ 2 / 3 * ‖f‖
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (compContinuous g e) f ≤ 2 / 3 * ‖f‖
have h3 : (0 : ℝ) < 3 := by norm_num1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
h3 : 0 < 3
h23 : 0 < 2 / 3
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (compContinuous g e) f ≤ 2 / 3 * ‖f‖
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
h3 : 0 < 3
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (compContinuous g e) f ≤ 2 / 3 * ‖f‖
have h23 : 0 < (2 / 3 : ℝ) := by norm_num1
case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
e : C(X, Y)
he : ClosedEmbedding ↑e
h3 : 0 < 3
h23 : 0 < 2 / 3
⊢ ∃ g, ‖g‖ ≤ ‖0‖ / 3 ∧ dist (compContinuous g 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 : ClosedEmbedding ↑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : f ≠ 0
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (compContinuous g e) f ≤ 2 / 3 * ‖f‖
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
h3 : 0 < 3
h23 : 0 < 2 / 3
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (compContinuous g e) f ≤ 2 / 3 * ‖f‖
rcases eq_or_ne f 0 with (rfl | hf)
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 : ClosedEmbedding ↑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (compContinuous g e) f ≤ 2 / 3 * ‖f‖
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 : ClosedEmbedding ↑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : f ≠ 0
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (compContinuous g e) f ≤ 2 / 3 * ‖f‖
replace hf : 0 < ‖f‖ := norm_pos_iff.2 hf
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 : ClosedEmbedding ↑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (compContinuous g e) f ≤ 2 / 3 * ‖f‖
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 : ClosedEmbedding ↑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (compContinuous g e) f ≤ 2 / 3 * ‖f‖
have hf3 : -‖f‖ / 3 < ‖f‖ / 3 := (div_lt_div_right h3).2 (Left.neg_lt_self hf)
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 : ClosedEmbedding ↑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed (↑e '' (↑f ⁻¹' Iic (-‖f‖ / 3)))
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (compContinuous g e) f ≤ 2 / 3 * ‖f‖
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 : ClosedEmbedding ↑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (compContinuous g e) f ≤ 2 / 3 * ‖f‖
have hc₁ : IsClosed (e '' (f ⁻¹' Iic (-‖f‖ / 3))) :=
  he.isClosedMap _ (isClosed_Iic.preimage f.continuous)
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 : ClosedEmbedding ↑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)))
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (compContinuous g e) f ≤ 2 / 3 * ‖f‖
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 : ClosedEmbedding ↑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed (↑e '' (↑f ⁻¹' Iic (-‖f‖ / 3)))
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (compContinuous g e) f ≤ 2 / 3 * ‖f‖
have hc₂ : IsClosed (e '' (f ⁻¹' Ici (‖f‖ / 3))) :=
  he.isClosedMap _ (isClosed_Ici.preimage f.continuous)
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 : ClosedEmbedding ↑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, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (compContinuous g e) f ≤ 2 / 3 * ‖f‖
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 : ClosedEmbedding ↑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)))
⊢ ∃ g, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (compContinuous g e) f ≤ 2 / 3 * ‖f‖
have hd : Disjoint (e '' (f ⁻¹' Iic (-‖f‖ / 3))) (e '' (f ⁻¹' Ici (‖f‖ / 3))) := by
  refine' disjoint_image_of_injective he.inj (Disjoint.preimage _ _)
  rwa [Iic_disjoint_Ici, not_le]
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 : ClosedEmbedding ↑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 (compContinuous g e) f ≤ 2 / 3 * ‖f‖
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 : ClosedEmbedding ↑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, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (compContinuous g e) f ≤ 2 / 3 * ‖f‖
rcases exists_bounded_mem_Icc_of_closed_of_le hc₁ hc₂ hd hf3.le with ⟨g, hg₁, hg₂, hgf⟩
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 : ClosedEmbedding ↑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 : ClosedEmbedding ↑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 (compContinuous g e) f ≤ 2 / 3 * ‖f‖
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 : ClosedEmbedding ↑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 (compContinuous g e) f ≤ 2 / 3 * ‖f‖
refine' ⟨g, _, _⟩
no goals
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
⊢ 0 < 3
norm_num1
no goals
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
h3 : 0 < 3
⊢ 0 < 2 / 3
norm_num1
case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
e : C(X, Y)
he : ClosedEmbedding ↑e
h3 : 0 < 3
h23 : 0 < 2 / 3
⊢ ‖0‖ ≤ ‖0‖ / 3 ∧ dist (compContinuous 0 e) 0 ≤ 2 / 3 * ‖0‖
case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
e : C(X, Y)
he : ClosedEmbedding ↑e
h3 : 0 < 3
h23 : 0 < 2 / 3
⊢ ∃ g, ‖g‖ ≤ ‖0‖ / 3 ∧ dist (compContinuous g e) 0 ≤ 2 / 3 * ‖0‖
use 0
no goals
case inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
e : C(X, Y)
he : ClosedEmbedding ↑e
h3 : 0 < 3
h23 : 0 < 2 / 3
⊢ ‖0‖ ≤ ‖0‖ / 3 ∧ dist (compContinuous 0 e) 0 ≤ 2 / 3 * ‖0‖
simp
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑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)))
⊢ Disjoint (Iic (-‖f‖ / 3)) (Ici (‖f‖ / 3))
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑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)))
⊢ Disjoint (↑e '' (↑f ⁻¹' Iic (-‖f‖ / 3))) (↑e '' (↑f ⁻¹' Ici (‖f‖ / 3)))
refine' disjoint_image_of_injective he.inj (Disjoint.preimage _ _)
no goals
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑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)))
⊢ Disjoint (Iic (-‖f‖ / 3)) (Ici (‖f‖ / 3))
rwa [Iic_disjoint_Ici, not_le]
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 : ClosedEmbedding ↑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
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 : ClosedEmbedding ↑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
refine' (norm_le <| div_nonneg hf.le h3.le).mpr fun y => _
no goals
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 : ClosedEmbedding ↑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
simpa [abs_le, neg_div] using hgf y
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 : ClosedEmbedding ↑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 (↑(compContinuous g e) x) (↑f x) ≤ 2 / 3 * ‖f‖
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 : ClosedEmbedding ↑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 (compContinuous g e) f ≤ 2 / 3 * ‖f‖
refine' (dist_le <| mul_nonneg h23.le hf.le).mpr fun x => _
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 : ClosedEmbedding ↑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 (↑(compContinuous g e) x) (↑f x) ≤ 2 / 3 * ‖f‖
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 : ClosedEmbedding ↑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 (↑(compContinuous g e) x) (↑f x) ≤ 2 / 3 * ‖f‖
have hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖ := by
  simpa only [Real.norm_eq_abs, abs_le] using f.norm_coe_le_norm x
case inr.intro.intro.intro.refine'_2.inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑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‖
hle₁ : ↑f x ≤ -‖f‖ / 3
⊢ dist (↑(compContinuous g e) x) (↑f x) ≤ 2 / 3 * ‖f‖

case inr.intro.intro.intro.refine'_2.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 : ClosedEmbedding ↑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‖
hle₁ : -‖f‖ / 3 ≤ ↑f x
⊢ dist (↑(compContinuous g e) x) (↑f x) ≤ 2 / 3 * ‖f‖
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 : ClosedEmbedding ↑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 (↑(compContinuous g e) x) (↑f x) ≤ 2 / 3 * ‖f‖
cases' le_total (f x) (-‖f‖ / 3) with hle₁ hle₁
no goals
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑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‖
simpa only [Real.norm_eq_abs, abs_le] using f.norm_coe_le_norm x
no goals
case inr.intro.intro.intro.refine'_2.inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑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‖
hle₁ : ↑f x ≤ -‖f‖ / 3
⊢ dist (↑(compContinuous g e) x) (↑f x) ≤ 2 / 3 * ‖f‖
calc
  |g (e x) - f x| = -‖f‖ / 3 - f x := by
    rw [hg₁ (mem_image_of_mem _ hle₁), Function.const_apply,
      abs_of_nonneg (sub_nonneg.2 hle₁)]
  _ ≤ 2 / 3 * ‖f‖ := by linarith
no goals
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑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‖
hle₁ : ↑f x ≤ -‖f‖ / 3
⊢ abs (↑g (↑e x) - ↑f x) = -‖f‖ / 3 - ↑f x
rw [hg₁ (mem_image_of_mem _ hle₁), Function.const_apply,
  abs_of_nonneg (sub_nonneg.2 hle₁)]
no goals
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑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‖
hle₁ : ↑f x ≤ -‖f‖ / 3
⊢ -‖f‖ / 3 - ↑f x ≤ 2 / 3 * ‖f‖
linarith
case inr.intro.intro.intro.refine'_2.inr.inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑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‖
hle₁ : -‖f‖ / 3 ≤ ↑f x
hle₂ : ↑f x ≤ ‖f‖ / 3
⊢ dist (↑(compContinuous g e) x) (↑f x) ≤ 2 / 3 * ‖f‖

case inr.intro.intro.intro.refine'_2.inr.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 : ClosedEmbedding ↑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‖
hle₁ : -‖f‖ / 3 ≤ ↑f x
hle₂ : ‖f‖ / 3 ≤ ↑f x
⊢ dist (↑(compContinuous g e) x) (↑f x) ≤ 2 / 3 * ‖f‖
case inr.intro.intro.intro.refine'_2.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 : ClosedEmbedding ↑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‖
hle₁ : -‖f‖ / 3 ≤ ↑f x
⊢ dist (↑(compContinuous g e) x) (↑f x) ≤ 2 / 3 * ‖f‖
cases' le_total (f x) (‖f‖ / 3) with hle₂ hle₂
case inr.intro.intro.intro.refine'_2.inr.inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
g : Y →ᵇ ℝ
x : X
hfx : -‖f‖ ≤ ↑f x ∧ ↑f x ≤ ‖f‖
hle₂ : ↑f x ≤ ‖f‖ / 3
hf3 : -(‖f‖ / 3) < ‖f‖ / 3
hc₁ : IsClosed ((fun a => ↑e a) '' (↑f ⁻¹' Iic (-(‖f‖ / 3))))
hc₂ : IsClosed ((fun a => ↑e a) '' (↑f ⁻¹' Ici (‖f‖ / 3)))
hd : Disjoint ((fun a => ↑e a) '' (↑f ⁻¹' Iic (-(‖f‖ / 3)))) ((fun a => ↑e a) '' (↑f ⁻¹' Ici (‖f‖ / 3)))
hg₁ : EqOn (↑g) (Function.const Y (-(‖f‖ / 3))) ((fun a => ↑e a) '' (↑f ⁻¹' Iic (-(‖f‖ / 3))))
hg₂ : EqOn (↑g) (Function.const Y (‖f‖ / 3)) ((fun a => ↑e a) '' (↑f ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), ↑g x ∈ Icc (-(‖f‖ / 3)) (‖f‖ / 3)
hle₁ : -(‖f‖ / 3) ≤ ↑f x
⊢ dist (↑(compContinuous g e) x) (↑f x) ≤ 2 / 3 * ‖f‖
case inr.intro.intro.intro.refine'_2.inr.inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑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‖
hle₁ : -‖f‖ / 3 ≤ ↑f x
hle₂ : ↑f x ≤ ‖f‖ / 3
⊢ dist (↑(compContinuous g e) x) (↑f x) ≤ 2 / 3 * ‖f‖
simp only [neg_div] at *
no goals
case inr.intro.intro.intro.refine'_2.inr.inl
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
g : Y →ᵇ ℝ
x : X
hfx : -‖f‖ ≤ ↑f x ∧ ↑f x ≤ ‖f‖
hle₂ : ↑f x ≤ ‖f‖ / 3
hf3 : -(‖f‖ / 3) < ‖f‖ / 3
hc₁ : IsClosed ((fun a => ↑e a) '' (↑f ⁻¹' Iic (-(‖f‖ / 3))))
hc₂ : IsClosed ((fun a => ↑e a) '' (↑f ⁻¹' Ici (‖f‖ / 3)))
hd : Disjoint ((fun a => ↑e a) '' (↑f ⁻¹' Iic (-(‖f‖ / 3)))) ((fun a => ↑e a) '' (↑f ⁻¹' Ici (‖f‖ / 3)))
hg₁ : EqOn (↑g) (Function.const Y (-(‖f‖ / 3))) ((fun a => ↑e a) '' (↑f ⁻¹' Iic (-(‖f‖ / 3))))
hg₂ : EqOn (↑g) (Function.const Y (‖f‖ / 3)) ((fun a => ↑e a) '' (↑f ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), ↑g x ∈ Icc (-(‖f‖ / 3)) (‖f‖ / 3)
hle₁ : -(‖f‖ / 3) ≤ ↑f x
⊢ dist (↑(compContinuous g e) x) (↑f x) ≤ 2 / 3 * ‖f‖
calc
  dist (g (e x)) (f x) ≤ |g (e x)| + |f x| := dist_le_norm_add_norm _ _
  _ ≤ ‖f‖ / 3 + ‖f‖ / 3 := (add_le_add (abs_le.2 <| hgf _) (abs_le.2 ⟨hle₁, hle₂⟩))
  _ = 2 / 3 * ‖f‖ := by linarith
no goals
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
g : Y →ᵇ ℝ
x : X
hfx : -‖f‖ ≤ ↑f x ∧ ↑f x ≤ ‖f‖
hle₂ : ↑f x ≤ ‖f‖ / 3
hf3 : -(‖f‖ / 3) < ‖f‖ / 3
hc₁ : IsClosed ((fun a => ↑e a) '' (↑f ⁻¹' Iic (-(‖f‖ / 3))))
hc₂ : IsClosed ((fun a => ↑e a) '' (↑f ⁻¹' Ici (‖f‖ / 3)))
hd : Disjoint ((fun a => ↑e a) '' (↑f ⁻¹' Iic (-(‖f‖ / 3)))) ((fun a => ↑e a) '' (↑f ⁻¹' Ici (‖f‖ / 3)))
hg₁ : EqOn (↑g) (Function.const Y (-(‖f‖ / 3))) ((fun a => ↑e a) '' (↑f ⁻¹' Iic (-(‖f‖ / 3))))
hg₂ : EqOn (↑g) (Function.const Y (‖f‖ / 3)) ((fun a => ↑e a) '' (↑f ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), ↑g x ∈ Icc (-(‖f‖ / 3)) (‖f‖ / 3)
hle₁ : -(‖f‖ / 3) ≤ ↑f x
⊢ ‖f‖ / 3 + ‖f‖ / 3 = 2 / 3 * ‖f‖
linarith
no goals
case inr.intro.intro.intro.refine'_2.inr.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 : ClosedEmbedding ↑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‖
hle₁ : -‖f‖ / 3 ≤ ↑f x
hle₂ : ‖f‖ / 3 ≤ ↑f x
⊢ dist (↑(compContinuous g e) x) (↑f x) ≤ 2 / 3 * ‖f‖
calc
  |g (e x) - f x| = f x - ‖f‖ / 3 := by
    rw [hg₂ (mem_image_of_mem _ hle₂), abs_sub_comm, Function.const_apply,
      abs_of_nonneg (sub_nonneg.2 hle₂)]
  _ ≤ 2 / 3 * ‖f‖ := by linarith
no goals
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑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‖
hle₁ : -‖f‖ / 3 ≤ ↑f x
hle₂ : ‖f‖ / 3 ≤ ↑f x
⊢ abs (↑g (↑e x) - ↑f x) = ↑f x - ‖f‖ / 3
rw [hg₂ (mem_image_of_mem _ hle₂), abs_sub_comm, Function.const_apply,
  abs_of_nonneg (sub_nonneg.2 hle₂)]
no goals
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : ClosedEmbedding ↑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‖
hle₁ : -‖f‖ / 3 ≤ ↑f x
hle₂ : ‖f‖ / 3 ≤ ↑f x
⊢ ↑f x - ‖f‖ / 3 ≤ 2 / 3 * ‖f‖
linarith