-- Mathlib/Topology/TietzeExtension.lean
theorem exists_extension_forall_exists_le_ge_of_isClosedEmbedding [Nonempty X] (f : X →ᵇ ℝ)
    {e : X → Y} (he : IsClosedEmbedding e) :
    ∃ g : Y →ᵇ ℝ, (∀ y, ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ g ∘ e = f

Proof state:
case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hgf : ⇑g ∘ e = ⇑f
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
⊢ ∀ ⦃a : Y⦄, a ∈ range e → a ∉ ⇑g ⁻¹' {b}

Tactic:
rintro _ ⟨x, rfl⟩ (rfl : g (e x) = b)

Result:
case refine_1.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
g : Y →ᵇ ℝ
hgf : ⇑g ∘ e = ⇑f
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
x : X
hb : IsLUB (range ⇑f) (g (e x))
hmem : ∀ (x_1 : X), f x_1 ∈ Icc a (g (e x))
hle : a ≤ g (e x)
hlt : a < g (e x)
c : ℝ := (a + g (e x)) / 2
hac : a < c
hcb : c < g (e x)
hsub : c - a = g (e x) - c
hgb : ∀ (y : Y), g y ≤ g (e x)
hb' : ¬∃ x_1, f x_1 = g (e x)
⊢ False

Proof state:
case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
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), g y ∈ Icc a b
hgf : ⇑g ∘ e = ⇑f
ha' : ¬∃ x, f x = a
⊢ ∀ ⦃a_1 : Y⦄, a_1 ∈ range e → a_1 ∉ ⇑g ⁻¹' {a}

Tactic:
rintro _ ⟨x, rfl⟩ (rfl : g (e x) = a)

Result:
case refine_1.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
b : ℝ
hb : IsLUB (range ⇑f) b
g : Y →ᵇ ℝ
hgf : ⇑g ∘ e = ⇑f
x : X
ha : IsGLB (range ⇑f) (g (e x))
hmem : ∀ (x_1 : X), f x_1 ∈ Icc (g (e x)) b
hle : g (e x) ≤ b
hlt : g (e x) < b
c : ℝ := (g (e x) + b) / 2
hac : g (e x) < c
hcb : c < b
hsub : c - g (e x) = b - c
hg_mem : ∀ (y : Y), g y ∈ Icc (g (e x)) b
ha' : ¬∃ x_1, f x_1 = g (e x)
⊢ False

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hgf : ⇑g ∘ e = ⇑f
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)
dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)
⊢ ∀ (x : X), (g - dg) (e x) = f x

Tactic:
intro x

Result:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hgf : ⇑g ∘ e = ⇑f
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)
dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)
x : X
⊢ (g - dg) (e x) = f x

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
⊢ ∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f

Tactic:
obtain ⟨a, ha⟩ : ∃ a, IsGLB (range f) a := ⟨_, isGLB_ciInf f.isBounded_range.bddBelow⟩

Result:
case intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
⊢ ∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f

Proof state:
case h
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
hb : IsLUB (range ⇑f) a
hmem : ∀ (x : X), f x ∈ Icc a a
hle : a ≤ a
this : ∀ (x : X), f x = a
⊢ (∀ (y : Y), ∃ x₁ x₂, (const Y a) y ∈ Icc (f x₁) (f x₂)) ∧ ⇑(const Y a) ∘ e = ⇑f

Tactic:
simp [this, funext_iff]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
⊢ ∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f

Tactic:
inhabit X

Result:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
⊢ ∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
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 → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
hgb : ∀ (y : Y), g y ≤ b
hb' : ¬∃ x, f x = b
hd : Disjoint (range e ∪ ⇑g ⁻¹' Iic c) (⇑g ⁻¹' {b})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Iic c)
dgb : EqOn (⇑dg) (Function.const Y (b - c)) (⇑g ⁻¹' {b})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (b - c)
hgf : ∀ (x : X), (g - dg) (e x) = f x
y : Y
hyb : (g - dg) y < b
xu : X
hyxu : (g - dg) y < f xu
right✝ : f xu ≤ b
hc : c < g y
h✝ : a ∉ range ⇑f
⊢ a < (g - dg) y

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 _

Result:
no goals