awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), Membership.mem (α := ℝ) t ((f : (a : X) → ℝ) x : ℝ)
hne : t.Nonempty
he : IsClosedEmbedding e
h_1 : Nonempty X
g : Y →ᵇ ℝ
hg :
  ∀ (y : Y),
    ∃ (x₁ : X) (x₂ : X),
      Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
        ((g : (a : Y) → ℝ) y : ℝ)
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
y : Y
xl xu : X
h :
  Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) xl) ((f : (a : X) → ℝ) xu) : Set ℝ)
    ((g : (a : Y) → ℝ) y : ℝ)
⊢ Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)

Tactic:
hs.out (hf _) (hf _) h

Premises used: Set.OrdConnected.out
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : X →ᵇ ℝ
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), Membership.mem (α := ℝ) t ((f : (a : X) → ℝ) x : ℝ)
hne : t.Nonempty
he : IsClosedEmbedding e
h_1 : Nonempty X
g : Y →ᵇ ℝ
hg :
  ∀ (y : Y),
    ∃ (x₁ : X) (x₂ : X),
      Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
        ((g : (a : Y) → ℝ) y : ℝ)
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
y : Y
xl xu : X
h :
  Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) xl) ((f : (a : X) → ℝ) xu) : Set ℝ)
    ((g : (a : Y) → ℝ) y : ℝ)
⊢ Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)

Tactic:
exact hs.out (hf _) (hf _) h

Premises used: Set.OrdConnected.out
-- Module: Mathlib.Topology.TietzeExtension
Goal:
Y : Type u_2
inst : TopologicalSpace Y
inst_1 : NormalSpace Y
s : Set Y
f : (↑s : Type u_2) →ᵇ ℝ
hs : IsClosed[inst] s
t : Set ℝ
inst_2 : t.OrdConnected
hf : ∀ (x : (↑s : Type u_2)), Membership.mem (α := ℝ) t ((f : (a : (↑s : Type u_2)) → ℝ) x : ℝ)
hne : t.Nonempty
obtain :
  ∀ (g : Y →ᵇ ℝ) (hg : ∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ))
    (hgf :
      Eq (α := (↑s : Type u_2) → ℝ) ((⇑g : (a : Y) → ℝ) ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ s))
        (⇑f : (a : (↑s : Type u_2)) → ℝ)),
    ∃ (g : Y →ᵇ ℝ), (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧ g.restrict s = f
⊢ ∃ (g : Y →ᵇ ℝ), (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧ g.restrict s = f

Tactic:
obtain ⟨g, hg, hgf⟩ :=
    exists_extension_forall_mem_of_isClosedEmbedding f hf hne hs.isClosedEmbedding_subtypeVal

Premises used: BoundedContinuousFunction.exists_extension_forall_mem_of_isClosedEmbedding, IsClosed.isClosedEmbedding_subtypeVal
-- Module: Mathlib.Topology.TietzeExtension
Goal:
Y : Type u_2
inst : TopologicalSpace Y
inst_1 : NormalSpace Y
s : Set Y
f : (↑s : Type u_2) →ᵇ ℝ
hs : IsClosed[inst] s
t : Set ℝ
inst_2 : t.OrdConnected
hf : ∀ (x : (↑s : Type u_2)), Membership.mem (α := ℝ) t ((f : (a : (↑s : Type u_2)) → ℝ) x : ℝ)
hne : t.Nonempty
g : Y →ᵇ ℝ
hg : ∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)
hgf :
  Eq (α := (↑s : Type u_2) → ℝ) ((⇑g : (a : Y) → ℝ) ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ s))
    (⇑f : (a : (↑s : Type u_2)) → ℝ)
⊢ ∃ (g : Y →ᵇ ℝ), (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧ g.restrict s = f

Tactic:
⟨g, hg, DFunLike.coe_injective hgf⟩

Premises used: DFunLike.coe_injective, And.intro, Exists.intro
-- Module: Mathlib.Topology.TietzeExtension
Goal:
Y : Type u_2
inst : TopologicalSpace Y
inst_1 : NormalSpace Y
s : Set Y
f : (↑s : Type u_2) →ᵇ ℝ
hs : IsClosed[inst] s
t : Set ℝ
inst_2 : t.OrdConnected
hf : ∀ (x : (↑s : Type u_2)), Membership.mem (α := ℝ) t ((f : (a : (↑s : Type u_2)) → ℝ) x : ℝ)
hne : t.Nonempty
g : Y →ᵇ ℝ
hg : ∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)
hgf :
  Eq (α := (↑s : Type u_2) → ℝ) ((⇑g : (a : Y) → ℝ) ∘ Subtype.val (p := fun (x : Y) ↦ x ∈ s))
    (⇑f : (a : (↑s : Type u_2)) → ℝ)
