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
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 →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c)
dga : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (c - a)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (c - a)) ((dg : (a : Y) → ℝ) x : ℝ)
hgf : ∀ (x : X), Eq (α := ℝ) ((g + dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
⊢ a < (g + dg : (a : Y) → ℝ) y

Tactic:
have hay : a < (g + dg) y := by
      rcases (hg_mem y).1.eq_or_lt with (rfl | hlt)
      · refine (lt_add_iff_pos_right _).2 ?_
        calc
          0 < c - g y := sub_pos.2 hac
          _ = dg y := (dga rfl).symm
      · exact hlt.trans_le (le_add_of_nonneg_right (dgmem y).1)
-- Module: Mathlib.Topology.TietzeExtension
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 →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c)
dga : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (c - a)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (c - a)) ((dg : (a : Y) → ℝ) x : ℝ)
hgf : ∀ (x : X), Eq (α := ℝ) ((g + dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
hay : a < (g + dg : (a : Y) → ℝ) y
inr :
  ∀ (x : X),
    a ≤ (f : (a : X) → ℝ) x →
      ∀ (hxy : LT.lt (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g + dg : (a : Y) → ℝ) y : ℝ)),
        ∃ (x : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g + dg : (a : Y) → ℝ) y : ℝ)
⊢ ∃ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g + dg : (a : Y) → ℝ) y : ℝ)

Tactic:
rcases ha.exists_between hay with ⟨_, ⟨x, rfl⟩, _, hxy⟩

Premises used: IsGLB.exists_between, 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
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 →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c)
dga : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (c - a)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (c - a)) ((dg : (a : Y) → ℝ) x : ℝ)
hgf : ∀ (x : X), Eq (α := ℝ) ((g + dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
hay : a < (g + dg : (a : Y) → ℝ) y
x : X
left : a ≤ (f : (a : X) → ℝ) x
hxy : LT.lt (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g + dg : (a : Y) → ℝ) y : ℝ)
⊢ ∃ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g + dg : (a : Y) → ℝ) y : ℝ)

Tactic:
⟨x, hxy.le, ?_⟩

Premises used: LT.lt.le, 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
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 →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c)
dga : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (c - a)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (c - a)) ((dg : (a : Y) → ℝ) x : ℝ)
hgf : ∀ (x : X), Eq (α := ℝ) ((g + dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
hay : a < (g + dg : (a : Y) → ℝ) y
x : X
left : a ≤ (f : (a : X) → ℝ) x
hxy : LT.lt (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g + dg : (a : Y) → ℝ) y : ℝ)
inr : (g + dg : (a : Y) → ℝ) y ≤ b
⊢ ∃ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g + dg : (a : Y) → ℝ) y : ℝ)

