-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
theorem _root_.MeasurableSet.isClopenable' {s : Set α} (hs : MeasurableSet s) :
    ∃ _ : TopologicalSpace α, BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s

Proof state:
case intro.intro.intro.measurable_eq
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
this : UpgradedStandardBorel α := upgradeStandardBorel α
t : TopologicalSpace α
hle : t ≤ UpgradedStandardBorel.toTopologicalSpace
ht : PolishSpace α
s_clopen : IsClosed s ∧ IsOpen s
⊢ inst✝¹ = borel α

Tactic:
rw [eq_borel_upgradeStandardBorel α, borel_eq_borel_of_le ht _ hle]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
this : UpgradedStandardBorel α := upgradeStandardBorel α
t : TopologicalSpace α
hle : t ≤ UpgradedStandardBorel.toTopologicalSpace
ht : PolishSpace α
s_clopen : IsClosed s ∧ IsOpen s
⊢ PolishSpace α

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
this : UpgradedStandardBorel α := upgradeStandardBorel α
t : TopologicalSpace α
hle : t ≤ UpgradedStandardBorel.toTopologicalSpace
ht : PolishSpace α
s_clopen : IsClosed s ∧ IsOpen s
⊢ BorelSpace α

Tactic:
constructor

Result:
case intro.intro.intro.measurable_eq
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
this : UpgradedStandardBorel α := upgradeStandardBorel α
t : TopologicalSpace α
hle : t ≤ UpgradedStandardBorel.toTopologicalSpace
ht : PolishSpace α
s_clopen : IsClosed s ∧ IsOpen s
⊢ inst✝¹ = borel α

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
⊢ ∃ x, BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s

Tactic:
letI := upgradeStandardBorel α

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
this : UpgradedStandardBorel α := upgradeStandardBorel α
⊢ ∃ x, BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
this : UpgradedStandardBorel α := upgradeStandardBorel α
t : TopologicalSpace α
hle : t ≤ UpgradedStandardBorel.toTopologicalSpace
ht : PolishSpace α
s_clopen : IsClosed s ∧ IsOpen s
⊢ PolishSpace α

Tactic:
infer_instance

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
this : UpgradedStandardBorel α := upgradeStandardBorel α
⊢ ∃ x, BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s

Tactic:
obtain ⟨t, hle, ht, s_clopen⟩ := hs.isClopenable

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
this : UpgradedStandardBorel α := upgradeStandardBorel α
t : TopologicalSpace α
hle : t ≤ UpgradedStandardBorel.toTopologicalSpace
ht : PolishSpace α
s_clopen : IsClosed s ∧ IsOpen s
⊢ ∃ x, BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
this : UpgradedStandardBorel α := upgradeStandardBorel α
t : TopologicalSpace α
hle : t ≤ UpgradedStandardBorel.toTopologicalSpace
ht : PolishSpace α
s_clopen : IsClosed s ∧ IsOpen s
⊢ ∃ x, BorelSpace α ∧ PolishSpace α ∧ IsClosed s ∧ IsOpen s

Tactic:
refine ⟨t, ?_, ht, s_clopen⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : StandardBorelSpace α
s : Set α
hs : MeasurableSet s
this : UpgradedStandardBorel α := upgradeStandardBorel α
t : TopologicalSpace α
hle : t ≤ UpgradedStandardBorel.toTopologicalSpace
ht : PolishSpace α
s_clopen : IsClosed s ∧ IsOpen s
⊢ BorelSpace α