⊢ ∃ (g : Y →ᵇ ℝ), (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧ g.restrict s = f

Tactic:
exact ⟨g, hg, DFunLike.coe_injective hgf⟩
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), Membership.mem (α := ℝ) t ((f : (a : X) → ℝ) x : ℝ)
hne : t.Nonempty
he : IsClosedEmbedding e
have :
  ∀ (h : ℝ ≃o (↑(Ioo (-1) 1) : Type)),
    ∃ (g : C(Y, ℝ)),
      (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
        Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
⊢ ∃ (g : C(Y, ℝ)),
    (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)

Tactic:
have h : ℝ ≃o Ioo (-1 : ℝ) 1 := orderIsoIooNegOneOne ℝ
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), Membership.mem (α := ℝ) t ((f : (a : X) → ℝ) x : ℝ)
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o (↑(Ioo (-1) 1) : Type)
⊢ Continuous[inst, _]
    (Function.comp (β := (↑(Ioo (-1) 1) : Type))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
      (Function.comp (β := ℝ) (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) (⇑f : (a : X) → ℝ)))

Tactic:
fun_prop
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), Membership.mem (α := ℝ) t ((f : (a : X) → ℝ) x : ℝ)
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o (↑(Ioo (-1) 1) : Type)
F : X →ᵇ ℝ :=
  {
    toFun :=
      Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (Function.comp (β := ℝ) (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) (⇑f : (a : X) → ℝ)),
    continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ :=
  Function.comp (β := (↑(Ioo (-1) 1) : Type))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
      (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) ''
    t
⊢ t' ⊆ Ioo (-1) 1

Tactic:
have ht_sub : t' ⊆ Ioo (-1 : ℝ) 1 := image_subset_iff.2 fun x _ => (h x).2
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), Membership.mem (α := ℝ) t ((f : (a : X) → ℝ) x : ℝ)
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o (↑(Ioo (-1) 1) : Type)
F : X →ᵇ ℝ :=
  {
    toFun :=
      Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (Function.comp (β := ℝ) (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) (⇑f : (a : X) → ℝ)),
    continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ :=
  Function.comp (β := (↑(Ioo (-1) 1) : Type))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
      (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) ''
    t
ht_sub : t' ⊆ Ioo (-1) 1
out' : ∀ ⦃x : ℝ⦄ (hx : x ∈ t') ⦃y : ℝ⦄ (hy : y ∈ t'), Icc x y ⊆ t'
⊢ t'.OrdConnected

Tactic:
constructor
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), Membership.mem (α := ℝ) t ((f : (a : X) → ℝ) x : ℝ)
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o (↑(Ioo (-1) 1) : Type)
F : X →ᵇ ℝ :=
  {
    toFun :=
      Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (Function.comp (β := ℝ) (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) (⇑f : (a : X) → ℝ)),
    continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ :=
  Function.comp (β := (↑(Ioo (-1) 1) : Type))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
      (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) ''
    t
ht_sub : t' ⊆ Ioo (-1) 1
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : ℝ
hz :
  Membership.mem (γ := Set ℝ)
    (Icc
      (Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) x)
      (Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) y))
    z
⊢ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) z

Tactic:
Icc_subset_Ioo (h x).2.1 (h y).2.2 hz

Premises used: And.right, And.left, Set.Icc_subset_Ioo, DFunLike.coe, Subtype.property
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), Membership.mem (α := ℝ) t ((f : (a : X) → ℝ) x : ℝ)
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o (↑(Ioo (-1) 1) : Type)
F : X →ᵇ ℝ :=
  {
    toFun :=
      Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (Function.comp (β := ℝ) (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) (⇑f : (a : X) → ℝ)),
    continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ :=
  Function.comp (β := (↑(Ioo (-1) 1) : Type))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
      (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) ''
    t
ht_sub : t' ⊆ Ioo (-1) 1
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : ℝ
hz :
  Membership.mem (γ := Set ℝ)
    (Icc
      (Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) x)
      (Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) y))
    z
