case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), ↑f x ∈ Icc a b
hle : a ≤ b
he : ClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ↑g ∘ e = ↑(f - const X ((a + b) / 2))
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ Icc a b) ∧ ↑g ∘ e = ↑f
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), ↑f x ∈ Icc a b
hle : a ≤ b
he : ClosedEmbedding e
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ Icc a b) ∧ ↑g ∘ e = ↑f
rcases exists_extension_norm_eq_of_closedEmbedding (f - const X ((a + b) / 2)) he with
  ⟨g, hgf, hge⟩
case intro.intro.refine'_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), ↑f x ∈ Icc a b
hle : a ≤ b
he : ClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ↑g ∘ e = ↑(f - const X ((a + b) / 2))
y : Y
⊢ ↑(const Y ((a + b) / 2) + g) y ∈ Icc a b

case intro.intro.refine'_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), ↑f x ∈ Icc a b
hle : a ≤ b
he : ClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ↑g ∘ e = ↑(f - const X ((a + b) / 2))
⊢ ↑(const Y ((a + b) / 2) + g) ∘ e = ↑f
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), ↑f x ∈ Icc a b
hle : a ≤ b
he : ClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ↑g ∘ e = ↑(f - const X ((a + b) / 2))
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ Icc a b) ∧ ↑g ∘ e = ↑f
refine' ⟨const Y ((a + b) / 2) + g, fun y => _, _⟩
case intro.intro.refine'_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), ↑f x ∈ Icc a b
hle : a ≤ b
he : ClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ↑g ∘ e = ↑(f - const X ((a + b) / 2))
y : Y
⊢ ‖f - const X ((a + b) / 2)‖ ≤ (b - a) / 2
case intro.intro.refine'_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), ↑f x ∈ Icc a b
hle : a ≤ b
he : ClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ↑g ∘ e = ↑(f - const X ((a + b) / 2))
y : Y
⊢ ↑(const Y ((a + b) / 2) + g) y ∈ Icc a b
suffices ‖f - const X ((a + b) / 2)‖ ≤ (b - a) / 2 by
  simpa [Real.Icc_eq_closedBall, add_mem_closedBall_iff_norm] using
    (norm_coe_le_norm g y).trans (hgf.trans_le this)
case intro.intro.refine'_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), ↑f x ∈ Icc a b
hle : a ≤ b
he : ClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ↑g ∘ e = ↑(f - const X ((a + b) / 2))
y : Y
x : X
⊢ ‖↑(f - const X ((a + b) / 2)) x‖ ≤ (b - a) / 2
case intro.intro.refine'_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), ↑f x ∈ Icc a b
hle : a ≤ b
he : ClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ↑g ∘ e = ↑(f - const X ((a + b) / 2))
y : Y
⊢ ‖f - const X ((a + b) / 2)‖ ≤ (b - a) / 2
refine' (norm_le <| div_nonneg (sub_nonneg.2 hle) zero_le_two).2 fun x => _
no goals
case intro.intro.refine'_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), ↑f x ∈ Icc a b
hle : a ≤ b
he : ClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ↑g ∘ e = ↑(f - const X ((a + b) / 2))
y : Y
x : X
⊢ ‖↑(f - const X ((a + b) / 2)) x‖ ≤ (b - a) / 2
simpa only [Real.Icc_eq_closedBall] using hf x
no goals
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), ↑f x ∈ Icc a b
hle : a ≤ b
he : ClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ↑g ∘ e = ↑(f - const X ((a + b) / 2))
y : Y
this : ‖f - const X ((a + b) / 2)‖ ≤ (b - a) / 2
⊢ ↑(const Y ((a + b) / 2) + g) y ∈ Icc a b
simpa [Real.Icc_eq_closedBall, add_mem_closedBall_iff_norm] using
  (norm_coe_le_norm g y).trans (hgf.trans_le this)
case intro.intro.refine'_2.h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), ↑f x ∈ Icc a b
hle : a ≤ b
he : ClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ↑g ∘ e = ↑(f - const X ((a + b) / 2))
x : X
⊢ (↑(const Y ((a + b) / 2) + g) ∘ e) x = ↑f x
case intro.intro.refine'_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), ↑f x ∈ Icc a b
hle : a ≤ b
he : ClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ↑g ∘ e = ↑(f - const X ((a + b) / 2))
⊢ ↑(const Y ((a + b) / 2) + g) ∘ e = ↑f
ext x
case intro.intro.refine'_2.h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), ↑f x ∈ Icc a b
hle : a ≤ b
he : ClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ↑g ∘ e = ↑(f - const X ((a + b) / 2))
x : X
this : ↑g (e x) = ↑f x - (a + b) / 2
⊢ (↑(const Y ((a + b) / 2) + g) ∘ e) x = ↑f x
case intro.intro.refine'_2.h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), ↑f x ∈ Icc a b
hle : a ≤ b
he : ClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ↑g ∘ e = ↑(f - const X ((a + b) / 2))
x : X
⊢ (↑(const Y ((a + b) / 2) + g) ∘ e) x = ↑f x
have : g (e x) = f x - (a + b) / 2 := congr_fun hge x
no goals
case intro.intro.refine'_2.h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), ↑f x ∈ Icc a b
hle : a ≤ b
he : ClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ↑g ∘ e = ↑(f - const X ((a + b) / 2))
x : X
this : ↑g (e x) = ↑f x - (a + b) / 2
⊢ (↑(const Y ((a + b) / 2) + g) ∘ e) x = ↑f x
simp [this]