-- 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 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

Tactic:
rw [← lt_add_one_iff, ← hp]

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 < o

Proof state:
case mp
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⟩
⊢ ∃ y ∈ u ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩

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

Result:
case mp.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
⊢ ∃ y ∈ u ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩

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

Tactic:
constructor

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

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

Proof state:
case h.right
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
y✝ : ↑(Iio o)
mem : y✝ ∈ Ioo ⟨q, ⋯⟩ ⟨p + 1, ho⟩ ∩ Iio o ↓∩ S
⊢ y✝ = ⟨p, hpo⟩

Tactic:
have aux1 := Subtype.mk_lt_mk.mp mem.1.1

Result:
case h.right
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
y✝ : ↑(Iio o)
mem : y✝ ∈ Ioo ⟨q, ⋯⟩ ⟨p + 1, ho⟩ ∩ Iio o ↓∩ S
aux1 : q < ↑y✝
⊢ y✝ = ⟨p, hpo⟩

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
hp : o = p + 1
⊢ 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
hp : o = 0 + 1
⊢ False

Proof state:
case neg.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
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⟩
⊢ ∃ y ∈ u ∩ S, y ≠ p

Tactic:
use x

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 ∈ u ∩ S ∧ ↑x ≠ p

Proof state:
case intro
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
hp : o = 0 + 1
x : ↑(Iio o)
hx : x ∈ Set.univ ∩ Iio o ↓∩ S ∧ x ≠ ⟨0, hpo⟩
⊢ False

Tactic:
have : ↑x < o := x.2

Result:
case intro
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
hp : o = 0 + 1
x : ↑(Iio o)
hx : x ∈ Set.univ ∩ Iio o ↓∩ S ∧ x ≠ ⟨0, hpo⟩
this : ↑x < o
⊢ False

Proof state:
case mp
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 ∈ 𝓝 ⟨p, hpo⟩, ∃ y ∈ U ∩ Iio o ↓∩ S, y ≠ ⟨p, hpo⟩

Tactic:
intro u hu

Result:
case mp
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⟩
⊢ ∃ 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
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⟩ ∧ ∀ y ∈ Ioo ⟨q, ⋯⟩ ⟨p + 1, ho⟩ ∩ Iio o ↓∩ S, y = ⟨p, hpo⟩

Tactic:
constructor

Result:
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⟩

case h.right
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
⊢ ∀ y ∈ Ioo ⟨q, ⋯⟩ ⟨p + 1, ho⟩ ∩ Iio o ↓∩ S, y = ⟨p, hpo⟩

Proof state:
case h.right
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
y✝ : ↑(Iio o)
mem : y✝ ∈ Ioo ⟨q, ⋯⟩ ⟨p + 1, ho⟩ ∩ Iio o ↓∩ S
aux1 : q < ↑y✝
aux2 : ↑y✝ < succ q + 1
⊢ ↑y✝ = succ q

Tactic:
exact ((succ_le_iff.mpr aux1).antisymm (le_of_lt_succ aux2)).symm

Result:
no goals

Proof state:
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⟩

Tactic:
refine ⟨?_, Subtype.coe_ne_coe.mp hx.2⟩

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

Proof state:
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

Tactic:
obtain ⟨x, hx⟩ := h (Ioi ⟨l, hl.1.trans hpo⟩) (Ioi_mem_nhds hl.1)

Result:
case neg.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
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⟩
⊢ ∃ y ∈ u ∩ S, y ≠ p

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
⊢ ∃ y ∈ u ∩ S, y ≠ p

Tactic:
have ppos : p ≠ 0 := by
  rintro rfl
  obtain ⟨x, hx⟩ := h Set.univ univ_mem
  have : ↑x < o := x.2
  simp_rw [hp, zero_add, lt_one_iff_zero] at this
  exact hx.2 (SetCoe.ext this)

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
ppos : p ≠ 0
⊢ ∃ y ∈ u ∩ S, y ≠ p

Proof state:
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

Tactic:
exact h.2 <| Subtype.mk_eq_mk.mpr (lt_one_iff_zero.mp h.1.1)

Result:
no goals