case intro.intro
X : Type ?u.107579
Y : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
s : Set Y
f : ↑s →ᵇ ℝ
hs : IsClosed s
t : Set ℝ
inst✝ : OrdConnected t
hf : ∀ (x : ↑s), ↑f x ∈ t
hne : Set.Nonempty t
g : Y →ᵇ ℝ
hg : ∀ (y : Y), ↑g y ∈ t
hgf : ↑g ∘ Subtype.val = ↑f
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ restrict g s = f
X : Type ?u.107579
Y : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
s : Set Y
f : ↑s →ᵇ ℝ
hs : IsClosed s
t : Set ℝ
inst✝ : OrdConnected t
hf : ∀ (x : ↑s), ↑f x ∈ t
hne : Set.Nonempty t
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ restrict g s = f
rcases exists_extension_forall_mem_of_closedEmbedding f hf hne
    (closedEmbedding_subtype_val hs) with
  ⟨g, hg, hgf⟩
no goals
case intro.intro
X : Type ?u.107579
Y : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
s : Set Y
f : ↑s →ᵇ ℝ
hs : IsClosed s
t : Set ℝ
inst✝ : OrdConnected t
hf : ∀ (x : ↑s), ↑f x ∈ t
hne : Set.Nonempty t
g : Y →ᵇ ℝ
hg : ∀ (y : Y), ↑g y ∈ t
hgf : ↑g ∘ Subtype.val = ↑f
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ restrict g s = f
exact ⟨g, hg, FunLike.coe_injective hgf⟩