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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
g : Y →ᵇ ℝ
xl : (y : Y) → X
hxl : ∀ (y : Y), LE.le (α := ℝ) ((f : (a : X) → ℝ) (xl y) : ℝ) ((g : (a : Y) → ℝ) y : ℝ)
hgb : ∀ (y : Y), (g : (a : Y) → ℝ) y ≤ b
hb' : ¬∃ (x : X), (f : (a : X) → ℝ) x = b
dg : Y →ᵇ ℝ
hgf : ∀ (x : X), Eq (α := ℝ) ((g - dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
hyb : (g - dg : (a : Y) → ℝ) y < b
xu : X
hyxu : LT.lt (α := ℝ) ((g - dg : (a : Y) → ℝ) y : ℝ) ((f : (a : X) → ℝ) xu : ℝ)
right : (f : (a : X) → ℝ) xu ≤ b
x : X
ha : IsGLB (α := ℝ) (range (ι := X) (⇑f : (a : X) → ℝ) : Set ℝ) ((f : (a : X) → ℝ) x : ℝ)
hmem :
  ∀ (x_1 : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((f : (a : X) → ℝ) x_1 : ℝ)
hle : (f : (a : X) → ℝ) x ≤ b
hlt : (f : (a : X) → ℝ) x < b
c : ℝ := HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) b / 2
hac : (f : (a : X) → ℝ) x < c
hcb : c < b
hsub : HSub.hSub (β := ℝ) c ((f : (a : X) → ℝ) x : ℝ) = b - c
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c)
dgb : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (b - c)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (b - c)) ((dg : (a : Y) → ℝ) x : ℝ)
hc : c < (g : (a : Y) → ℝ) y
⊢ (f : (a : X) → ℝ) x = c - (b - c)
have rw : (f : (a : X) → ℝ) x = c - HSub.hSub (β := ℝ) c ((f : (a : X) → ℝ) x : ℝ)
Tactic: rw [← hsub, sub_sub_cancel]
-- 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
g : Y →ᵇ ℝ
xl : (y : Y) → X
hxl : ∀ (y : Y), LE.le (α := ℝ) ((f : (a : X) → ℝ) (xl y) : ℝ) ((g : (a : Y) → ℝ) y : ℝ)
hgb : ∀ (y : Y), (g : (a : Y) → ℝ) y ≤ b
hb' : ¬∃ (x : X), (f : (a : X) → ℝ) x = b
dg : Y →ᵇ ℝ
hgf : ∀ (x : X), Eq (α := ℝ) ((g - dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
hyb : (g - dg : (a : Y) → ℝ) y < b
xu : X
hyxu : LT.lt (α := ℝ) ((g - dg : (a : Y) → ℝ) y : ℝ) ((f : (a : X) → ℝ) xu : ℝ)
right : (f : (a : X) → ℝ) xu ≤ b
x : X
ha : IsGLB (α := ℝ) (range (ι := X) (⇑f : (a : X) → ℝ) : Set ℝ) ((f : (a : X) → ℝ) x : ℝ)
hmem :
  ∀ (x_1 : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((f : (a : X) → ℝ) x_1 : ℝ)
hle : (f : (a : X) → ℝ) x ≤ b
hlt : (f : (a : X) → ℝ) x < b
c : ℝ := HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) b / 2
hac : (f : (a : X) → ℝ) x < c
hcb : c < b
hsub : HSub.hSub (β := ℝ) c ((f : (a : X) → ℝ) x : ℝ) = b - c
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c)
dgb : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (b - c)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (b - c)) ((dg : (a : Y) → ℝ) x : ℝ)
hc : c < (g : (a : Y) → ℝ) y
rw : (f : (a : X) → ℝ) x = c - HSub.hSub (β := ℝ) c ((f : (a : X) → ℝ) x : ℝ)
⊢ (f : (a : X) → ℝ) x = c - (b - c)
have rw₁ : Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
Tactic: rw [← hsub, sub_sub_cancel]
-- 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
g : Y →ᵇ ℝ
xl : (y : Y) → X
hxl : ∀ (y : Y), LE.le (α := ℝ) ((f : (a : X) → ℝ) (xl y) : ℝ) ((g : (a : Y) → ℝ) y : ℝ)
hgb : ∀ (y : Y), (g : (a : Y) → ℝ) y ≤ b
hb' : ¬∃ (x : X), (f : (a : X) → ℝ) x = b
dg : Y →ᵇ ℝ
hgf : ∀ (x : X), Eq (α := ℝ) ((g - dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
hyb : (g - dg : (a : Y) → ℝ) y < b
xu : X
hyxu : LT.lt (α := ℝ) ((g - dg : (a : Y) → ℝ) y : ℝ) ((f : (a : X) → ℝ) xu : ℝ)
right : (f : (a : X) → ℝ) xu ≤ b
x : X
ha : IsGLB (α := ℝ) (range (ι := X) (⇑f : (a : X) → ℝ) : Set ℝ) ((f : (a : X) → ℝ) x : ℝ)
hmem :
  ∀ (x_1 : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((f : (a : X) → ℝ) x_1 : ℝ)
hle : (f : (a : X) → ℝ) x ≤ b
hlt : (f : (a : X) → ℝ) x < b
c : ℝ := HAdd.hAdd (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) b / 2
hac : (f : (a : X) → ℝ) x < c
hcb : c < b
hsub : HSub.hSub (β := ℝ) c ((f : (a : X) → ℝ) x : ℝ) = b - c
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c)
dgb : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (b - c)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (b - c)) ((dg : (a : Y) → ℝ) x : ℝ)
hc : c < (g : (a : Y) → ℝ) y
⊢ LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g - dg : (a : Y) → ℝ) y : ℝ)
have f₁ : (f : (a : X) → ℝ) x = c - (b - c)
Tactic: calc
        f x = c - (b - c) := by rw [← hsub, sub_sub_cancel]
        _ ≤ g y - dg y := sub_le_sub hc.le (dgmem _).2
