X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
have h : ℝ ≃o Ioo (-1 : ℝ) 1 := orderIsoIooNegOneOne ℝ
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
let F : X →ᵇ ℝ :=
  { toFun := (↑) ∘ h ∘ f
    continuous_toFun := continuous_subtype_val.comp (h.continuous.comp f.continuous)
    map_bounded' :=
      bounded_range_iff.1
        ((bounded_Ioo (-1 : ℝ) 1).mono <| forall_range_iff.2 fun x => (h (f x)).2) }
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
let t' : Set ℝ := (↑) ∘ h '' t
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
have ht_sub : t' ⊆ Ioo (-1 : ℝ) 1 := image_subset_iff.2 fun x _ => (h x).2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : OrdConnected t'
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
have : OrdConnected t' := by
  constructor
  rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ z hz
  lift z to Ioo (-1 : ℝ) 1 using Icc_subset_Ioo (h x).2.1 (h y).2.2 hz
  change z ∈ Icc (h x) (h y) at hz
  rw [← h.image_Icc] at hz
  rcases hz with ⟨z, hz, rfl⟩
  exact ⟨z, hs.out hx hy hz, rfl⟩
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : OrdConnected t'
hFt : ∀ (x : X), ↑F x ∈ t'
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : OrdConnected t'
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
have hFt : ∀ x, F x ∈ t' := fun x => mem_image_of_mem _ (hf x)
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : OrdConnected t'
hFt : ∀ (x : X), ↑F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), ↑G y ∈ t'
hGF : ↑G ∘ e = ↑F
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : OrdConnected t'
hFt : ∀ (x : X), ↑F x ∈ t'
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
rcases F.exists_extension_forall_mem_of_closedEmbedding hFt (hne.image _) he with ⟨G, hG, hGF⟩
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : OrdConnected t'
hFt : ∀ (x : X), ↑F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), ↑G y ∈ t'
hGF : ↑G ∘ e = ↑F
g : C(Y, ℝ) := mk (↑(OrderIso.symm h) ∘ Set.codRestrict (↑G) (Ioo (-1) 1) (_ : ∀ (y : Y), ↑G y ∈ Ioo (-1) 1))
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : OrdConnected t'
hFt : ∀ (x : X), ↑F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), ↑G y ∈ t'
hGF : ↑G ∘ e = ↑F
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
let g : C(Y, ℝ) :=
  ⟨h.symm ∘ codRestrict G _ fun y => ht_sub (hG y),
    h.symm.continuous.comp <| G.continuous.subtype_mk _⟩
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : OrdConnected t'
hFt : ∀ (x : X), ↑F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), ↑G y ∈ t'
hGF : ↑G ∘ e = ↑F
g : C(Y, ℝ) := mk (↑(OrderIso.symm h) ∘ Set.codRestrict (↑G) (Ioo (-1) 1) (_ : ∀ (y : Y), ↑G y ∈ Ioo (-1) 1))
hgG : ∀ {y : Y} {a : (fun x => ℝ) y}, ↑g y = a ↔ ↑G y = ↑(↑h a)
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : OrdConnected t'
hFt : ∀ (x : X), ↑F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), ↑G y ∈ t'
hGF : ↑G ∘ e = ↑F
g : C(Y, ℝ) := mk (↑(OrderIso.symm h) ∘ Set.codRestrict (↑G) (Ioo (-1) 1) (_ : ∀ (y : Y), ↑G y ∈ Ioo (-1) 1))
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
have hgG : ∀ {y a}, g y = a ↔ G y = h a := @fun y a =>
  h.toEquiv.symm_apply_eq.trans Subtype.ext_iff
case intro.intro.refine'_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : OrdConnected t'
hFt : ∀ (x : X), ↑F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), ↑G y ∈ t'
hGF : ↑G ∘ e = ↑F
g : C(Y, ℝ) := mk (↑(OrderIso.symm h) ∘ Set.codRestrict (↑G) (Ioo (-1) 1) (_ : ∀ (y : Y), ↑G y ∈ Ioo (-1) 1))
hgG : ∀ {y : Y} {a : (fun x => ℝ) y}, ↑g y = a ↔ ↑G y = ↑(↑h a)
y : Y
⊢ ↑g y ∈ t