Tactic:
refine ⟨x, hxy.le, ?_⟩
-- Module: Mathlib.Topology.TietzeExtension
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 →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c)
dga : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (c - a)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (c - a)) ((dg : (a : Y) → ℝ) x : ℝ)
hgf : ∀ (x : X), Eq (α := ℝ) ((g + dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
hay : a < (g + dg : (a : Y) → ℝ) y
x : X
left : a ≤ (f : (a : X) → ℝ) x
hxy : LT.lt (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g + dg : (a : Y) → ℝ) y : ℝ)
inr : ∀ (hc : c ≤ (g : (a : Y) → ℝ) y), (g + dg : (a : Y) → ℝ) y ≤ b
inr₁ : ∀ (hc : (g : (a : Y) → ℝ) y ≤ c), (g + dg : (a : Y) → ℝ) y ≤ b
⊢ (g + dg : (a : Y) → ℝ) y ≤ b

Tactic:
rcases le_total c (g y) with hc | hc

Premises used: le_total, 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
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 →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c)
dga : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (c - a)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (c - a)) ((dg : (a : Y) → ℝ) x : ℝ)
hgf : ∀ (x : X), Eq (α := ℝ) ((g + dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
hay : a < (g + dg : (a : Y) → ℝ) y
x : X
left : a ≤ (f : (a : X) → ℝ) x
hxy : LT.lt (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g + dg : (a : Y) → ℝ) y : ℝ)
hc : c ≤ (g : (a : Y) → ℝ) y
⊢ (g + dg : (a : Y) → ℝ) y ≤ b

Tactic:
simp [dg0 (Or.inr hc), (hg_mem y).2]

Premises used: And.right, Or.inr
-- Module: Mathlib.Topology.TietzeExtension
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 →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c)
dga : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (c - a)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (c - a)) ((dg : (a : Y) → ℝ) x : ℝ)
hgf : ∀ (x : X), Eq (α := ℝ) ((g + dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
hay : a < (g + dg : (a : Y) → ℝ) y
x : X
left : a ≤ (f : (a : X) → ℝ) x
hxy : LT.lt (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g + dg : (a : Y) → ℝ) y : ℝ)
hc : (g : (a : Y) → ℝ) y ≤ c
⊢ HAdd.hAdd (α := ℝ) (β := ℝ) ((g : (a : Y) → ℝ) y : ℝ) ((dg : (a : Y) → ℝ) y : ℝ) ≤ c + (c - a)

Tactic:
add_le_add hc (dgmem _).2

Premises used: add_le_add, And.right
-- Module: Mathlib.Topology.TietzeExtension
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 →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c)
dga : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (c - a)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (c - a)) ((dg : (a : Y) → ℝ) x : ℝ)
hgf : ∀ (x : X), Eq (α := ℝ) ((g + dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
hay : a < (g + dg : (a : Y) → ℝ) y
x : X
left : a ≤ (f : (a : X) → ℝ) x
hxy : LT.lt (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g + dg : (a : Y) → ℝ) y : ℝ)
hc : (g : (a : Y) → ℝ) y ≤ c
rw : c + (b - c) = b
rw₁ rw₂ : b = b
⊢ c + (c - a) = b

Tactic:
rw [hsub, add_sub_cancel]

Premises used: add_sub_cancel
-- Module: Mathlib.Topology.TietzeExtension
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 →ᵇ ℝ
hg_mem : ∀ (y : Y), Membership.mem (α := ℝ) (Icc a b) ((g : (a : Y) → ℝ) y : ℝ)
ha' : ¬∃ (x : X), (f : (a : X) → ℝ) x = a
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (β := ℝ) (⇑dg : (a : Y) → ℝ) (Function.const Y 0) (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Ici c)
dga : EqOn (⇑dg : (a : Y) → ℝ) (Function.const Y (c - a)) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {a})
dgmem : ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (c - a)) ((dg : (a : Y) → ℝ) x : ℝ)
hgf : ∀ (x : X), Eq (α := ℝ) ((g + dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
hay : a < (g + dg : (a : Y) → ℝ) y
x : X
left : a ≤ (f : (a : X) → ℝ) x
hxy : LT.lt (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g + dg : (a : Y) → ℝ) y : ℝ)
hc : (g : (a : Y) → ℝ) y ≤ c
g₁ : c + (c - a) = b
⊢ (g + dg : (a : Y) → ℝ) y ≤ b

Tactic:
calc
        g y + dg y ≤ c + (c - a) := add_le_add hc (dgmem _).2
        _ = b := by rw [hsub, add_sub_cancel]

Premises used: add_le_add, HSub.hSub, And.right, 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
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 →ᵇ ℝ
hg_mem :
  ∀ (y : Y),
    ∃ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x) b : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ)
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
inr :
  ∀ (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),
    ∃ (g : Y →ᵇ ℝ),
      (∀ (y : Y),
          ∃ (x₁ : X) (x₂ : X),
            Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
              ((g : (a : Y) → ℝ) y : ℝ)) ∧
        Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)

Tactic:
choose xl hxl hgb using hg_mem
-- Module: Mathlib.Topology.TietzeExtension
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 →ᵇ ℝ
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
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
inr :
  ∀ (x : X) (hb : IsLUB (α := ℝ) (range (ι := X) (⇑f : (a : X) → ℝ) : Set ℝ) ((f : (a : X) → ℝ) x : ℝ))
    (hmem : ∀ (x_1 : X), Membership.mem (α := ℝ) (Icc a ((f : (a : X) → ℝ) x)) ((f : (a : X) → ℝ) x_1 : ℝ))
    (hle : a ≤ (f : (a : X) → ℝ) x) (hlt : a < (f : (a : X) → ℝ) x),
    let c := HAdd.hAdd (β := ℝ) a ((f : (a : X) → ℝ) x : ℝ) / 2;
    ∀ (hac : a < c) (hcb : c < (f : (a : X) → ℝ) x) (hsub : c - a = HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) c)
      (hgb : ∀ (y : Y), LE.le (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ) ((f : (a : X) → ℝ) x : ℝ)),
      ∃ (g : Y →ᵇ ℝ),
        (∀ (y : Y),
            ∃ (x₁ : X) (x₂ : X),
              Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
                ((g : (a : Y) → ℝ) y : ℝ)) ∧
          Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
