case refine'_1
s : Set Ordinal
a : Ordinal
h : IsOpen {a}
x✝ : IsLimit a
h₀ : a ≠ 0
hsucc : ∀ (a_1 : Ordinal), a_1 < a → succ a_1 < a
⊢ False

case refine'_2
s : Set Ordinal
a : Ordinal
ha : ¬IsLimit a
⊢ IsOpen {a}
s : Set Ordinal
a : Ordinal
⊢ IsOpen {a} ↔ ¬IsLimit a
refine' ⟨fun h ⟨h₀, hsucc⟩ => _, fun ha => _⟩
case refine'_1.intro.intro.intro
s : Set Ordinal
a : Ordinal
h : IsOpen {a}
x✝ : IsLimit a
h₀ : a ≠ 0
hsucc : ∀ (a_1 : Ordinal), a_1 < a → succ a_1 < a
b c : Ordinal
hbc : a ∈ Set.Ioo b c
hbc' : Set.Ioo b c ⊆ {a}
⊢ False
case refine'_1
s : Set Ordinal
a : Ordinal
h : IsOpen {a}
x✝ : IsLimit a
h₀ : a ≠ 0
hsucc : ∀ (a_1 : Ordinal), a_1 < a → succ a_1 < a
⊢ False
obtain ⟨b, c, hbc, hbc'⟩ :=
  (mem_nhds_iff_exists_Ioo_subset' ⟨0, Ordinal.pos_iff_ne_zero.2 h₀⟩ ⟨_, lt_succ a⟩).1
    (h.mem_nhds rfl)
case refine'_1.intro.intro.intro
s : Set Ordinal
a : Ordinal
h : IsOpen {a}
x✝ : IsLimit a
h₀ : a ≠ 0
hsucc : ∀ (a_1 : Ordinal), a_1 < a → succ a_1 < a
b c : Ordinal
hbc : a ∈ Set.Ioo b c
hbc' : Set.Ioo b c ⊆ {a}
hba : succ b < a
⊢ False
case refine'_1.intro.intro.intro
s : Set Ordinal
a : Ordinal
h : IsOpen {a}
x✝ : IsLimit a
h₀ : a ≠ 0
hsucc : ∀ (a_1 : Ordinal), a_1 < a → succ a_1 < a
b c : Ordinal
hbc : a ∈ Set.Ioo b c
hbc' : Set.Ioo b c ⊆ {a}
⊢ False
have hba := hsucc b hbc.1
no goals
case refine'_1.intro.intro.intro
s : Set Ordinal
a : Ordinal
h : IsOpen {a}
x✝ : IsLimit a
h₀ : a ≠ 0
hsucc : ∀ (a_1 : Ordinal), a_1 < a → succ a_1 < a
b c : Ordinal
hbc : a ∈ Set.Ioo b c
hbc' : Set.Ioo b c ⊆ {a}
hba : succ b < a
⊢ False
exact hba.ne (hbc' ⟨lt_succ b, hba.trans hbc.2⟩)
case refine'_2.inl
s : Set Ordinal
ha : ¬IsLimit 0
⊢ IsOpen {0}

case refine'_2.inr.inl.intro
s : Set Ordinal
b : Ordinal
ha : ¬IsLimit (succ b)
⊢ IsOpen {succ b}

case refine'_2.inr.inr
s : Set Ordinal
a : Ordinal
ha : ¬IsLimit a
ha' : IsLimit a
⊢ IsOpen {a}
case refine'_2
s : Set Ordinal
a : Ordinal
ha : ¬IsLimit a
⊢ IsOpen {a}
rcases zero_or_succ_or_limit a with (rfl | ⟨b, rfl⟩ | ha')
case refine'_2.inl
s : Set Ordinal
ha : ¬IsLimit 0
⊢ IsOpen (Set.Iio (succ ⊥))
case refine'_2.inl
s : Set Ordinal
ha : ¬IsLimit 0
⊢ IsOpen {0}
rw [← bot_eq_zero, ← Set.Iic_bot, ← Iio_succ]
no goals
case refine'_2.inl
s : Set Ordinal
ha : ¬IsLimit 0
⊢ IsOpen (Set.Iio (succ ⊥))
exact isOpen_Iio
case refine'_2.inr.inl.intro
s : Set Ordinal
b : Ordinal
ha : ¬IsLimit (succ b)
⊢ IsOpen (Set.Ioo b (succ (succ b)))
case refine'_2.inr.inl.intro
s : Set Ordinal
b : Ordinal
ha : ¬IsLimit (succ b)
⊢ IsOpen {succ b}
rw [← Set.Icc_self, Icc_succ_left, ← Ioo_succ_right]
no goals
case refine'_2.inr.inl.intro
s : Set Ordinal
b : Ordinal
ha : ¬IsLimit (succ b)
⊢ IsOpen (Set.Ioo b (succ (succ b)))
exact isOpen_Ioo
no goals
case refine'_2.inr.inr
s : Set Ordinal
a : Ordinal
ha : ¬IsLimit a
ha' : IsLimit a
⊢ IsOpen {a}
exact (ha ha').elim