s : Set Ordinal
a o : Ordinal
ho : o ∈ s
⊢ s ∈ 𝓝 o ↔ IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
s : Set Ordinal
a : Ordinal
⊢ IsOpen s ↔ ∀ (o : Ordinal), o ∈ s → IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
refine isOpen_iff_mem_nhds.trans <| forall₂_congr fun o ho => ?_
case pos
s : Set Ordinal
a o : Ordinal
ho : o ∈ s
ho' : IsLimit o
⊢ s ∈ 𝓝 o ↔ IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s

case neg
s : Set Ordinal
a o : Ordinal
ho : o ∈ s
ho' : ¬IsLimit o
⊢ s ∈ 𝓝 o ↔ IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
s : Set Ordinal
a o : Ordinal
ho : o ∈ s
⊢ s ∈ 𝓝 o ↔ IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
by_cases ho' : IsLimit o
case pos
s : Set Ordinal
a o : Ordinal
ho : o ∈ s
ho' : IsLimit o
⊢ (∃ i, i < o ∧ Set.Ioc i o ⊆ s) ↔ ∃ a, a < o ∧ Set.Ioo a o ⊆ s
case pos
s : Set Ordinal
a o : Ordinal
ho : o ∈ s
ho' : IsLimit o
⊢ s ∈ 𝓝 o ↔ IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
simp only [(nhdsBasis_Ioc ho'.1).mem_iff, ho', true_implies]
case pos
s : Set Ordinal
a✝ o : Ordinal
ho : o ∈ s
ho' : IsLimit o
a : Ordinal
ha : a < o
⊢ Set.Ioc a o ⊆ s ↔ Set.Ioo a o ⊆ s
case pos
s : Set Ordinal
a o : Ordinal
ho : o ∈ s
ho' : IsLimit o
⊢ (∃ i, i < o ∧ Set.Ioc i o ⊆ s) ↔ ∃ a, a < o ∧ Set.Ioo a o ⊆ s
refine exists_congr fun a => and_congr_right fun ha => ?_
no goals
case pos
s : Set Ordinal
a✝ o : Ordinal
ho : o ∈ s
ho' : IsLimit o
a : Ordinal
ha : a < o
⊢ Set.Ioc a o ⊆ s ↔ Set.Ioo a o ⊆ s
simp only [← Set.Ioo_insert_right ha, Set.insert_subset, ho, true_and]
no goals
case neg
s : Set Ordinal
a o : Ordinal
ho : o ∈ s
ho' : ¬IsLimit o
⊢ s ∈ 𝓝 o ↔ IsLimit o → ∃ a, a < o ∧ Set.Ioo a o ⊆ s
simp [nhds_eq_pure.2 ho', ho, ho']