-- Mathlib/Topology/MetricSpace/Polish.lean
theorem _root_.Topology.IsClosedEmbedding.polishSpace [TopologicalSpace α] [TopologicalSpace β]
    [PolishSpace β] {f : α → β} (hf : IsClosedEmbedding f) : PolishSpace α

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this✝¹ : UpgradedPolishSpace β := upgradePolishSpace β
this✝ : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
this : SecondCountableTopology α
⊢ PolishSpace α

Tactic:
have : CompleteSpace α := by
  rw [completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing]
  exact hf.isClosed_range.isComplete

Result:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this✝² : UpgradedPolishSpace β := upgradePolishSpace β
this✝¹ : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
this✝ : SecondCountableTopology α
this : CompleteSpace α
⊢ PolishSpace α

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
⊢ PolishSpace α

Tactic:
letI := upgradePolishSpace β

Result:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this : UpgradedPolishSpace β := upgradePolishSpace β
⊢ PolishSpace α

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this✝² : UpgradedPolishSpace β := upgradePolishSpace β
this✝¹ : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
this✝ : SecondCountableTopology α
this : CompleteSpace α
⊢ PolishSpace α

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this : UpgradedPolishSpace β := upgradePolishSpace β
⊢ PolishSpace α

Tactic:
letI : MetricSpace α := hf.isEmbedding.comapMetricSpace f

Result:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this✝ : UpgradedPolishSpace β := upgradePolishSpace β
this : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
⊢ PolishSpace α

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this✝¹ : UpgradedPolishSpace β := upgradePolishSpace β
this✝ : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
this : SecondCountableTopology α
⊢ IsComplete (range f)

Tactic:
exact hf.isClosed_range.isComplete

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this✝ : UpgradedPolishSpace β := upgradePolishSpace β
this : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
⊢ PolishSpace α

Tactic:
haveI : SecondCountableTopology α := hf.isEmbedding.secondCountableTopology

Result:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this✝¹ : UpgradedPolishSpace β := upgradePolishSpace β
this✝ : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
this : SecondCountableTopology α
⊢ PolishSpace α

Proof state:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this✝¹ : UpgradedPolishSpace β := upgradePolishSpace β
this✝ : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
this : SecondCountableTopology α
⊢ CompleteSpace α

Tactic:
rw [completeSpace_iff_isComplete_range hf.isEmbedding.to_isometry.isUniformInducing]

Result:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PolishSpace β
f : α → β
hf : IsClosedEmbedding f
this✝¹ : UpgradedPolishSpace β := upgradePolishSpace β
this✝ : MetricSpace α := IsEmbedding.comapMetricSpace f ⋯
this : SecondCountableTopology α
⊢ IsComplete (range f)