-- Mathlib/SetTheory/Ordinal/Topology.lean
theorem accPt_subtype {p o : Ordinal} (S : Set Ordinal) (hpo : p < o) :
    AccPt p (𝓟 S) ↔ AccPt ⟨p, hpo⟩ (𝓟 (Iio o ↓∩ S))

Proof state:
case mp.intro.intro
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 p, ∃ y ∈ U ∩ S, y ≠ p
plim : p.IsLimit
u : Set ↑(Iio o)
hu : u ∈ 𝓝 ⟨p, hpo⟩
l : ↑(Iio o)
hl : l < ⟨p, hpo⟩ ∧ Ioc l ⟨p, hpo⟩ ⊆ u
x : Ordinal.{u_1}
hx : x ∈ Ioo (↑l) (p + 1) ∩ S ∧ x ≠ p
⊢ ∃ y ∈ u ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩

Tactic:
use ⟨x, lt_of_le_of_lt (lt_succ_iff.mp hx.1.1.2) hpo⟩

Result:
case h
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 p, ∃ y ∈ U ∩ S, y ≠ p
plim : p.IsLimit
u : Set ↑(Iio o)
hu : u ∈ 𝓝 ⟨p, hpo⟩
l : ↑(Iio o)
hl : l < ⟨p, hpo⟩ ∧ Ioc l ⟨p, hpo⟩ ⊆ u
x : Ordinal.{u_1}
hx : x ∈ Ioo (↑l) (p + 1) ∩ S ∧ x ≠ p
⊢ ⟨x, ⋯⟩ ∈ u ∩ Iio o ↓∩ S ∧ ⟨x, ⋯⟩ ≠ ⟨p, hpo⟩

Proof state:
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
h : ¬p.IsLimit
⊢ ∃ U ∈ 𝓝 ⟨p, hpo⟩, ∀ y ∈ U ∩ Iio o ↓∩ S, y = ⟨p, hpo⟩

Tactic:
obtain ⟨q, hq⟩ := ((zero_or_succ_or_limit p).resolve_left ppos).resolve_right h

Result:
case intro
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
h : ¬p.IsLimit
q : Ordinal.{u_1}
hq : p = succ q
⊢ ∃ U ∈ 𝓝 ⟨p, hpo⟩, ∀ y ∈ U ∩ Iio o ↓∩ S, y = ⟨p, hpo⟩

Proof state:
case h
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : ¬p + 1 < o
hp : o = p + 1
ppos : p ≠ 0
l : Ordinal.{u_1}
hl : l < p ∧ Ioc l p ⊆ u
x : ↑(Iio o)
hx : x ∈ Ioi ⟨l, ⋯⟩ ∩ Iio o ↓∩ S ∧ x ≠ ⟨p, hpo⟩
⊢ ↑x < o

Tactic:
exact x.2

Result:
no goals

Proof state:
case neg
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : ¬p + 1 < o
hp : o = p + 1
ppos : p ≠ 0
⊢ ∃ y ∈ u ∩ S, y ≠ p

Tactic:
obtain ⟨l, hl⟩ := exists_Ioc_subset_of_mem_nhds hu ⟨0, Ordinal.pos_iff_ne_zero.mpr ppos⟩

Result:
case neg.intro
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : ¬p + 1 < o
hp : o = p + 1
ppos : p ≠ 0
l : Ordinal.{u_1}
hl : l < p ∧ Ioc l p ⊆ u
⊢ ∃ y ∈ u ∩ S, y ≠ p

Proof state:
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
⊢ p.IsLimit

Tactic:
contrapose! h

Result:
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
h : ¬p.IsLimit
⊢ ∃ U ∈ 𝓝 ⟨p, hpo⟩, ∀ y ∈ U ∩ Iio o ↓∩ S, y = ⟨p, hpo⟩

Proof state:
o : Ordinal.{u_1}
S u : Set Ordinal.{u_1}
hpo : 0 < o
h : ∀ U ∈ 𝓝 ⟨0, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨0, hpo⟩
hu : u ∈ 𝓝 0
ho : 1 < o
⊢ False

Tactic:
specialize h (Iio ⟨1, ho⟩) (Iio_mem_nhds (Subtype.mk_lt_mk.mpr zero_lt_one))

Result:
o : Ordinal.{u_1}
S u : Set Ordinal.{u_1}
hpo : 0 < o
hu : u ∈ 𝓝 0
ho : 1 < o
h : ∃ y ∈ Iio ⟨1, ho⟩ ∩ Iio o ↓∩ S, y ≠ ⟨0, hpo⟩
⊢ False

Proof state:
case h
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : ¬p + 1 < o
hp : o = p + 1
ppos : p ≠ 0
l : Ordinal.{u_1}
hl : l < p ∧ Ioc l p ⊆ u
x : ↑(Iio o)
hx : x ∈ Ioi ⟨l, ⋯⟩ ∩ Iio o ↓∩ S ∧ x ≠ ⟨p, hpo⟩
⊢ ↑x ∈ u ∩ S ∧ ↑x ≠ p

