-- Mathlib/Topology/MetricSpace/Polish.lean
theorem _root_.IsClosed.isClopenable [TopologicalSpace α] [PolishSpace α] {s : Set α}
    (hs : IsClosed 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✝¹
⊢ IsOpen ((fun x => (Equiv.Set.sumCompl s) (Sum.inl x)) ⁻¹' s) ∧
    IsOpen ((fun x => (Equiv.Set.sumCompl s) (Sum.inr x)) ⁻¹' s)

Tactic:
have inl (x : s) : (Equiv.Set.sumCompl s) (Sum.inl x) = x := Equiv.Set.sumCompl_apply_inl ..

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
⊢ 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_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 (Sum.inl ⁻¹' (⇑f ⁻¹' s)) ∧ IsOpen (Sum.inr ⁻¹' (⇑f ⁻¹' s))

Tactic:
simp only [preimage_preimage, f]

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✝¹
⊢ 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_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

Tactic:
rw [isOpen_coinduced, isOpen_sum_iff]

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✝¹
⊢ IsOpen (Sum.inl ⁻¹' (⇑f ⁻¹' s)) ∧ IsOpen (Sum.inr ⁻¹' (⇑f ⁻¹' 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
⊢ IsClopenable s

Tactic:
have hle : TopologicalSpace.coinduced f instTopologicalSpaceSum ≤ ‹_› := by
  simp only [instTopologicalSpaceSum, coinduced_sup, coinduced_compose, sup_le_iff,
    ← continuous_iff_coinduced_le]
  exact ⟨continuous_subtype_val, continuous_subtype_val⟩

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
hle : coinduced (⇑f) instTopologicalSpaceSum ≤ inst✝¹
⊢ 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 ((fun x => ↑x) ⁻¹' s)

Tactic:
rw [Subtype.preimage_coe_compl']

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 ∅