-- Mathlib/Topology/MetricSpace/Polish.lean
theorem _root_.IsClosed.isClopenable [TopologicalSpace α] [PolishSpace α] {s : Set α}
    (hs : IsClosed s) : IsClopenable s

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this : PolishSpace ↑s
⊢ IsClopenable s

Tactic:
let t : Set α := sᶜ

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this : PolishSpace ↑s
t : Set α := sᶜ
⊢ IsClopenable s

Proof state:
case refine_2
α : Type u_1
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✝¹
inl : ∀ (x : ↑s), (Equiv.Set.sumCompl s) (Sum.inl x) = ↑x
inr : ∀ (x : ↑sᶜ), (Equiv.Set.sumCompl s) (Sum.inr x) = ↑x
⊢ IsOpen univ ∧ IsOpen ((fun x => ↑x) ⁻¹' s)

Tactic:
simp only [isOpen_univ, true_and]

Result:
case refine_2
α : Type u_1
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✝¹
inl : ∀ (x : ↑s), (Equiv.Set.sumCompl s) (Sum.inl x) = ↑x
inr : ∀ (x : ↑sᶜ), (Equiv.Set.sumCompl s) (Sum.inr x) = ↑x
⊢ IsOpen ((fun x => ↑x) ⁻¹' s)

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this : PolishSpace ↑s
t : Set α := sᶜ
⊢ IsClopenable s

Tactic:
haveI : PolishSpace t := hs.isOpen_compl.polishSpace

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
⊢ IsClopenable s

Proof state:
α : Type u_1
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

Tactic:
refine ⟨.coinduced f instTopologicalSpaceSum, hle, ?_, hs.mono hle, ?_⟩

Result:
case refine_1
α : Type u_1
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
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

Proof state:
α : Type u_1
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✝¹

Tactic:
simp only [instTopologicalSpaceSum, coinduced_sup, coinduced_compose, sup_le_iff,
  ← continuous_iff_coinduced_le]

Result:
α : Type u_1
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 (⇑f ∘ Sum.inl) ∧ Continuous (⇑f ∘ Sum.inr)

Proof state:
case refine_2
α : Type u_1
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✝¹
inl : ∀ (x : ↑s), (Equiv.Set.sumCompl s) (Sum.inl x) = ↑x
⊢ IsOpen ((fun x => (Equiv.Set.sumCompl s) (Sum.inl x)) ⁻¹' s) ∧
    IsOpen ((fun x => (Equiv.Set.sumCompl s) (Sum.inr x)) ⁻¹' s)

Tactic:
have inr (x : ↑sᶜ) : (Equiv.Set.sumCompl s) (Sum.inr x) = x := Equiv.Set.sumCompl_apply_inr ..

Result:
case refine_2
α : Type u_1
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✝¹
inl : ∀ (x : ↑s), (Equiv.Set.sumCompl s) (Sum.inl x) = ↑x
inr : ∀ (x : ↑sᶜ), (Equiv.Set.sumCompl s) (Sum.inr x) = ↑x
⊢ IsOpen ((fun x => (Equiv.Set.sumCompl s) (Sum.inl x)) ⁻¹' s) ∧
    IsOpen ((fun x => (Equiv.Set.sumCompl s) (Sum.inr x)) ⁻¹' s)

Proof state:
case refine_1
α : Type u_1
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 α

Tactic:
exact f.symm.polishSpace_induced

Result:
no goals

Proof state:
α : Type u_1
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 (⇑f ∘ Sum.inl) ∧ Continuous (⇑f ∘ Sum.inr)

Tactic:
exact ⟨continuous_subtype_val, continuous_subtype_val⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this✝ : PolishSpace ↑s
t : Set α := sᶜ
this : PolishSpace ↑t
⊢ IsClopenable s

Tactic:
let f : s ⊕ t ≃ α := Equiv.Set.sumCompl s

Result:
α : Type u_1
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

Proof state:
case refine_2
α : Type u_1
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✝¹
inl : ∀ (x : ↑s), (Equiv.Set.sumCompl s) (Sum.inl x) = ↑x
inr : ∀ (x : ↑sᶜ), (Equiv.Set.sumCompl s) (Sum.inr x) = ↑x
⊢ IsOpen ∅

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
α : Type u_1
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✝¹
inl : ∀ (x : ↑s), (Equiv.Set.sumCompl s) (Sum.inl x) = ↑x
inr : ∀ (x : ↑sᶜ), (Equiv.Set.sumCompl s) (Sum.inr x) = ↑x
⊢ IsOpen ((fun x => (Equiv.Set.sumCompl s) (Sum.inl x)) ⁻¹' s) ∧
    IsOpen ((fun x => (Equiv.Set.sumCompl s) (Sum.inr x)) ⁻¹' s)

Tactic:
simp_rw [t, inl, inr, Subtype.coe_preimage_self]

Result:
case refine_2
α : Type u_1
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✝¹
inl : ∀ (x : ↑s), (Equiv.Set.sumCompl s) (Sum.inl x) = ↑x
inr : ∀ (x : ↑sᶜ), (Equiv.Set.sumCompl s) (Sum.inr x) = ↑x
⊢ IsOpen univ ∧ IsOpen ((fun x => ↑x) ⁻¹' s)

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
⊢ IsClopenable s

Tactic:
haveI : PolishSpace s := hs.polishSpace

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PolishSpace α
s : Set α
hs : IsClosed s
this : PolishSpace ↑s
⊢ IsClopenable s