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 : 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 := ⋯ }
hgG :
  ∀ {y : Y} {a : ℝ},
    (g : (a : Y) → ℝ) y = a ↔
      Eq (α := ℝ) ((G : (a : Y) → ℝ) y : ℝ) ((↑((h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) a) : ℝ) : ℝ)
⊢ ∃ (g : C(Y, ℝ)),
    (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)

Tactic:
⟨g, fun y => ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- 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 := ⋯ }
hgG :
  ∀ {y : Y} {a : ℝ},
    (g : (a : Y) → ℝ) y = a ↔
      Eq (α := ℝ) ((G : (a : Y) → ℝ) y : ℝ) ((↑((h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) a) : ℝ) : ℝ)
refine_1 : ∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)
refine_2 : 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:
refine ⟨g, fun y => ?_, ?_⟩
-- 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 := ⋯ }
hgG :
  ∀ {y : Y} {a : ℝ},
    (g : (a : Y) → ℝ) y = a ↔
      Eq (α := ℝ) ((G : (a : Y) → ℝ) y : ℝ) ((↑((h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) a) : ℝ) : ℝ)
y : Y
refine_1 :
  ∀ (a : ℝ) (ha : a ∈ t)
    (hay :
      Eq (α := ℝ)
        (Function.comp (β := (↑(Ioo (-1) 1) : Type))
            (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
            (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) a :
          ℝ)
        ((G : (a : Y) → ℝ) y : ℝ)),
    Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)
⊢ Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)

Tactic:
rcases hG y with ⟨a, ha, hay⟩
-- 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 := ⋯ }
hgG :
  ∀ {y : Y} {a : ℝ},
    (g : (a : Y) → ℝ) y = a ↔
      Eq (α := ℝ) ((G : (a : Y) → ℝ) y : ℝ) ((↑((h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) a) : ℝ) : ℝ)
y : Y
a : ℝ
ha : a ∈ t
hay :
  Eq (α := ℝ)
    (Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) a :
      ℝ)
    ((G : (a : Y) → ℝ) y : ℝ)
⊢ a ∈ t

Tactic:
ha
-- 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 := ⋯ }
hgG :
  ∀ {y : Y} {a : ℝ},
    (g : (a : Y) → ℝ) y = a ↔
      Eq (α := ℝ) ((G : (a : Y) → ℝ) y : ℝ) ((↑((h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) a) : ℝ) : ℝ)
y : Y
a : ℝ
ha : a ∈ t
hay :
  Eq (α := ℝ)
    (Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) a :
      ℝ)
    ((G : (a : Y) → ℝ) y : ℝ)
h₁ : (g : (a : Y) → ℝ) y = a
⊢ Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)

Tactic:
convert! ha
-- 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 := ⋯ }
hgG :
  ∀ {y : Y} {a : ℝ},
    (g : (a : Y) → ℝ) y = a ↔
      Eq (α := ℝ) ((G : (a : Y) → ℝ) y : ℝ) ((↑((h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) a) : ℝ) : ℝ)
y : Y
a : ℝ
ha : a ∈ t
hay :
  Eq (α := ℝ)
    (Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) a :
      ℝ)
    ((G : (a : Y) → ℝ) y : ℝ)
⊢ (g : (a : Y) → ℝ) y = a

Tactic:
hgG.2 hay.symm

Premises used: Iff.mpr, Eq.symm
-- 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 := ⋯ }
hgG :
  ∀ {y : Y} {a : ℝ},
    (g : (a : Y) → ℝ) y = a ↔
      Eq (α := ℝ) ((G : (a : Y) → ℝ) y : ℝ) ((↑((h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) a) : ℝ) : ℝ)
y : Y
a : ℝ
ha : a ∈ t
hay :
  Eq (α := ℝ)
    (Function.comp (β := (↑(Ioo (-1) 1) : Type))
        (Subtype.val (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Ioo (-1) 1) x))
        (⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) a :
      ℝ)
    ((G : (a : Y) → ℝ) y : ℝ)
⊢ (g : (a : Y) → ℝ) y = a

Tactic:
exact hgG.2 hay.symm

Premises used: Iff.mpr, Eq.symm
-- 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 := ⋯ }
hgG :
  ∀ {y : Y} {a : ℝ},
    (g : (a : Y) → ℝ) y = a ↔
      Eq (α := ℝ) ((G : (a : Y) → ℝ) y : ℝ) ((↑((h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) a) : ℝ) : ℝ)
refine_2 : ∀ (x : X), Eq (α := ℝ) (((⇑g : (a : Y) → ℝ) ∘ e) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
⊢ Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)

Tactic:
ext 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 : ℝ)
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 := ⋯ }
hgG :
  ∀ {y : Y} {a : ℝ},
    (g : (a : Y) → ℝ) y = a ↔
      Eq (α := ℝ) ((G : (a : Y) → ℝ) y : ℝ) ((↑((h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) a) : ℝ) : ℝ)