out' :
  ∀ (z : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x })
    (hz :
      Membership.mem (γ := Set ℝ)
        (Icc
          (Function.comp (β := (↑(Ioo (-1) 1) : Type))
            (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
            (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) x)
          (Function.comp (β := (↑(Ioo (-1) 1) : Type))
            (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
            (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) y))
        (↑z : ℝ)),
    (↑z : ℝ) ∈ t'
⊢ z ∈ t'

Tactic:
lift z to Ioo (-1 : ℝ) 1 using Icc_subset_Ioo (h x).2.1 (h y).2.2 hz

Premises used: And.right, And.left, Set.Icc_subset_Ioo, OfNat.ofNat, DFunLike.coe, Set.Ioo, Neg.neg, Subtype.property
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), Membership.mem (α := ℝ) t ((f : (a : X) → ℝ) x : ℝ)
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o (↑(Ioo (-1) 1) : Type)
F : X →ᵇ ℝ :=
  {
    toFun :=
      Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (Function.comp (β := ℝ) (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) (⇑f : (a : X) → ℝ)),
    continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ :=
  Function.comp (β := (↑(Ioo (-1) 1) : Type))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
      (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) ''
    t
ht_sub : t' ⊆ Ioo (-1) 1
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x }
hz :
  Membership.mem (γ := Set ℝ)
    (Icc
      (Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) x)
      (Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) y))
    (↑z : ℝ)
⊢ Membership.mem (γ := Set (↑(Ioo (-1) 1) : Type))
    (Icc ((h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) x) ((h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) y) :
      Set (↑(Ioo (-1) 1) : Type))
    z

Tactic:
change z ∈ Icc (h x) (h y) at hz

Premises used: Set.Icc, DFunLike.coe
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), Membership.mem (α := ℝ) t ((f : (a : X) → ℝ) x : ℝ)
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o (↑(Ioo (-1) 1) : Type)
F : X →ᵇ ℝ :=
  {
    toFun :=
      Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (Function.comp (β := ℝ) (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) (⇑f : (a : X) → ℝ)),
    continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ :=
  Function.comp (β := (↑(Ioo (-1) 1) : Type))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
      (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) ''
    t
ht_sub : t' ⊆ Ioo (-1) 1
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x }
hz :
  Membership.mem (γ := Set (↑(Ioo (-1) 1) : Type))
    (Icc ((h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) x) ((h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) y) :
      Set (↑(Ioo (-1) 1) : Type))
    z
⊢ Membership.mem (γ := Set (↑(Ioo (-1) 1) : Type)) ((⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) '' Icc x y) z

Tactic:
rw [← h.image_Icc] at hz

