-- Mathlib/Topology/TietzeExtension.lean
theorem ContinuousMap.exists_extension (he : IsClosedEmbedding e) (f : C(X₁, Y)) :
    ∃ (g : C(X, Y)), g.comp ⟨e, he.continuous⟩ = f

Proof state:
X₁ : Type u₁
inst✝⁴ : TopologicalSpace X₁
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : NormalSpace X
e : X₁ → X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
e' : X₁ ≃ₜ ↑(Set.range e) := Homeomorph.ofIsEmbedding e ⋯
g : C(X, Y)
hg : restrict (Set.range e) g = f.comp ↑e'.symm
⊢ g.comp { toFun := e, continuous_toFun := ⋯ } = f

Tactic:
ext x

Result:
case h
X₁ : Type u₁
inst✝⁴ : TopologicalSpace X₁
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : NormalSpace X
e : X₁ → X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
e' : X₁ ≃ₜ ↑(Set.range e) := Homeomorph.ofIsEmbedding e ⋯
g : C(X, Y)
hg : restrict (Set.range e) g = f.comp ↑e'.symm
x : X₁
⊢ (g.comp { toFun := e, continuous_toFun := ⋯ }) x = f x

Proof state:
X₁ : Type u₁
inst✝⁴ : TopologicalSpace X₁
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : NormalSpace X
e : X₁ → X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
⊢ ∃ g, g.comp { toFun := e, continuous_toFun := ⋯ } = f

Tactic:
let e' : X₁ ≃ₜ Set.range e := Homeomorph.ofIsEmbedding _ he.isEmbedding

Result:
X₁ : Type u₁
inst✝⁴ : TopologicalSpace X₁
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : NormalSpace X
e : X₁ → X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
e' : X₁ ≃ₜ ↑(Set.range e) := Homeomorph.ofIsEmbedding e ⋯
⊢ ∃ g, g.comp { toFun := e, continuous_toFun := ⋯ } = f

Proof state:
X₁ : Type u₁
inst✝⁴ : TopologicalSpace X₁
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : NormalSpace X
e : X₁ → X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
e' : X₁ ≃ₜ ↑(Set.range e) := Homeomorph.ofIsEmbedding e ⋯
⊢ ∃ g, g.comp { toFun := e, continuous_toFun := ⋯ } = f

Tactic:
obtain ⟨g, hg⟩ := (f.comp e'.symm).exists_restrict_eq he.isClosed_range

Result:
case intro
X₁ : Type u₁
inst✝⁴ : TopologicalSpace X₁
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : NormalSpace X
e : X₁ → X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
e' : X₁ ≃ₜ ↑(Set.range e) := Homeomorph.ofIsEmbedding e ⋯
g : C(X, Y)
hg : restrict (Set.range e) g = f.comp ↑e'.symm
⊢ ∃ g, g.comp { toFun := e, continuous_toFun := ⋯ } = f

Proof state:
case h
X₁ : Type u₁
inst✝⁴ : TopologicalSpace X₁
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : NormalSpace X
e : X₁ → X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
e' : X₁ ≃ₜ ↑(Set.range e) := Homeomorph.ofIsEmbedding e ⋯
g : C(X, Y)
hg : restrict (Set.range e) g = f.comp ↑e'.symm
x : X₁
⊢ (g.comp { toFun := e, continuous_toFun := ⋯ }) x = f x

Tactic:
simpa using congr($(hg) ⟨e' x, x, rfl⟩)

Result:
no goals

Proof state:
case intro
X₁ : Type u₁
inst✝⁴ : TopologicalSpace X₁
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : NormalSpace X
e : X₁ → X
Y : Type v
inst✝¹ : TopologicalSpace Y
inst✝ : TietzeExtension Y
he : IsClosedEmbedding e
f : C(X₁, Y)
e' : X₁ ≃ₜ ↑(Set.range e) := Homeomorph.ofIsEmbedding e ⋯
g : C(X, Y)
hg : restrict (Set.range e) g = f.comp ↑e'.symm
⊢ ∃ g, g.comp { toFun := e, continuous_toFun := ⋯ } = f

Tactic:
exact ⟨g, by ext x; simpa using congr($(hg) ⟨e' x, x, rfl⟩)⟩

Result:
no goals