inr₁ :
  ∀ (hb' : ¬∃ (x : X), (f : (a : X) → ℝ) x = b),
    ∃ (g : Y →ᵇ ℝ),
      (∀ (y : Y),
          ∃ (x₁ : X) (x₂ : X),
            Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
              ((g : (a : Y) → ℝ) y : ℝ)) ∧
        Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)

Tactic:
rcases em (∃ x, f x = b) with (⟨x, rfl⟩ | hb')

Premises used: Exists, em, Eq, DFunLike.coe, 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
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
g : Y →ᵇ ℝ
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
xl : (y : Y) → X
hxl : ∀ (y : Y), LE.le (α := ℝ) ((f : (a : X) → ℝ) (xl y) : ℝ) ((g : (a : Y) → ℝ) y : ℝ)
x : X
hb : IsLUB (α := ℝ) (range (ι := X) (⇑f : (a : X) → ℝ) : Set ℝ) ((f : (a : X) → ℝ) x : ℝ)
hmem : ∀ (x_1 : X), Membership.mem (α := ℝ) (Icc a ((f : (a : X) → ℝ) x)) ((f : (a : X) → ℝ) x_1 : ℝ)
hle : a ≤ (f : (a : X) → ℝ) x
hlt : a < (f : (a : X) → ℝ) x
c : ℝ := HAdd.hAdd (β := ℝ) a ((f : (a : X) → ℝ) x : ℝ) / 2
hac : a < c
hcb : c < (f : (a : X) → ℝ) x
hsub : c - a = HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) c
hgb : ∀ (y : Y), LE.le (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ) ((f : (a : X) → ℝ) x : ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)

Tactic:
⟨g, fun y => ⟨xl y, x, hxl y, hgb y⟩, hgf⟩

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
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
g : Y →ᵇ ℝ
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
xl : (y : Y) → X
hxl : ∀ (y : Y), LE.le (α := ℝ) ((f : (a : X) → ℝ) (xl y) : ℝ) ((g : (a : Y) → ℝ) y : ℝ)
x : X
hb : IsLUB (α := ℝ) (range (ι := X) (⇑f : (a : X) → ℝ) : Set ℝ) ((f : (a : X) → ℝ) x : ℝ)
hmem : ∀ (x_1 : X), Membership.mem (α := ℝ) (Icc a ((f : (a : X) → ℝ) x)) ((f : (a : X) → ℝ) x_1 : ℝ)
hle : a ≤ (f : (a : X) → ℝ) x
hlt : a < (f : (a : X) → ℝ) x
c : ℝ := HAdd.hAdd (β := ℝ) a ((f : (a : X) → ℝ) x : ℝ) / 2
hac : a < c
hcb : c < (f : (a : X) → ℝ) x
hsub : c - a = HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) c
hgb : ∀ (y : Y), LE.le (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ) ((f : (a : X) → ℝ) x : ℝ)
⊢ ∃ (g : Y →ᵇ ℝ),
    (∀ (y : Y),
        ∃ (x₁ : X) (x₂ : X),
          Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
            ((g : (a : Y) → ℝ) y : ℝ)) ∧
      Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)

Tactic:
exact ⟨g, fun y => ⟨xl y, x, hxl y, hgb y⟩, 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
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 →ᵇ ℝ
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
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
⊢ Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})

Tactic:
disjoint_union_left.2 ⟨?_, Disjoint.preimage _ ?_⟩

Premises used: Iff.mpr, And.intro, Disjoint.preimage, Set.disjoint_union_left
-- Module: Mathlib.Topology.TietzeExtension
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 →ᵇ ℝ
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
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
refine_1 : Disjoint (range e) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})
refine_2 : Disjoint (Iic c) {b}
⊢ Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})

Tactic:
refine disjoint_union_left.2 ⟨?_, Disjoint.preimage _ ?_⟩

Premises used: Iff.mpr, And.intro, Disjoint.preimage, Set.disjoint_union_left
-- Module: Mathlib.Topology.TietzeExtension
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 →ᵇ ℝ
hgf : Eq (α := X → ℝ) ((⇑g : (a : Y) → ℝ) ∘ e) (⇑f : (a : X) → ℝ)
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
refine_1 : ∀ ⦃a : Y⦄, a ∈ range e → a ∉ preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b}
⊢ Disjoint (range e) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})

Tactic:
rw [Set.disjoint_left]

Premises used: Set.disjoint_left