awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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
have out' : ∀ ⦃x : ℝ⦄ (hx : x ∈ t') ⦃y : ℝ⦄ (hy : y ∈ t'), Icc x y ⊆ t'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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
⊢ z ∈ t'
have 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'
Tactic: lift z to Ioo (-1 : ℝ) 1 using Icc_subset_Ioo (h x).2.1 (h y).2.2 hz
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (hypothesis)
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 : ℝ)
⊢ (↑z : ℝ) ∈ t'
have 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
Tactic: change z ∈ Icc (h x) (h y) at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (hypothesis)
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
⊢ (↑z : ℝ) ∈ t'
have hz₁ : Membership.mem (γ := Set (↑(Ioo (-1) 1) : Type)) ((⇑h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) '' Icc x y) z
Tactic: rw [← h.image_Icc] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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
⊢ (↑z : ℝ) ∈ t'
have out' : ∀ (z : ℝ) (hz : z ∈ Icc x y), (↑((h : (a : ℝ) → (↑(Ioo (-1) 1) : Type)) z) : ℝ) ∈ t'
Tactic: rcases hz with ⟨z, hz, rfl⟩
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (hypothesis)
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
⊢ ∃ (g : C(Y, ℝ)),
    (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have this : 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⟩
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (hypothesis)
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
⊢ ∃ (g : C(Y, ℝ)),
    (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have hFt : ∀ (x : X), Membership.mem (α := ℝ) t' ((F : (a : X) → ℝ) x : ℝ)
Tactic: have hFt : ∀ x, F x ∈ t' := fun x => mem_image_of_mem _ (hf x)
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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 : C(Y, ℝ)),
    (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have 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) → ℝ)
Tactic: rcases F.exists_extension_forall_mem_of_isClosedEmbedding hFt (hne.image _) he with ⟨G, hG, hGF⟩
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (hypothesis)
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 := ⋯ }
⊢ ∃ (g : C(Y, ℝ)),
    (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have hgG : ∀ {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
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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) → ℝ)
have refine_1 : ∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)
Tactic: refine ⟨g, fun y => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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 : ℝ)
⊢ ∃ (g : C(Y, ℝ)),
    (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have refine_2 : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
Tactic: refine ⟨g, fun y => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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
⊢ Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)
have 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 : ℝ)
Tactic: rcases hG y with ⟨a, ha, hay⟩
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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 : ℝ)
⊢ Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)
have h₁ : (g : (a : Y) → ℝ) y = a
Tactic: convert! ha
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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) : ℝ) : ℝ)
⊢ Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have refine_2 : ∀ (x : X), Eq (α := ℝ) (((⇑g : (a : Y) → ℝ) ∘ e) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
⊢ { toFun := Real.toNNReal, continuous_toFun := continuous_real_toNNReal : C(ℝ, ℝ≥0) }.comp
      { toFun := toReal, continuous_toFun := continuous_coe : C(ℝ≥0, ℝ) } =
    ContinuousMap.id ℝ≥0
have 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) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Ultrafilter (goal)
Goal:
X : Type u
x : X
inst : TopologicalSpace X
f : Filter X
⊢ ClusterPt x f ↔ ∃ (u : Ultrafilter X), (↑u : Filter X) ≤ f ∧ (↑u : Filter X) ≤ 𝓝 x
have simp_rw : (𝓝 x ⊓ f).NeBot ↔ ∃ (u : Ultrafilter X), (↑u : Filter X) ≤ f ∧ (↑u : Filter X) ≤ 𝓝 x
Tactic: simp_rw [ClusterPt, ← le_inf_iff, exists_ultrafilter_iff, inf_comm]
-- Lean 4 proof step from Mathlib.Topology.Ultrafilter (goal)
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
⊢ ClusterPt x f ↔ ∃ (u : Ultrafilter X), (↑u : Filter X) ≤ f ∧ (↑u : Filter X) ≤ 𝓝 x
have simp_rw₁ : (𝓝 x ⊓ f).NeBot ↔ ∃ (u : Ultrafilter X), (↑u : Filter X) ≤ f ⊓ 𝓝 x
Tactic: simp_rw [ClusterPt, ← le_inf_iff, exists_ultrafilter_iff, inf_comm]