α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this : PolishSpace ↑s
⊢ IsClopenable s
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
⊢ IsClopenable s
haveI : PolishSpace s := hs.polishSpace
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this : PolishSpace ↑s
t : Set α := sᶜ
⊢ IsClopenable s
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this : PolishSpace ↑s
⊢ IsClopenable s
let t : Set α := sᶜ
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
⊢ IsClopenable s
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this : PolishSpace ↑s
t : Set α := sᶜ
⊢ IsClopenable s
haveI : PolishSpace t := hs.isOpen_compl.polishSpace
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
⊢ IsClopenable s
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
⊢ IsClopenable s
let f : s ⊕ t ≃ α := Equiv.Set.sumCompl s
case hle
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
⊢ coinduced (↑f) instTopologicalSpaceSum ≤ inst✝¹

α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
hle : coinduced (↑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ IsClopenable s
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
⊢ IsClopenable s
have hle : TopologicalSpace.coinduced f instTopologicalSpaceSum ≤ ‹_›
case refine_1
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
hle : coinduced (↑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ PolishSpace α

case refine_2
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
hle : coinduced (↑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ IsOpen s
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
hle : coinduced (↑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ IsClopenable s
refine ⟨.coinduced f instTopologicalSpaceSum, hle, ?_, hs.mono hle, ?_⟩
case hle
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
⊢ Continuous (↑(Equiv.Set.sumCompl s) ∘ Sum.inl) ∧ Continuous (↑(Equiv.Set.sumCompl s) ∘ Sum.inr)
case hle
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
⊢ coinduced (↑f) instTopologicalSpaceSum ≤ inst✝¹
simp only [instTopologicalSpaceSum, coinduced_sup, coinduced_compose, sup_le_iff,
  ← continuous_iff_coinduced_le]
no goals
case hle
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
⊢ Continuous (↑(Equiv.Set.sumCompl s) ∘ Sum.inl) ∧ Continuous (↑(Equiv.Set.sumCompl s) ∘ Sum.inr)
exact ⟨continuous_subtype_val, continuous_subtype_val⟩
case refine_1
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
hle : coinduced (↑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ PolishSpace α
case refine_1
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
hle : coinduced (↑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ PolishSpace α
rw [← f.induced_symm]
no goals
case refine_1
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
hle : coinduced (↑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ PolishSpace α
exact f.symm.polishSpace_induced
case refine_2
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
hle : coinduced (↑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ IsOpen (Sum.inl ⁻¹' (↑f ⁻¹' s)) ∧ IsOpen (Sum.inr ⁻¹' (↑f ⁻¹' s))
case refine_2
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
hle : coinduced (↑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ IsOpen s
rw [isOpen_coinduced, isOpen_sum_iff]
no goals
case refine_2
α : Type u_1
β : Type ?u.35108
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
f : ↑s ⊕ ↑t ≃ α := Equiv.Set.sumCompl s
hle : coinduced (↑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ IsOpen (Sum.inl ⁻¹' (↑f ⁻¹' s)) ∧ IsOpen (Sum.inr ⁻¹' (↑f ⁻¹' s))
convert And.intro (isOpen_univ (α := s)) (isOpen_empty (α := (sᶜ : Set α)))
  <;> ext ⟨x, hx⟩ <;> simpa using hx