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 →ᵇ ℝ
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 ℝ) ((g : (a : Y) → ℝ) (e x) : ℝ)
hmem : ∀ (x_1 : X), Membership.mem (α := ℝ) (Icc a ((g : (a : Y) → ℝ) (e x))) ((f : (a : X) → ℝ) x_1 : ℝ)
hle : a ≤ (g : (a : Y) → ℝ) (e x)
hlt : a < (g : (a : Y) → ℝ) (e x)
c : ℝ := HAdd.hAdd (β := ℝ) a ((g : (a : Y) → ℝ) (e x) : ℝ) / 2
hac : a < c
hcb : c < (g : (a : Y) → ℝ) (e x)
hsub : c - a = HSub.hSub (α := ℝ) ((g : (a : Y) → ℝ) (e x) : ℝ) c
hgb : ∀ (y : Y), LE.le (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ) ((g : (a : Y) → ℝ) (e x) : ℝ)
hb' : ¬∃ (x_1 : X), Eq (α := ℝ) ((f : (a : X) → ℝ) x_1 : ℝ) ((g : (a : Y) → ℝ) (e x) : ℝ)
⊢ False

Tactic:
hb' ⟨x, (congr_fun hgf x).symm⟩

Premises used: Exists.intro, congr_fun, Eq.symm
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
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 ℝ) ((g : (a : Y) → ℝ) (e x) : ℝ)
hmem : ∀ (x_1 : X), Membership.mem (α := ℝ) (Icc a ((g : (a : Y) → ℝ) (e x))) ((f : (a : X) → ℝ) x_1 : ℝ)
hle : a ≤ (g : (a : Y) → ℝ) (e x)
hlt : a < (g : (a : Y) → ℝ) (e x)
c : ℝ := HAdd.hAdd (β := ℝ) a ((g : (a : Y) → ℝ) (e x) : ℝ) / 2
hac : a < c
hcb : c < (g : (a : Y) → ℝ) (e x)
hsub : c - a = HSub.hSub (α := ℝ) ((g : (a : Y) → ℝ) (e x) : ℝ) c
hgb : ∀ (y : Y), LE.le (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ) ((g : (a : Y) → ℝ) (e x) : ℝ)
hb' : ¬∃ (x_1 : X), Eq (α := ℝ) ((f : (a : X) → ℝ) x_1 : ℝ) ((g : (a : Y) → ℝ) (e x) : ℝ)
⊢ False

Tactic:
exact hb' ⟨x, (congr_fun hgf x).symm⟩

Premises used: Exists.intro, congr_fun, Eq.symm
-- Module: Mathlib.Topology.TietzeExtension
Goal:
X : Type u_1
Y : Type u_2
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NormalSpace Y
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 (Iic c) {b}

Tactic:
Set.disjoint_singleton_right.2 hcb.not_ge

Premises used: Iff.mpr, Set.disjoint_singleton_right, LT.lt.not_ge
-- 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 (Iic c) {b}

Tactic:
exact Set.disjoint_singleton_right.2 hcb.not_ge

Premises used: Iff.mpr, Set.disjoint_singleton_right, LT.lt.not_ge
-- 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:
have hd : Disjoint (range e ∪ g ⁻¹' Iic c) (g ⁻¹' {b}) := by
    refine disjoint_union_left.2 ⟨?_, Disjoint.preimage _ ?_⟩
    · rw [Set.disjoint_left]
      rintro _ ⟨x, rfl⟩ (rfl : g (e x) = b)
      exact hb' ⟨x, (congr_fun hgf x).symm⟩
    · exact Set.disjoint_singleton_right.2 hcb.not_ge
-- 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
hd : Disjoint (range e ∪ (⇑g : (a : Y) → ℝ) ⁻¹' Iic c) (preimage (β := ℝ) (⇑g : (a : Y) → ℝ) {b})
inr :
  ∀ (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 : ℝ)),
    ∃ (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 exists_bounded_mem_Icc_of_closed_of_le
      (he.isClosed_range.union <| isClosed_Iic.preimage g.continuous)
      (isClosed_singleton.preimage g.continuous) hd (sub_nonneg.2 hcb.le) with
    ⟨dg, dg0, dgb, dgmem⟩

Premises used: Iff.mpr, IsClosed.union, LT.lt.le, BoundedContinuousFunction.continuous, exists_bounded_mem_Icc_of_closed_of_le, isClosed_Iic, IsClosed.preimage, isClosed_singleton, sub_nonneg, Topology.IsClosedEmbedding.isClosed_range
-- 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
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 : ℝ)
x : X
⊢ Eq (α := ℝ) ((g - dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
simp [dg0 (Or.inl <| mem_range_self _), ← hgf]

Premises used: Set.mem_range_self, Or.inl
-- 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
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 : ℝ)
⊢ ∀ (x : X), Eq (α := ℝ) ((g - dg : (a : Y) → ℝ) (e x) : ℝ) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
replace hgf : ∀ x, (g - dg) (e x) = f x := by
    intro x
    simp [dg0 (Or.inl <| mem_range_self _), ← 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 →ᵇ ℝ
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 : ℝ)
⊢ ∃ (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 - dg, fun y => ?_, funext hgf⟩

Premises used: HSub.hSub, funext, 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 →ᵇ ℝ
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 : ℝ)
inr :
  ∀ (y : Y),
    ∃ (x₁ : X) (x₂ : X),
      Membership.mem (α := ℝ) (γ := Set ℝ) (Icc ((f : (a : X) → ℝ) x₁) ((f : (a : X) → ℝ) x₂) : Set ℝ)
        ((g - dg : (a : Y) → ℝ) y : ℝ)
⊢ ∃ (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:
refine ⟨g - dg, fun y => ?_, funext 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 →ᵇ ℝ
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
inl :
  ∀ (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),
    let 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 (α := ℝ) ((g - dg : (a : Y) → ℝ) y : ℝ) ((g : (a : Y) → ℝ) y : ℝ)
inr : ∀ (hlt : (g : (a : Y) → ℝ) y < b), (g - dg : (a : Y) → ℝ) y < b
⊢ (g - dg : (a : Y) → ℝ) y < b

Tactic:
rcases (hgb y).eq_or_lt with (rfl | hlt)

Premises used: LE.le.eq_or_lt, 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 →ᵇ ℝ
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 (α := ℝ) ((g - dg : (a : Y) → ℝ) y : ℝ) ((g : (a : Y) → ℝ) y : ℝ)

Tactic:
(sub_lt_self_iff _).2 ?_

Premises used: Iff.mpr, sub_lt_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
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 : ℝ)
inl : LT.lt (α := ℝ) (0 : ℝ) ((dg : (a : Y) → ℝ) y : ℝ)
⊢ LT.lt (α := ℝ) ((g - dg : (a : Y) → ℝ) y : ℝ) ((g : (a : Y) → ℝ) y : ℝ)

Tactic:
refine (sub_lt_self_iff _).2 ?_

Premises used: Iff.mpr, sub_lt_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
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 : ℝ)
⊢ 0 < HSub.hSub (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ) c

Tactic:
sub_pos.2 hcb

Premises used: Iff.mpr, sub_pos
-- 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 : ℝ)
⊢ HSub.hSub (α := ℝ) ((g : (a : Y) → ℝ) y : ℝ) c = (dg : (a : Y) → ℝ) y

Tactic:
(dgb rfl).symm

Premises used: Eq.symm, rfl