case h
X✝ : Type ?u.21432
Y : Type ?u.21435
Z : Type ?u.21438
α : Type ?u.21441
inst✝² : TopologicalSpace X✝
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∈ ↑(ofClopen hU) ⁻¹' {1} ↔ x✝ ∈ Uᶜ
X✝ : Type ?u.21432
Y : Type ?u.21435
Z : Type ?u.21438
α : Type ?u.21441
inst✝² : TopologicalSpace X✝
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ ↑(ofClopen hU) ⁻¹' {1} = Uᶜ
ext
no goals
case h
X✝ : Type ?u.21432
Y : Type ?u.21435
Z : Type ?u.21438
α : Type ?u.21441
inst✝² : TopologicalSpace X✝
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
x✝ : X
⊢ x✝ ∈ ↑(ofClopen hU) ⁻¹' {1} ↔ x✝ ∈ Uᶜ
simp only [ofClopen, mem_singleton_iff, coe_mk, Fin.zero_eq_one_iff, mem_preimage,
  ite_eq_right_iff, mem_compl_iff, Nat.succ_succ_ne_one]