-- 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
xl : (y : Y) → X
hxl : ∀ (y : Y), LE.le (α := ℝ) ((f : (a : X) → ℝ) (xl y) : ℝ) ((g : (a : Y) → ℝ) y : ℝ)
hgb : ∀ (y : Y), (g : (a : Y) → ℝ) y ≤ b
hb' : ¬∃ (x : X), (f : (a : X) → ℝ) x = b
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c)
dgb : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (b - c)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (b - c)) ((dg : (a : Y) → ℝ) x : ℝ)
hgf : ∀ (x : X), Eq (α := ℝ) ((g - dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
hyb : (g - dg : (a : Y) → ℝ) y < b
xu : X
hyxu : LT.lt (α := ℝ) ((g - dg : (a : Y) → ℝ) y : ℝ) ((f : (a : X) → ℝ) xu : ℝ)
right : (f : (a : X) → ℝ) xu ≤ b
hc : c < (g : (a : Y) → ℝ) y
h : a ∉ range (ι := X) (⇑f : (a : X) → ℝ)
⊢ a = c - (b - c)
have rw : a = c - (c - a)
Tactic: rw [← hsub, sub_sub_cancel]
-- 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
xl : (y : Y) → X
hxl : ∀ (y : Y), LE.le (α := ℝ) ((f : (a : X) → ℝ) (xl y) : ℝ) ((g : (a : Y) → ℝ) y : ℝ)
hgb : ∀ (y : Y), (g : (a : Y) → ℝ) y ≤ b
hb' : ¬∃ (x : X), (f : (a : X) → ℝ) x = b
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c)
dgb : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (b - c)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (b - c)) ((dg : (a : Y) → ℝ) x : ℝ)
hgf : ∀ (x : X), Eq (α := ℝ) ((g - dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
hyb : (g - dg : (a : Y) → ℝ) y < b
xu : X
hyxu : LT.lt (α := ℝ) ((g - dg : (a : Y) → ℝ) y : ℝ) ((f : (a : X) → ℝ) xu : ℝ)
right : (f : (a : X) → ℝ) xu ≤ b
hc : c < (g : (a : Y) → ℝ) y
h : a ∉ range (ι := X) (⇑f : (a : X) → ℝ)
rw : a = c - (c - a)
⊢ a = c - (b - c)
have rw₁ : a = a
Tactic: rw [← hsub, sub_sub_cancel]
-- 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
xl : (y : Y) → X
hxl : ∀ (y : Y), LE.le (α := ℝ) ((f : (a : X) → ℝ) (xl y) : ℝ) ((g : (a : Y) → ℝ) y : ℝ)
hgb : ∀ (y : Y), (g : (a : Y) → ℝ) y ≤ b
hb' : ¬∃ (x : X), (f : (a : X) → ℝ) x = b
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c)
dgb : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (b - c)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (b - c)) ((dg : (a : Y) → ℝ) x : ℝ)
hgf : ∀ (x : X), Eq (α := ℝ) ((g - dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
hyb : (g - dg : (a : Y) → ℝ) y < b
xu : X
hyxu : LT.lt (α := ℝ) ((g - dg : (a : Y) → ℝ) y : ℝ) ((f : (a : X) → ℝ) xu : ℝ)
right : (f : (a : X) → ℝ) xu ≤ b
hc : c < (g : (a : Y) → ℝ) y
h : a ∉ range (ι := X) (⇑f : (a : X) → ℝ)
⊢ a < (g - dg : (a : Y) → ℝ) y
have a₁ : a = c - (b - c)
Tactic: calc
          a = c - (b - c) := by rw [← hsub, sub_sub_cancel]
          _ < g y - (b - c) := sub_lt_sub_right hc _
          _ ≤ g y - dg y := sub_le_sub_left (dgmem _).2 _
-- 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
xl : (y : Y) → X
hxl : ∀ (y : Y), LE.le (α := ℝ) ((f : (a : X) → ℝ) (xl y) : ℝ) ((g : (a : Y) → ℝ) y : ℝ)
hgb : ∀ (y : Y), (g : (a : Y) → ℝ) y ≤ b
hb' : ¬∃ (x : X), (f : (a : X) → ℝ) x = b
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c)
dgb : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (b - c)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (b - c)) ((dg : (a : Y) → ℝ) x : ℝ)
hgf : ∀ (x : X), Eq (α := ℝ) ((g - dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
hyb : (g - dg : (a : Y) → ℝ) y < b
xu : X
hyxu : LT.lt (α := ℝ) ((g - dg : (a : Y) → ℝ) y : ℝ) ((f : (a : X) → ℝ) xu : ℝ)
right : (f : (a : X) → ℝ) xu ≤ b
hc : c < (g : (a : Y) → ℝ) y
h : a ∉ range (ι := X) (⇑f : (a : X) → ℝ)
⊢ ∃ (x₁ : X) (x₂ : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
      ((g - dg : (a : Y) → ℝ) y : ℝ)
have hay : a < (g - dg : (a : Y) → ℝ) y
Tactic: have hay : a < (g - dg) y := by
        calc
          a = c - (b - c) := by rw [← hsub, sub_sub_cancel]
          _ < g y - (b - c) := sub_lt_sub_right hc _
          _ ≤ g y - dg y := sub_le_sub_left (dgmem _).2 _
-- 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
xl : (y : Y) → X
hxl : ∀ (y : Y), LE.le (α := ℝ) ((f : (a : X) → ℝ) (xl y) : ℝ) ((g : (a : Y) → ℝ) y : ℝ)
hgb : ∀ (y : Y), (g : (a : Y) → ℝ) y ≤ b
hb' : ¬∃ (x : X), (f : (a : X) → ℝ) x = b
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c)
dgb : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (b - c)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (b - c)) ((dg : (a : Y) → ℝ) x : ℝ)
hgf : ∀ (x : X), Eq (α := ℝ) ((g - dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
hyb : (g - dg : (a : Y) → ℝ) y < b
xu : X
hyxu : LT.lt (α := ℝ) ((g - dg : (a : Y) → ℝ) y : ℝ) ((f : (a : X) → ℝ) xu : ℝ)
right : (f : (a : X) → ℝ) xu ≤ b
hc : c < (g : (a : Y) → ℝ) y
h : a ∉ range (ι := X) (⇑f : (a : X) → ℝ)
hay : a < (g - dg : (a : Y) → ℝ) y
⊢ ∃ (x₁ : X) (x₂ : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
      ((g - dg : (a : Y) → ℝ) y : ℝ)
have inr : ∀ (x : X),
  a ≤ (f : (a : X) → ℝ) x →
    ∀ (hxy : LT.lt (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g - dg : (a : Y) → ℝ) y : ℝ)),
      ∃ (x₁ : X) (x₂ : X),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
          ((g - dg : (a : Y) → ℝ) y : ℝ)
Tactic: rcases ha.exists_between hay with ⟨_, ⟨x, rfl⟩, _, hxy⟩
-- 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
inst_3 : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range (ι := X) (⇑f : (a : X) → ℝ)) a
b : ℝ
hb : IsLUB (range (ι := X) (⇑f : (a : X) → ℝ)) b
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a b) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
xl : (y : Y) → X
hxl : ∀ (y : Y), LE.le (α := ℝ) ((f : (a : X) → ℝ) (xl y) : ℝ) ((g : (a : Y) → ℝ) y : ℝ)
hgb : ∀ (y : Y), (g : (a : Y) → ℝ) y ≤ b
hb' : ¬∃ (x : X), (f : (a : X) → ℝ) x = b
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c)
dgb : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (b - c)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (b - c)) ((dg : (a : Y) → ℝ) x : ℝ)
hgf : ∀ (x : X), Eq (α := ℝ) ((g - dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
hyb : (g - dg : (a : Y) → ℝ) y < b
xu : X
hyxu : LT.lt (α := ℝ) ((g - dg : (a : Y) → ℝ) y : ℝ) ((f : (a : X) → ℝ) xu : ℝ)
right : (f : (a : X) → ℝ) xu ≤ b
hc : (g : (a : Y) → ℝ) y ≤ c
⊢ ∃ (x₁ : X) (x₂ : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
      ((g - dg : (a : Y) → ℝ) y : ℝ)
have inr : LE.le (α := ℝ) ((f : (a : X) → ℝ) (xl y) : ℝ) ((g - dg : (a : Y) → ℝ) y : ℝ)
Tactic: refine ⟨xl y, xu, ?_, hyxu.le⟩
-- 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 : 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
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have inl : IsEmpty X →
  ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
Tactic: cases isEmpty_or_nonempty 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 : 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
inl :
  IsEmpty X →
    ∃ (g : Y →ᵇ ℝ),
      (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
        Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have inr : Nonempty X →
  ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
Tactic: cases isEmpty_or_nonempty 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 : 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 : IsEmpty X
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have inl : ∀ (c : ℝ) (hc : c ∈ t),
  ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
Tactic: rcases hne with ⟨c, hc⟩
Cleared hypotheses: hne
-- 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 : 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 : Nonempty X
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have inr : ∀ (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) → ℝ)),
  ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
Tactic: rcases exists_extension_forall_exists_le_ge_of_isClosedEmbedding f he with ⟨g, hg, hgf⟩
-- 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 : 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 : 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) → ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have inr : ∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)
Tactic: refine ⟨g, fun y => ?_, hgf⟩
-- 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 : 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 : 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
⊢ Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)
have inr : ∀ (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: rcases hg y with ⟨xl, xu, h⟩
-- Lean 4 proof step from Mathlib.Topology.TietzeExtension (goal)
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 →ᵇ ℝ), (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧ g.restrict s = f
have 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
Tactic: obtain ⟨g, hg, hgf⟩ :=
    exists_extension_forall_mem_of_isClosedEmbedding f hf hne hs.isClosedEmbedding_subtypeVal
-- 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
⊢ ∃ (g : C(Y, ℝ)),
    (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have 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) → ℝ)
Tactic: have h : ℝ ≃o Ioo (-1 : ℝ) 1 := orderIsoIooNegOneOne ℝ
-- 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
⊢ ∃ (g : C(Y, ℝ)),
    (∀ (y : Y), Membership.mem (α := ℝ) t ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
have ht_sub : t' ⊆ Ioo (-1) 1
Tactic: have ht_sub : t' ⊆ Ioo (-1 : ℝ) 1 := image_subset_iff.2 fun x _ => (h x).2