x : X
⊢ Eq (α := ℝ) (((⇑g : (a : Y) → ℝ) ∘ e) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
hgG.2 (congr_fun hGF _)

Premises used: Iff.mpr, congr_fun
-- 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 := ⋯ }
hgG :
  ∀ {y : Y} {a : ℝ},
    (g : (a : Y) → ℝ) y = a ↔
      Eq (α := ℝ) ((G : (a : Y) → ℝ) y : ℝ) ((↑((h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) a) : ℝ) : ℝ)
x : X
⊢ Eq (α := ℝ) (((⇑g : (a : Y) → ℝ) ∘ e) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
exact hgG.2 (congr_fun hGF _)

Premises used: Iff.mpr, congr_fun
-- Module: Mathlib.Topology.TietzeExtension
Goal:
Y : Type u_2
inst : TopologicalSpace Y
inst_1 : NormalSpace Y
s : Set Y
f : C((↑s : Type u_2), ℝ)
t : Set ℝ
inst_2 : t.OrdConnected
ht : ∀ (x : (↑s : Type u_2)), Membership.mem (α := ℝ) t ((f : (a : (↑s : Type u_2)) → ℝ) x : ℝ)
hne : t.Nonempty
hs : IsClosed[inst] s
⊢ ∃ (g : C(Y, ℝ)), (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧ restrict s g = f

Tactic:
let ⟨g, hgt, hgf⟩ :=
    exists_extension_forall_mem_of_isClosedEmbedding f ht hne hs.isClosedEmbedding_subtypeVal
  ⟨g, hgt, coe_injective hgf⟩

Premises used: Exists, ContinuousMap.coe_injective, And, And.intro, Exists.intro, IsClosed.isClosedEmbedding_subtypeVal, _private.0.ContinuousMap.exists_restrict_eq_forall_mem_of_closed.match_1, Eq, ContinuousMap.exists_extension_forall_mem_of_isClosedEmbedding, ContinuousMap.restrict
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
⊢ Continuous toReal

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
h :
  ∀ (a : ℝ≥0),
    (↑(({ toFun := Real.toNNReal, continuous_toFun := continuous_real_toNNReal : C(ℝ, ℝ≥0) }.comp
                { toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) } :
              (a : ℝ≥0) → ℝ≥0)
            a) :
        ℝ) =
      (↑((ContinuousMap.id ℝ≥0 : (a : ℝ≥0) → ℝ≥0) a) : ℝ)
⊢ { toFun := Real.toNNReal, continuous_toFun := continuous_real_toNNReal : C(ℝ, ℝ≥0) }.comp
      { toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) } =
    ContinuousMap.id ℝ≥0

Tactic:
ext
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
a : ℝ≥0
⊢ (↑(({ toFun := Real.toNNReal, continuous_toFun := continuous_real_toNNReal : C(ℝ, ℝ≥0) }.comp
              { toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) } :
            (a : ℝ≥0) → ℝ≥0)
          a) :
      ℝ) =
    (↑((ContinuousMap.id ℝ≥0 : (a : ℝ≥0) → ℝ≥0) a) : ℝ)

Tactic:
simp
-- Module: Mathlib.Topology.Ultrafilter
Goal:
X : Type u
x : X
inst : TopologicalSpace X
f : Ultrafilter X
⊢ ClusterPt x (↑f : Filter X) ↔ (↑f : Filter X) ≤ 𝓝 x

Tactic:
⟨f.le_of_inf_neBot', fun h => ClusterPt.of_le_nhds h⟩

Premises used: ClusterPt.of_le_nhds, Iff.intro, Ultrafilter.le_of_inf_neBot'
-- Module: Mathlib.Topology.Ultrafilter
Goal:
X : Type u
x : X
inst : TopologicalSpace X
f : Filter X
simp_rw : (𝓝 x ⊓ f).NeBot ↔ ∃ (u : Ultrafilter X), (↑u : Filter X) ≤ f ∧ (↑u : Filter X) ≤ 𝓝 x
simp_rw₁ : (𝓝 x ⊓ f).NeBot ↔ ∃ (u : Ultrafilter X), (↑u : Filter X) ≤ f ⊓ 𝓝 x
simp_rw₂ : (𝓝 x ⊓ f).NeBot ↔ (f ⊓ 𝓝 x).NeBot
⊢ ClusterPt x f ↔ ∃ (u : Ultrafilter X), (↑u : Filter X) ≤ f ∧ (↑u : Filter X) ≤ 𝓝 x

Tactic:
simp_rw [ClusterPt, ← le_inf_iff, exists_ultrafilter_iff, inf_comm]