case intro.intro.refine'_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : OrdConnected t'
hFt : ∀ (x : X), ↑F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), ↑G y ∈ t'
hGF : ↑G ∘ e = ↑F
g : C(Y, ℝ) := mk (↑(OrderIso.symm h) ∘ Set.codRestrict (↑G) (Ioo (-1) 1) (_ : ∀ (y : Y), ↑G y ∈ Ioo (-1) 1))
hgG : ∀ {y : Y} {a : (fun x => ℝ) y}, ↑g y = a ↔ ↑G y = ↑(↑h a)
⊢ ↑g ∘ e = ↑f
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : OrdConnected t'
hFt : ∀ (x : X), ↑F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), ↑G y ∈ t'
hGF : ↑G ∘ e = ↑F
g : C(Y, ℝ) := mk (↑(OrderIso.symm h) ∘ Set.codRestrict (↑G) (Ioo (-1) 1) (_ : ∀ (y : Y), ↑G y ∈ Ioo (-1) 1))
hgG : ∀ {y : Y} {a : (fun x => ℝ) y}, ↑g y = a ↔ ↑G y = ↑(↑h a)
⊢ ∃ g, (∀ (y : Y), ↑g y ∈ t) ∧ ↑g ∘ e = ↑f
refine' ⟨g, fun y => _, _⟩
case out'
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
⊢ ∀ ⦃x : ℝ⦄, x ∈ t' → ∀ ⦃y : ℝ⦄, y ∈ t' → Icc x y ⊆ t'
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
⊢ OrdConnected t'
constructor
case out'.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : ℝ
hz : z ∈ Icc ((Subtype.val ∘ ↑h) x) ((Subtype.val ∘ ↑h) y)
⊢ z ∈ t'
case out'
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
⊢ ∀ ⦃x : ℝ⦄, x ∈ t' → ∀ ⦃y : ℝ⦄, y ∈ t' → Icc x y ⊆ t'
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ z hz
case out'.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : { x // x ∈ Ioo (-1) 1 }
hz : ↑z ∈ Icc ((Subtype.val ∘ ↑h) x) ((Subtype.val ∘ ↑h) y)
⊢ ↑z ∈ t'
case out'.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : ℝ
hz : z ∈ Icc ((Subtype.val ∘ ↑h) x) ((Subtype.val ∘ ↑h) y)
⊢ z ∈ t'
lift z to Ioo (-1 : ℝ) 1 using Icc_subset_Ioo (h x).2.1 (h y).2.2 hz
case out'.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : { x // x ∈ Ioo (-1) 1 }
hz : z ∈ Icc (↑h x) (↑h y)
⊢ ↑z ∈ t'
case out'.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : { x // x ∈ Ioo (-1) 1 }
hz : ↑z ∈ Icc ((Subtype.val ∘ ↑h) x) ((Subtype.val ∘ ↑h) y)
⊢ ↑z ∈ t'
change z ∈ Icc (h x) (h y) at hz
case out'.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : { x // x ∈ Ioo (-1) 1 }
hz : z ∈ ↑h '' Icc x y
⊢ ↑z ∈ t'
case out'.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : { x // x ∈ Ioo (-1) 1 }
hz : z ∈ Icc (↑h x) (↑h y)
⊢ ↑z ∈ t'
rw [← h.image_Icc] at hz
case out'.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : ℝ
hz : z ∈ Icc x y
⊢ ↑(↑h z) ∈ t'
case out'.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : { x // x ∈ Ioo (-1) 1 }
hz : z ∈ ↑h '' Icc x y
⊢ ↑z ∈ t'
rcases hz with ⟨z, hz, rfl⟩
no goals
case out'.intro.intro.intro.intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : ℝ
hz : z ∈ Icc x y
⊢ ↑(↑h z) ∈ t'
exact ⟨z, hs.out hx hy hz, rfl⟩
case intro.intro.refine'_1.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : OrdConnected t'
hFt : ∀ (x : X), ↑F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), ↑G y ∈ t'
hGF : ↑G ∘ e = ↑F
g : C(Y, ℝ) := mk (↑(OrderIso.symm h) ∘ Set.codRestrict (↑G) (Ioo (-1) 1) (_ : ∀ (y : Y), ↑G y ∈ Ioo (-1) 1))
hgG : ∀ {y : Y} {a : (fun x => ℝ) y}, ↑g y = a ↔ ↑G y = ↑(↑h a)
y : Y
a : ℝ
ha : a ∈ t
hay : (Subtype.val ∘ ↑h) a = ↑G y
⊢ ↑g y ∈ t
case intro.intro.refine'_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : OrdConnected t'
hFt : ∀ (x : X), ↑F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), ↑G y ∈ t'
hGF : ↑G ∘ e = ↑F
g : C(Y, ℝ) := mk (↑(OrderIso.symm h) ∘ Set.codRestrict (↑G) (Ioo (-1) 1) (_ : ∀ (y : Y), ↑G y ∈ Ioo (-1) 1))
hgG : ∀ {y : Y} {a : (fun x => ℝ) y}, ↑g y = a ↔ ↑G y = ↑(↑h a)
y : Y
⊢ ↑g y ∈ t
rcases hG y with ⟨a, ha, hay⟩
case h.e'_4
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : OrdConnected t'
hFt : ∀ (x : X), ↑F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), ↑G y ∈ t'
hGF : ↑G ∘ e = ↑F
g : C(Y, ℝ) := mk (↑(OrderIso.symm h) ∘ Set.codRestrict (↑G) (Ioo (-1) 1) (_ : ∀ (y : Y), ↑G y ∈ Ioo (-1) 1))
hgG : ∀ {y : Y} {a : (fun x => ℝ) y}, ↑g y = a ↔ ↑G y = ↑(↑h a)
y : Y
a : ℝ
ha : a ∈ t
hay : (Subtype.val ∘ ↑h) a = ↑G y
⊢ ↑g y = a
case intro.intro.refine'_1.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : OrdConnected t'
hFt : ∀ (x : X), ↑F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), ↑G y ∈ t'
hGF : ↑G ∘ e = ↑F
g : C(Y, ℝ) := mk (↑(OrderIso.symm h) ∘ Set.codRestrict (↑G) (Ioo (-1) 1) (_ : ∀ (y : Y), ↑G y ∈ Ioo (-1) 1))
hgG : ∀ {y : Y} {a : (fun x => ℝ) y}, ↑g y = a ↔ ↑G y = ↑(↑h a)
y : Y
a : ℝ
ha : a ∈ t
hay : (Subtype.val ∘ ↑h) a = ↑G y
⊢ ↑g y ∈ t
convert ha
no goals
case h.e'_4
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : OrdConnected t'
hFt : ∀ (x : X), ↑F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), ↑G y ∈ t'
hGF : ↑G ∘ e = ↑F
g : C(Y, ℝ) := mk (↑(OrderIso.symm h) ∘ Set.codRestrict (↑G) (Ioo (-1) 1) (_ : ∀ (y : Y), ↑G y ∈ Ioo (-1) 1))
hgG : ∀ {y : Y} {a : (fun x => ℝ) y}, ↑g y = a ↔ ↑G y = ↑(↑h a)
y : Y
a : ℝ
ha : a ∈ t
hay : (Subtype.val ∘ ↑h) a = ↑G y
⊢ ↑g y = a
exact hgG.2 hay.symm
case intro.intro.refine'_2.h
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : OrdConnected t'
hFt : ∀ (x : X), ↑F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), ↑G y ∈ t'
hGF : ↑G ∘ e = ↑F
g : C(Y, ℝ) := mk (↑(OrderIso.symm h) ∘ Set.codRestrict (↑G) (Ioo (-1) 1) (_ : ∀ (y : Y), ↑G y ∈ Ioo (-1) 1))
hgG : ∀ {y : Y} {a : (fun x => ℝ) y}, ↑g y = a ↔ ↑G y = ↑(↑h a)
x : X
⊢ (↑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 : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : OrdConnected t'
hFt : ∀ (x : X), ↑F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), ↑G y ∈ t'
hGF : ↑G ∘ e = ↑F
g : C(Y, ℝ) := mk (↑(OrderIso.symm h) ∘ Set.codRestrict (↑G) (Ioo (-1) 1) (_ : ∀ (y : Y), ↑G y ∈ Ioo (-1) 1))
hgG : ∀ {y : Y} {a : (fun x => ℝ) y}, ↑g y = a ↔ ↑G y = ↑(↑h a)
⊢ ↑g ∘ e = ↑f
ext 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 : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : OrdConnected t
hf : ∀ (x : X), ↑f x ∈ t
hne : Set.Nonempty t
he : ClosedEmbedding e
h : ℝ ≃o ↑(Ioo (-1) 1)
F : X →ᵇ ℝ :=
  { toContinuousMap := mk (Subtype.val ∘ ↑h ∘ ↑f),
    map_bounded' :=
      (_ :
        ∃ C,
          ∀ (x y : X),
            dist (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) x)
                (ContinuousMap.toFun (mk (Subtype.val ∘ ↑h ∘ ↑f)) y) ≤
              C) }
t' : Set ℝ := Subtype.val ∘ ↑h '' t
ht_sub : t' ⊆ Ioo (-1) 1
this : OrdConnected t'
hFt : ∀ (x : X), ↑F x ∈ t'
G : Y →ᵇ ℝ
hG : ∀ (y : Y), ↑G y ∈ t'
hGF : ↑G ∘ e = ↑F
g : C(Y, ℝ) := mk (↑(OrderIso.symm h) ∘ Set.codRestrict (↑G) (Ioo (-1) 1) (_ : ∀ (y : Y), ↑G y ∈ Ioo (-1) 1))
hgG : ∀ {y : Y} {a : (fun x => ℝ) y}, ↑g y = a ↔ ↑G y = ↑(↑h a)
x : X
⊢ (↑g ∘ e) x = ↑f x
exact hgG.2 (congr_fun hGF _)