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
g : Y →ᵇ ℝ
xl : (y : Y) → X
hxl : ∀ (y : Y), LE.le (α := ℝ) ((f : (a : X) → ℝ) (xl y) : ℝ) ((g : (a : Y) → ℝ) y : ℝ)
dg : Y →ᵇ ℝ
hgf : ∀ (x : X), Eq (α := ℝ) ((g - dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)
y : Y
hb : IsLUB (α := ℝ) (range (ι := X) (⇑f : (a : X) → ℝ) : Set ℝ) ((g : (a : Y) → ℝ) y : ℝ)
hmem : ∀ (x : X), Membership.mem (α := ℝ) (Icc a ((g : (a : Y) → ℝ) y)) ((f : (a : X) → ℝ) x : ℝ)
hle : a ≤ (g : (a : Y) → ℝ) y
hlt : a < (g : (a : Y) → ℝ) y
c : ℝ := HAdd.hAdd (β := ℝ) a ((g : (a : Y) → ℝ) y : ℝ) / 2
hac : a < c
hcb : c < (g : (a : Y) → ℝ) y
hsub : c - a = HSub.hSub (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ) c
hgb : ∀ (y_1 : Y), LE.le (α := ℝ) ((g : (a : Y) → ℝ) y_1 : ℝ) ((g : (a : Y) → ℝ) y : ℝ)
hb' : ¬∃ (x : X), Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g : (a : Y) → ℝ) y : ℝ)
hd :
  Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c)
    (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) (singleton (α := ℝ) ((g : (a : Y) → ℝ) 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 (HSub.hSub (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ) c))
    (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) (singleton (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ)))
dgmem :
  ∀ (x : Y), Membership.mem (α := ℝ) (Icc 0 (HSub.hSub (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ) c)) ((dg : (a : Y) → ℝ) x : ℝ)
⊢ LT.lt (α := ℝ) (0 : ℝ) ((dg : (a : Y) → ℝ) y : ℝ)

Tactic:
calc
        0 < g y - c := sub_pos.2 hcb
        _ = dg y := (dgb rfl).symm

Premises used: Iff.mpr, sub_pos, Eq.symm, 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
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_1 : 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
hlt : (g : (a : Y) → ℝ) y < b
⊢ (g - dg : (a : Y) → ℝ) y < b

Tactic:
((sub_le_self_iff _).2 (dgmem _).1).trans_lt hlt

Premises used: Iff.mpr, And.left, LE.le.trans_lt, sub_le_self_iff
-- 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_1 : 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
hlt : (g : (a : Y) → ℝ) y < b
⊢ (g - dg : (a : Y) → ℝ) y < b

Tactic:
exact ((sub_le_self_iff _).2 (dgmem _).1).trans_lt hlt

Premises used: Iff.mpr, And.left, LE.le.trans_lt, sub_le_self_iff
-- 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 →ᵇ ℝ
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
⊢ (g - dg : (a : Y) → ℝ) y < b

Tactic:
have hyb : (g - dg) y < b := by
    rcases (hgb y).eq_or_lt with (rfl | hlt)
    · refine (sub_lt_self_iff _).2 ?_
      calc
        0 < g y - c := sub_pos.2 hcb
        _ = dg y := (dgb rfl).symm
    · exact ((sub_le_self_iff _).2 (dgmem _).1).trans_lt hlt
-- 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 →ᵇ ℝ
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
inr :
  ∀ (xu : X) (hyxu : LT.lt (α := ℝ) ((g - dg : (a : Y) → ℝ) y : ℝ) ((f : (a : X) → ℝ) xu : ℝ)),
    (f : (a : X) → ℝ) xu ≤ b →
      ∃ (x₁ : X) (x₂ : X),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
          ((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 hb.exists_between hyb with ⟨_, ⟨xu, rfl⟩, hyxu, _⟩

Premises used: IsLUB.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 →ᵇ ℝ
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
inr :
  ∀ (hc : c < (g : (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 : ℝ)
inr₁ :
  ∀ (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 : ℝ)
⊢ ∃ (x₁ : X) (x₂ : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
      ((g - dg : (a : Y) → ℝ) y : ℝ)

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

Premises used: lt_or_ge, 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 →ᵇ ℝ
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
inr :
  ∀ (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),
    let 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),
      ∃ (x₁ : X) (x₂ : X),
        Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
          ((g - dg : (a : Y) → ℝ) y : ℝ)
inr₁ :
  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 : ℝ)
⊢ ∃ (x₁ : X) (x₂ : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
      ((g - dg : (a : Y) → ℝ) y : ℝ)

Tactic:
rcases em (a ∈ range f) with (⟨x, rfl⟩ | _)

Premises used: Membership.mem, em, Set.range, 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
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
⊢ ∃ (x₁ : X) (x₂ : X),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
      ((g - dg : (a : Y) → ℝ) y : ℝ)

Tactic:
⟨x, xu, ?_, hyxu.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
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
inr : LE.le (α := ℝ) ((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:
refine ⟨x, xu, ?_, hyxu.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
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 : ℝ)
rw₁ rw₂ : Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((f : (a : X) → ℝ) x : ℝ)
⊢ (f : (a : X) → ℝ) x = c - (b - c)

Tactic:
rw [← hsub, sub_sub_cancel]

Premises used: sub_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
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
⊢ c - (b - c) ≤ HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : Y) → ℝ) y : ℝ) ((dg : (a : Y) → ℝ) y : ℝ)

Tactic:
sub_le_sub hc.le (dgmem _).2

Premises used: LT.lt.le, And.right, sub_le_sub
-- 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
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₁ : (f : (a : X) → ℝ) x = c - (b - c)
⊢ LE.le (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) ((g - dg : (a : Y) → ℝ) y : ℝ)

Tactic:
calc
        f x = c - (b - c) := by rw [← hsub, sub_sub_cancel]
        _ ≤ g y - dg y := sub_le_sub hc.le (dgmem _).2

Premises used: HSub.hSub, LT.lt.le, And.right, sub_le_sub, 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 →ᵇ ℝ
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)
rw₁ rw₂ : a = a
⊢ a = c - (b - c)

Tactic:
rw [← hsub, sub_sub_cancel]

Premises used: sub_sub_cancel