Premises used: Filter.exists_ultrafilter_iff, inf_comm, le_inf_iff, ClusterPt
-- Module: Mathlib.Topology.Ultrafilter
Goal:
X : Type u
α : Type u_1
x : X
inst : TopologicalSpace X
F : Filter α
u : α → X
simp_rw : ClusterPt x (map u F) ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
simp_rw₁ : (𝓝 x ⊓ map u F).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
simp_rw₂ :
  (map u (comap u (𝓝 x) ⊓ F)).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
simp_rw₃ : (comap u (𝓝 x) ⊓ F).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)
simp_rw₄ : (comap u (𝓝 x) ⊓ F).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ (↑U : Filter α) ≤ comap u (𝓝 x)
simp_rw₅ : (comap u (𝓝 x) ⊓ F).NeBot ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ⊓ comap u (𝓝 x)
simp_rw₆ : (comap u (𝓝 x) ⊓ F).NeBot ↔ (F ⊓ comap u (𝓝 x)).NeBot
⊢ MapClusterPt x F u ↔ ∃ (U : Ultrafilter α), (↑U : Filter α) ≤ F ∧ Tendsto u (↑U : Filter α) (𝓝 x)

Tactic:
simp_rw [MapClusterPt, ClusterPt, ← Filter.push_pull', map_neBot_iff, tendsto_iff_comap,
    ← le_inf_iff, exists_ultrafilter_iff, inf_comm]

Premises used: Filter.push_pull', Filter.tendsto_iff_comap, Filter.exists_ultrafilter_iff, inf_comm, le_inf_iff, ClusterPt, MapClusterPt, Filter.map_neBot_iff
-- Module: Mathlib.Topology.Ultrafilter
Goal:
X : Type u
s : Set X
inst : TopologicalSpace X
simp_rw : (∀ x ∈ s, s ∈ 𝓝 x) ↔ ∀ x ∈ s, ∀ (l : Ultrafilter X), (↑l : Filter X) ≤ 𝓝 x → s ∈ l
⊢ IsOpen[inst] s ↔ ∀ x ∈ s, ∀ (l : Ultrafilter X), (↑l : Filter X) ≤ 𝓝 x → s ∈ l

Tactic:
simp_rw [isOpen_iff_mem_nhds, ← mem_iff_ultrafilter]

Premises used: Filter.mem_iff_ultrafilter, isOpen_iff_mem_nhds
-- Module: Mathlib.Topology.Ultrafilter
Goal:
X : Type u
x : X
s : Set X
inst : TopologicalSpace X
⊢ x ∈ closure[inst] s ↔ ∃ (u : Ultrafilter X), s ∈ u ∧ (↑u : Filter X) ≤ 𝓝 x

Tactic:
simp [closure_eq_cluster_pts, ClusterPt, ← exists_ultrafilter_iff, and_comm]

Premises used: closure_eq_cluster_pts, and_comm, Filter.exists_ultrafilter_iff, ClusterPt
-- Module: Mathlib.Topology.Ultrafilter
Goal:
X : Type u
s : Set X
inst : TopologicalSpace X
⊢ IsClosed[inst] s ↔ ∀ (x : X) (u : Ultrafilter X), (↑u : Filter X) ≤ 𝓝 x → s ∈ u → x ∈ s

Tactic:
simp [isClosed_iff_clusterPt, ClusterPt, ← exists_ultrafilter_iff]

Premises used: Filter.exists_ultrafilter_iff, ClusterPt, isClosed_iff_clusterPt
-- Module: Mathlib.Topology.Ultrafilter
Goal:
X : Type u
Y : Type v
x : X
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ ContinuousAt f x ↔ ∀ (g : Ultrafilter X), (↑g : Filter X) ≤ 𝓝 x → Tendsto f (↑g : Filter X) (𝓝 (f x))

Tactic:
tendsto_iff_ultrafilter f (𝓝 x) (𝓝 (f x))

Premises used: Filter.tendsto_iff_ultrafilter, ContinuousAt, nhds
-- Module: Mathlib.Topology.Ultrafilter
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
⊢ Continuous[inst, inst_1] f ↔
    ∀ (x : X) (g : Ultrafilter X), (↑g : Filter X) ≤ 𝓝 x → Tendsto f (↑g : Filter X) (𝓝 (f x))

Tactic:
simp only [continuous_iff_continuousAt, continuousAt_iff_ultrafilter]

Premises used: continuousAt_iff_ultrafilter, continuous_iff_continuousAt
-- Module: Mathlib.Topology.UniformSpace.AbsoluteValue
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
R : Type u_2
inst_3 : CommRing R
abv : AbsoluteValue R 𝕜
⊢ ∀ (x : R), Eq.{u_1 + 1} (α := 𝕜) ((fun (x y : R) ↦ ((abv : (a : R) → 𝕜) (y - x) : 𝕜)) x x) 0

Tactic:
simp