Tactic:
refine ⟨⟨hl.2 ⟨hx.1.1, ?_⟩, hx.1.2⟩, fun h ↦ hx.2 (SetCoe.ext h)⟩

Result:
case h
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : ¬p + 1 < o
hp : o = p + 1
ppos : p ≠ 0
l : Ordinal.{u_1}
hl : l < p ∧ Ioc l p ⊆ u
x : ↑(Iio o)
hx : x ∈ Ioi ⟨l, ⋯⟩ ∩ Iio o ↓∩ S ∧ x ≠ ⟨p, hpo⟩
⊢ ↑x ≤ p

Proof state:
case mp
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : AccPt p (𝓟 S)
⊢ AccPt ⟨p, hpo⟩ (𝓟 (Iio o ↓∩ S))

Tactic:
have plim : p.IsLimit := IsAcc.isLimit h

Result:
case mp
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : AccPt p (𝓟 S)
plim : p.IsLimit
⊢ AccPt ⟨p, hpo⟩ (𝓟 (Iio o ↓∩ S))

Proof state:
case pos.intro
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
plim : p.IsLimit
l : Ordinal.{u_1}
hl : l < p ∧ Ioc l p ⊆ u
⊢ ∃ y ∈ u ∩ S, y ≠ p

Tactic:
obtain ⟨x, hx⟩ := h (Ioo ⟨l, hl.1.trans hpo⟩ ⟨p + 1, ho⟩) (Ioo_mem_nhds hl.1 (lt_add_one p))

Result:
case pos.intro.intro
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
plim : p.IsLimit
l : Ordinal.{u_1}
hl : l < p ∧ Ioc l p ⊆ u
x : ↑(Iio o)
hx : x ∈ Ioo ⟨l, ⋯⟩ ⟨p + 1, ho⟩ ∩ Iio o ↓∩ S ∧ x ≠ ⟨p, hpo⟩
⊢ ∃ y ∈ u ∩ S, y ≠ p

Proof state:
case pos
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
plim : p.IsLimit
⊢ ∃ y ∈ u ∩ S, y ≠ p

Tactic:
obtain ⟨l, hl⟩ := exists_Ioc_subset_of_mem_nhds hu ⟨0, plim.pos⟩

Result:
case pos.intro
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
plim : p.IsLimit
l : Ordinal.{u_1}
hl : l < p ∧ Ioc l p ⊆ u
⊢ ∃ y ∈ u ∩ S, y ≠ p

Proof state:
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
h : ¬p.IsLimit
q : Ordinal.{u_1}
hq : p = succ q
⊢ ⟨q, ⋯⟩ < ⟨p, hpo⟩

Tactic:
simp only [hq, Subtype.mk_lt_mk, lt_succ]

Result:
no goals

Proof state:
case neg
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : ¬p + 1 < o
⊢ ∃ y ∈ u ∩ S, y ≠ p

Tactic:
have hp : o = p + 1 := (le_succ_iff_eq_or_le.mp (le_of_not_lt ho)).resolve_right
  (not_le_of_lt hpo)

Result:
case neg
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : ¬p + 1 < o
hp : o = p + 1
⊢ ∃ y ∈ u ∩ S, y ≠ p

Proof state:
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
h : ∀ U ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
⊢ p ≠ 0

Tactic:
rintro rfl

Result:
o : Ordinal.{u_1}
S u : Set Ordinal.{u_1}
hpo : 0 < o
h : ∀ U ∈ 𝓝 ⟨0, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨0, hpo⟩
hu : u ∈ 𝓝 0
ho : 0 + 1 < o
⊢ False

Proof state:
case h.left
p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
u : Set Ordinal.{u_1}
hu : u ∈ 𝓝 p
ho : p + 1 < o
ppos : p ≠ 0
h : ¬p.IsLimit
q : Ordinal.{u_1}
hq : p = succ q
⊢ Ioo ⟨q, ⋯⟩ ⟨p + 1, ho⟩ ∈ 𝓝 ⟨p, hpo⟩

Tactic:
exact Ioo_mem_nhds (by simp only [hq, Subtype.mk_lt_mk, lt_succ]) (lt_succ p)

Result:
no goals

Proof state:
o : Ordinal.{u_1}
S u : Set Ordinal.{u_1}
hpo : 0 < o
hu : u ∈ 𝓝 0
ho : 1 < o
h : ∃ y ∈ Iio ⟨1, ho⟩ ∩ Iio o ↓∩ S, y ≠ ⟨0, hpo⟩
⊢ False

Tactic:
obtain ⟨_, h⟩ := h

Result:
case intro
o : Ordinal.{u_1}
S u : Set Ordinal.{u_1}
hpo : 0 < o
hu : u ∈ 𝓝 0
ho : 1 < o
w✝ : ↑(Iio o)
h : w✝ ∈ Iio ⟨1, ho⟩ ∩ Iio o ↓∩ S ∧ w✝ ≠ ⟨0, hpo⟩
⊢ False