case h
X✝ : Type ?u.19442
Y : Type ?u.19445
Z : Type ?u.19448
α : Type ?u.19451
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) ⁻¹' {0} ↔ x✝ ∈ U
X✝ : Type ?u.19442
Y : Type ?u.19445
Z : Type ?u.19448
α : Type ?u.19451
inst✝² : TopologicalSpace X✝
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ ↑(ofClopen hU) ⁻¹' {0} = U
ext
case h
X✝ : Type ?u.19442
Y : Type ?u.19445
Z : Type ?u.19448
α : Type ?u.19451
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✝ ∈ U → False ↔ x✝ ∈ U
case h
X✝ : Type ?u.19442
Y : Type ?u.19445
Z : Type ?u.19448
α : Type ?u.19451
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) ⁻¹' {0} ↔ x✝ ∈ U
simp only [ofClopen, mem_singleton_iff, Fin.one_eq_zero_iff, coe_mk, mem_preimage,
  ite_eq_left_iff, Nat.succ_succ_ne_one]
no goals
case h
X✝ : Type ?u.19442
Y : Type ?u.19445
Z : Type ?u.19448
α : Type ?u.19451
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✝ ∈ U → False ↔ x✝ ∈ U
tauto