Premises used: OrderIso.image_Icc
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), Membership.mem (α := ℝ) t ((f : (a : X) → ℝ) x : ℝ)
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o (↑(Ioo (-1) 1) : Type)
F : X →ᵇ ℝ :=
  {
    toFun :=
      Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (Function.comp (β := ℝ) (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) (⇑f : (a : X) → ℝ)),
    continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ :=
  Function.comp (β := (↑(Ioo (-1) 1) : Type))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
      (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) ''
    t
ht_sub : t' ⊆ Ioo (-1) 1
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : { x : ℝ // Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x }
hz : Membership.mem (γ := Set (↑(Ioo (-1) 1) : Type)) ((⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) '' Icc x y) z
out' : ∀ (z : ℝ) (hz : z ∈ Icc x y), (↑((h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) z) : ℝ) ∈ t'
⊢ (↑z : ℝ) ∈ t'

Tactic:
rcases hz with ⟨z, hz, rfl⟩

Premises used: rfl
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), Membership.mem (α := ℝ) t ((f : (a : X) → ℝ) x : ℝ)
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o (↑(Ioo (-1) 1) : Type)
F : X →ᵇ ℝ :=
  {
    toFun :=
      Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (Function.comp (β := ℝ) (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) (⇑f : (a : X) → ℝ)),
    continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ :=
  Function.comp (β := (↑(Ioo (-1) 1) : Type))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
      (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) ''
    t
ht_sub : t' ⊆ Ioo (-1) 1
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : ℝ
hz : z ∈ Icc x y
⊢ (↑((h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) z) : ℝ) ∈ t'

Tactic:
⟨z, hs.out hx hy hz, rfl⟩

Premises used: Set.Mem, setOf, Set.OrdConnected.out, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), Membership.mem (α := ℝ) t ((f : (a : X) → ℝ) x : ℝ)
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o (↑(Ioo (-1) 1) : Type)
F : X →ᵇ ℝ :=
  {
    toFun :=
      Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (Function.comp (β := ℝ) (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) (⇑f : (a : X) → ℝ)),
    continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ :=
  Function.comp (β := (↑(Ioo (-1) 1) : Type))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
      (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) ''
    t
ht_sub : t' ⊆ Ioo (-1) 1
x : ℝ
hx : x ∈ t
y : ℝ
hy : y ∈ t
z : ℝ
hz : z ∈ Icc x y
⊢ (↑((h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) z) : ℝ) ∈ t'

Tactic:
exact ⟨z, hs.out hx hy hz, rfl⟩
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), Membership.mem (α := ℝ) t ((f : (a : X) → ℝ) x : ℝ)
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o (↑(Ioo (-1) 1) : Type)
F : X →ᵇ ℝ :=
  {
    toFun :=
      Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (Function.comp (β := ℝ) (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) (⇑f : (a : X) → ℝ)),
    continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ :=
  Function.comp (β := (↑(Ioo (-1) 1) : Type))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
      (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) ''
    t
ht_sub : t' ⊆ Ioo (-1) 1
⊢ t'.OrdConnected

Tactic:
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⟩
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), Membership.mem (α := ℝ) t ((f : (a : X) → ℝ) x : ℝ)
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o (↑(Ioo (-1) 1) : Type)
F : X →ᵇ ℝ :=
  {
    toFun :=
      Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (Function.comp (β := ℝ) (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) (⇑f : (a : X) → ℝ)),
    continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ :=
  Function.comp (β := (↑(Ioo (-1) 1) : Type))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
      (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) ''
    t
ht_sub : t' ⊆ Ioo (-1) 1
this : t'.OrdConnected
⊢ ∀ (x : X), Membership.mem (α := ℝ) t' ((F : (a : X) → ℝ) x : ℝ)

Tactic:
have hFt : ∀ x, F x ∈ t' := fun x => mem_image_of_mem _ (hf x)
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), Membership.mem (α := ℝ) t ((f : (a : X) → ℝ) x : ℝ)
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o (↑(Ioo (-1) 1) : Type)
F : X →ᵇ ℝ :=
  {
    toFun :=
      Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (Function.comp (β := ℝ) (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) (⇑f : (a : X) → ℝ)),
    continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ :=
  Function.comp (β := (↑(Ioo (-1) 1) : Type))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
      (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) ''
    t
ht_sub : t' ⊆ Ioo (-1) 1
this : t'.OrdConnected
hFt : ∀ (x : X), Membership.mem (α := ℝ) t' ((F : (a : X) → ℝ) x : ℝ)
rcases :
  ∀ (G : Y →ᵇ ℝ) (hG : ∀ (y : Y), Membership.mem (α := ℝ) t' ((G : (a : Y) → ℝ) y : ℝ))
    (hGF : Eq (α := X → ℝ) ((⇑G : (a : Y) → ℝ) ∘ e) (⇑F : (a : X) → ℝ)),
    ∃ (g : C(Y, ℝ)),
      (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
        Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
⊢ ∃ (g : C(Y, ℝ)),
    (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)

Tactic:
rcases F.exists_extension_forall_mem_of_isClosedEmbedding hFt (hne.image _) he with ⟨G, hG, hGF⟩

Premises used: Set.Nonempty.image, BoundedContinuousFunction.exists_extension_forall_mem_of_isClosedEmbedding
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
f : C(X, ℝ)
t : Set ℝ
e : X → Y
hs : t.OrdConnected
hf : ∀ (x : X), Membership.mem (α := ℝ) t ((f : (a : X) → ℝ) x : ℝ)
hne : t.Nonempty
he : IsClosedEmbedding e
h : ℝ ≃o (↑(Ioo (-1) 1) : Type)
F : X →ᵇ ℝ :=
  {
    toFun :=
      Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (Function.comp (β := ℝ) (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) (⇑f : (a : X) → ℝ)),
    continuous_toFun := ⋯, map_bounded' := ⋯ }
t' : Set ℝ :=
  Function.comp (β := (↑(Ioo (-1) 1) : Type))
      (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
      (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) ''
    t
ht_sub : t' ⊆ Ioo (-1) 1
this : t'.OrdConnected
hFt : ∀ (x : X), Membership.mem (α := ℝ) t' ((F : (a : X) → ℝ) x : ℝ)
G : Y →ᵇ ℝ
hG : ∀ (y : Y), Membership.mem (α := ℝ) t' ((G : (a : Y) → ℝ) y : ℝ)
hGF : Eq (α := X → ℝ) ((⇑G : (a : Y) → ℝ) ∘ e) (⇑F : (a : X) → ℝ)
g : C(Y, ℝ) :=
  {
    toFun :=
      Function.comp (β := (↑(Ioo (-1) 1) : Type)) (⇑h.symm : (a : (↑(Ioo (-1) 1) : Type)) → ℝ)
        (Set.codRestrict (⇑G : (a : Y) → ℝ) (Ioo (-1) 1) ⋯),
    continuous_toFun := ⋯ }
⊢ ∀ {y : Y} {a : ℝ},
    (g : (a : Y) → ℝ) y = a ↔
      Eq (α := ℝ) ((G : (a : Y) → ℝ) y : ℝ) ((↑((h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) a) : ℝ) : ℝ)

Tactic:
have hgG : ∀ {y a}, g y = a ↔ G y = h a := @fun y a =>
    h.toEquiv.symm_apply_eq.trans Subtype.ext_iff